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.Examples"
begin
lemma [named_ss vcg_bb]:
"lhsv (Inline c) = lhsv c"
unfolding Inline_def ..
lemma lran_split:
"lran a l h = lran a l p @ lran a p h" if "l \<le> p" "p \<le> h"
using that by (induction p; simp; simp add: lran.simps)
lemma lran_eq_iff':
"lran a l h = as @ bs \<longleftrightarrow> (\<exists> i. l \<le> i \<and> i \<le> h \<and> as = lran a l i \<and> bs = lran a i h)" if "l \<le> h"
apply safe
subgoal
using that
proof (induction as arbitrary: l)
case Nil
then show ?case
by auto
next
case (Cons x as)
from this(2-) have "lran a (l + 1) h = as @ bs" "a l = x" "l + 1 \<le> h"
apply -
subgoal
by simp
subgoal
by (smt append_Cons list.inject lran.simps lran_append1)
subgoal
using add1_zle_eq by fastforce
done
from Cons.IH[OF this(1,3)] guess i by safe
note IH = this
with \<open>a l = x\<close> show ?case
apply (intro exI[where x = i])
apply auto
by (smt IH(3) lran_prepend1)
qed
apply (subst lran_split; simp)
done
end
theory Submission
imports Defs
begin
theorem array_assign: "(x[] ::= a;; a[] ::= x) \<sim> (x[] ::= a)"
sorry
theorem
"(x[i] ::= Vidx a j;; a[j] ::= Vidx x i) \<sim> (x[i] ::= Vidx a j)"
oops
program_spec partition
assumes "l\<le>h"
ensures "mset_ran a {l\<^sub>0..<i} = filter_mset (\<lambda>x. x \<ge> 0) (mset_ran a\<^sub>0 {l\<^sub>0..<h\<^sub>0})
\<and> mset_ran a {i..<h\<^sub>0} = filter_mset (\<lambda>x. x < 0) (mset_ran a\<^sub>0 {l\<^sub>0..<h\<^sub>0})"
defines
\<open>
a[] = a;
i = 0;
j = l;
i = h;
temp = i
\<close>
sorry
program_spec substring_final
assumes "l \<le> h \<and> 0 \<le> len"
ensures "match = 1 \<longleftrightarrow> (\<exists>as bs. lran a l\<^sub>0 h\<^sub>0 = as @ lran b 0 len @ bs)"
for l h len match a[] b[]
defines \<open>
match = 1
\<close>
sorry
end
theory Check
imports Submission
begin
theorem array_assign: "(x[] ::= a;; a[] ::= x) \<sim> (x[] ::= a)"
by (rule Submission.array_assign)
theorem partition_spec:
"HT_mods {''j'', ''a'', ''i'', ''temp''} (\<lambda>\<ss>. VAR (\<ss> ''l'' 0) (\<lambda>l. VAR (\<ss> ''h'' 0) (\<lambda>s. BB_PROTECT (l \<le> s)))) partition
(\<lambda>\<ss>\<^sub>0 \<ss>.
VAR (\<ss>\<^sub>0 ''l'' 0)
(\<lambda>l\<^sub>0. VAR (\<ss>\<^sub>0 ''h'' 0)
(\<lambda>h\<^sub>0. VAR (\<ss>\<^sub>0 ''a'')
(\<lambda>a\<^sub>0. VAR (\<ss> ''i'' 0)
(\<lambda>i. VAR (\<ss> ''a'')
(\<lambda>a. BB_PROTECT
(mset_ran a {l\<^sub>0..<i} = filter_mset ((\<le>) 0) (mset_ran a\<^sub>0 {l\<^sub>0..<h\<^sub>0}) \<and>
mset_ran a {i..<h\<^sub>0} = {#x \<in># mset_ran a\<^sub>0 {l\<^sub>0..<h\<^sub>0}. x < 0#})))))))"
by (rule Submission.partition_spec)
end