Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 08

## Resources

### 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```

Terms and Conditions