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.ASM" begin
inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r where
refl: "star r x x"
| step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
lemma star_prepend: "\<lbrakk>r x y; star r y z\<rbrakk> \<Longrightarrow> star r x z"
by (rule step)
lemma star_append: "\<lbrakk> star r x y; r y z \<rbrakk> \<Longrightarrow> star r x z"
by (induct rule: star.induct) (auto intro: star.intros)
inductive star' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r where
refl': "star' r x x"
| step': "\<lbrakk>star' r x y; r y z\<rbrakk> \<Longrightarrow> star' r x z"
lemma star'_prepend: "\<lbrakk>star' r y z; r x y\<rbrakk> \<Longrightarrow> star' r x z"
apply (induction rule: star'.induct)
apply (auto intro: star'.intros)
done
lemma "star r x y = star' r x y"
proof
assume "star r x y"
thus "star' r x y"
by induct (auto intro: star'.intros star'_prepend)
next
assume "star' r x y"
thus "star r x y"
by induct (auto intro: star.intros star_append)
qed
fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack option" where
"exec1 (LOADI n) _ stk = Some (n # stk)"
| "exec1 (LOAD x) s stk = Some (s(x) # stk)"
| "exec1 ADD _ stk = (case stk of
a # b # c \<Rightarrow> Some ((a + b) # c)
| _ \<Rightarrow> None)"
fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack option" where
"exec [] _ stk = Some stk"
| "exec (i # ins) s stk = (case exec1 i s stk of
Some stk \<Rightarrow> exec ins s stk
| None \<Rightarrow> None)"
lemma exec_append[simp]:
"exec (ins1 @ ins2) s stk = (case exec ins1 s stk of
Some stk \<Rightarrow> exec ins2 s stk
| None \<Rightarrow> None)"
apply(induction ins1 arbitrary: stk)
apply (auto split: option.split)
done
theorem exec_comp: "exec (comp a) s stk = Some (aval a s # stk)"
apply(induction a arbitrary: stk)
apply (auto)
done
lemma
assumes total: "\<forall> x y. T x y \<or> T y x"
and anti: "\<forall> x y. A x y \<and> A y x \<longrightarrow> x = y"
and subset: "\<forall> x y. T x y \<longrightarrow> A x y"
shows "A x y \<longrightarrow> T x y"
proof
fix x y assume "A x y"
from total have "T x y \<or> T y x" by simp
then show "T x y"
proof
assume "T x y"
then show ?thesis .
next
assume "T y x"
with subset have "A y x" by simp
with \<open>A x y\<close> anti have "x = y" by simp
with \<open>T y x\<close> show ?thesis by simp
qed
qed
end
theory Submission imports Defs begin
fun can_execute :: "nat \<Rightarrow> instr list \<Rightarrow> bool" where
"can_execute _ = undefined"
theorem can_exec_correct:
"can_execute (length stk) ins \<Longrightarrow> exec ins s stk \<noteq> None"
sorry
theorem can_exec_complete:
"exec ins s stk = Some res \<Longrightarrow> can_execute (length stk) ins"
sorry
inductive exec1r :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack \<Rightarrow> bool"
inductive execr :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack \<Rightarrow> bool"
theorem step_equiv: "exec1r i s stk stk' \<longleftrightarrow> exec1 i s stk = Some stk'"
sorry
theorem exec_equiv: "execr ins s stk stk' \<longleftrightarrow> (exec ins s stk = Some stk')"
sorry
datatype bexp = Var vname | Not bexp | And bexp bexp | Or bexp bexp
type_synonym state = "vname \<Rightarrow> bool"
fun is_var :: "bexp \<Rightarrow> bool" where
"is_var (Var _) = True"
| "is_var _ = False" where
"is_var _ = undefined"
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
"bval _ = undefined"
inductive is_nnf :: "bexp \<Rightarrow> bool"
fun sub :: "bexp \<Rightarrow> bexp set" where
"sub _ = undefined"
value "sub (And (Not (Var ''x'')) (Var ''y'')) =
{
Var ''x'',
Var ''y'',
Not (Var (''x'')),
And (Not (Var ''x'')) (Var ''y'')
}"
theorem nnf_not: "is_nnf b = (\<forall>b'. Not b' \<in> sub b \<longrightarrow> is_var b')"
sorry
fun nnf :: "bexp \<Rightarrow> bexp" where
"nnf _ = undefined"
theorem nnf_sound: "is_nnf (nnf b)"
sorry
theorem nnf_compl: "bval (nnf b) s = bval b s"
sorry
end
theory Check imports Submission begin theorem can_exec_correct: "can_execute (length stk) ins \<Longrightarrow> exec ins s stk \<noteq> None" by (rule Submission.can_exec_correct) theorem can_exec_complete: "exec ins s stk = Some res \<Longrightarrow> can_execute (length stk) ins" by (rule Submission.can_exec_complete) theorem step_equiv: "exec1r i s stk stk' \<longleftrightarrow> exec1 i s stk = Some stk'" by (rule Submission.step_equiv) theorem exec_equiv: "execr ins s stk stk' \<longleftrightarrow> (exec ins s stk = Some stk')" by (rule Submission.exec_equiv) theorem nnf_not: "is_nnf b = (\<forall>b'. Not b' \<in> sub b \<longrightarrow> is_var b')" by (rule Submission.nnf_not) theorem nnf_sound: "is_nnf (nnf b)" by (rule Submission.nnf_sound) theorem nnf_compl: "bval (nnf b) s = bval b s" by (rule Submission.nnf_compl) end