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