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 end
theory Submission imports Defs begin
datatype
com = Skip ("SKIP")
| Assign vname aexp ("_::=_" [1000, 61] 61)
| Seq com com ("_;;/ _" [60, 61] 60)
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
| Break ("BREAK")
inductive
big_step :: "com \<times> state \<Rightarrow> bool \<times> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
sorry
inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
inductive_cases BreakE[elim!]: "(BREAK,s) \<Rightarrow> t"
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
lemma assign_simp:
"(x ::= a,s) \<Rightarrow> (brk,s') \<longleftrightarrow> (s' = s(x := aval a s) \<and> \<not>brk)"
by auto
fun break_ok :: "com \<Rightarrow> bool" where
"break_ok _ = undefined"
theorem ok_brk: "\<lbrakk>(c, s) \<Rightarrow> (brk, t); break_ok c\<rbrakk> \<Longrightarrow> \<not>brk"
sorry
fun elim :: "com \<Rightarrow> com" where
"elim _ = undefined"
abbreviation equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
"c \<sim> c' \<equiv> (\<forall>s t. (c, s) \<Rightarrow> t = (c', s) \<Rightarrow> t)"
theorem elim_complete: "(c, s) \<Rightarrow> (b, s') \<Longrightarrow> (elim c, s) \<Rightarrow> (b, s')"
sorry
theorem elim_sound: "(elim c, s) \<Rightarrow> (b, s') \<Longrightarrow> (c, s) \<Rightarrow> (b, s')"
sorry
lemma "elim c \<sim> c"
using elim_sound elim_complete by fast
fun exec :: "com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> (bool \<times> state) option" where where
"exec _ = undefined"
value "(case (
exec (
WHILE (Bc True) DO
IF (Less (V ''x'') (N 4))
THEN ''x''::= (Plus (V ''x'') (N 1))
ELSE BREAK
) <> 10
) of (Some (False, s)) \<Rightarrow>
s ''x''
) = 4"
theorem exec_imp_bigstep: "exec c s f = Some s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
sorry
theorem exec_add: "exec c s f = Some s' \<Longrightarrow> exec c s (f + k) = Some s'"
sorry
lemma exec_mono: "exec c s f = Some (brk, s') \<Longrightarrow> f' \<ge> f \<Longrightarrow> exec c s f' = Some (brk, s')"
by (auto simp: exec_add dest: le_Suc_ex)
theorem bigstep_imp_si:
"(c,s) \<Rightarrow> (brk, s') \<Longrightarrow> \<exists>k. exec c s k = Some (brk, s')"
proof (induct rule: big_step_induct)
case (Skip s) have "exec SKIP s 1 = Some (False, s)" by auto
thus ?case by blast
next
case (WhileTrue b s1 c s2 brk3 s3)
then obtain f1 f2 where "exec c s1 f1 = Some (False, s2)"
and "exec (WHILE b DO c) s2 f2 = Some (brk3, s3)" by auto
with exec_mono[of c s1 f1 False s2 "max f1 f2"]
exec_mono[of "WHILE b DO c" s2 f2 brk3 s3 "max f1 f2"] have
"exec c s1 (max f1 f2) = Some (False, s2)"
and "exec (WHILE b DO c) s2 (max f1 f2) = Some (brk3, s3)"
by auto
hence "exec (WHILE b DO c) s1 (Suc (max f1 f2)) = Some (brk3, s3)"
using \<open>bval b s1\<close> by (auto simp add: add_ac)
thus ?case by blast
next
case (IfTrue b s c1 brk' t c2)
then obtain k where "exec c1 s k = Some (brk', t)" by blast
hence "exec (IF b THEN c1 ELSE c2) s k = Some (brk', t)"
using \<open>bval b s\<close> by (cases k) auto
thus ?case by blast
next
sorry
lemma "(\<exists>k. exec c s k = Some (brk, s')) \<longleftrightarrow> (c,s) \<Rightarrow> (brk, s')"
by (metis exec_imp_bigstep bigstep_imp_si)
end
theory Check imports Submission begin theorem ok_brk: "\<lbrakk>(c, s) \<Rightarrow> (brk, t); break_ok c\<rbrakk> \<Longrightarrow> \<not>brk" by (rule Submission.ok_brk) theorem elim_complete: "(c, s) \<Rightarrow> (b, s') \<Longrightarrow> (elim c, s) \<Rightarrow> (b, s')" by (rule Submission.elim_complete) theorem elim_sound: "(elim c, s) \<Rightarrow> (b, s') \<Longrightarrow> (c, s) \<Rightarrow> (b, s')" by (rule Submission.elim_sound) theorem exec_imp_bigstep: "exec c s f = Some s' \<Longrightarrow> (c, s) \<Rightarrow> s'" by (rule Submission.exec_imp_bigstep) theorem exec_add: "exec c s f = Some s' \<Longrightarrow> exec c s (f + k) = Some s'" by (rule Submission.exec_add) theorem bigstep_imp_si: "(c,s) \<Rightarrow> (brk, s') \<Longrightarrow> \<exists>k. exec c s k = Some (brk, s')" by (rule Submission.bigstep_imp_si) end