src/HOL/Library/While_Combinator.thy
changeset 11701 3d51fbf81c17
parent 11626 0dbfb578bf75
child 11704 3c50a2cd6f00
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -22,9 +22,9 @@
     1.4  recdef (permissive) while_aux
     1.5    "same_fst (\<lambda>b. True) (\<lambda>b. same_fst (\<lambda>c. True) (\<lambda>c.
     1.6        {(t, s).  b s \<and> c s = t \<and>
     1.7 -        \<not> (\<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))}))"
     1.8 +        \<not> (\<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))}))"
     1.9    "while_aux (b, c, s) =
    1.10 -    (if (\<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))
    1.11 +    (if (\<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))
    1.12        then arbitrary
    1.13        else if b s then while_aux (b, c, c s)
    1.14        else s)"
    1.15 @@ -42,11 +42,10 @@
    1.16  
    1.17  lemma while_aux_unfold:
    1.18    "while_aux (b, c, s) =
    1.19 -    (if \<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))
    1.20 +    (if \<exists>f. f (0::nat) = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))
    1.21        then arbitrary
    1.22        else if b s then while_aux (b, c, c s)
    1.23        else s)"
    1.24 -thm while_aux.simps
    1.25    apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]])
    1.26    apply (rule refl)
    1.27    done
    1.28 @@ -136,14 +135,14 @@
    1.29   theory.}
    1.30  *}
    1.31  
    1.32 -theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
    1.33 -    P {#0, #4, #2}"
    1.34 +theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + # 2) mod # 6 | n. n \<in> N})) =
    1.35 +    P {Numeral0, # 4, # 2}"
    1.36  proof -
    1.37    have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
    1.38      apply blast
    1.39      done
    1.40    show ?thesis
    1.41 -    apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
    1.42 +    apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, # 2, # 3, # 4, # 5}"])
    1.43         apply (rule monoI)
    1.44        apply blast
    1.45       apply simp