src/HOL/Library/While_Combinator.thy
author wenzelm
Tue Sep 03 22:04:23 2013 +0200 (2013-09-03)
changeset 53381 355a4cac5440
parent 53220 daa550823c9f
child 54047 83fb090dae9e
permissions -rw-r--r--
tuned proofs -- less guessing;
     1 (*  Title:      HOL/Library/While_Combinator.thy
     2     Author:     Tobias Nipkow
     3     Author:     Alexander Krauss
     4     Copyright   2000 TU Muenchen
     5 *)
     6 
     7 header {* A general ``while'' combinator *}
     8 
     9 theory While_Combinator
    10 imports Main
    11 begin
    12 
    13 subsection {* Partial version *}
    14 
    15 definition while_option :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
    16 "while_option b c s = (if (\<exists>k. ~ b ((c ^^ k) s))
    17    then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s)
    18    else None)"
    19 
    20 theorem while_option_unfold[code]:
    21 "while_option b c s = (if b s then while_option b c (c s) else Some s)"
    22 proof cases
    23   assume "b s"
    24   show ?thesis
    25   proof (cases "\<exists>k. ~ b ((c ^^ k) s)")
    26     case True
    27     then obtain k where 1: "~ b ((c ^^ k) s)" ..
    28     with `b s` obtain l where "k = Suc l" by (cases k) auto
    29     with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1)
    30     then have 2: "\<exists>l. ~ b ((c ^^ l) (c s))" ..
    31     from 1
    32     have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))"
    33       by (rule Least_Suc) (simp add: `b s`)
    34     also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))"
    35       by (simp add: funpow_swap1)
    36     finally
    37     show ?thesis 
    38       using True 2 `b s` by (simp add: funpow_swap1 while_option_def)
    39   next
    40     case False
    41     then have "~ (\<exists>l. ~ b ((c ^^ Suc l) s))" by blast
    42     then have "~ (\<exists>l. ~ b ((c ^^ l) (c s)))"
    43       by (simp add: funpow_swap1)
    44     with False  `b s` show ?thesis by (simp add: while_option_def)
    45   qed
    46 next
    47   assume [simp]: "~ b s"
    48   have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0"
    49     by (rule Least_equality) auto
    50   moreover 
    51   have "\<exists>k. ~ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
    52   ultimately show ?thesis unfolding while_option_def by auto 
    53 qed
    54 
    55 lemma while_option_stop2:
    56  "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
    57 apply(simp add: while_option_def split: if_splits)
    58 by (metis (lifting) LeastI_ex)
    59 
    60 lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t"
    61 by(metis while_option_stop2)
    62 
    63 theorem while_option_rule:
    64 assumes step: "!!s. P s ==> b s ==> P (c s)"
    65 and result: "while_option b c s = Some t"
    66 and init: "P s"
    67 shows "P t"
    68 proof -
    69   def k == "LEAST k. ~ b ((c ^^ k) s)"
    70   from assms have t: "t = (c ^^ k) s"
    71     by (simp add: while_option_def k_def split: if_splits)    
    72   have 1: "ALL i<k. b ((c ^^ i) s)"
    73     by (auto simp: k_def dest: not_less_Least)
    74 
    75   { fix i assume "i <= k" then have "P ((c ^^ i) s)"
    76       by (induct i) (auto simp: init step 1) }
    77   thus "P t" by (auto simp: t)
    78 qed
    79 
    80 lemma funpow_commute: 
    81   "\<lbrakk>\<forall>k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\<rbrakk> \<Longrightarrow> f ((c^^k) s) = (c'^^k) (f s)"
    82 by (induct k arbitrary: s) auto
    83 
    84 lemma while_option_commute:
    85   assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" 
    86   shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
    87 unfolding while_option_def
    88 proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
    89   fix k assume "\<not> b ((c ^^ k) s)"
    90   thus "\<exists>k. \<not> b' ((c' ^^ k) (f s))"
    91   proof (induction k arbitrary: s)
    92     case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0])
    93   next
    94     case (Suc k)
    95     hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1)
    96     from Suc.IH[OF this] obtain k where "\<not> b' ((c' ^^ k) (f (c s)))" ..
    97     with assms show ?case
    98       by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
    99   qed
   100 next
   101   fix k assume "\<not> b' ((c' ^^ k) (f s))"
   102   thus "\<exists>k. \<not> b ((c ^^ k) s)"
   103   proof (induction k arbitrary: s)
   104     case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0])
   105   next
   106     case (Suc k)
   107     hence *: "\<not> b' ((c'^^k) (c' (f s)))" by (auto simp: funpow_swap1)
   108     show ?case
   109     proof (cases "b s")
   110       case True
   111       with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp
   112       from Suc.IH[OF this] obtain k where "\<not> b ((c ^^ k) (c s))" ..
   113       thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"])
   114     qed (auto intro: exI[of _ "0"])
   115   qed
   116 next
   117   fix k assume k: "\<not> b' ((c' ^^ k) (f s))"
   118   have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))" (is "?k' = ?k")
   119   proof (cases ?k')
   120     case 0
   121     have "\<not> b' ((c'^^0) (f s))" unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k)
   122     hence "\<not> b s" unfolding assms(1) by simp
   123     hence "?k = 0" by (intro Least_equality) auto
   124     with 0 show ?thesis by auto
   125   next
   126     case (Suc k')
   127     have "\<not> b' ((c'^^Suc k') (f s))" unfolding Suc[symmetric] by (rule LeastI) (rule k)
   128     moreover
   129     { fix k assume "k \<le> k'"
   130       hence "k < ?k'" unfolding Suc by simp
   131       hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least])
   132     } note b' = this
   133     { fix k assume "k \<le> k'"
   134       hence "f ((c ^^ k) s) = (c'^^k) (f s)" by (induct k) (auto simp: b' assms)
   135       with `k \<le> k'` have "b ((c^^k) s)"
   136       proof (induct k)
   137         case (Suc k) thus ?case unfolding assms(1) by (simp only: b')
   138       qed (simp add: b'[of 0, simplified] assms(1))
   139     } note b = this
   140     hence k': "f ((c^^k') s) = (c'^^k') (f s)" by (induct k') (auto simp: assms(2))
   141     ultimately show ?thesis unfolding Suc using b
   142     by (intro sym[OF Least_equality])
   143        (auto simp add: assms(1) assms(2)[OF b] k' not_less_eq_eq[symmetric])
   144   qed
   145   have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
   146     by (auto intro: funpow_commute assms(2) dest: not_less_Least)
   147   thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast
   148 qed
   149 
   150 subsection {* Total version *}
   151 
   152 definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
   153 where "while b c s = the (while_option b c s)"
   154 
   155 lemma while_unfold [code]:
   156   "while b c s = (if b s then while b c (c s) else s)"
   157 unfolding while_def by (subst while_option_unfold) simp
   158 
   159 lemma def_while_unfold:
   160   assumes fdef: "f == while test do"
   161   shows "f x = (if test x then f(do x) else x)"
   162 unfolding fdef by (fact while_unfold)
   163 
   164 
   165 text {*
   166  The proof rule for @{term while}, where @{term P} is the invariant.
   167 *}
   168 
   169 theorem while_rule_lemma:
   170   assumes invariant: "!!s. P s ==> b s ==> P (c s)"
   171     and terminate: "!!s. P s ==> \<not> b s ==> Q s"
   172     and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
   173   shows "P s \<Longrightarrow> Q (while b c s)"
   174   using wf
   175   apply (induct s)
   176   apply simp
   177   apply (subst while_unfold)
   178   apply (simp add: invariant terminate)
   179   done
   180 
   181 theorem while_rule:
   182   "[| P s;
   183       !!s. [| P s; b s  |] ==> P (c s);
   184       !!s. [| P s; \<not> b s  |] ==> Q s;
   185       wf r;
   186       !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
   187    Q (while b c s)"
   188   apply (rule while_rule_lemma)
   189      prefer 4 apply assumption
   190     apply blast
   191    apply blast
   192   apply (erule wf_subset)
   193   apply blast
   194   done
   195 
   196 text{* Proving termination: *}
   197 
   198 theorem wf_while_option_Some:
   199   assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
   200   and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
   201   shows "EX t. while_option b c s = Some t"
   202 using assms(1,3)
   203 apply (induct s)
   204 using assms(2)
   205 apply (subst while_option_unfold)
   206 apply simp
   207 done
   208 
   209 theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
   210 shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
   211   \<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t"
   212 by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
   213 
   214 text{* Kleene iteration starting from the empty set and assuming some finite
   215 bounding set: *}
   216 
   217 lemma while_option_finite_subset_Some: fixes C :: "'a set"
   218   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
   219   shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
   220 proof(rule measure_while_option_Some[where
   221     f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
   222   fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"
   223   show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
   224     (is "?L \<and> ?R")
   225   proof
   226     show ?L by(metis A(1) assms(2) monoD[OF `mono f`])
   227     show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
   228   qed
   229 qed simp
   230 
   231 lemma lfp_the_while_option:
   232   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
   233   shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
   234 proof-
   235   obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
   236     using while_option_finite_subset_Some[OF assms] by blast
   237   with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
   238   show ?thesis by auto
   239 qed
   240 
   241 lemma lfp_while:
   242   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
   243   shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
   244 unfolding while_def using assms by (rule lfp_the_while_option) blast
   245 
   246 
   247 text{* Computing the reflexive, transitive closure by iterating a successor
   248 function. Stops when an element is found that dos not satisfy the test.
   249 
   250 More refined (and hence more efficient) versions can be found in ITP 2011 paper
   251 by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow)
   252 and the AFP article Executable Transitive Closures by René Thiemann. *}
   253 
   254 definition rtrancl_while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a list) \<Rightarrow> 'a
   255   \<Rightarrow> ('a list * 'a set) option"
   256 where "rtrancl_while p f x =
   257   while_option (%(ws,_). ws \<noteq> [] \<and> p(hd ws))
   258     ((%(ws,Z).
   259      let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
   260      in (new @ tl ws, set new \<union> insert x Z)))
   261     ([x],{x})"
   262 
   263 lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)"
   264 shows "if ws = []
   265        then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z)
   266        else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}"
   267 proof-
   268   let ?test = "(%(ws,_). ws \<noteq> [] \<and> p(hd ws))"
   269   let ?step = "(%(ws,Z).
   270      let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
   271      in (new @ tl ws, set new \<union> insert x Z))"
   272   let ?R = "{(x,y). y \<in> set(f x)}"
   273   let ?Inv = "%(ws,Z). x \<in> Z \<and> set ws \<subseteq> Z \<and> ?R `` (Z - set ws) \<subseteq> Z \<and>
   274                        Z \<subseteq> ?R^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z)"
   275   { fix ws Z assume 1: "?Inv(ws,Z)" and 2: "?test(ws,Z)"
   276     from 2 obtain v vs where [simp]: "ws = v#vs" by (auto simp: neq_Nil_conv)
   277     have "?Inv(?step (ws,Z))" using 1 2
   278       by (auto intro: rtrancl.rtrancl_into_rtrancl)
   279   } note inv = this
   280   hence "!!p. ?Inv p \<Longrightarrow> ?test p \<Longrightarrow> ?Inv(?step p)"
   281     apply(tactic {* split_all_tac @{context} 1 *})
   282     using inv by iprover
   283   moreover have "?Inv ([x],{x})" by (simp)
   284   ultimately have I: "?Inv (ws,Z)"
   285     by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
   286   { assume "ws = []"
   287     hence ?thesis using I
   288       by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
   289   } moreover
   290   { assume "ws \<noteq> []"
   291     hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
   292       by (simp add: subset_iff)
   293   }
   294   ultimately show ?thesis by simp
   295 qed
   296 
   297 end