src/HOL/Library/While_Combinator.thy
author blanchet
Fri Feb 14 07:53:46 2014 +0100 (2014-02-14)
changeset 55466 786edc984c98
parent 54196 0c188a3c671a
child 58881 b9556a055632
permissions -rw-r--r--
merged 'Option.map' and 'Option.map_option'
     1 (*  Title:      HOL/Library/While_Combinator.thy
     2     Author:     Tobias Nipkow
     3     Author:     Alexander Krauss
     4 *)
     5 
     6 header {* A general ``while'' combinator *}
     7 
     8 theory While_Combinator
     9 imports Main
    10 begin
    11 
    12 subsection {* Partial version *}
    13 
    14 definition while_option :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
    15 "while_option b c s = (if (\<exists>k. ~ b ((c ^^ k) s))
    16    then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s)
    17    else None)"
    18 
    19 theorem while_option_unfold[code]:
    20 "while_option b c s = (if b s then while_option b c (c s) else Some s)"
    21 proof cases
    22   assume "b s"
    23   show ?thesis
    24   proof (cases "\<exists>k. ~ b ((c ^^ k) s)")
    25     case True
    26     then obtain k where 1: "~ b ((c ^^ k) s)" ..
    27     with `b s` obtain l where "k = Suc l" by (cases k) auto
    28     with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1)
    29     then have 2: "\<exists>l. ~ b ((c ^^ l) (c s))" ..
    30     from 1
    31     have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))"
    32       by (rule Least_Suc) (simp add: `b s`)
    33     also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))"
    34       by (simp add: funpow_swap1)
    35     finally
    36     show ?thesis 
    37       using True 2 `b s` by (simp add: funpow_swap1 while_option_def)
    38   next
    39     case False
    40     then have "~ (\<exists>l. ~ b ((c ^^ Suc l) s))" by blast
    41     then have "~ (\<exists>l. ~ b ((c ^^ l) (c s)))"
    42       by (simp add: funpow_swap1)
    43     with False  `b s` show ?thesis by (simp add: while_option_def)
    44   qed
    45 next
    46   assume [simp]: "~ b s"
    47   have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0"
    48     by (rule Least_equality) auto
    49   moreover 
    50   have "\<exists>k. ~ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
    51   ultimately show ?thesis unfolding while_option_def by auto 
    52 qed
    53 
    54 lemma while_option_stop2:
    55  "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
    56 apply(simp add: while_option_def split: if_splits)
    57 by (metis (lifting) LeastI_ex)
    58 
    59 lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t"
    60 by(metis while_option_stop2)
    61 
    62 theorem while_option_rule:
    63 assumes step: "!!s. P s ==> b s ==> P (c s)"
    64 and result: "while_option b c s = Some t"
    65 and init: "P s"
    66 shows "P t"
    67 proof -
    68   def k == "LEAST k. ~ b ((c ^^ k) s)"
    69   from assms have t: "t = (c ^^ k) s"
    70     by (simp add: while_option_def k_def split: if_splits)    
    71   have 1: "ALL i<k. b ((c ^^ i) s)"
    72     by (auto simp: k_def dest: not_less_Least)
    73 
    74   { fix i assume "i <= k" then have "P ((c ^^ i) s)"
    75       by (induct i) (auto simp: init step 1) }
    76   thus "P t" by (auto simp: t)
    77 qed
    78 
    79 lemma funpow_commute: 
    80   "\<lbrakk>\<forall>k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\<rbrakk> \<Longrightarrow> f ((c^^k) s) = (c'^^k) (f s)"
    81 by (induct k arbitrary: s) auto
    82 
    83 lemma while_option_commute_invariant:
    84 assumes Invariant: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P (c s)"
    85 assumes TestCommute: "\<And>s. P s \<Longrightarrow> b s = b' (f s)"
    86 assumes BodyCommute: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> f (c s) = c' (f s)"
    87 assumes Initial: "P s"
    88 shows "map_option f (while_option b c s) = while_option b' c' (f s)"
    89 unfolding while_option_def
    90 proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
    91   fix k
    92   assume "\<not> b ((c ^^ k) s)"
    93   with Initial show "\<exists>k. \<not> b' ((c' ^^ k) (f s))"
    94   proof (induction k arbitrary: s)
    95     case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
    96   next
    97     case (Suc k) thus ?case
    98     proof (cases "b s")
    99       assume "b s"
   100       with Suc.IH[of "c s"] Suc.prems show ?thesis
   101         by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
   102     next
   103       assume "\<not> b s"
   104       with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
   105     qed
   106   qed
   107 next
   108   fix k
   109   assume "\<not> b' ((c' ^^ k) (f s))"
   110   with Initial show "\<exists>k. \<not> b ((c ^^ k) s)"
   111   proof (induction k arbitrary: s)
   112     case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
   113   next
   114     case (Suc k) thus ?case
   115     proof (cases "b s")
   116        assume "b s"
   117       with Suc.IH[of "c s"] Suc.prems show ?thesis
   118         by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
   119     next
   120       assume "\<not> b s"
   121       with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
   122     qed
   123   qed
   124 next
   125   fix k
   126   assume k: "\<not> b' ((c' ^^ k) (f s))"
   127   have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))"
   128           (is "?k' = ?k")
   129   proof (cases ?k')
   130     case 0
   131     have "\<not> b' ((c' ^^ 0) (f s))"
   132       unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k)
   133     hence "\<not> b s" by (auto simp: TestCommute Initial)
   134     hence "?k = 0" by (intro Least_equality) auto
   135     with 0 show ?thesis by auto
   136   next
   137     case (Suc k')
   138     have "\<not> b' ((c' ^^ Suc k') (f s))"
   139       unfolding Suc[symmetric] by (rule LeastI) (rule k)
   140     moreover
   141     { fix k assume "k \<le> k'"
   142       hence "k < ?k'" unfolding Suc by simp
   143       hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least])
   144     }
   145     note b' = this
   146     { fix k assume "k \<le> k'"
   147       hence "f ((c ^^ k) s) = (c' ^^ k) (f s)"
   148       and "b ((c ^^ k) s) = b' ((c' ^^ k) (f s))"
   149       and "P ((c ^^ k) s)"
   150         by (induct k) (auto simp: b' assms)
   151       with `k \<le> k'`
   152       have "b ((c ^^ k) s)"
   153       and "f ((c ^^ k) s) = (c' ^^ k) (f s)"
   154       and "P ((c ^^ k) s)"
   155         by (auto simp: b')
   156     }
   157     note b = this(1) and body = this(2) and inv = this(3)
   158     hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
   159     ultimately show ?thesis unfolding Suc using b
   160     proof (intro Least_equality[symmetric])
   161       case goal1
   162       hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
   163         by (auto simp: BodyCommute inv b)
   164       have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b)
   165       with Test show ?case by (auto simp: TestCommute)
   166     next
   167       case goal2 thus ?case by (metis not_less_eq_eq)
   168     qed
   169   qed
   170   have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
   171   proof (rule funpow_commute, clarify)
   172     fix k assume "k < ?k"
   173     hence TestTrue: "b ((c ^^ k) s)" by (auto dest: not_less_Least)
   174     from `k < ?k` have "P ((c ^^ k) s)"
   175     proof (induct k)
   176       case 0 thus ?case by (auto simp: assms)
   177     next
   178       case (Suc h)
   179       hence "P ((c ^^ h) s)" by auto
   180       with Suc show ?case
   181         by (auto, metis (lifting, no_types) Invariant Suc_lessD not_less_Least)
   182     qed
   183     with TestTrue show "f (c ((c ^^ k) s)) = c' (f ((c ^^ k) s))"
   184       by (metis BodyCommute)
   185   qed
   186   thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast
   187 qed
   188 
   189 lemma while_option_commute:
   190   assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" 
   191   shows "map_option f (while_option b c s) = while_option b' c' (f s)"
   192 by(rule while_option_commute_invariant[where P = "\<lambda>_. True"])
   193   (auto simp add: assms)
   194 
   195 subsection {* Total version *}
   196 
   197 definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
   198 where "while b c s = the (while_option b c s)"
   199 
   200 lemma while_unfold [code]:
   201   "while b c s = (if b s then while b c (c s) else s)"
   202 unfolding while_def by (subst while_option_unfold) simp
   203 
   204 lemma def_while_unfold:
   205   assumes fdef: "f == while test do"
   206   shows "f x = (if test x then f(do x) else x)"
   207 unfolding fdef by (fact while_unfold)
   208 
   209 
   210 text {*
   211  The proof rule for @{term while}, where @{term P} is the invariant.
   212 *}
   213 
   214 theorem while_rule_lemma:
   215   assumes invariant: "!!s. P s ==> b s ==> P (c s)"
   216     and terminate: "!!s. P s ==> \<not> b s ==> Q s"
   217     and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
   218   shows "P s \<Longrightarrow> Q (while b c s)"
   219   using wf
   220   apply (induct s)
   221   apply simp
   222   apply (subst while_unfold)
   223   apply (simp add: invariant terminate)
   224   done
   225 
   226 theorem while_rule:
   227   "[| P s;
   228       !!s. [| P s; b s  |] ==> P (c s);
   229       !!s. [| P s; \<not> b s  |] ==> Q s;
   230       wf r;
   231       !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
   232    Q (while b c s)"
   233   apply (rule while_rule_lemma)
   234      prefer 4 apply assumption
   235     apply blast
   236    apply blast
   237   apply (erule wf_subset)
   238   apply blast
   239   done
   240 
   241 text{* Proving termination: *}
   242 
   243 theorem wf_while_option_Some:
   244   assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
   245   and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
   246   shows "EX t. while_option b c s = Some t"
   247 using assms(1,3)
   248 proof (induction s)
   249   case less thus ?case using assms(2)
   250     by (subst while_option_unfold) simp
   251 qed
   252 
   253 lemma wf_rel_while_option_Some:
   254 assumes wf: "wf R"
   255 assumes smaller: "\<And>s. P s \<and> b s \<Longrightarrow> (c s, s) \<in> R"
   256 assumes inv: "\<And>s. P s \<and> b s \<Longrightarrow> P(c s)"
   257 assumes init: "P s"
   258 shows "\<exists>t. while_option b c s = Some t"
   259 proof -
   260  from smaller have "{(t,s). P s \<and> b s \<and> t = c s} \<subseteq> R" by auto
   261  with wf have "wf {(t,s). P s \<and> b s \<and> t = c s}" by (auto simp: wf_subset)
   262  with inv init show ?thesis by (auto simp: wf_while_option_Some)
   263 qed
   264 
   265 theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
   266 shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
   267   \<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t"
   268 by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
   269 
   270 text{* Kleene iteration starting from the empty set and assuming some finite
   271 bounding set: *}
   272 
   273 lemma while_option_finite_subset_Some: fixes C :: "'a set"
   274   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
   275   shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
   276 proof(rule measure_while_option_Some[where
   277     f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
   278   fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"
   279   show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
   280     (is "?L \<and> ?R")
   281   proof
   282     show ?L by(metis A(1) assms(2) monoD[OF `mono f`])
   283     show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
   284   qed
   285 qed simp
   286 
   287 lemma lfp_the_while_option:
   288   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
   289   shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
   290 proof-
   291   obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
   292     using while_option_finite_subset_Some[OF assms] by blast
   293   with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
   294   show ?thesis by auto
   295 qed
   296 
   297 lemma lfp_while:
   298   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
   299   shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
   300 unfolding while_def using assms by (rule lfp_the_while_option) blast
   301 
   302 
   303 text{* Computing the reflexive, transitive closure by iterating a successor
   304 function. Stops when an element is found that dos not satisfy the test.
   305 
   306 More refined (and hence more efficient) versions can be found in ITP 2011 paper
   307 by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow)
   308 and the AFP article Executable Transitive Closures by René Thiemann. *}
   309 
   310 context
   311 fixes p :: "'a \<Rightarrow> bool"
   312 and f :: "'a \<Rightarrow> 'a list"
   313 and x :: 'a
   314 begin
   315 
   316 fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
   317 where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))"
   318 
   319 fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
   320 where "rtrancl_while_step (ws, Z) =
   321   (let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x))
   322   in (new @ tl ws, set new \<union> Z))"
   323 
   324 definition rtrancl_while :: "('a list * 'a set) option"
   325 where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})"
   326 
   327 fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
   328 where "rtrancl_while_invariant (ws, Z) =
   329    (x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and>
   330     Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
   331 
   332 lemma rtrancl_while_invariant: 
   333   assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
   334   shows   "rtrancl_while_invariant (rtrancl_while_step st)"
   335 proof (cases st)
   336   fix ws Z assume st: "st = (ws, Z)"
   337   with test obtain h t where "ws = h # t" "p h" by (cases ws) auto
   338   with inv st show ?thesis by (auto intro: rtrancl.rtrancl_into_rtrancl)
   339 qed
   340 
   341 lemma rtrancl_while_Some: assumes "rtrancl_while = Some(ws,Z)"
   342 shows "if ws = []
   343        then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z)
   344        else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}"
   345 proof -
   346   have "rtrancl_while_invariant ([x],{x})" by simp
   347   with rtrancl_while_invariant have I: "rtrancl_while_invariant (ws,Z)"
   348     by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
   349   { assume "ws = []"
   350     hence ?thesis using I
   351       by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
   352   } moreover
   353   { assume "ws \<noteq> []"
   354     hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
   355       by (simp add: subset_iff)
   356   }
   357   ultimately show ?thesis by simp
   358 qed
   359 
   360 lemma rtrancl_while_finite_Some:
   361   assumes "finite ({(x, y). y \<in> set (f x)}\<^sup>* `` {x})" (is "finite ?Cl")
   362   shows "\<exists>y. rtrancl_while = Some y"
   363 proof -
   364   let ?R = "(\<lambda>(_, Z). card (?Cl - Z)) <*mlex*> (\<lambda>(ws, _). length ws) <*mlex*> {}"
   365   have "wf ?R" by (blast intro: wf_mlex)
   366   then show ?thesis unfolding rtrancl_while_def
   367   proof (rule wf_rel_while_option_Some[of ?R rtrancl_while_invariant])
   368     fix st assume *: "rtrancl_while_invariant st \<and> rtrancl_while_test st"
   369     hence I: "rtrancl_while_invariant (rtrancl_while_step st)"
   370       by (blast intro: rtrancl_while_invariant)
   371     show "(rtrancl_while_step st, st) \<in> ?R"
   372     proof (cases st)
   373       fix ws Z let ?ws = "fst (rtrancl_while_step st)" and ?Z = "snd (rtrancl_while_step st)"
   374       assume st: "st = (ws, Z)"
   375       with * obtain h t where ws: "ws = h # t" "p h" by (cases ws) auto
   376       { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) \<noteq> []"
   377         then obtain z where "z \<in> set (remdups (filter (\<lambda>y. y \<notin> Z) (f h)))" by fastforce
   378         with st ws I have "Z \<subset> ?Z" "Z \<subseteq> ?Cl" "?Z \<subseteq> ?Cl" by auto
   379         with assms have "card (?Cl - ?Z) < card (?Cl - Z)" by (blast intro: psubset_card_mono)
   380         with st ws have ?thesis unfolding mlex_prod_def by simp
   381       }
   382       moreover
   383       { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) = []"
   384         with st ws have "?Z = Z" "?ws = t"  by (auto simp: filter_empty_conv)
   385         with st ws have ?thesis unfolding mlex_prod_def by simp
   386       }
   387       ultimately show ?thesis by blast
   388     qed
   389   qed (simp_all add: rtrancl_while_invariant)
   390 qed
   391 
   392 end
   393 
   394 hide_const (open) rtrancl_while_test rtrancl_while_step rtrancl_while_invariant
   395 hide_fact (open) rtrancl_while_invariant
   396 
   397 end