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.6  
     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.11 - about @{term while}.
    1.12 +text {* 
    1.13 +  We define the while combinator as the "mother of all tail recursive functions".
    1.14  *}
    1.15  
    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.41  
    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.70  
    1.71  lemma def_while_unfold:
    1.72    assumes fdef: "f == while test do"