--- a/src/ZF/ZF.thy Thu Mar 29 13:59:54 2001 +0200
+++ b/src/ZF/ZF.thy Fri Mar 30 12:31:10 2001 +0200
@@ -150,9 +150,9 @@
"op <=" :: [i, i] => o (infixl "\\<subseteq>" 50)
"op :" :: [i, i] => o (infixl "\\<in>" 50)
"op ~:" :: [i, i] => o (infixl "\\<notin>" 50)
- "@Collect" :: [pttrn, i, o] => i ("(1{_\\<in> _ ./ _})")
- "@Replace" :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _\\<in> _, _})")
- "@RepFun" :: [i, pttrn, i] => i ("(1{_ ./ _\\<in> _})" [51,0,51])
+ "@Collect" :: [pttrn, i, o] => i ("(1{_ \\<in> _ ./ _})")
+ "@Replace" :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _ \\<in> _, _})")
+ "@RepFun" :: [i, pttrn, i] => i ("(1{_ ./ _ \\<in> _})" [51,0,51])
"@INTER" :: [pttrn, i, i] => i ("(3\\<Inter>_\\<in>_./ _)" 10)
"@UNION" :: [pttrn, i, i] => i ("(3\\<Union>_\\<in>_./ _)" 10)
"@PROD" :: [pttrn, i, i] => i ("(3\\<Pi>_\\<in>_./ _)" 10)
--- a/src/ZF/ex/LList.ML Thu Mar 29 13:59:54 2001 +0200
+++ b/src/ZF/ex/LList.ML Fri Mar 30 12:31:10 2001 +0200
@@ -23,7 +23,7 @@
val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)";
Goal "llist(A) = {0} <+> (A <*> llist(A))";
-let open llist; val rew = rewrite_rule con_defs in
+let open llist val rew = rewrite_rule con_defs in
by (fast_tac (claset() addSIs (subsetI ::map rew intrs) addEs [rew elim]) 1)
end;
qed "llist_unfold";
@@ -191,6 +191,5 @@
by (etac RepFunE 1);
by (etac llist.elim 1);
by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [flip_type, not_not]) 1);
-by (fast_tac (claset() addSIs [not_type]) 1);
+by (asm_full_simp_tac (simpset() addsimps [flip_type, not_not]) 1);
qed "flip_flip";
--- a/src/ZF/ex/PropLog.ML Thu Mar 29 13:59:54 2001 +0200
+++ b/src/ZF/ex/PropLog.ML Fri Mar 30 12:31:10 2001 +0200
@@ -190,9 +190,7 @@
could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*)
Goal "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
by (induct_tac "p" 1);
-by (asm_simp_tac (simpset() addsimps [UN_I]) 2);
-by (ALLGOALS Asm_simp_tac);
-by (blast_tac (claset() addIs Fin.intrs) 1);
+by Auto_tac;
qed "hyps_finite";
val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
--- a/src/ZF/ex/misc.ML Thu Mar 29 13:59:54 2001 +0200
+++ b/src/ZF/ex/misc.ML Fri Mar 30 12:31:10 2001 +0200
@@ -105,7 +105,7 @@
fun forw_iterate tyrls rls facts 0 = facts
| forw_iterate tyrls rls facts n =
let val facts' =
- gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts);
+ gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts)
in forw_iterate tyrls rls facts' (n-1) end;
val pastre_rls =
@@ -171,7 +171,8 @@
by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")]
lam_bijective 1);
(*Auto_tac no longer proves it*)
-by (REPEAT (fast_tac (claset() addss (simpset())) 1));
+by Auto_tac;
+by (ALLGOALS Blast_tac);
qed "Pow_sum_bij";
(*As a special case, we have bij(Pow(A*B), A -> Pow B) *)
--- a/src/ZF/simpdata.ML Thu Mar 29 13:59:54 2001 +0200
+++ b/src/ZF/simpdata.ML Fri Mar 30 12:31:10 2001 +0200
@@ -117,4 +117,59 @@
addsplits [split_if]
setSolver (mk_solver "types" Type_solver_tac);
+(** One-point rule for bounded quantifiers: see HOL/Set.ML **)
+
+Goal "(EX x:A. x=a) <-> (a:A)";
+by (Blast_tac 1);
+qed "bex_triv_one_point1";
+
+Goal "(EX x:A. a=x) <-> (a:A)";
+by (Blast_tac 1);
+qed "bex_triv_one_point2";
+
+Goal "(EX x:A. x=a & P(x)) <-> (a:A & P(a))";
+by (Blast_tac 1);
+qed "bex_one_point1";
+
+Goal "(EX x:A. a=x & P(x)) <-> (a:A & P(a))";
+by(Blast_tac 1);
+qed "bex_one_point2";
+
+Goal "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))";
+by (Blast_tac 1);
+qed "ball_one_point1";
+
+Goal "(ALL x:A. a=x --> P(x)) <-> (a:A --> P(a))";
+by (Blast_tac 1);
+qed "ball_one_point2";
+
+Addsimps [bex_triv_one_point1,bex_triv_one_point2,
+ bex_one_point1,bex_one_point2,
+ ball_one_point1,ball_one_point2];
+
+let
+val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
+ ("EX x:A. P(x) & Q(x)",FOLogic.oT)
+
+val prove_bex_tac = rewrite_goals_tac [Bex_def] THEN
+ Quantifier1.prove_one_point_ex_tac;
+
+val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
+
+val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
+ ("ALL x:A. P(x) --> Q(x)",FOLogic.oT)
+
+val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN
+ Quantifier1.prove_one_point_all_tac;
+
+val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
+
+val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
+val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
+in
+
+Addsimprocs [defBALL_regroup,defBEX_regroup]
+
+end;
+
val ZF_ss = simpset();