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