# HG changeset patch
# User kleing
# Date 1392807743 -39600
# Node ID a0134252ac29d17d4717e197efbbfc5b86362b2c
# Parent  20054fc56d1794ff31bb6b3f8a10862721b11c1b
moved advanced folding into separate exercise

diff -r 20054fc56d17 -r a0134252ac29 src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Wed Feb 19 22:02:00 2014 +1100
+++ b/src/HOL/IMP/Fold.thy	Wed Feb 19 22:02:23 2014 +1100
@@ -202,185 +202,4 @@
   by (simp add: equiv_up_to_True sim_sym)
 
 
-
-subsection {* More ambitious folding including boolean expressions *}
-
-
-fun bfold :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where
-"bfold (Less a1 a2) t = less (afold a1 t) (afold a2 t)" |
-"bfold (And b1 b2) t = and (bfold b1 t) (bfold b2 t)" |
-"bfold (Not b) t = not(bfold b t)" |
-"bfold (Bc bc) _ = Bc bc"
-
-theorem bval_bfold [simp]:
-  assumes "approx t s"
-  shows "bval (bfold b t) s = bval b s"
-  using assms by (induct b) auto
-
-lemma not_Bc [simp]: "not (Bc v) = Bc (\<not>v)"
-  by (cases v) auto
-
-lemma not_Bc_eq [simp]: "(not b = Bc v) = (b = Bc (\<not>v))"
-  by (cases b) auto
-
-lemma and_Bc_eq:
-  "(and a b = Bc v) =
-   (a = Bc False \<and> \<not>v  \<or>  b = Bc False \<and> \<not>v \<or>
-    (\<exists>v1 v2. a = Bc v1 \<and> b = Bc v2 \<and> v = v1 \<and> v2))"
-  by (rule and.induct) auto
-
-lemma less_Bc_eq [simp]:
-  "(less a b = Bc v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
-  by (rule less.induct) auto
-
-theorem bval_bfold_Bc:
-assumes "approx t s"
-shows "bfold b t = Bc v \<Longrightarrow> bval b s = v"
-  using assms
-  by (induct b arbitrary: v)
-     (auto simp: approx_def and_Bc_eq aval_afold_N
-           split: bexp.splits bool.splits)
-
-
-primrec "bdefs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
-"bdefs SKIP t = t" |
-"bdefs (x ::= a) t =
-  (case afold a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
-"bdefs (c1;;c2) t = (bdefs c2 o bdefs c1) t" |
-"bdefs (IF b THEN c1 ELSE c2) t = (case bfold b t of
-    Bc True \<Rightarrow> bdefs c1 t
-  | Bc False \<Rightarrow> bdefs c2 t
-  | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
-"bdefs (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 (bdefs c1 t))" |
-"fold' (IF b THEN c1 ELSE c2) t = (case bfold b t of
-    Bc True \<Rightarrow> fold' c1 t
-  | Bc False \<Rightarrow> fold' c2 t
-  | _ \<Rightarrow> IF bfold b t THEN fold' c1 t ELSE fold' c2 t)" |
-"fold' (WHILE b DO c) t = (case bfold b t of
-    Bc False \<Rightarrow> SKIP
-  | _ \<Rightarrow> WHILE bfold b (t |` (-lvars c)) DO fold' c (t |` (-lvars c)))"
-
-
-lemma bdefs_restrict:
-  "bdefs c t |` (- lvars c) = t |` (- lvars c)"
-proof (induction c arbitrary: t)
-  case (Seq c1 c2)
-  hence "bdefs c1 t |` (- lvars c1) = t |` (- lvars c1)"
-    by simp
-  hence "bdefs c1 t |` (- lvars c1) |` (-lvars c2) =
-         t |` (- lvars c1) |` (-lvars c2)" by simp
-  moreover
-  from Seq
-  have "bdefs c2 (bdefs c1 t) |` (- lvars c2) =
-        bdefs c1 t |` (- lvars c2)"
-    by simp
-  hence "bdefs c2 (bdefs c1 t) |` (- lvars c2) |` (- lvars c1) =
-         bdefs c1 t |` (- lvars c2) |` (- lvars c1)"
-    by simp
-  ultimately
-  show ?case by (clarsimp simp: Int_commute)
-next
-  case (If b c1 c2)
-  hence "bdefs c1 t |` (- lvars c1) = t |` (- lvars c1)" by simp
-  hence "bdefs c1 t |` (- lvars c1) |` (-lvars c2) =
-         t |` (- lvars c1) |` (-lvars c2)" by simp
-  moreover
-  from If
-  have "bdefs c2 t |` (- lvars c2) = t |` (- lvars c2)" by simp
-  hence "bdefs c2 t |` (- lvars c2) |` (-lvars c1) =
-         t |` (- lvars c2) |` (-lvars 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) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs 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 (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 simp
-next
-  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 bval_bfold_Bc
-                 split: bexp.splits bool.splits)
-next
-  case (IfFalse b s c2 s')
-  hence "approx (bdefs c2 t) s'" by simp
-  thus ?case using `\<not>bval b s` `approx t s`
-    by (clarsimp simp: approx_merge bval_bfold_Bc
-                 split: bexp.splits bool.splits)
-next
-  case WhileFalse
-  thus ?case
-    by (clarsimp simp: bval_bfold_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 |` (- lvars c)) s3"
-    by simp
-  thus ?case
-    by (simp add: bdefs_restrict)
-qed
-
-lemma fold'_equiv:
-  "approx t \<Turnstile> c \<sim> fold' c t"
-proof (induction c arbitrary: t)
-  case SKIP show ?case by simp
-next
-  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 \<sim>
-                   IF bfold b t THEN fold' c1 t ELSE fold' c2 t"
-    by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def)
-  thus ?case using If
-    by (fastforce simp: bval_bfold_Bc split: bexp.splits bool.splits
-                 intro: equiv_up_to_trans)
-  next
-  case (While b c)
-  hence "approx (t |` (- lvars c)) \<Turnstile>
-                   WHILE b DO c \<sim>
-                   WHILE bfold b (t |` (- lvars c))
-                      DO fold' c (t |` (- lvars c))" (is "_ \<Turnstile> ?W \<sim> ?W'")
-    by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict
-             simp: bequiv_up_to_def)
-  hence "approx t \<Turnstile> ?W \<sim> ?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: bval_bfold_Bc)
-qed
-
-
-theorem constant_folding_equiv':
-  "fold' c empty \<sim> c"
-  using fold'_equiv [of empty c]
-  by (simp add: equiv_up_to_True sim_sym)
-
-
 end