src/HOL/Library/While_Combinator.thy
author wenzelm
Thu Jun 25 23:33:47 2015 +0200 (2015-06-25)
changeset 60580 7e741e22d7fc
parent 60500 903bb1495239
child 61115 3a4400985780
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Library/While_Combinator.thy
     2     Author:     Tobias Nipkow
     3     Author:     Alexander Krauss
     4 *)
     5 
     6 section \<open>A general ``while'' combinator\<close>
     7 
     8 theory While_Combinator
     9 imports Main
    10 begin
    11 
    12 subsection \<open>Partial version\<close>
    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 \<open>b s\<close> 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: \<open>b s\<close>)
    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 \<open>b s\<close> 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  \<open>b s\<close> 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 \<open>k \<le> k'\<close>
   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], goals)
   161       case 1
   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 2
   168       thus ?case by (metis not_less_eq_eq)
   169     qed
   170   qed
   171   have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
   172   proof (rule funpow_commute, clarify)
   173     fix k assume "k < ?k"
   174     hence TestTrue: "b ((c ^^ k) s)" by (auto dest: not_less_Least)
   175     from \<open>k < ?k\<close> have "P ((c ^^ k) s)"
   176     proof (induct k)
   177       case 0 thus ?case by (auto simp: assms)
   178     next
   179       case (Suc h)
   180       hence "P ((c ^^ h) s)" by auto
   181       with Suc show ?case
   182         by (auto, metis (lifting, no_types) Invariant Suc_lessD not_less_Least)
   183     qed
   184     with TestTrue show "f (c ((c ^^ k) s)) = c' (f ((c ^^ k) s))"
   185       by (metis BodyCommute)
   186   qed
   187   thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast
   188 qed
   189 
   190 lemma while_option_commute:
   191   assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" 
   192   shows "map_option f (while_option b c s) = while_option b' c' (f s)"
   193 by(rule while_option_commute_invariant[where P = "\<lambda>_. True"])
   194   (auto simp add: assms)
   195 
   196 subsection \<open>Total version\<close>
   197 
   198 definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
   199 where "while b c s = the (while_option b c s)"
   200 
   201 lemma while_unfold [code]:
   202   "while b c s = (if b s then while b c (c s) else s)"
   203 unfolding while_def by (subst while_option_unfold) simp
   204 
   205 lemma def_while_unfold:
   206   assumes fdef: "f == while test do"
   207   shows "f x = (if test x then f(do x) else x)"
   208 unfolding fdef by (fact while_unfold)
   209 
   210 
   211 text \<open>
   212  The proof rule for @{term while}, where @{term P} is the invariant.
   213 \<close>
   214 
   215 theorem while_rule_lemma:
   216   assumes invariant: "!!s. P s ==> b s ==> P (c s)"
   217     and terminate: "!!s. P s ==> \<not> b s ==> Q s"
   218     and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
   219   shows "P s \<Longrightarrow> Q (while b c s)"
   220   using wf
   221   apply (induct s)
   222   apply simp
   223   apply (subst while_unfold)
   224   apply (simp add: invariant terminate)
   225   done
   226 
   227 theorem while_rule:
   228   "[| P s;
   229       !!s. [| P s; b s  |] ==> P (c s);
   230       !!s. [| P s; \<not> b s  |] ==> Q s;
   231       wf r;
   232       !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
   233    Q (while b c s)"
   234   apply (rule while_rule_lemma)
   235      prefer 4 apply assumption
   236     apply blast
   237    apply blast
   238   apply (erule wf_subset)
   239   apply blast
   240   done
   241 
   242 text\<open>Proving termination:\<close>
   243 
   244 theorem wf_while_option_Some:
   245   assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
   246   and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
   247   shows "EX t. while_option b c s = Some t"
   248 using assms(1,3)
   249 proof (induction s)
   250   case less thus ?case using assms(2)
   251     by (subst while_option_unfold) simp
   252 qed
   253 
   254 lemma wf_rel_while_option_Some:
   255 assumes wf: "wf R"
   256 assumes smaller: "\<And>s. P s \<and> b s \<Longrightarrow> (c s, s) \<in> R"
   257 assumes inv: "\<And>s. P s \<and> b s \<Longrightarrow> P(c s)"
   258 assumes init: "P s"
   259 shows "\<exists>t. while_option b c s = Some t"
   260 proof -
   261  from smaller have "{(t,s). P s \<and> b s \<and> t = c s} \<subseteq> R" by auto
   262  with wf have "wf {(t,s). P s \<and> b s \<and> t = c s}" by (auto simp: wf_subset)
   263  with inv init show ?thesis by (auto simp: wf_while_option_Some)
   264 qed
   265 
   266 theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
   267 shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
   268   \<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t"
   269 by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
   270 
   271 text\<open>Kleene iteration starting from the empty set and assuming some finite
   272 bounding set:\<close>
   273 
   274 lemma while_option_finite_subset_Some: fixes C :: "'a set"
   275   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
   276   shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
   277 proof(rule measure_while_option_Some[where
   278     f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
   279   fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"
   280   show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
   281     (is "?L \<and> ?R")
   282   proof
   283     show ?L by(metis A(1) assms(2) monoD[OF \<open>mono f\<close>])
   284     show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
   285   qed
   286 qed simp
   287 
   288 lemma lfp_the_while_option:
   289   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
   290   shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
   291 proof-
   292   obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
   293     using while_option_finite_subset_Some[OF assms] by blast
   294   with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
   295   show ?thesis by auto
   296 qed
   297 
   298 lemma lfp_while:
   299   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
   300   shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
   301 unfolding while_def using assms by (rule lfp_the_while_option) blast
   302 
   303 
   304 text\<open>Computing the reflexive, transitive closure by iterating a successor
   305 function. Stops when an element is found that dos not satisfy the test.
   306 
   307 More refined (and hence more efficient) versions can be found in ITP 2011 paper
   308 by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow)
   309 and the AFP article Executable Transitive Closures by René Thiemann.\<close>
   310 
   311 context
   312 fixes p :: "'a \<Rightarrow> bool"
   313 and f :: "'a \<Rightarrow> 'a list"
   314 and x :: 'a
   315 begin
   316 
   317 fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
   318 where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))"
   319 
   320 fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
   321 where "rtrancl_while_step (ws, Z) =
   322   (let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x))
   323   in (new @ tl ws, set new \<union> Z))"
   324 
   325 definition rtrancl_while :: "('a list * 'a set) option"
   326 where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})"
   327 
   328 fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
   329 where "rtrancl_while_invariant (ws, Z) =
   330    (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>
   331     Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
   332 
   333 lemma rtrancl_while_invariant: 
   334   assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
   335   shows   "rtrancl_while_invariant (rtrancl_while_step st)"
   336 proof (cases st)
   337   fix ws Z assume st: "st = (ws, Z)"
   338   with test obtain h t where "ws = h # t" "p h" by (cases ws) auto
   339   with inv st show ?thesis by (auto intro: rtrancl.rtrancl_into_rtrancl)
   340 qed
   341 
   342 lemma rtrancl_while_Some: assumes "rtrancl_while = Some(ws,Z)"
   343 shows "if ws = []
   344        then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z)
   345        else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}"
   346 proof -
   347   have "rtrancl_while_invariant ([x],{x})" by simp
   348   with rtrancl_while_invariant have I: "rtrancl_while_invariant (ws,Z)"
   349     by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
   350   { assume "ws = []"
   351     hence ?thesis using I
   352       by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
   353   } moreover
   354   { assume "ws \<noteq> []"
   355     hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
   356       by (simp add: subset_iff)
   357   }
   358   ultimately show ?thesis by simp
   359 qed
   360 
   361 lemma rtrancl_while_finite_Some:
   362   assumes "finite ({(x, y). y \<in> set (f x)}\<^sup>* `` {x})" (is "finite ?Cl")
   363   shows "\<exists>y. rtrancl_while = Some y"
   364 proof -
   365   let ?R = "(\<lambda>(_, Z). card (?Cl - Z)) <*mlex*> (\<lambda>(ws, _). length ws) <*mlex*> {}"
   366   have "wf ?R" by (blast intro: wf_mlex)
   367   then show ?thesis unfolding rtrancl_while_def
   368   proof (rule wf_rel_while_option_Some[of ?R rtrancl_while_invariant])
   369     fix st assume *: "rtrancl_while_invariant st \<and> rtrancl_while_test st"
   370     hence I: "rtrancl_while_invariant (rtrancl_while_step st)"
   371       by (blast intro: rtrancl_while_invariant)
   372     show "(rtrancl_while_step st, st) \<in> ?R"
   373     proof (cases st)
   374       fix ws Z let ?ws = "fst (rtrancl_while_step st)" and ?Z = "snd (rtrancl_while_step st)"
   375       assume st: "st = (ws, Z)"
   376       with * obtain h t where ws: "ws = h # t" "p h" by (cases ws) auto
   377       { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) \<noteq> []"
   378         then obtain z where "z \<in> set (remdups (filter (\<lambda>y. y \<notin> Z) (f h)))" by fastforce
   379         with st ws I have "Z \<subset> ?Z" "Z \<subseteq> ?Cl" "?Z \<subseteq> ?Cl" by auto
   380         with assms have "card (?Cl - ?Z) < card (?Cl - Z)" by (blast intro: psubset_card_mono)
   381         with st ws have ?thesis unfolding mlex_prod_def by simp
   382       }
   383       moreover
   384       { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) = []"
   385         with st ws have "?Z = Z" "?ws = t"  by (auto simp: filter_empty_conv)
   386         with st ws have ?thesis unfolding mlex_prod_def by simp
   387       }
   388       ultimately show ?thesis by blast
   389     qed
   390   qed (simp_all add: rtrancl_while_invariant)
   391 qed
   392 
   393 end
   394 
   395 hide_const (open) rtrancl_while_test rtrancl_while_step rtrancl_while_invariant
   396 hide_fact (open) rtrancl_while_invariant
   397 
   398 end