src/HOL/Library/While_Combinator.thy
 changeset 23821 2acd9d79d855 parent 22803 5129e02f4df2 child 27368 9f90ac19e32b
1.1 --- a/src/HOL/Library/While_Combinator.thy	Mon Jul 16 21:26:35 2007 +0200
1.2 +++ b/src/HOL/Library/While_Combinator.thy	Mon Jul 16 21:39:56 2007 +0200
1.3 @@ -10,62 +10,16 @@
1.4  imports Main
1.5  begin
1.7 -text {*
1.8 - We define a while-combinator @{term while} and prove: (a) an
1.9 - unrestricted unfolding law (even if while diverges!)  (I got this
1.10 - idea from Wolfgang Goerigk), and (b) the invariant rule for reasoning
1.12 +text {*
1.13 +  We define the while combinator as the "mother of all tail recursive functions".
1.14  *}
1.16 -consts while_aux :: "('a => bool) \<times> ('a => 'a) \<times> 'a => 'a"
1.17 -recdef (permissive) while_aux
1.18 -  "same_fst (\<lambda>b. True) (\<lambda>b. same_fst (\<lambda>c. True) (\<lambda>c.
1.19 -      {(t, s).  b s \<and> c s = t \<and>
1.20 -        \<not> (\<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))}))"
1.21 -  "while_aux (b, c, s) =
1.22 -    (if (\<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))
1.23 -      then arbitrary
1.24 -      else if b s then while_aux (b, c, c s)
1.25 -      else s)"
1.26 -
1.27 -recdef_tc while_aux_tc: while_aux
1.28 -  apply (rule wf_same_fst)
1.29 -  apply (rule wf_same_fst)
1.30 -  apply (simp add: wf_iff_no_infinite_down_chain)
1.31 -  apply blast
1.32 -  done
1.33 -
1.34 -definition
1.35 -  while :: "('a => bool) => ('a => 'a) => 'a => 'a" where
1.36 -  "while b c s = while_aux (b, c, s)"
1.37 +function (tailrec) while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
1.38 +where
1.39 +  while_unfold[simp del]: "while b c s = (if b s then while b c (c s) else s)"
1.40 +by auto
1.42 -lemma while_aux_unfold:
1.43 -  "while_aux (b, c, s) =
1.44 -    (if \<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))
1.45 -      then arbitrary
1.46 -      else if b s then while_aux (b, c, c s)
1.47 -      else s)"
1.48 -  apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]])
1.49 -  apply (rule refl)
1.50 -  done
1.51 -
1.52 -text {*
1.53 - The recursion equation for @{term while}: directly executable!
1.54 -*}
1.55 -
1.56 -theorem while_unfold [code]:
1.57 -    "while b c s = (if b s then while b c (c s) else s)"
1.58 -  apply (unfold while_def)
1.59 -  apply (rule while_aux_unfold [THEN trans])
1.60 -  apply auto
1.61 -  apply (subst while_aux_unfold)
1.62 -  apply simp
1.63 -  apply clarify
1.64 -  apply (erule_tac x = "\<lambda>i. f (Suc i)" in allE)
1.65 -  apply blast
1.66 -  done
1.67 -
1.68 -hide const while_aux
1.69 +declare while_unfold[code]
1.71  lemma def_while_unfold:
1.72    assumes fdef: "f == while test do"