src/HOL/IMP/Live_True.thy
changeset 48256 5fa4fc4d721a
parent 47818 151d137f1095
child 50007 56f269baae76
equal deleted inserted replaced
48255:968602739b54 48256:5fa4fc4d721a
   121 by (induction b) auto
   121 by (induction b) auto
   122 
   122 
   123 lemma cfinite[simp]: "finite(vars(c::com))"
   123 lemma cfinite[simp]: "finite(vars(c::com))"
   124 by (induction c) auto
   124 by (induction c) auto
   125 
   125 
   126 (* move to Inductive; call Kleene? *)
       
   127 lemma lfp_finite_iter: assumes "mono f" and "(f^^Suc k) bot = (f^^k) bot"
       
   128 shows "lfp f = (f^^k) bot"
       
   129 proof(rule antisym)
       
   130   show "lfp f \<le> (f^^k) bot"
       
   131   proof(rule lfp_lowerbound)
       
   132     show "f ((f^^k) bot) \<le> (f^^k) bot" using assms(2) by simp
       
   133   qed
       
   134 next
       
   135   show "(f^^k) bot \<le> lfp f"
       
   136   proof(induction k)
       
   137     case 0 show ?case by simp
       
   138   next
       
   139     case Suc
       
   140     from monoD[OF assms(1) Suc] lfp_unfold[OF assms(1)]
       
   141     show ?case by simp
       
   142   qed
       
   143 qed
       
   144 
       
   145 (* move to While_Combinator *)
       
   146 lemma while_option_stop2:
       
   147  "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
       
   148 apply(simp add: while_option_def split: if_splits)
       
   149 by (metis (lifting) LeastI_ex)
       
   150 (* move to While_Combinator *)
       
   151 lemma while_option_finite_subset_Some: fixes C :: "'a set"
       
   152   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
       
   153   shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
       
   154 proof(rule measure_while_option_Some[where
       
   155     f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
       
   156   fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"
       
   157   show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
       
   158     (is "?L \<and> ?R")
       
   159   proof
       
   160     show ?L by(metis A(1) assms(2) monoD[OF `mono f`])
       
   161     show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
       
   162   qed
       
   163 qed simp
       
   164 (* move to While_Combinator *)
       
   165 lemma lfp_eq_while_option:
       
   166   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
       
   167   shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
       
   168 proof-
       
   169   obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
       
   170     using while_option_finite_subset_Some[OF assms] by blast
       
   171   with while_option_stop2[OF this] lfp_finite_iter[OF assms(1)]
       
   172   show ?thesis by auto
       
   173 qed
       
   174 
       
   175 text{* For code generation: *}
   126 text{* For code generation: *}
   176 lemma L_While: fixes b c X
   127 lemma L_While: fixes b c X
   177 assumes "finite X" defines "f == \<lambda>A. vars b \<union> X \<union> L c A"
   128 assumes "finite X" defines "f == \<lambda>A. vars b \<union> X \<union> L c A"
   178 shows "L (WHILE b DO c) X = the(while_option (\<lambda>A. f A \<noteq> A) f {})" (is "_ = ?r")
   129 shows "L (WHILE b DO c) X = the(while_option (\<lambda>A. f A \<noteq> A) f {})" (is "_ = ?r")
   179 proof -
   130 proof -
   180   let ?V = "vars b \<union> vars c \<union> X"
   131   let ?V = "vars b \<union> vars c \<union> X"
   181   have "lfp f = ?r"
   132   have "lfp f = ?r"
   182   proof(rule lfp_eq_while_option[where C = "?V"])
   133   proof(rule lfp_the_while_option[where C = "?V"])
   183     show "mono f" by(simp add: f_def mono_union_L)
   134     show "mono f" by(simp add: f_def mono_union_L)
   184   next
   135   next
   185     fix Y show "Y \<subseteq> ?V \<Longrightarrow> f Y \<subseteq> ?V"
   136     fix Y show "Y \<subseteq> ?V \<Longrightarrow> f Y \<subseteq> ?V"
   186       unfolding f_def using L_subset_vars[of c] by blast
   137       unfolding f_def using L_subset_vars[of c] by blast
   187   next
   138   next