I agree 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.
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
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
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