# HG changeset patch # User paulson # Date 985948270 -7200 # Node ID 34c81a796ee3d1d5ffae35c94e894a6df449221c # Parent 558a4feebb049d981b47726ed8de977047563e0f the one-point rule for bounded quantifiers diff -r 558a4feebb04 -r 34c81a796ee3 src/ZF/ZF.thy --- 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 "\\" 50) "op :" :: [i, i] => o (infixl "\\" 50) "op ~:" :: [i, i] => o (infixl "\\" 50) - "@Collect" :: [pttrn, i, o] => i ("(1{_\\ _ ./ _})") - "@Replace" :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _\\ _, _})") - "@RepFun" :: [i, pttrn, i] => i ("(1{_ ./ _\\ _})" [51,0,51]) + "@Collect" :: [pttrn, i, o] => i ("(1{_ \\ _ ./ _})") + "@Replace" :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _ \\ _, _})") + "@RepFun" :: [i, pttrn, i] => i ("(1{_ ./ _ \\ _})" [51,0,51]) "@INTER" :: [pttrn, i, i] => i ("(3\\_\\_./ _)" 10) "@UNION" :: [pttrn, i, i] => i ("(3\\_\\_./ _)" 10) "@PROD" :: [pttrn, i, i] => i ("(3\\_\\_./ _)" 10) diff -r 558a4feebb04 -r 34c81a796ee3 src/ZF/ex/LList.ML --- 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"; diff -r 558a4feebb04 -r 34c81a796ee3 src/ZF/ex/PropLog.ML --- 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; diff -r 558a4feebb04 -r 34c81a796ee3 src/ZF/ex/misc.ML --- 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", "%.{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) *) diff -r 558a4feebb04 -r 34c81a796ee3 src/ZF/simpdata.ML --- 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();