Theory Fold

Up to index of Isabelle/HOL/HOL-IMP

theory Fold
imports Sem_Equiv
`header "Constant Folding"theory Fold imports Sem_Equiv beginsubsection "Simple folding of arithmetic expressions"type_synonym  tab = "vname => val option"(* maybe better as the composition of substitution and the existing simp_const(0) *)fun simp_const :: "aexp => tab => aexp" where"simp_const (N n) _ = N n" |"simp_const (V x) t = (case t x of None => V x | Some k => N k)" |"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const 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_simp_const[simp]:assumes "approx t s"shows "aval (simp_const a t) s = aval a s"  using assms  by (induct a) (auto simp: approx_def split: aexp.split option.split)theorem aval_simp_const_N:assumes "approx t s"shows "simp_const a t = N n ==> aval a s = n"  using assms  by (induct a arbitrary: n)     (auto simp: approx_def split: aexp.splits option.splits)definition  "merge t1 t2 = (λm. if t1 m = t2 m then t1 m else None)"primrec lnames :: "com => vname set" where"lnames SKIP = {}" |"lnames (x ::= a) = {x}" |"lnames (c1; c2) = lnames c1 ∪ lnames c2" |"lnames (IF b THEN c1 ELSE c2) = lnames c1 ∪ lnames c2" |"lnames (WHILE b DO c) = lnames c"primrec "defs" :: "com => tab => tab" where"defs SKIP t = t" |"defs (x ::= a) t =  (case simp_const 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 |` (-lnames c)"primrec fold where"fold SKIP _ = SKIP" |"fold (x ::= a) t = (x ::= (simp_const 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 |` (-lnames 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 intro: ext)qedlemma defs_restrict:  "defs c t |` (- lnames c) = t |` (- lnames c)"proof (induction c arbitrary: t)  case (Seq c1 c2)  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)"    by simp  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =         t |` (- lnames c1) |` (-lnames c2)" by simp  moreover  from Seq  have "defs c2 (defs c1 t) |` (- lnames c2) =        defs c1 t |` (- lnames c2)"    by simp  hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) =         defs c1 t |` (- lnames c2) |` (- lnames c1)"    by simp  ultimately  show ?case by (clarsimp simp: Int_commute)next  case (If b c1 c2)  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =         t |` (- lnames c1) |` (-lnames c2)" by simp  moreover  from If  have "defs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp  hence "defs c2 t |` (- lnames c2) |` (-lnames c1) =         t |` (- lnames c2) |` (-lnames 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 simpnext  case Assign  thus ?case    by (clarsimp simp: aval_simp_const_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 simpnext  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 |` (-lnames c)) s3" by simp  thus ?case by (simp add: defs_restrict)qedlemma big_step_pres_approx_restrict:  "(c,s) => s' ==> approx (t |` (-lnames c)) s ==> approx (t |` (-lnames 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 |` (-lnames c2) |` (-lnames c1)) s1"    by (simp add: Int_commute)  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"    by (rule Seq)  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2"    by (simp add: Int_commute)  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3"    by (rule Seq)  thus ?case by simpnext  case (IfTrue b s c1 s' c2)  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s"    by (simp add: Int_commute)  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'"    by (rule IfTrue)  thus ?case by (simp add: Int_commute)next  case (IfFalse b s c2 s' c1)  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s"    by simp  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'"    by (rule IfFalse)  thus ?case by simpqed autodeclare assign_simp [simp]lemma approx_eq:  "approx t \<Turnstile> c ∼ fold c t"proof (induction c arbitrary: t)  case SKIP show ?case by simpnext  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 |` (- lnames c)) \<Turnstile>         WHILE b DO c ∼ WHILE b DO fold c (t |` (- lnames 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)qedlemma approx_empty [simp]:  "approx empty = (λ_. True)"  by (auto intro!: ext simp: approx_def)lemma equiv_sym:  "c ∼ c' <-> c' ∼ c"  by (auto simp add: equiv_def)theorem constant_folding_equiv:  "fold c empty ∼ c"  using approx_eq [of empty c]  by (simp add: equiv_up_to_True equiv_sym)subsection {* More ambitious folding including boolean expressions *}fun bsimp_const :: "bexp => tab => bexp" where"bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" |"bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" |"bsimp_const (Not b) t = not(bsimp_const b t)" |"bsimp_const (Bc bc) _ = Bc bc"theorem bvalsimp_const [simp]:  assumes "approx t s"  shows "bval (bsimp_const b t) s = bval b s"  using assms by (induct b) autolemma not_Bc [simp]: "not (Bc v) = Bc (¬v)"  by (cases v) autolemma not_Bc_eq [simp]: "(not b = Bc v) = (b = Bc (¬v))"  by (cases b) autolemma and_Bc_eq:  "(and a b = Bc v) =   (a = Bc False ∧ ¬v  ∨  b = Bc False ∧ ¬v ∨    (∃v1 v2. a = Bc v1 ∧ b = Bc v2 ∧ v = v1 ∧ v2))"  by (rule and.induct) autolemma less_Bc_eq [simp]:  "(less a b = Bc v) = (∃n1 n2. a = N n1 ∧ b = N n2 ∧ v = (n1 < n2))"  by (rule less.induct) autotheorem bvalsimp_const_Bc:assumes "approx t s"shows "bsimp_const b t = Bc v ==> bval b s = v"  using assms  by (induct b arbitrary: v)     (auto simp: approx_def and_Bc_eq aval_simp_const_N           split: bexp.splits bool.splits)primrec "bdefs" :: "com => tab => tab" where"bdefs SKIP t = t" |"bdefs (x ::= a) t =  (case simp_const a t of N k => t(x \<mapsto> k) | _ => t(x:=None))" |"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" |"bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of    Bc True => bdefs c1 t  | Bc False => bdefs c2 t  | _ => merge (bdefs c1 t) (bdefs c2 t))" |"bdefs (WHILE b DO c) t = t |` (-lnames c)"primrec bfold where"bfold SKIP _ = SKIP" |"bfold (x ::= a) t = (x ::= (simp_const a t))" |"bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))" |"bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of    Bc True => bfold c1 t  | Bc False => bfold c2 t  | _ => IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)" |"bfold (WHILE b DO c) t = (case bsimp_const b t of    Bc False => SKIP  | _ => WHILE bsimp_const b (t |` (-lnames c)) DO bfold c (t |` (-lnames c)))"lemma bdefs_restrict:  "bdefs c t |` (- lnames c) = t |` (- lnames c)"proof (induction c arbitrary: t)  case (Seq c1 c2)  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)"    by simp  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =         t |` (- lnames c1) |` (-lnames c2)" by simp  moreover  from Seq  have "bdefs c2 (bdefs c1 t) |` (- lnames c2) =        bdefs c1 t |` (- lnames c2)"    by simp  hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) =         bdefs c1 t |` (- lnames c2) |` (- lnames c1)"    by simp  ultimately  show ?case by (clarsimp simp: Int_commute)next  case (If b c1 c2)  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =         t |` (- lnames c1) |` (-lnames c2)" by simp  moreover  from If  have "bdefs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp  hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) =         t |` (- lnames c2) |` (-lnames c1)" by simp  ultimately  show ?case    by (auto simp: Int_commute intro: merge_restrict             split: bexp.splits bool.splits)qed (auto split: aexp.split bexp.split bool.split)lemma big_step_pres_approx_b:  "(c,s) => s' ==> approx t s ==> approx (bdefs c t) s'"proof (induction arbitrary: t rule: big_step_induct)  case Skip thus ?case by simpnext  case Assign  thus ?case    by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)next  case (Seq c1 s1 s2 c2 s3)  have "approx (bdefs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems])  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Seq.IH(2))  thus ?case by simpnext  case (IfTrue b s c1 s')  hence "approx (bdefs c1 t) s'" by simp  thus ?case using `bval b s` `approx t s`    by (clarsimp simp: approx_merge bvalsimp_const_Bc                 split: bexp.splits bool.splits)next  case (IfFalse b s c2 s')  hence "approx (bdefs c2 t) s'" by simp  thus ?case using `¬bval b s` `approx t s`    by (clarsimp simp: approx_merge bvalsimp_const_Bc                 split: bexp.splits bool.splits)next  case WhileFalse  thus ?case    by (clarsimp simp: bvalsimp_const_Bc approx_def restrict_map_def                 split: bexp.splits bool.splits)next  case (WhileTrue b s1 c s2 s3)  hence "approx (bdefs c t) s2" by simp  with WhileTrue  have "approx (bdefs c t |` (- lnames c)) s3"    by simp  thus ?case    by (simp add: bdefs_restrict)qedlemma bfold_equiv:  "approx t \<Turnstile> c ∼ bfold c t"proof (induction c arbitrary: t)  case SKIP show ?case by simpnext  case Assign  thus ?case by (simp add: equiv_up_to_def)next  case Seq  thus ?case by (auto intro!: equiv_up_to_seq big_step_pres_approx_b)next  case (If b c1 c2)  hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 ∼                   IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"    by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def)  thus ?case using If    by (fastforce simp: bvalsimp_const_Bc split: bexp.splits bool.splits                 intro: equiv_up_to_trans)  next  case (While b c)  hence "approx (t |` (- lnames c)) \<Turnstile>                   WHILE b DO c ∼                   WHILE bsimp_const b (t |` (- lnames c))                      DO bfold c (t |` (- lnames c))" (is "_ \<Turnstile> ?W ∼ ?W'")    by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict             simp: bequiv_up_to_def)  hence "approx t \<Turnstile> ?W ∼ ?W'"    by (auto intro: equiv_up_to_weaken approx_map_le)  thus ?case    by (auto split: bexp.splits bool.splits             intro: equiv_up_to_while_False             simp: bvalsimp_const_Bc)qedtheorem constant_bfolding_equiv:  "bfold c empty ∼ c"  using bfold_equiv [of empty c]  by (simp add: equiv_up_to_True equiv_sym)end`