author krauss Fri Jul 09 16:32:25 2010 +0200 (2010-07-09 ago) changeset 37757 dc78d2d9e90a parent 37756 59caa6180fff child 37759 00ff97087ab5
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
```     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.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
```