src/HOL/Library/While_Combinator.thy
changeset 15197 19e735596e51
parent 15140 322485b816ac
child 18372 2bffdf62fe7f
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Sep 10 14:54:54 2004 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Sep 10 20:04:14 2004 +0200
     1.3 @@ -143,6 +143,13 @@
     1.4   An example of using the @{term while} combinator.
     1.5  *}
     1.6  
     1.7 +text{* Cannot use @{thm[source]set_eq_subset} because it leads to
     1.8 +looping because the antisymmetry simproc turns the subset relationship
     1.9 +back into equality. *}
    1.10 +
    1.11 +lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))"
    1.12 +by blast
    1.13 +
    1.14  theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
    1.15    P {0, 4, 2}"
    1.16  proof -
    1.17 @@ -156,7 +163,7 @@
    1.18       apply simp
    1.19      apply (simp add: aux set_eq_subset)
    1.20      txt {* The fixpoint computation is performed purely by rewriting: *}
    1.21 -    apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
    1.22 +    apply (simp add: while_unfold aux seteq del: subset_empty)
    1.23      done
    1.24  qed
    1.25