added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
authorkrauss
Fri Jul 09 16:32:25 2010 +0200 (2010-07-09 ago)
changeset 37757dc78d2d9e90a
parent 37756 59caa6180fff
child 37759 00ff97087ab5
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
src/HOL/Library/While_Combinator.thy
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Jul 09 10:08:10 2010 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Jul 09 16:32:25 2010 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:      HOL/Library/While_Combinator.thy
     1.5      Author:     Tobias Nipkow
     1.6 +    Author:     Alexander Krauss
     1.7      Copyright   2000 TU Muenchen
     1.8  *)
     1.9  
    1.10 @@ -9,27 +10,90 @@
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -text {* 
    1.15 -  We define the while combinator as the "mother of all tail recursive functions".
    1.16 -*}
    1.17 +subsection {* Option result *}
    1.18 +
    1.19 +definition while_option :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
    1.20 +"while_option b c s = (if (\<exists>k. ~ b ((c ^^ k) s))
    1.21 +   then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s)
    1.22 +   else None)"
    1.23  
    1.24 -function (tailrec) while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
    1.25 -where
    1.26 -  while_unfold[simp del]: "while b c s = (if b s then while b c (c s) else s)"
    1.27 -by auto
    1.28 +theorem while_option_unfold[code]:
    1.29 +"while_option b c s = (if b s then while_option b c (c s) else Some s)"
    1.30 +proof cases
    1.31 +  assume "b s"
    1.32 +  show ?thesis
    1.33 +  proof (cases "\<exists>k. ~ b ((c ^^ k) s)")
    1.34 +    case True
    1.35 +    then obtain k where 1: "~ b ((c ^^ k) s)" ..
    1.36 +    with `b s` obtain l where "k = Suc l" by (cases k) auto
    1.37 +    with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1)
    1.38 +    then have 2: "\<exists>l. ~ b ((c ^^ l) (c s))" ..
    1.39 +    from 1
    1.40 +    have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))"
    1.41 +      by (rule Least_Suc) (simp add: `b s`)
    1.42 +    also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))"
    1.43 +      by (simp add: funpow_swap1)
    1.44 +    finally
    1.45 +    show ?thesis 
    1.46 +      using True 2 `b s` by (simp add: funpow_swap1 while_option_def)
    1.47 +  next
    1.48 +    case False
    1.49 +    then have "~ (\<exists>l. ~ b ((c ^^ Suc l) s))" by blast
    1.50 +    then have "~ (\<exists>l. ~ b ((c ^^ l) (c s)))"
    1.51 +      by (simp add: funpow_swap1)
    1.52 +    with False  `b s` show ?thesis by (simp add: while_option_def)
    1.53 +  qed
    1.54 +next
    1.55 +  assume [simp]: "~ b s"
    1.56 +  have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0"
    1.57 +    by (rule Least_equality) auto
    1.58 +  moreover 
    1.59 +  have "\<exists>k. ~ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
    1.60 +  ultimately show ?thesis unfolding while_option_def by auto 
    1.61 +qed
    1.62  
    1.63 -declare while_unfold[code]
    1.64 +lemma while_option_stop:
    1.65 +assumes "while_option b c s = Some t"
    1.66 +shows "~ b t"
    1.67 +proof -
    1.68 +  from assms have ex: "\<exists>k. ~ b ((c ^^ k) s)"
    1.69 +  and t: "t = (c ^^ (LEAST k. ~ b ((c ^^ k) s))) s"
    1.70 +    by (auto simp: while_option_def split: if_splits)
    1.71 +  from LeastI_ex[OF ex]
    1.72 +  show "~ b t" unfolding t .
    1.73 +qed
    1.74 +
    1.75 +theorem while_option_rule:
    1.76 +assumes step: "!!s. P s ==> b s ==> P (c s)"
    1.77 +and result: "while_option b c s = Some t"
    1.78 +and init: "P s"
    1.79 +shows "P t"
    1.80 +proof -
    1.81 +  def k == "LEAST k. ~ b ((c ^^ k) s)"
    1.82 +  from assms have t: "t = (c ^^ k) s"
    1.83 +    by (simp add: while_option_def k_def split: if_splits)    
    1.84 +  have 1: "ALL i<k. b ((c ^^ i) s)"
    1.85 +    by (auto simp: k_def dest: not_less_Least)
    1.86 +
    1.87 +  { fix i assume "i <= k" then have "P ((c ^^ i) s)"
    1.88 +      by (induct i) (auto simp: init step 1) }
    1.89 +  thus "P t" by (auto simp: t)
    1.90 +qed
    1.91 +
    1.92 +
    1.93 +subsection {* Totalized version *}
    1.94 +
    1.95 +definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
    1.96 +where "while b c s = the (while_option b c s)"
    1.97 +
    1.98 +lemma while_unfold:
    1.99 +  "while b c s = (if b s then while b c (c s) else s)"
   1.100 +unfolding while_def by (subst while_option_unfold) simp
   1.101  
   1.102  lemma def_while_unfold:
   1.103    assumes fdef: "f == while test do"
   1.104    shows "f x = (if test x then f(do x) else x)"
   1.105 -proof -
   1.106 -  have "f x = while test do x" using fdef by simp
   1.107 -  also have "\<dots> = (if test x then while test do (do x) else x)"
   1.108 -    by(rule while_unfold)
   1.109 -  also have "\<dots> = (if test x then f(do x) else x)" by(simp add:fdef[symmetric])
   1.110 -  finally show ?thesis .
   1.111 -qed
   1.112 +unfolding fdef by (fact while_unfold)
   1.113  
   1.114  
   1.115  text {*
   1.116 @@ -88,9 +152,7 @@
   1.117  done
   1.118  
   1.119  
   1.120 -text {*
   1.121 - An example of using the @{term while} combinator.
   1.122 -*}
   1.123 +subsection {* Example *}
   1.124  
   1.125  text{* Cannot use @{thm[source]set_eq_subset} because it leads to
   1.126  looping because the antisymmetry simproc turns the subset relationship