better simplification of trivial existential equalities
authorpaulson
Wed May 15 10:42:32 2002 +0200 (2002-05-15)
changeset 13149773657d466cb
parent 13148 fe118a977a6d
child 13150 0c50d13d449a
better simplification of trivial existential equalities
src/FOL/simpdata.ML
src/ZF/AC.thy
src/ZF/Epsilon.ML
src/ZF/List.ML
src/ZF/OrdQuant.thy
     1.1 --- a/src/FOL/simpdata.ML	Tue May 14 12:33:42 2002 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Wed May 15 10:42:32 2002 +0200
     1.3 @@ -57,6 +57,7 @@
     1.4    "(ALL x. x=t --> P(x)) <-> P(t)",
     1.5    "(ALL x. t=x --> P(x)) <-> P(t)",
     1.6    "(EX x. P) <-> P",
     1.7 +  "EX x. x=t", "EX x. t=x",
     1.8    "(EX x. x=t & P(x)) <-> P(t)",
     1.9    "(EX x. t=x & P(x)) <-> P(t)"]);
    1.10  
     2.1 --- a/src/ZF/AC.thy	Tue May 14 12:33:42 2002 +0200
     2.2 +++ b/src/ZF/AC.thy	Wed May 15 10:42:32 2002 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  (*The same as AC, but no premise a \<in> A*)
     2.5  lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
     2.6  apply (case_tac "A=0")
     2.7 -apply (simp add: Pi_empty1, blast)
     2.8 +apply (simp add: Pi_empty1)
     2.9  (*The non-trivial case*)
    2.10  apply (blast intro: AC)
    2.11  done
     3.1 --- a/src/ZF/Epsilon.ML	Tue May 14 12:33:42 2002 +0200
     3.2 +++ b/src/ZF/Epsilon.ML	Wed May 15 10:42:32 2002 +0200
     3.3 @@ -314,7 +314,6 @@
     3.4  Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
     3.5  by (rtac (transrec2_def RS def_transrec RS trans) 1);
     3.6  by (simp_tac (simpset() addsimps [the_equality, if_P]) 1);
     3.7 -by (Blast_tac 1);
     3.8  qed "transrec2_succ";
     3.9  
    3.10  Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
     4.1 --- a/src/ZF/List.ML	Tue May 14 12:33:42 2002 +0200
     4.2 +++ b/src/ZF/List.ML	Wed May 15 10:42:32 2002 +0200
     4.3 @@ -238,7 +238,6 @@
     4.4  \          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
     4.5  by (etac list.induct 1);
     4.6  by (ALLGOALS Asm_simp_tac);
     4.7 -by (Blast_tac 1);
     4.8  qed_spec_mp "drop_length_Cons";
     4.9  
    4.10  Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";
     5.1 --- a/src/ZF/OrdQuant.thy	Tue May 14 12:33:42 2002 +0200
     5.2 +++ b/src/ZF/OrdQuant.thy	Wed May 15 10:42:32 2002 +0200
     5.3 @@ -84,7 +84,7 @@
     5.4  by (simp add: function_def lam_def) 
     5.5  
     5.6  lemma relation_lam: "relation (lam x:A. b(x))"  
     5.7 -by (simp add: relation_def lam_def, blast) 
     5.8 +by (simp add: relation_def lam_def) 
     5.9  
    5.10  lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
    5.11  by (simp add: restrict_def)