src/HOL/IMP/Fold.thy
 author paulson Mon May 23 15:33:24 2016 +0100 (2016-05-23) changeset 63114 27afe7af7379 parent 55583 a0134252ac29 child 67613 ce654b0e6d69 permissions -rw-r--r--
Lots of new material for multivariate analysis
```     1 theory Fold imports Sem_Equiv Vars begin
```
```     2
```
```     3 subsection "Simple folding of arithmetic expressions"
```
```     4
```
```     5 type_synonym
```
```     6   tab = "vname \<Rightarrow> val option"
```
```     7
```
```     8 fun afold :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
```
```     9 "afold (N n) _ = N n" |
```
```    10 "afold (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |
```
```    11 "afold (Plus e1 e2) t = (case (afold e1 t, afold e2 t) of
```
```    12   (N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')"
```
```    13
```
```    14 definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)"
```
```    15
```
```    16 theorem aval_afold[simp]:
```
```    17 assumes "approx t s"
```
```    18 shows "aval (afold a t) s = aval a s"
```
```    19   using assms
```
```    20   by (induct a) (auto simp: approx_def split: aexp.split option.split)
```
```    21
```
```    22 theorem aval_afold_N:
```
```    23 assumes "approx t s"
```
```    24 shows "afold a t = N n \<Longrightarrow> aval a s = n"
```
```    25   by (metis assms aval.simps(1) aval_afold)
```
```    26
```
```    27 definition
```
```    28   "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"
```
```    29
```
```    30 primrec "defs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
```
```    31 "defs SKIP t = t" |
```
```    32 "defs (x ::= a) t =
```
```    33   (case afold a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
```
```    34 "defs (c1;;c2) t = (defs c2 o defs c1) t" |
```
```    35 "defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
```
```    36 "defs (WHILE b DO c) t = t |` (-lvars c)"
```
```    37
```
```    38 primrec fold where
```
```    39 "fold SKIP _ = SKIP" |
```
```    40 "fold (x ::= a) t = (x ::= (afold a t))" |
```
```    41 "fold (c1;;c2) t = (fold c1 t;; fold c2 (defs c1 t))" |
```
```    42 "fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" |
```
```    43 "fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lvars c))"
```
```    44
```
```    45 lemma approx_merge:
```
```    46   "approx t1 s \<or> approx t2 s \<Longrightarrow> approx (merge t1 t2) s"
```
```    47   by (fastforce simp: merge_def approx_def)
```
```    48
```
```    49 lemma approx_map_le:
```
```    50   "approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s"
```
```    51   by (clarsimp simp: approx_def map_le_def dom_def)
```
```    52
```
```    53 lemma restrict_map_le [intro!, simp]: "t |` S \<subseteq>\<^sub>m t"
```
```    54   by (clarsimp simp: restrict_map_def map_le_def)
```
```    55
```
```    56 lemma merge_restrict:
```
```    57   assumes "t1 |` S = t |` S"
```
```    58   assumes "t2 |` S = t |` S"
```
```    59   shows "merge t1 t2 |` S = t |` S"
```
```    60 proof -
```
```    61   from assms
```
```    62   have "\<forall>x. (t1 |` S) x = (t |` S) x"
```
```    63    and "\<forall>x. (t2 |` S) x = (t |` S) x" by auto
```
```    64   thus ?thesis
```
```    65     by (auto simp: merge_def restrict_map_def
```
```    66              split: if_splits)
```
```    67 qed
```
```    68
```
```    69
```
```    70 lemma defs_restrict:
```
```    71   "defs c t |` (- lvars c) = t |` (- lvars c)"
```
```    72 proof (induction c arbitrary: t)
```
```    73   case (Seq c1 c2)
```
```    74   hence "defs c1 t |` (- lvars c1) = t |` (- lvars c1)"
```
```    75     by simp
```
```    76   hence "defs c1 t |` (- lvars c1) |` (-lvars c2) =
```
```    77          t |` (- lvars c1) |` (-lvars c2)" by simp
```
```    78   moreover
```
```    79   from Seq
```
```    80   have "defs c2 (defs c1 t) |` (- lvars c2) =
```
```    81         defs c1 t |` (- lvars c2)"
```
```    82     by simp
```
```    83   hence "defs c2 (defs c1 t) |` (- lvars c2) |` (- lvars c1) =
```
```    84          defs c1 t |` (- lvars c2) |` (- lvars c1)"
```
```    85     by simp
```
```    86   ultimately
```
```    87   show ?case by (clarsimp simp: Int_commute)
```
```    88 next
```
```    89   case (If b c1 c2)
```
```    90   hence "defs c1 t |` (- lvars c1) = t |` (- lvars c1)" by simp
```
```    91   hence "defs c1 t |` (- lvars c1) |` (-lvars c2) =
```
```    92          t |` (- lvars c1) |` (-lvars c2)" by simp
```
```    93   moreover
```
```    94   from If
```
```    95   have "defs c2 t |` (- lvars c2) = t |` (- lvars c2)" by simp
```
```    96   hence "defs c2 t |` (- lvars c2) |` (-lvars c1) =
```
```    97          t |` (- lvars c2) |` (-lvars c1)" by simp
```
```    98   ultimately
```
```    99   show ?case by (auto simp: Int_commute intro: merge_restrict)
```
```   100 qed (auto split: aexp.split)
```
```   101
```
```   102
```
```   103 lemma big_step_pres_approx:
```
```   104   "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"
```
```   105 proof (induction arbitrary: t rule: big_step_induct)
```
```   106   case Skip thus ?case by simp
```
```   107 next
```
```   108   case Assign
```
```   109   thus ?case
```
```   110     by (clarsimp simp: aval_afold_N approx_def split: aexp.split)
```
```   111 next
```
```   112   case (Seq c1 s1 s2 c2 s3)
```
```   113   have "approx (defs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems])
```
```   114   hence "approx (defs c2 (defs c1 t)) s3" by (rule Seq.IH(2))
```
```   115   thus ?case by simp
```
```   116 next
```
```   117   case (IfTrue b s c1 s')
```
```   118   hence "approx (defs c1 t) s'" by simp
```
```   119   thus ?case by (simp add: approx_merge)
```
```   120 next
```
```   121   case (IfFalse b s c2 s')
```
```   122   hence "approx (defs c2 t) s'" by simp
```
```   123   thus ?case by (simp add: approx_merge)
```
```   124 next
```
```   125   case WhileFalse
```
```   126   thus ?case by (simp add: approx_def restrict_map_def)
```
```   127 next
```
```   128   case (WhileTrue b s1 c s2 s3)
```
```   129   hence "approx (defs c t) s2" by simp
```
```   130   with WhileTrue
```
```   131   have "approx (defs c t |` (-lvars c)) s3" by simp
```
```   132   thus ?case by (simp add: defs_restrict)
```
```   133 qed
```
```   134
```
```   135
```
```   136 lemma big_step_pres_approx_restrict:
```
```   137   "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lvars c)) s \<Longrightarrow> approx (t |` (-lvars c)) s'"
```
```   138 proof (induction arbitrary: t rule: big_step_induct)
```
```   139   case Assign
```
```   140   thus ?case by (clarsimp simp: approx_def)
```
```   141 next
```
```   142   case (Seq c1 s1 s2 c2 s3)
```
```   143   hence "approx (t |` (-lvars c2) |` (-lvars c1)) s1"
```
```   144     by (simp add: Int_commute)
```
```   145   hence "approx (t |` (-lvars c2) |` (-lvars c1)) s2"
```
```   146     by (rule Seq)
```
```   147   hence "approx (t |` (-lvars c1) |` (-lvars c2)) s2"
```
```   148     by (simp add: Int_commute)
```
```   149   hence "approx (t |` (-lvars c1) |` (-lvars c2)) s3"
```
```   150     by (rule Seq)
```
```   151   thus ?case by simp
```
```   152 next
```
```   153   case (IfTrue b s c1 s' c2)
```
```   154   hence "approx (t |` (-lvars c2) |` (-lvars c1)) s"
```
```   155     by (simp add: Int_commute)
```
```   156   hence "approx (t |` (-lvars c2) |` (-lvars c1)) s'"
```
```   157     by (rule IfTrue)
```
```   158   thus ?case by (simp add: Int_commute)
```
```   159 next
```
```   160   case (IfFalse b s c2 s' c1)
```
```   161   hence "approx (t |` (-lvars c1) |` (-lvars c2)) s"
```
```   162     by simp
```
```   163   hence "approx (t |` (-lvars c1) |` (-lvars c2)) s'"
```
```   164     by (rule IfFalse)
```
```   165   thus ?case by simp
```
```   166 qed auto
```
```   167
```
```   168
```
```   169 declare assign_simp [simp]
```
```   170
```
```   171 lemma approx_eq:
```
```   172   "approx t \<Turnstile> c \<sim> fold c t"
```
```   173 proof (induction c arbitrary: t)
```
```   174   case SKIP show ?case by simp
```
```   175 next
```
```   176   case Assign
```
```   177   show ?case by (simp add: equiv_up_to_def)
```
```   178 next
```
```   179   case Seq
```
```   180   thus ?case by (auto intro!: equiv_up_to_seq big_step_pres_approx)
```
```   181 next
```
```   182   case If
```
```   183   thus ?case by (auto intro!: equiv_up_to_if_weak)
```
```   184 next
```
```   185   case (While b c)
```
```   186   hence "approx (t |` (- lvars c)) \<Turnstile>
```
```   187          WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lvars c))"
```
```   188     by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict)
```
```   189   thus ?case
```
```   190     by (auto intro: equiv_up_to_weaken approx_map_le)
```
```   191 qed
```
```   192
```
```   193
```
```   194 lemma approx_empty [simp]:
```
```   195   "approx empty = (\<lambda>_. True)"
```
```   196   by (auto simp: approx_def)
```
```   197
```
```   198
```
```   199 theorem constant_folding_equiv:
```
```   200   "fold c empty \<sim> c"
```
```   201   using approx_eq [of empty c]
```
```   202   by (simp add: equiv_up_to_True sim_sym)
```
```   203
```
```   204
```
```   205 end
```