# HG changeset patch # User paulson # Date 1021452152 -7200 # Node ID 773657d466cba07acb70511cf4b2613d590c4dea # Parent fe118a977a6dd02a2b6b7ebcec9e2f4bace014fa better simplification of trivial existential equalities diff -r fe118a977a6d -r 773657d466cb src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Tue May 14 12:33:42 2002 +0200 +++ b/src/FOL/simpdata.ML Wed May 15 10:42:32 2002 +0200 @@ -57,6 +57,7 @@ "(ALL x. x=t --> P(x)) <-> P(t)", "(ALL x. t=x --> P(x)) <-> P(t)", "(EX x. P) <-> P", + "EX x. x=t", "EX x. t=x", "(EX x. x=t & P(x)) <-> P(t)", "(EX x. t=x & P(x)) <-> P(t)"]); diff -r fe118a977a6d -r 773657d466cb src/ZF/AC.thy --- a/src/ZF/AC.thy Tue May 14 12:33:42 2002 +0200 +++ b/src/ZF/AC.thy Wed May 15 10:42:32 2002 +0200 @@ -15,7 +15,7 @@ (*The same as AC, but no premise a \ A*) lemma AC_Pi: "[| !!x. x \ A ==> (\y. y \ B(x)) |] ==> \z. z \ Pi(A,B)" apply (case_tac "A=0") -apply (simp add: Pi_empty1, blast) +apply (simp add: Pi_empty1) (*The non-trivial case*) apply (blast intro: AC) done diff -r fe118a977a6d -r 773657d466cb src/ZF/Epsilon.ML --- a/src/ZF/Epsilon.ML Tue May 14 12:33:42 2002 +0200 +++ b/src/ZF/Epsilon.ML Wed May 15 10:42:32 2002 +0200 @@ -314,7 +314,6 @@ Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"; by (rtac (transrec2_def RS def_transrec RS trans) 1); by (simp_tac (simpset() addsimps [the_equality, if_P]) 1); -by (Blast_tac 1); qed "transrec2_succ"; Goal "Limit(i) ==> transrec2(i,a,b) = (UN j ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))"; diff -r fe118a977a6d -r 773657d466cb src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Tue May 14 12:33:42 2002 +0200 +++ b/src/ZF/OrdQuant.thy Wed May 15 10:42:32 2002 +0200 @@ -84,7 +84,7 @@ by (simp add: function_def lam_def) lemma relation_lam: "relation (lam x:A. b(x))" -by (simp add: relation_def lam_def, blast) +by (simp add: relation_def lam_def) lemma restrict_iff: "z \ restrict(r,A) \ z \ r & (\x\A. \y. z = \x, y\)" by (simp add: restrict_def)