Homework 08

Definitions File

theory Defs
  imports "IMP2.VCG"
begin

lemma intvs_singleton[simp]: 
  "{i::int..<i + 1} = {i}" 
  "{i-1..<i::int} = {i-1}" 
  by auto

lemma intvs_incr_h:
  "l\<le>h \<Longrightarrow> {l::int..<h + 1} = insert h {l..<h}"
  by auto

lemma intvs_decr_h:
  "{l::int..<h - 1} = {l..<h} - {h-1}"
  by auto
  
lemma intvs_incr_l:
  "{l+1..<h::int} = {l..<h} - {l}"
  by auto

lemma intvs_decr_l:
  "l\<le>h \<Longrightarrow> {l-1..<h::int} = insert (l-1) {l..<h}"
  by auto
  
lemmas intvs_incdec = intvs_incr_h intvs_incr_l intvs_decr_h intvs_decr_l

lemma intvs_lower_incr: "l<h \<Longrightarrow> {l::int..<h} = insert l ({l+1..<h})" by auto
lemma intvs_upper_decr: "l<h \<Longrightarrow> {l::int..<h} = insert (h-1) ({l..<h-1})" by auto


definition "is_equil a l h i \<equiv> l\<le>i \<and> i<h \<and> (\<Sum>j=l..<i. a j) = (\<Sum>j=i..<h. a j)"

end

Template File

theory Submission
  imports Defs
begin

program_spec euclid_extended
  assumes "a>0 \<and> b>0"
  ensures "old_r = gcd a\<^sub>0 b\<^sub>0 \<and> gcd a\<^sub>0 b\<^sub>0 = a\<^sub>0 * old_s + b\<^sub>0 * old_t"
defines \<open>
    s = 0;    old_s = 1;
    t = 1;    old_t = 0;
    r = b;    old_r = a;
    while (r\<noteq>0) 
      @invariant\<open>undefined :: bool\<close>      @variant\<open>nat undefined\<close>    {
      quotient = old_r / r;
      temp = old_r;
      old_r = r;
      r = temp - quotient * r;
      temp = old_s;
      old_s = s;
      s = temp - quotient * s;
      temp = old_t;
      old_t = t;
      t = temp - quotient * t
    }
  \<close>
  sorry

program_spec equilibrium
  assumes \<open>l\<le>h\<close>
  ensures \<open>is_equil a l h i \<or> i=h \<and> (\<nexists>i. is_equil a l h i)\<close>
  defines \<open>
    usum=0; i=l;
    while (i<h) 
      @variant\<open>nat undefined\<close>      @invariant\<open>undefined :: bool\<close>    { 
      usum = usum + a[i]; i=i+1 
    };
    i=l; lsum=0;
    while (usum \<noteq> lsum \<and> i<h) 
      @variant\<open>nat undefined\<close>      @invariant\<open>undefined :: bool\<close>    {
      lsum = lsum + a[i];
      usum = usum - a[i];
      i=i+1
    }
  \<close>
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem euclid_extended_spec:
 "HT_mods {''t'', ''r'', ''s'', ''temp'', ''old_t'', ''old_r'', ''old_s'', ''quotient''}
  (\<lambda>\<ss>. VAR (\<ss> ''b'' 0) (\<lambda>b. VAR (\<ss> ''a'' 0) (\<lambda>a. BB_PROTECT (0 < a \<and> 0 < b)))) euclid_extended
  (\<lambda>\<ss>\<^sub>0 \<ss>.
      VAR (\<ss>\<^sub>0 ''b'' 0)
       (\<lambda>b\<^sub>0. VAR (\<ss>\<^sub>0 ''a'' 0)
               (\<lambda>a\<^sub>0. VAR (\<ss> ''old_t'' 0)
                       (\<lambda>old_t.
                           VAR (\<ss> ''old_s'' 0)
                            (\<lambda>old_s.
                                VAR (\<ss> ''old_r'' 0)
                                 (\<lambda>old_r.
                                     BB_PROTECT
                                      (old_r = gcd a\<^sub>0 b\<^sub>0 \<and> gcd a\<^sub>0 b\<^sub>0 = a\<^sub>0 * old_s + b\<^sub>0 * old_t)))))))"
  by (rule Submission.euclid_extended_spec)

theorem equilibrium_spec:
 "HT_mods {''i'', ''lsum'', ''usum''} (\<lambda>\<ss>. VAR (\<ss> ''l'' 0) (\<lambda>l. VAR (\<ss> ''h'' 0) (\<lambda>s. BB_PROTECT (l \<le> s))))
  equilibrium
  (\<lambda>\<ss>\<^sub>0 \<ss>.
      VAR (\<ss> ''l'' 0)
       (\<lambda>l. VAR (\<ss> ''i'' 0)
             (\<lambda>i. VAR (\<ss> ''h'' 0)
                   (\<lambda>h. VAR (\<ss> ''a'') (\<lambda>a. BB_PROTECT (is_equil a l h i \<or> i = h \<and> \<not> Ex (is_equil a l h)))))))
"
  by (rule Submission.equilibrium_spec)

end