src/HOL/IMP/Live_True.thy
author nipkow
Sat, 28 Apr 2012 07:38:22 +0200
changeset 47818 151d137f1095
parent 46365 547d1a1dcaf6
child 48256 5fa4fc4d721a
permissions -rw-r--r--
renamed Semi to Seq
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45812
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
     2
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
     3
theory Live_True
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
     4
imports "~~/src/HOL/Library/While_Combinator" Vars Big_Step
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
     5
begin
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
     6
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
     7
subsection "True Liveness Analysis"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
     8
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
     9
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    10
"L SKIP X = X" |
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    11
"L (x ::= a) X = (if x:X then X-{x} \<union> vars a else X)" |
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    12
"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    13
"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    14
"L (WHILE b DO c) X = lfp(%Y. vars b \<union> X \<union> L c Y)"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    15
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    16
lemma L_mono: "mono (L c)"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    17
proof-
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    18
  { fix X Y have "X \<subseteq> Y \<Longrightarrow> L c X \<subseteq> L c Y"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    19
    proof(induction c arbitrary: X Y)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    20
      case (While b c)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    21
      show ?case
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    22
      proof(simp, rule lfp_mono)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    23
        fix Z show "vars b \<union> X \<union> L c Z \<subseteq> vars b \<union> Y \<union> L c Z"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    24
          using While by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    25
      qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    26
    next
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    27
      case If thus ?case by(auto simp: subset_iff)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    28
    qed auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    29
  } thus ?thesis by(rule monoI)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    30
qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    31
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    32
lemma mono_union_L:
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    33
  "mono (%Y. X \<union> L c Y)"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    34
by (metis (no_types) L_mono mono_def order_eq_iff set_eq_subset sup_mono)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    35
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    36
lemma L_While_unfold:
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    37
  "L (WHILE b DO c) X = vars b \<union> X \<union> L c (L (WHILE b DO c) X)"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    38
by(metis lfp_unfold[OF mono_union_L] L.simps(5))
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    39
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    40
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    41
subsection "Soundness"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    42
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    43
theorem L_sound:
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    44
  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    45
  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    46
proof (induction arbitrary: X t rule: big_step_induct)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    47
  case Skip then show ?case by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    48
next
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    49
  case Assign then show ?case
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    50
    by (auto simp: ball_Un)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    51
next
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 46365
diff changeset
    52
  case (Seq c1 s1 s2 c2 s3 X t1)
151d137f1095 renamed Semi to Seq
nipkow
parents: 46365
diff changeset
    53
  from Seq.IH(1) Seq.prems obtain t2 where
45812
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    54
    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    55
    by simp blast
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 46365
diff changeset
    56
  from Seq.IH(2)[OF s2t2] obtain t3 where
45812
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    57
    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    58
    by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    59
  show ?case using t12 t23 s3t3 by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    60
next
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    61
  case (IfTrue b s c1 s' c2)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    62
  hence "s = t on vars b" "s = t on L c1 X" by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    63
  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    64
  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    65
    "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    66
  thus ?case using `bval b t` by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    67
next
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    68
  case (IfFalse b s c2 s' c1)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    69
  hence "s = t on vars b" "s = t on L c2 X" by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    70
  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    71
  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    72
    "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    73
  thus ?case using `~bval b t` by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    74
next
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    75
  case (WhileFalse b s c)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    76
  hence "~ bval b t"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    77
    by (metis L_While_unfold UnI1 bval_eq_if_eq_on_vars)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    78
  thus ?case using WhileFalse.prems L_While_unfold[of b c X] by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    79
next
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    80
  case (WhileTrue b s1 c s2 s3 X t1)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    81
  let ?w = "WHILE b DO c"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    82
  from `bval b s1` WhileTrue.prems have "bval b t1"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    83
    by (metis L_While_unfold UnI1 bval_eq_if_eq_on_vars)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    84
  have "s1 = t1 on L c (L ?w X)" using  L_While_unfold WhileTrue.prems
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    85
    by (blast)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    86
  from WhileTrue.IH(1)[OF this] obtain t2 where
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    87
    "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    88
  from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    89
    by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    90
  with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    91
qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    92
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    93
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    94
instantiation com :: vars
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    95
begin
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    96
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    97
fun vars_com :: "com \<Rightarrow> vname set" where
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    98
"vars SKIP = {}" |
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
    99
"vars (x::=e) = vars e" |
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   100
"vars (c\<^isub>1; c\<^isub>2) = vars c\<^isub>1 \<union> vars c\<^isub>2" |
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   101
"vars (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> vars c\<^isub>1 \<union> vars c\<^isub>2" |
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   102
"vars (WHILE b DO c) = vars b \<union> vars c"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   103
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   104
instance ..
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   105
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   106
end
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   107
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   108
lemma L_subset_vars: "L c X \<subseteq> vars c \<union> X"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   109
proof(induction c arbitrary: X)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   110
  case (While b c)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   111
  have "lfp(%Y. vars b \<union> X \<union> L c Y) \<subseteq> vars b \<union> vars c \<union> X"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   112
    using While.IH[of "vars b \<union> vars c \<union> X"]
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   113
    by (auto intro!: lfp_lowerbound)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   114
  thus ?case by simp
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   115
qed auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   116
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   117
lemma afinite[simp]: "finite(vars(a::aexp))"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   118
by (induction a) auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   119
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   120
lemma bfinite[simp]: "finite(vars(b::bexp))"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   121
by (induction b) auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   122
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   123
lemma cfinite[simp]: "finite(vars(c::com))"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   124
by (induction c) auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   125
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   126
(* move to Inductive; call Kleene? *)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   127
lemma lfp_finite_iter: assumes "mono f" and "(f^^Suc k) bot = (f^^k) bot"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   128
shows "lfp f = (f^^k) bot"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   129
proof(rule antisym)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   130
  show "lfp f \<le> (f^^k) bot"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   131
  proof(rule lfp_lowerbound)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   132
    show "f ((f^^k) bot) \<le> (f^^k) bot" using assms(2) by simp
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   133
  qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   134
next
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   135
  show "(f^^k) bot \<le> lfp f"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   136
  proof(induction k)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   137
    case 0 show ?case by simp
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   138
  next
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   139
    case Suc
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   140
    from monoD[OF assms(1) Suc] lfp_unfold[OF assms(1)]
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   141
    show ?case by simp
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   142
  qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   143
qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   144
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   145
(* move to While_Combinator *)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   146
lemma while_option_stop2:
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   147
 "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   148
apply(simp add: while_option_def split: if_splits)
46365
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 45812
diff changeset
   149
by (metis (lifting) LeastI_ex)
45812
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   150
(* move to While_Combinator *)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   151
lemma while_option_finite_subset_Some: fixes C :: "'a set"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   152
  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   153
  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   154
proof(rule measure_while_option_Some[where
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   155
    f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   156
  fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   157
  show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   158
    (is "?L \<and> ?R")
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   159
  proof
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   160
    show ?L by(metis A(1) assms(2) monoD[OF `mono f`])
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   161
    show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   162
  qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   163
qed simp
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   164
(* move to While_Combinator *)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   165
lemma lfp_eq_while_option:
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   166
  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   167
  shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   168
proof-
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   169
  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   170
    using while_option_finite_subset_Some[OF assms] by blast
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   171
  with while_option_stop2[OF this] lfp_finite_iter[OF assms(1)]
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   172
  show ?thesis by auto
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   173
qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   174
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   175
text{* For code generation: *}
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   176
lemma L_While: fixes b c X
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   177
assumes "finite X" defines "f == \<lambda>A. vars b \<union> X \<union> L c A"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   178
shows "L (WHILE b DO c) X = the(while_option (\<lambda>A. f A \<noteq> A) f {})" (is "_ = ?r")
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   179
proof -
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   180
  let ?V = "vars b \<union> vars c \<union> X"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   181
  have "lfp f = ?r"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   182
  proof(rule lfp_eq_while_option[where C = "?V"])
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   183
    show "mono f" by(simp add: f_def mono_union_L)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   184
  next
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   185
    fix Y show "Y \<subseteq> ?V \<Longrightarrow> f Y \<subseteq> ?V"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   186
      unfolding f_def using L_subset_vars[of c] by blast
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   187
  next
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   188
    show "finite ?V" using `finite X` by simp
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   189
  qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   190
  thus ?thesis by (simp add: f_def)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   191
qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   192
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   193
text{* An approximate computation of the WHILE-case: *}
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   194
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   195
fun iter :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   196
where
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   197
"iter f 0 p d = d" |
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   198
"iter f (Suc n) p d = (if f p = p then p else iter f n (f p) d)"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   199
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   200
lemma iter_pfp:
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   201
  "f d \<le> d \<Longrightarrow> mono f \<Longrightarrow> x \<le> f x \<Longrightarrow> f(iter f i x d) \<le> iter f i x d"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   202
apply(induction i arbitrary: x)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   203
 apply simp
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   204
apply (simp add: mono_def)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   205
done
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   206
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   207
lemma iter_While_pfp:
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   208
fixes b c X W k f
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   209
defines "f == \<lambda>A. vars b \<union> X \<union> L c A" and "W == vars b \<union> vars c \<union> X"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   210
and "P == iter f k {} W"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   211
shows "f P \<subseteq> P"
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   212
proof-
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   213
  have "f W \<subseteq> W" unfolding f_def W_def using L_subset_vars[of c] by blast
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   214
  have "mono f" by(simp add: f_def mono_union_L)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   215
  from iter_pfp[of f, OF `f W \<subseteq> W` `mono f` empty_subsetI]
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   216
  show ?thesis by(simp add: P_def)
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   217
qed
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   218
0b02adadf384 added IMP/Live_True.thy
nipkow
parents:
diff changeset
   219
end