theory Fold imports Sem_Equiv Vars begin subsection "Simple folding of arithmetic expressions" type_synonym tab = "vname => val option" fun afold :: "aexp => tab => aexp" where "afold (N n) _ = N n" | "afold (V x) t = (case t x of None => V x | Some k => N k)" | "afold (Plus e1 e2) t = (case (afold e1 t, afold e2 t) of (N n1, N n2) => N(n1+n2) | (e1',e2') => Plus e1' e2')" definition "approx t s <-> (ALL x k. t x = Some k --> s x = k)" theorem aval_afold[simp]: assumes "approx t s" shows "aval (afold a t) s = aval a s" using assms by (induct a) (auto simp: approx_def split: aexp.split option.split) theorem aval_afold_N: assumes "approx t s" shows "afold a t = N n ==> aval a s = n" by (metis assms aval.simps(1) aval_afold) definition "merge t1 t2 = (λm. if t1 m = t2 m then t1 m else None)" primrec "defs" :: "com => tab => tab" where "defs SKIP t = t" | "defs (x ::= a) t = (case afold a t of N k => t(x \<mapsto> k) | _ => t(x:=None))" | "defs (c1;;c2) t = (defs c2 o defs c1) t" | "defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" | "defs (WHILE b DO c) t = t |` (-lvars c)" primrec fold where "fold SKIP _ = SKIP" | "fold (x ::= a) t = (x ::= (afold a t))" | "fold (c1;;c2) t = (fold c1 t;; fold c2 (defs c1 t))" | "fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" | "fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lvars c))" lemma approx_merge: "approx t1 s ∨ approx t2 s ==> approx (merge t1 t2) s" by (fastforce simp: merge_def approx_def) lemma approx_map_le: "approx t2 s ==> t1 ⊆⇩_{m}t2 ==> approx t1 s" by (clarsimp simp: approx_def map_le_def dom_def) lemma restrict_map_le [intro!, simp]: "t |` S ⊆⇩_{m}t" by (clarsimp simp: restrict_map_def map_le_def) lemma merge_restrict: assumes "t1 |` S = t |` S" assumes "t2 |` S = t |` S" shows "merge t1 t2 |` S = t |` S" proof - from assms have "∀x. (t1 |` S) x = (t |` S) x" and "∀x. (t2 |` S) x = (t |` S) x" by auto thus ?thesis by (auto simp: merge_def restrict_map_def split: if_splits) qed lemma defs_restrict: "defs c t |` (- lvars c) = t |` (- lvars c)" proof (induction c arbitrary: t) case (Seq c1 c2) hence "defs c1 t |` (- lvars c1) = t |` (- lvars c1)" by simp hence "defs c1 t |` (- lvars c1) |` (-lvars c2) = t |` (- lvars c1) |` (-lvars c2)" by simp moreover from Seq have "defs c2 (defs c1 t) |` (- lvars c2) = defs c1 t |` (- lvars c2)" by simp hence "defs c2 (defs c1 t) |` (- lvars c2) |` (- lvars c1) = defs c1 t |` (- lvars c2) |` (- lvars c1)" by simp ultimately show ?case by (clarsimp simp: Int_commute) next case (If b c1 c2) hence "defs c1 t |` (- lvars c1) = t |` (- lvars c1)" by simp hence "defs c1 t |` (- lvars c1) |` (-lvars c2) = t |` (- lvars c1) |` (-lvars c2)" by simp moreover from If have "defs c2 t |` (- lvars c2) = t |` (- lvars c2)" by simp hence "defs c2 t |` (- lvars c2) |` (-lvars c1) = t |` (- lvars c2) |` (-lvars c1)" by simp ultimately show ?case by (auto simp: Int_commute intro: merge_restrict) qed (auto split: aexp.split) lemma big_step_pres_approx: "(c,s) => s' ==> approx t s ==> approx (defs c t) s'" proof (induction arbitrary: t rule: big_step_induct) case Skip thus ?case by simp next case Assign thus ?case by (clarsimp simp: aval_afold_N approx_def split: aexp.split) next case (Seq c1 s1 s2 c2 s3) have "approx (defs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems]) hence "approx (defs c2 (defs c1 t)) s3" by (rule Seq.IH(2)) thus ?case by simp next case (IfTrue b s c1 s') hence "approx (defs c1 t) s'" by simp thus ?case by (simp add: approx_merge) next case (IfFalse b s c2 s') hence "approx (defs c2 t) s'" by simp thus ?case by (simp add: approx_merge) next case WhileFalse thus ?case by (simp add: approx_def restrict_map_def) next case (WhileTrue b s1 c s2 s3) hence "approx (defs c t) s2" by simp with WhileTrue have "approx (defs c t |` (-lvars c)) s3" by simp thus ?case by (simp add: defs_restrict) qed lemma big_step_pres_approx_restrict: "(c,s) => s' ==> approx (t |` (-lvars c)) s ==> approx (t |` (-lvars c)) s'" proof (induction arbitrary: t rule: big_step_induct) case Assign thus ?case by (clarsimp simp: approx_def) next case (Seq c1 s1 s2 c2 s3) hence "approx (t |` (-lvars c2) |` (-lvars c1)) s1" by (simp add: Int_commute) hence "approx (t |` (-lvars c2) |` (-lvars c1)) s2" by (rule Seq) hence "approx (t |` (-lvars c1) |` (-lvars c2)) s2" by (simp add: Int_commute) hence "approx (t |` (-lvars c1) |` (-lvars c2)) s3" by (rule Seq) thus ?case by simp next case (IfTrue b s c1 s' c2) hence "approx (t |` (-lvars c2) |` (-lvars c1)) s" by (simp add: Int_commute) hence "approx (t |` (-lvars c2) |` (-lvars c1)) s'" by (rule IfTrue) thus ?case by (simp add: Int_commute) next case (IfFalse b s c2 s' c1) hence "approx (t |` (-lvars c1) |` (-lvars c2)) s" by simp hence "approx (t |` (-lvars c1) |` (-lvars c2)) s'" by (rule IfFalse) thus ?case by simp qed auto declare assign_simp [simp] lemma approx_eq: "approx t \<Turnstile> c ∼ fold c t" proof (induction c arbitrary: t) case SKIP show ?case by simp next case Assign show ?case by (simp add: equiv_up_to_def) next case Seq thus ?case by (auto intro!: equiv_up_to_seq big_step_pres_approx) next case If thus ?case by (auto intro!: equiv_up_to_if_weak) next case (While b c) hence "approx (t |` (- lvars c)) \<Turnstile> WHILE b DO c ∼ WHILE b DO fold c (t |` (- lvars c))" by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict) thus ?case by (auto intro: equiv_up_to_weaken approx_map_le) qed lemma approx_empty [simp]: "approx empty = (λ_. True)" by (auto simp: approx_def) theorem constant_folding_equiv: "fold c empty ∼ c" using approx_eq [of empty c] by (simp add: equiv_up_to_True sim_sym) end