src/HOL/IMP/Fold.thy
author paulson <lp15@cam.ac.uk>
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