author paulson Wed, 15 May 2002 10:42:32 +0200 changeset 13149 773657d466cb parent 13148 fe118a977a6d child 13150 0c50d13d449a
better simplification of trivial existential equalities
 src/FOL/simpdata.ML file | annotate | diff | comparison | revisions src/ZF/AC.thy file | annotate | diff | comparison | revisions src/ZF/Epsilon.ML file | annotate | diff | comparison | revisions src/ZF/List.ML file | annotate | diff | comparison | revisions src/ZF/OrdQuant.thy file | annotate | diff | comparison | revisions
```--- 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)"]);
```
```--- 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 \<in> A*)
lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
apply (case_tac "A=0")
(*The non-trivial case*)
apply (blast intro: AC)
done```
```--- 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<i. transrec2(j,a,b))";```
```--- a/src/ZF/List.ML	Tue May 14 12:33:42 2002 +0200
+++ b/src/ZF/List.ML	Wed May 15 10:42:32 2002 +0200
@@ -238,7 +238,6 @@
\          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
qed_spec_mp "drop_length_Cons";

Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";```
```--- 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 @@