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 "HOL-IMP.AExp" "HOL-IMP.BExp"
begin
fun deduplicate :: "'a list \<Rightarrow> 'a list" where
"deduplicate [] = []"
| "deduplicate [x] = [x]"
| "deduplicate (x # y # xs) = (if x = y then deduplicate (y # xs) else x # deduplicate (y # xs))"
lemma "length (deduplicate xs) \<le> length xs"
by (induction xs rule: deduplicate.induct) auto
fun subst :: "vname \<Rightarrow> aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
"subst x a' (N n) = N n"
| "subst x a' (V y) = (if x=y then a' else V y)"
| "subst x a' (Plus a1 a2) = Plus (subst x a' a1) (subst x a' a2)"
lemma subst_lemma: "aval (subst x a' a) s = aval a (s(x:=aval a' s))"
by (induct a) auto
lemma comp: "aval a1 s = aval a2 s \<Longrightarrow> aval (subst x a1 a) s = aval (subst x a2 a) s"
by (simp add: subst_lemma)
datatype aexp' = N' int | V' vname | PI' vname | Plus' aexp' aexp'
fun aval' where
"aval' (N' n) s = (n,s)" |
"aval' (V' x) s = (s x, s)" |
"aval' (PI' x) s = (s x, s(x := 1 + s x))" |
"aval' (Plus' a1 a2) s = (
let (v1, s') = aval' a1 s; (v2, s'') = aval' a2 s'
in (v1 + v2, s''))"
lemma "aval' (Plus' (PI' x) (V' x)) <> \<noteq> aval' (Plus' (V' x) (PI' x)) <>"
by auto
lemma aval'_inc': "aval' a s = (v,s') \<Longrightarrow> s x \<le> s' x"
apply (induct a arbitrary: s s' v)
apply (auto split: prod.splits)
apply fastforce
done
lemma aval'_inc:
"aval' a <> = (v, s') \<Longrightarrow> 0 \<le> s' x"
using aval'_inc' by (fastforce simp: null_state_def)
end
theory Submission
imports Defs
begin
fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"add _ = undefined"
theorem add_assoc: "add (add x y) z = add x (add y z)"
sorry
theorem add_commut: "add x y = add y x"
sorry
datatype wexp = N val | V vname | Plus wexp wexp | Where wexp vname wexp
fun wval :: "wexp \<Rightarrow> state \<Rightarrow> val" where
"wval _ = undefined"
fun inline :: "wexp \<Rightarrow> aexp" where
"inline _ = undefined"
value
"inline (Where (Plus (V ''x'') (V ''x'')) ''x'' (Plus (N 1) (N 1))) =
aexp.Plus (aexp.Plus (aexp.N 1) (aexp.N 1)) (aexp.Plus (aexp.N 1) (aexp.N 1))"
theorem val_inline: "aval (inline e) s = wval e s"
sorry
fun elim :: "wexp \<Rightarrow> wexp" where
"elim _ = undefined"
theorem wval_elim: "wval (elim e) s = wval e s"
sorry
end
theory Check imports Submission begin theorem add_assoc: "add (add x y) z = add x (add y z)" by (rule Submission.add_assoc) theorem add_commut: "add x y = add y x" by (rule Submission.add_commut) theorem val_inline: "aval (inline e) s = wval e s" by (rule Submission.val_inline) theorem wval_elim: "wval (elim e) s = wval e s" by (rule Submission.wval_elim) end