src/HOL/IMP/Live_True.thy
 author paulson Mon May 23 15:33:24 2016 +0100 (2016-05-23) changeset 63114 27afe7af7379 parent 53015 a1119cf551e8 child 66453 cc19f7ca2ed6 permissions -rw-r--r--
Lots of new material for multivariate analysis
```     1 (* Author: Tobias Nipkow *)
```
```     2
```
```     3 theory Live_True
```
```     4 imports "~~/src/HOL/Library/While_Combinator" Vars Big_Step
```
```     5 begin
```
```     6
```
```     7 subsection "True Liveness Analysis"
```
```     8
```
```     9 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
```
```    10 "L SKIP X = X" |
```
```    11 "L (x ::= a) X = (if x \<in> X then vars a \<union> (X - {x}) else X)" |
```
```    12 "L (c\<^sub>1;; c\<^sub>2) X = L c\<^sub>1 (L c\<^sub>2 X)" |
```
```    13 "L (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = vars b \<union> L c\<^sub>1 X \<union> L c\<^sub>2 X" |
```
```    14 "L (WHILE b DO c) X = lfp(\<lambda>Y. vars b \<union> X \<union> L c Y)"
```
```    15
```
```    16 lemma L_mono: "mono (L c)"
```
```    17 proof-
```
```    18   { fix X Y have "X \<subseteq> Y \<Longrightarrow> L c X \<subseteq> L c Y"
```
```    19     proof(induction c arbitrary: X Y)
```
```    20       case (While b c)
```
```    21       show ?case
```
```    22       proof(simp, rule lfp_mono)
```
```    23         fix Z show "vars b \<union> X \<union> L c Z \<subseteq> vars b \<union> Y \<union> L c Z"
```
```    24           using While by auto
```
```    25       qed
```
```    26     next
```
```    27       case If thus ?case by(auto simp: subset_iff)
```
```    28     qed auto
```
```    29   } thus ?thesis by(rule monoI)
```
```    30 qed
```
```    31
```
```    32 lemma mono_union_L:
```
```    33   "mono (\<lambda>Y. X \<union> L c Y)"
```
```    34 by (metis (no_types) L_mono mono_def order_eq_iff set_eq_subset sup_mono)
```
```    35
```
```    36 lemma L_While_unfold:
```
```    37   "L (WHILE b DO c) X = vars b \<union> X \<union> L c (L (WHILE b DO c) X)"
```
```    38 by(metis lfp_unfold[OF mono_union_L] L.simps(5))
```
```    39
```
```    40 lemma L_While_pfp: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
```
```    41 using L_While_unfold by blast
```
```    42
```
```    43 lemma L_While_vars: "vars b \<subseteq> L (WHILE b DO c) X"
```
```    44 using L_While_unfold by blast
```
```    45
```
```    46 lemma L_While_X: "X \<subseteq> L (WHILE b DO c) X"
```
```    47 using L_While_unfold by blast
```
```    48
```
```    49 text{* Disable @{text "L WHILE"} equation and reason only with @{text "L WHILE"} constraints: *}
```
```    50 declare L.simps(5)[simp del]
```
```    51
```
```    52
```
```    53 subsection "Correctness"
```
```    54
```
```    55 theorem L_correct:
```
```    56   "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
```
```    57   \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
```
```    58 proof (induction arbitrary: X t rule: big_step_induct)
```
```    59   case Skip then show ?case by auto
```
```    60 next
```
```    61   case Assign then show ?case
```
```    62     by (auto simp: ball_Un)
```
```    63 next
```
```    64   case (Seq c1 s1 s2 c2 s3 X t1)
```
```    65   from Seq.IH(1) Seq.prems obtain t2 where
```
```    66     t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
```
```    67     by simp blast
```
```    68   from Seq.IH(2)[OF s2t2] obtain t3 where
```
```    69     t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
```
```    70     by auto
```
```    71   show ?case using t12 t23 s3t3 by auto
```
```    72 next
```
```    73   case (IfTrue b s c1 s' c2)
```
```    74   hence "s = t on vars b" and "s = t on L c1 X" by auto
```
```    75   from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
```
```    76   from IfTrue.IH[OF `s = t on L c1 X`] obtain t' where
```
```    77     "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
```
```    78   thus ?case using `bval b t` by auto
```
```    79 next
```
```    80   case (IfFalse b s c2 s' c1)
```
```    81   hence "s = t on vars b" "s = t on L c2 X" by auto
```
```    82   from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
```
```    83   from IfFalse.IH[OF `s = t on L c2 X`] obtain t' where
```
```    84     "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
```
```    85   thus ?case using `~bval b t` by auto
```
```    86 next
```
```    87   case (WhileFalse b s c)
```
```    88   hence "~ bval b t"
```
```    89     by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
```
```    90   thus ?case using WhileFalse.prems L_While_X[of X b c] by auto
```
```    91 next
```
```    92   case (WhileTrue b s1 c s2 s3 X t1)
```
```    93   let ?w = "WHILE b DO c"
```
```    94   from `bval b s1` WhileTrue.prems have "bval b t1"
```
```    95     by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
```
```    96   have "s1 = t1 on L c (L ?w X)" using  L_While_pfp WhileTrue.prems
```
```    97     by (blast)
```
```    98   from WhileTrue.IH(1)[OF this] obtain t2 where
```
```    99     "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
```
```   100   from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
```
```   101     by auto
```
```   102   with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
```
```   103 qed
```
```   104
```
```   105
```
```   106 subsection "Executability"
```
```   107
```
```   108 lemma L_subset_vars: "L c X \<subseteq> rvars c \<union> X"
```
```   109 proof(induction c arbitrary: X)
```
```   110   case (While b c)
```
```   111   have "lfp(\<lambda>Y. vars b \<union> X \<union> L c Y) \<subseteq> vars b \<union> rvars c \<union> X"
```
```   112     using While.IH[of "vars b \<union> rvars c \<union> X"]
```
```   113     by (auto intro!: lfp_lowerbound)
```
```   114   thus ?case by (simp add: L.simps(5))
```
```   115 qed auto
```
```   116
```
```   117 text{* Make @{const L} executable by replacing @{const lfp} with the @{const
```
```   118 while} combinator from theory @{theory While_Combinator}. The @{const while}
```
```   119 combinator obeys the recursion equation
```
```   120 @{thm[display] While_Combinator.while_unfold[no_vars]}
```
```   121 and is thus executable. *}
```
```   122
```
```   123 lemma L_While: fixes b c X
```
```   124 assumes "finite X" defines "f == \<lambda>Y. vars b \<union> X \<union> L c Y"
```
```   125 shows "L (WHILE b DO c) X = while (\<lambda>Y. f Y \<noteq> Y) f {}" (is "_ = ?r")
```
```   126 proof -
```
```   127   let ?V = "vars b \<union> rvars c \<union> X"
```
```   128   have "lfp f = ?r"
```
```   129   proof(rule lfp_while[where C = "?V"])
```
```   130     show "mono f" by(simp add: f_def mono_union_L)
```
```   131   next
```
```   132     fix Y show "Y \<subseteq> ?V \<Longrightarrow> f Y \<subseteq> ?V"
```
```   133       unfolding f_def using L_subset_vars[of c] by blast
```
```   134   next
```
```   135     show "finite ?V" using `finite X` by simp
```
```   136   qed
```
```   137   thus ?thesis by (simp add: f_def L.simps(5))
```
```   138 qed
```
```   139
```
```   140 lemma L_While_let: "finite X \<Longrightarrow> L (WHILE b DO c) X =
```
```   141   (let f = (\<lambda>Y. vars b \<union> X \<union> L c Y)
```
```   142    in while (\<lambda>Y. f Y \<noteq> Y) f {})"
```
```   143 by(simp add: L_While)
```
```   144
```
```   145 lemma L_While_set: "L (WHILE b DO c) (set xs) =
```
```   146   (let f = (\<lambda>Y. vars b \<union> set xs \<union> L c Y)
```
```   147    in while (\<lambda>Y. f Y \<noteq> Y) f {})"
```
```   148 by(rule L_While_let, simp)
```
```   149
```
```   150 text{* Replace the equation for @{text "L (WHILE \<dots>)"} by the executable @{thm[source] L_While_set}: *}
```
```   151 lemmas [code] = L.simps(1-4) L_While_set
```
```   152 text{* Sorry, this syntax is odd. *}
```
```   153
```
```   154 text{* A test: *}
```
```   155 lemma "(let b = Less (N 0) (V ''y''); c = ''y'' ::= V ''x'';; ''x'' ::= V ''z''
```
```   156   in L (WHILE b DO c) {''y''}) = {''x'', ''y'', ''z''}"
```
```   157 by eval
```
```   158
```
```   159
```
```   160 subsection "Limiting the number of iterations"
```
```   161
```
```   162 text{* The final parameter is the default value: *}
```
```   163
```
```   164 fun iter :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
```
```   165 "iter f 0 p d = d" |
```
```   166 "iter f (Suc n) p d = (if f p = p then p else iter f n (f p) d)"
```
```   167
```
```   168 text{* A version of @{const L} with a bounded number of iterations (here: 2)
```
```   169 in the WHILE case: *}
```
```   170
```
```   171 fun Lb :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
```
```   172 "Lb SKIP X = X" |
```
```   173 "Lb (x ::= a) X = (if x \<in> X then X - {x} \<union> vars a else X)" |
```
```   174 "Lb (c\<^sub>1;; c\<^sub>2) X = (Lb c\<^sub>1 \<circ> Lb c\<^sub>2) X" |
```
```   175 "Lb (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = vars b \<union> Lb c\<^sub>1 X \<union> Lb c\<^sub>2 X" |
```
```   176 "Lb (WHILE b DO c) X = iter (\<lambda>A. vars b \<union> X \<union> Lb c A) 2 {} (vars b \<union> rvars c \<union> X)"
```
```   177
```
```   178 text{* @{const Lb} (and @{const iter}) is not monotone! *}
```
```   179 lemma "let w = WHILE Bc False DO (''x'' ::= V ''y'';; ''z'' ::= V ''x'')
```
```   180   in \<not> (Lb w {''z''} \<subseteq> Lb w {''y'',''z''})"
```
```   181 by eval
```
```   182
```
```   183 lemma lfp_subset_iter:
```
```   184   "\<lbrakk> mono f; !!X. f X \<subseteq> f' X; lfp f \<subseteq> D \<rbrakk> \<Longrightarrow> lfp f \<subseteq> iter f' n A D"
```
```   185 proof(induction n arbitrary: A)
```
```   186   case 0 thus ?case by simp
```
```   187 next
```
```   188   case Suc thus ?case by simp (metis lfp_lowerbound)
```
```   189 qed
```
```   190
```
```   191 lemma "L c X \<subseteq> Lb c X"
```
```   192 proof(induction c arbitrary: X)
```
```   193   case (While b c)
```
```   194   let ?f  = "\<lambda>A. vars b \<union> X \<union> L  c A"
```
```   195   let ?fb = "\<lambda>A. vars b \<union> X \<union> Lb c A"
```
```   196   show ?case
```
```   197   proof (simp add: L.simps(5), rule lfp_subset_iter[OF mono_union_L])
```
```   198     show "!!X. ?f X \<subseteq> ?fb X" using While.IH by blast
```
```   199     show "lfp ?f \<subseteq> vars b \<union> rvars c \<union> X"
```
```   200       by (metis (full_types) L.simps(5) L_subset_vars rvars.simps(5))
```
```   201   qed
```
```   202 next
```
```   203   case Seq thus ?case by simp (metis (full_types) L_mono monoD subset_trans)
```
```   204 qed auto
```
```   205
```
```   206 end
```