--- a/src/ZF/Constructible/Wellorderings.thy Wed Jan 15 16:44:21 2003 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy Wed Jan 15 16:45:32 2003 +0100
@@ -84,7 +84,7 @@
lemma (in M_basic) wellfounded_on_iff_wellfounded:
"wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)"
apply (simp add: wellfounded_on_def wellfounded_def, safe)
- apply blast
+ apply force
apply (drule_tac x=x in rspec, assumption, blast)
done
--- a/src/ZF/Datatype.ML Wed Jan 15 16:44:21 2003 +0100
+++ b/src/ZF/Datatype.ML Wed Jan 15 16:45:32 2003 +0100
@@ -97,7 +97,8 @@
val conv =
- Simplifier.simproc (Theory.sign_of ZF.thy) "data_free" ["(x::i) = y"] proc;
+ Simplifier.simproc (Theory.sign_of (theory "ZF")) "data_free"
+ ["(x::i) = y"] proc;
end;
--- a/src/ZF/IsaMakefile Wed Jan 15 16:44:21 2003 +0100
+++ b/src/ZF/IsaMakefile Wed Jan 15 16:45:32 2003 +0100
@@ -36,7 +36,7 @@
InfDatatype.thy Integ/Bin.thy \
Integ/EquivClass.thy Integ/Int.thy Integ/IntArith.thy \
Integ/IntDiv.thy Integ/int_arith.ML \
- Let.ML Let.thy List.thy Main.ML Main.thy \
+ List.thy Main.ML Main.thy \
Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \
OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy \
QPair.thy QUniv.thy ROOT.ML \
@@ -44,7 +44,7 @@
Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \
Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \
Trancl.thy Univ.thy \
- WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \
+ WF.thy ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \
ind_syntax.ML pair.thy simpdata.ML \
thy_syntax.ML upair.thy
@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
--- a/src/ZF/Let.ML Wed Jan 15 16:44:21 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(* Title: ZF/Let
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-
-Let expressions -- borrowed from HOL
-*)
-
-val [prem] = goalw (the_context ())
- [Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))";
-by (rtac (refl RS prem) 1);
-qed "LetI";
--- a/src/ZF/Let.thy Wed Jan 15 16:44:21 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: ZF/Let
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-
-Let expressions, and tuple pattern-matching (borrowed from HOL)
-*)
-
-Let = FOL +
-
-types
- letbinds letbind
-
-consts
- Let :: "['a::logic, 'a => 'b] => ('b::logic)"
-
-syntax
- "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10)
- "" :: "letbind => letbinds" ("_")
- "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
- "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
-
-translations
- "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
- "let x = a in e" == "Let(a, %x. e)"
-
-defs
- Let_def "Let(s, f) == f(s)"
-
-end
--- a/src/ZF/WF.thy Wed Jan 15 16:44:21 2003 +0100
+++ b/src/ZF/WF.thy Wed Jan 15 16:45:32 2003 +0100
@@ -50,9 +50,7 @@
subsubsection{*Equivalences between @{term wf} and @{term wf_on}*}
lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
-apply (unfold wf_def wf_on_def, clarify) (*needed for blast's efficiency*)
-apply blast
-done
+by (unfold wf_def wf_on_def, force)
lemma wf_on_imp_wf: "[|wf[A](r); r <= A*A|] ==> wf(r)";
by (simp add: wf_on_def subset_Int_iff)
--- a/src/ZF/ZF.ML Wed Jan 15 16:44:21 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,510 +0,0 @@
-(* Title: ZF/ZF.ML
- ID: $Id$
- Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Basic introduction and elimination rules for Zermelo-Fraenkel Set Theory
-*)
-
-(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *)
-Goal "[| b:A; a=b |] ==> a:A";
-by (etac ssubst 1);
-by (assume_tac 1);
-qed "subst_elem";
-
-
-(*** Bounded universal quantifier ***)
-
-val prems= Goalw [Ball_def]
- "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
-by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ;
-qed "ballI";
-
-Goalw [Ball_def] "[| ALL x:A. P(x); x: A |] ==> P(x)";
-by (etac (spec RS mp) 1);
-by (assume_tac 1) ;
-qed "bspec";
-
-val major::prems= Goalw [Ball_def]
- "[| ALL x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q";
-by (rtac (major RS allE) 1);
-by (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ;
-qed "ballE";
-
-(*Used in the datatype package*)
-Goal "[| x: A; ALL x:A. P(x) |] ==> P(x)";
-by (REPEAT (ares_tac [bspec] 1)) ;
-qed "rev_bspec";
-
-(*Instantiates x first: better for automatic theorem proving?*)
-val major::prems= Goal
- "[| ALL x:A. P(x); x~:A ==> Q; P(x) ==> Q |] ==> Q";
-by (rtac (major RS ballE) 1);
-by (REPEAT (eresolve_tac prems 1)) ;
-qed "rev_ballE";
-
-AddSIs [ballI];
-AddEs [rev_ballE];
-
-(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
-val ball_tac = dtac bspec THEN' assume_tac;
-
-(*Trival rewrite rule; (ALL x:A.P)<->P holds only if A is nonempty!*)
-Goal "(ALL x:A. P) <-> ((EX x. x:A) --> P)";
-by (simp_tac (simpset() addsimps [Ball_def]) 1) ;
-qed "ball_triv";
-Addsimps [ball_triv];
-
-(*Congruence rule for rewriting*)
-val prems= Goalw [Ball_def]
- "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] \
-\ ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))";
-by (simp_tac (FOL_ss addsimps prems) 1) ;
-qed "ball_cong";
-
-(*** Bounded existential quantifier ***)
-
-Goalw [Bex_def] "[| P(x); x: A |] ==> EX x:A. P(x)";
-by (Blast_tac 1);
-qed "bexI";
-
-(*The best argument order when there is only one x:A*)
-Goalw [Bex_def] "[| x:A; P(x) |] ==> EX x:A. P(x)";
-by (Blast_tac 1);
-qed "rev_bexI";
-
-(*Not of the general form for such rules; ~EX has become ALL~ *)
-val prems= Goal "[| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A. P(x)";
-by (rtac classical 1);
-by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ;
-qed "bexCI";
-
-val major::prems= Goalw [Bex_def]
- "[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q \
-\ |] ==> Q";
-by (rtac (major RS exE) 1);
-by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
-qed "bexE";
-
-AddIs [bexI];
-AddSEs [bexE];
-
-(*We do not even have (EX x:A. True) <-> True unless A is nonempty!!*)
-Goal "(EX x:A. P) <-> ((EX x. x:A) & P)";
-by (simp_tac (simpset() addsimps [Bex_def]) 1) ;
-qed "bex_triv";
-Addsimps [bex_triv];
-
-val prems= Goalw [Bex_def]
- "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] \
-\ ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))";
-by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ;
-qed "bex_cong";
-
-Addcongs [ball_cong, bex_cong];
-
-
-(*** Rules for subsets ***)
-
-val prems= Goalw [subset_def]
- "(!!x. x:A ==> x:B) ==> A <= B";
-by (REPEAT (ares_tac (prems @ [ballI]) 1)) ;
-qed "subsetI";
-
-(*Rule in Modus Ponens style [was called subsetE] *)
-Goalw [subset_def] "[| A <= B; c:A |] ==> c:B";
-by (etac bspec 1);
-by (assume_tac 1) ;
-qed "subsetD";
-
-(*Classical elimination rule*)
-val major::prems= Goalw [subset_def]
- "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P";
-by (rtac (major RS ballE) 1);
-by (REPEAT (eresolve_tac prems 1)) ;
-qed "subsetCE";
-
-AddSIs [subsetI];
-AddEs [subsetCE, subsetD];
-
-
-(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
-val set_mp_tac = dtac subsetD THEN' assume_tac;
-
-(*Sometimes useful with premises in this order*)
-Goal "[| c:A; A<=B |] ==> c:B";
-by (Blast_tac 1);
-qed "rev_subsetD";
-
-(*Converts A<=B to x:A ==> x:B*)
-fun impOfSubs th = th RSN (2, rev_subsetD);
-
-Goal "[| A <= B; c ~: B |] ==> c ~: A";
-by (Blast_tac 1);
-qed "contra_subsetD";
-
-Goal "[| c ~: B; A <= B |] ==> c ~: A";
-by (Blast_tac 1);
-qed "rev_contra_subsetD";
-
-Goal "A <= A";
-by (Blast_tac 1);
-qed "subset_refl";
-
-Addsimps [subset_refl];
-
-Goal "[| A<=B; B<=C |] ==> A<=C";
-by (Blast_tac 1);
-qed "subset_trans";
-
-(*Useful for proving A<=B by rewriting in some cases*)
-Goalw [subset_def,Ball_def]
- "A<=B <-> (ALL x. x:A --> x:B)";
-by (rtac iff_refl 1) ;
-qed "subset_iff";
-
-
-(*** Rules for equality ***)
-
-(*Anti-symmetry of the subset relation*)
-Goal "[| A <= B; B <= A |] ==> A = B";
-by (REPEAT (ares_tac [conjI, extension RS iffD2] 1)) ;
-qed "equalityI";
-
-AddIs [equalityI];
-
-val [prem] = Goal "(!!x. x:A <-> x:B) ==> A = B";
-by (rtac equalityI 1);
-by (REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ;
-qed "equality_iffI";
-
-bind_thm ("equalityD1", extension RS iffD1 RS conjunct1);
-bind_thm ("equalityD2", extension RS iffD1 RS conjunct2);
-
-val prems = Goal "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P";
-by (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ;
-qed "equalityE";
-
-val major::prems= Goal
- "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P";
-by (rtac (major RS equalityE) 1);
-by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ;
-qed "equalityCE";
-
-(*Lemma for creating induction formulae -- for "pattern matching" on p
- To make the induction hypotheses usable, apply "spec" or "bspec" to
- put universal quantifiers over the free variables in p.
- Would it be better to do subgoal_tac "ALL z. p = f(z) --> R(z)" ??*)
-val prems = Goal "[| p: A; !!z. z: A ==> p=z --> R |] ==> R";
-by (rtac mp 1);
-by (REPEAT (resolve_tac (refl::prems) 1)) ;
-qed "setup_induction";
-
-
-(*** Rules for Replace -- the derived form of replacement ***)
-
-Goalw [Replace_def]
- "b : {y. x:A, P(x,y)} <-> (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))";
-by (rtac (replacement RS iff_trans) 1);
-by (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1
- ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ;
-qed "Replace_iff";
-
-(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
-val prems = Goal
- "[| P(x,b); x: A; !!y. P(x,y) ==> y=b |] ==> \
-\ b : {y. x:A, P(x,y)}";
-by (rtac (Replace_iff RS iffD2) 1);
-by (REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ;
-qed "ReplaceI";
-
-(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
-val prems = Goal
- "[| b : {y. x:A, P(x,y)}; \
-\ !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R \
-\ |] ==> R";
-by (rtac (Replace_iff RS iffD1 RS bexE) 1);
-by (etac conjE 2);
-by (REPEAT (ares_tac prems 1)) ;
-qed "ReplaceE";
-
-(*As above but without the (generally useless) 3rd assumption*)
-val major::prems = Goal
- "[| b : {y. x:A, P(x,y)}; \
-\ !!x. [| x: A; P(x,b) |] ==> R \
-\ |] ==> R";
-by (rtac (major RS ReplaceE) 1);
-by (REPEAT (ares_tac prems 1)) ;
-qed "ReplaceE2";
-
-AddIs [ReplaceI];
-AddSEs [ReplaceE2];
-
-val prems = Goal
- "[| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
-\ Replace(A,P) = Replace(B,Q)";
-by (rtac equalityI 1);
-by (REPEAT
- (eresolve_tac ((prems RL [subst, ssubst])@[asm_rl, ReplaceE, spec RS mp]) 1 ORELSE resolve_tac [subsetI, ReplaceI] 1
- ORELSE (resolve_tac (prems RL [iffD1,iffD2]) 1 THEN assume_tac 2)));
-qed "Replace_cong";
-
-Addcongs [Replace_cong];
-
-(*** Rules for RepFun ***)
-
-Goalw [RepFun_def] "a : A ==> f(a) : {f(x). x:A}";
-by (REPEAT (ares_tac [ReplaceI,refl] 1)) ;
-qed "RepFunI";
-
-(*Useful for coinduction proofs*)
-Goal "[| b=f(a); a : A |] ==> b : {f(x). x:A}";
-by (etac ssubst 1);
-by (etac RepFunI 1) ;
-qed "RepFun_eqI";
-
-val major::prems= Goalw [RepFun_def]
- "[| b : {f(x). x:A}; \
-\ !!x.[| x:A; b=f(x) |] ==> P |] ==> \
-\ P";
-by (rtac (major RS ReplaceE) 1);
-by (REPEAT (ares_tac prems 1)) ;
-qed "RepFunE";
-
-AddIs [RepFun_eqI];
-AddSEs [RepFunE];
-
-val prems= Goalw [RepFun_def]
- "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)";
-by (simp_tac (simpset() addsimps prems) 1) ;
-qed "RepFun_cong";
-
-Addcongs [RepFun_cong];
-
-Goalw [Bex_def] "b : {f(x). x:A} <-> (EX x:A. b=f(x))";
-by (Blast_tac 1);
-qed "RepFun_iff";
-
-Goal "{x. x:A} = A";
-by (Blast_tac 1);
-qed "triv_RepFun";
-
-Addsimps [RepFun_iff, triv_RepFun];
-
-(*** Rules for Collect -- forming a subset by separation ***)
-
-(*Separation is derivable from Replacement*)
-Goalw [Collect_def] "a : {x:A. P(x)} <-> a:A & P(a)";
-by (Blast_tac 1);
-qed "separation";
-
-Addsimps [separation];
-
-Goal "[| a:A; P(a) |] ==> a : {x:A. P(x)}";
-by (Asm_simp_tac 1);
-qed "CollectI";
-
-val prems = Goal
- "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> R |] ==> R";
-by (rtac (separation RS iffD1 RS conjE) 1);
-by (REPEAT (ares_tac prems 1)) ;
-qed "CollectE";
-
-Goal "a : {x:A. P(x)} ==> a:A";
-by (etac CollectE 1);
-by (assume_tac 1) ;
-qed "CollectD1";
-
-Goal "a : {x:A. P(x)} ==> P(a)";
-by (etac CollectE 1);
-by (assume_tac 1) ;
-qed "CollectD2";
-
-val prems= Goalw [Collect_def]
- "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] \
-\ ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))";
-by (simp_tac (simpset() addsimps prems) 1) ;
-qed "Collect_cong";
-
-AddSIs [CollectI];
-AddSEs [CollectE];
-Addcongs [Collect_cong];
-
-(*** Rules for Unions ***)
-
-Addsimps [Union_iff];
-
-(*The order of the premises presupposes that C is rigid; A may be flexible*)
-Goal "[| B: C; A: B |] ==> A: Union(C)";
-by (Simp_tac 1);
-by (Blast_tac 1) ;
-qed "UnionI";
-
-val prems = Goal "[| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R";
-by (resolve_tac [Union_iff RS iffD1 RS bexE] 1);
-by (REPEAT (ares_tac prems 1)) ;
-qed "UnionE";
-
-(*** Rules for Unions of families ***)
-(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
-
-Goalw [Bex_def] "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))";
-by (Simp_tac 1);
-by (Blast_tac 1) ;
-qed "UN_iff";
-
-Addsimps [UN_iff];
-
-(*The order of the premises presupposes that A is rigid; b may be flexible*)
-Goal "[| a: A; b: B(a) |] ==> b: (UN x:A. B(x))";
-by (Simp_tac 1);
-by (Blast_tac 1) ;
-qed "UN_I";
-
-val major::prems= Goal
- "[| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R";
-by (rtac (major RS UnionE) 1);
-by (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ;
-qed "UN_E";
-
-val prems = Goal
- "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A. C(x)) = (UN x:B. D(x))";
-by (simp_tac (simpset() addsimps prems) 1) ;
-qed "UN_cong";
-
-(*No "Addcongs [UN_cong]" because UN is a combination of constants*)
-
-(* UN_E appears before UnionE so that it is tried first, to avoid expensive
- calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: would enlarge
- the search space.*)
-AddIs [UnionI];
-AddSEs [UN_E];
-AddSEs [UnionE];
-
-
-(*** Rules for Inter ***)
-
-(*Not obviously useful towards proving InterI, InterD, InterE*)
-Goalw [Inter_def,Ball_def]
- "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)";
-by (Simp_tac 1);
-by (Blast_tac 1) ;
-qed "Inter_iff";
-
-(* Intersection is well-behaved only if the family is non-empty! *)
-val prems = Goal
- "[| !!x. x: C ==> A: x; EX c. c:C |] ==> A : Inter(C)";
-by (simp_tac (simpset() addsimps [Inter_iff]) 1);
-by (blast_tac (claset() addIs prems) 1) ;
-qed "InterI";
-
-(*A "destruct" rule -- every B in C contains A as an element, but
- A:B can hold when B:C does not! This rule is analogous to "spec". *)
-Goalw [Inter_def] "[| A : Inter(C); B : C |] ==> A : B";
-by (Blast_tac 1);
-qed "InterD";
-
-(*"Classical" elimination rule -- does not require exhibiting B:C *)
-val major::prems= Goalw [Inter_def]
- "[| A : Inter(C); B~:C ==> R; A:B ==> R |] ==> R";
-by (rtac (major RS CollectD2 RS ballE) 1);
-by (REPEAT (eresolve_tac prems 1)) ;
-qed "InterE";
-
-AddSIs [InterI];
-AddEs [InterD, InterE];
-
-(*** Rules for Intersections of families ***)
-(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
-
-Goalw [Inter_def] "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)";
-by (Simp_tac 1);
-by (Best_tac 1) ;
-qed "INT_iff";
-
-val prems = Goal
- "[| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x))";
-by (blast_tac (claset() addIs prems) 1);
-qed "INT_I";
-
-Goal "[| b : (INT x:A. B(x)); a: A |] ==> b : B(a)";
-by (Blast_tac 1);
-qed "INT_E";
-
-val prems = Goal
- "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A. C(x)) = (INT x:B. D(x))";
-by (simp_tac (simpset() addsimps prems) 1) ;
-qed "INT_cong";
-
-(*No "Addcongs [INT_cong]" because INT is a combination of constants*)
-
-
-(*** Rules for Powersets ***)
-
-Goal "A <= B ==> A : Pow(B)";
-by (etac (Pow_iff RS iffD2) 1) ;
-qed "PowI";
-
-Goal "A : Pow(B) ==> A<=B";
-by (etac (Pow_iff RS iffD1) 1) ;
-qed "PowD";
-
-AddIffs [Pow_iff];
-
-
-(*** Rules for the empty set ***)
-
-(*The set {x:0.False} is empty; by foundation it equals 0
- See Suppes, page 21.*)
-Goal "a ~: 0";
-by (cut_facts_tac [foundation] 1);
-by (best_tac (claset() addDs [equalityD2]) 1) ;
-qed "not_mem_empty";
-
-bind_thm ("emptyE", not_mem_empty RS notE);
-
-Addsimps [not_mem_empty];
-AddSEs [emptyE];
-
-Goal "0 <= A";
-by (Blast_tac 1);
-qed "empty_subsetI";
-
-Addsimps [empty_subsetI];
-
-val prems = Goal "[| !!y. y:A ==> False |] ==> A=0";
-by (blast_tac (claset() addDs prems) 1) ;
-qed "equals0I";
-
-Goal "A=0 ==> a ~: A";
-by (Blast_tac 1);
-qed "equals0D";
-
-AddDs [equals0D, sym RS equals0D];
-
-Goal "a:A ==> A ~= 0";
-by (Blast_tac 1);
-qed "not_emptyI";
-
-val [major,minor]= Goal "[| A ~= 0; !!x. x:A ==> R |] ==> R";
-by (rtac ([major, equals0I] MRS swap) 1);
-by (swap_res_tac [minor] 1);
-by (assume_tac 1) ;
-qed "not_emptyE";
-
-
-(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
-
-val cantor_cs = FOL_cs (*precisely the rules needed for the proof*)
- addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI]
- addSEs [CollectE, equalityCE];
-
-(*The search is undirected; similar proof attempts may fail.
- b represents ANY map, such as (lam x:A.b(x)): A->Pow(A). *)
-Goal "EX S: Pow(A). ALL x:A. b(x) ~= S";
-by (best_tac cantor_cs 1);
-qed "cantor";
-
-Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))";
-by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
-qed "atomize_ball";
--- a/src/ZF/ZF.thy Wed Jan 15 16:44:21 2003 +0100
+++ b/src/ZF/ZF.thy Wed Jan 15 16:45:32 2003 +0100
@@ -6,11 +6,11 @@
Zermelo-Fraenkel Set Theory
*)
-ZF = Let +
+theory ZF = FOL:
global
-types
+typedecl
i
arities
@@ -23,23 +23,21 @@
Inf :: "i" (*infinite set*)
(* Bounded Quantifiers *)
-
- Ball, Bex :: "[i, i => o] => o"
+ Ball :: "[i, i => o] => o"
+ Bex :: "[i, i => o] => o"
(* General Union and Intersection *)
-
- Union,Inter :: "i => i"
+ Union :: "i => i"
+ Inter :: "i => i"
(* Variations on Replacement *)
-
PrimReplace :: "[i, [i, i] => o] => i"
Replace :: "[i, [i, i] => o] => i"
RepFun :: "[i, i => i] => i"
Collect :: "[i, i => o] => i"
(* Descriptions *)
-
- The :: (i => o) => i (binder "THE " 10)
+ The :: "(i => o) => i" (binder "THE " 10)
If :: "[o, i, i] => i" ("(if (_)/ then (_)/ else (_))" [10] 10)
syntax
@@ -50,24 +48,25 @@
consts
+
(* Finite Sets *)
-
- Upair, cons :: "[i, i] => i"
- succ :: "i => i"
+ Upair :: "[i, i] => i"
+ cons :: "[i, i] => i"
+ succ :: "i => i"
(* Ordered Pairing *)
-
- Pair :: "[i, i] => i"
- fst, snd :: "i => i"
- split :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*)
+ Pair :: "[i, i] => i"
+ fst :: "i => i"
+ snd :: "i => i"
+ split :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*)
(* Sigma and Pi Operators *)
-
- Sigma, Pi :: "[i, i => i] => i"
+ Sigma :: "[i, i => i] => i"
+ Pi :: "[i, i => i] => i"
(* Relations and Functions *)
- domain :: "i => i"
+ "domain" :: "i => i"
range :: "i => i"
field :: "i => i"
converse :: "i => i"
@@ -81,19 +80,17 @@
"``" :: "[i, i] => i" (infixl 90) (*image*)
"-``" :: "[i, i] => i" (infixl 90) (*inverse image*)
"`" :: "[i, i] => i" (infixl 90) (*function application*)
-(*"*" :: "[i, i] => i" (infixr 80) (*Cartesian product*)*)
+(*"*" :: "[i, i] => i" (infixr 80) [virtual] Cartesian product*)
"Int" :: "[i, i] => i" (infixl 70) (*binary intersection*)
"Un" :: "[i, i] => i" (infixl 65) (*binary union*)
"-" :: "[i, i] => i" (infixl 65) (*set difference*)
-(*"->" :: "[i, i] => i" (infixr 60) (*function space*)*)
+(*"->" :: "[i, i] => i" (infixr 60) [virtual] function spac\<epsilon>*)
"<=" :: "[i, i] => o" (infixl 50) (*subset relation*)
":" :: "[i, i] => o" (infixl 50) (*membership relation*)
(*"~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)*)
-types
- is
- patterns
+nonterminals "is" patterns
syntax
"" :: "i => is" ("_")
@@ -144,62 +141,62 @@
syntax (xsymbols)
- "op *" :: "[i, i] => i" (infixr "\\<times>" 80)
- "op Int" :: "[i, i] => i" (infixl "\\<inter>" 70)
- "op Un" :: "[i, i] => i" (infixl "\\<union>" 65)
- "op ->" :: "[i, i] => i" (infixr "\\<rightarrow>" 60)
- "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])
- "@UNION" :: "[pttrn, i, i] => i" ("(3\\<Union>_\\<in>_./ _)" 10)
- "@INTER" :: "[pttrn, i, i] => i" ("(3\\<Inter>_\\<in>_./ _)" 10)
- Union :: "i =>i" ("\\<Union>_" [90] 90)
- Inter :: "i =>i" ("\\<Inter>_" [90] 90)
- "@PROD" :: "[pttrn, i, i] => i" ("(3\\<Pi>_\\<in>_./ _)" 10)
- "@SUM" :: "[pttrn, i, i] => i" ("(3\\<Sigma>_\\<in>_./ _)" 10)
- "@lam" :: "[pttrn, i, i] => i" ("(3\\<lambda>_\\<in>_./ _)" 10)
- "@Ball" :: "[pttrn, i, o] => o" ("(3\\<forall>_\\<in>_./ _)" 10)
- "@Bex" :: "[pttrn, i, o] => o" ("(3\\<exists>_\\<in>_./ _)" 10)
- "@Tuple" :: "[i, is] => i" ("\\<langle>(_,/ _)\\<rangle>")
- "@pattern" :: "patterns => pttrn" ("\\<langle>_\\<rangle>")
+ "op *" :: "[i, i] => i" (infixr "\<times>" 80)
+ "op Int" :: "[i, i] => i" (infixl "\<inter>" 70)
+ "op Un" :: "[i, i] => i" (infixl "\<union>" 65)
+ "op ->" :: "[i, i] => i" (infixr "\<rightarrow>" 60)
+ "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])
+ "@UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
+ "@INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
+ Union :: "i =>i" ("\<Union>_" [90] 90)
+ Inter :: "i =>i" ("\<Inter>_" [90] 90)
+ "@PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10)
+ "@SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10)
+ "@lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
+ "@Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10)
+ "@Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10)
+ "@Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
+ "@pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
syntax (HTML output)
- "op *" :: "[i, i] => i" (infixr "\\<times>" 80)
+ "op *" :: "[i, i] => i" (infixr "\<times>" 80)
-defs
+defs
+(*don't try to use constdefs: the declaration order is tightly constrained*)
(* Bounded Quantifiers *)
- Ball_def "Ball(A, P) == ALL x. x:A --> P(x)"
- Bex_def "Bex(A, P) == EX x. x:A & P(x)"
+ Ball_def: "Ball(A, P) == ALL x. x:A --> P(x)"
+ Bex_def: "Bex(A, P) == EX x. x:A & P(x)"
- subset_def "A <= B == ALL x:A. x:B"
- succ_def "succ(i) == cons(i, i)"
+ subset_def: "A <= B == ALL x:A. x:B"
local
-rules
+axioms
(* ZF axioms -- see Suppes p.238
Axioms for Union, Pow and Replace state existence only,
uniqueness is derivable using extensionality. *)
- extension "A = B <-> A <= B & B <= A"
- Union_iff "A : Union(C) <-> (EX B:C. A:B)"
- Pow_iff "A : Pow(B) <-> A <= B"
+ extension: "A = B <-> A <= B & B <= A"
+ Union_iff: "A : Union(C) <-> (EX B:C. A:B)"
+ Pow_iff: "A : Pow(B) <-> A <= B"
(*We may name this set, though it is not uniquely defined.*)
- infinity "0:Inf & (ALL y:Inf. succ(y): Inf)"
+ infinity: "0:Inf & (ALL y:Inf. succ(y): Inf)"
(*This formulation facilitates case analysis on A.*)
- foundation "A=0 | (EX x:A. ALL y:x. y~:A)"
+ foundation: "A=0 | (EX x:A. ALL y:x. y~:A)"
(*Schema axiom since predicate P is a higher-order variable*)
- replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
+ replacement: "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
defs
@@ -208,73 +205,525 @@
The resulting set (for functional P) is the same as with
PrimReplace, but the rules are simpler. *)
- Replace_def "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
+ Replace_def: "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
(* Functional form of replacement -- analgous to ML's map functional *)
- RepFun_def "RepFun(A,f) == {y . x:A, y=f(x)}"
+ RepFun_def: "RepFun(A,f) == {y . x:A, y=f(x)}"
(* Separation and Pairing can be derived from the Replacement
and Powerset Axioms using the following definitions. *)
- Collect_def "Collect(A,P) == {y . x:A, x=y & P(x)}"
+ Collect_def: "Collect(A,P) == {y . x:A, x=y & P(x)}"
(*Unordered pairs (Upair) express binary union/intersection and cons;
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
- Upair_def "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
- cons_def "cons(a,A) == Upair(a,a) Un A"
+ Upair_def: "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
+ cons_def: "cons(a,A) == Upair(a,a) Un A"
+ succ_def: "succ(i) == cons(i, i)"
(* Difference, general intersection, binary union and small intersection *)
- Diff_def "A - B == { x:A . ~(x:B) }"
- Inter_def "Inter(A) == { x:Union(A) . ALL y:A. x:y}"
- Un_def "A Un B == Union(Upair(A,B))"
- Int_def "A Int B == Inter(Upair(A,B))"
+ Diff_def: "A - B == { x:A . ~(x:B) }"
+ Inter_def: "Inter(A) == { x:Union(A) . ALL y:A. x:y}"
+ Un_def: "A Un B == Union(Upair(A,B))"
+ Int_def: "A Int B == Inter(Upair(A,B))"
(* Definite descriptions -- via Replace over the set "1" *)
- the_def "The(P) == Union({y . x:{0}, P(y)})"
- if_def "if(P,a,b) == THE z. P & z=a | ~P & z=b"
+ the_def: "The(P) == Union({y . x:{0}, P(y)})"
+ if_def: "if(P,a,b) == THE z. P & z=a | ~P & z=b"
(* this "symmetric" definition works better than {{a}, {a,b}} *)
- Pair_def "<a,b> == {{a,a}, {a,b}}"
- fst_def "fst(p) == THE a. EX b. p=<a,b>"
- snd_def "snd(p) == THE b. EX a. p=<a,b>"
- split_def "split(c) == %p. c(fst(p), snd(p))"
- Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
+ Pair_def: "<a,b> == {{a,a}, {a,b}}"
+ fst_def: "fst(p) == THE a. EX b. p=<a,b>"
+ snd_def: "snd(p) == THE b. EX a. p=<a,b>"
+ split_def: "split(c) == %p. c(fst(p), snd(p))"
+ Sigma_def: "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
(* Operations on relations *)
(*converse of relation r, inverse of function*)
- converse_def "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}"
+ converse_def: "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}"
- domain_def "domain(r) == {x. w:r, EX y. w=<x,y>}"
- range_def "range(r) == domain(converse(r))"
- field_def "field(r) == domain(r) Un range(r)"
- relation_def "relation(r) == ALL z:r. EX x y. z = <x,y>"
- function_def "function(r) ==
+ domain_def: "domain(r) == {x. w:r, EX y. w=<x,y>}"
+ range_def: "range(r) == domain(converse(r))"
+ field_def: "field(r) == domain(r) Un range(r)"
+ relation_def: "relation(r) == ALL z:r. EX x y. z = <x,y>"
+ function_def: "function(r) ==
ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y')"
- image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}"
- vimage_def "r -`` A == converse(r)``A"
+ image_def: "r `` A == {y : range(r) . EX x:A. <x,y> : r}"
+ vimage_def: "r -`` A == converse(r)``A"
(* Abstraction, application and Cartesian product of a family of sets *)
- lam_def "Lambda(A,b) == {<x,b(x)> . x:A}"
- apply_def "f`a == Union(f``{a})"
- Pi_def "Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
+ lam_def: "Lambda(A,b) == {<x,b(x)> . x:A}"
+ apply_def: "f`a == Union(f``{a})"
+ Pi_def: "Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
(* Restrict the relation r to the domain A *)
- restrict_def "restrict(r,A) == {z : r. EX x:A. EX y. z = <x,y>}"
+ restrict_def: "restrict(r,A) == {z : r. EX x:A. EX y. z = <x,y>}"
+
+(* Pattern-matching and 'Dependent' type operators *)
+
+print_translation {*
+ [("Pi", dependent_tr' ("@PROD", "op ->")),
+ ("Sigma", dependent_tr' ("@SUM", "op *"))];
+*}
+
+subsection {* Substitution*}
+
+(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *)
+lemma subst_elem: "[| b:A; a=b |] ==> a:A"
+by (erule ssubst, assumption)
+
+
+subsection{*Bounded universal quantifier*}
+
+lemma ballI [intro!]: "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
+by (simp add: Ball_def)
+
+lemma bspec [dest?]: "[| ALL x:A. P(x); x: A |] ==> P(x)"
+by (simp add: Ball_def)
+
+(*Instantiates x first: better for automatic theorem proving?*)
+lemma rev_ballE [elim]:
+ "[| ALL x:A. P(x); x~:A ==> Q; P(x) ==> Q |] ==> Q"
+by (simp add: Ball_def, blast)
+
+lemma ballE: "[| ALL x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q"
+by blast
+
+(*Used in the datatype package*)
+lemma rev_bspec: "[| x: A; ALL x:A. P(x) |] ==> P(x)"
+by (simp add: Ball_def)
+
+(*Trival rewrite rule; (ALL x:A.P)<->P holds only if A is nonempty!*)
+lemma ball_triv [simp]: "(ALL x:A. P) <-> ((EX x. x:A) --> P)"
+by (simp add: Ball_def)
+
+(*Congruence rule for rewriting*)
+lemma ball_cong [cong]:
+ "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
+by (simp add: Ball_def)
+
+
+subsection{*Bounded existential quantifier*}
+
+lemma bexI [intro]: "[| P(x); x: A |] ==> EX x:A. P(x)"
+by (simp add: Bex_def, blast)
+
+(*The best argument order when there is only one x:A*)
+lemma rev_bexI: "[| x:A; P(x) |] ==> EX x:A. P(x)"
+by blast
+
+(*Not of the general form for such rules; ~EX has become ALL~ *)
+lemma bexCI: "[| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A. P(x)"
+by blast
+
+lemma bexE [elim!]: "[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"
+by (simp add: Bex_def, blast)
+
+(*We do not even have (EX x:A. True) <-> True unless A is nonempty!!*)
+lemma bex_triv [simp]: "(EX x:A. P) <-> ((EX x. x:A) & P)"
+by (simp add: Bex_def)
+
+lemma bex_cong [cong]:
+ "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |]
+ ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
+by (simp add: Bex_def cong: conj_cong)
+
+
+
+subsection{*Rules for subsets*}
+
+lemma subsetI [intro!]:
+ "(!!x. x:A ==> x:B) ==> A <= B"
+by (simp add: subset_def)
+
+(*Rule in Modus Ponens style [was called subsetE] *)
+lemma subsetD [elim]: "[| A <= B; c:A |] ==> c:B"
+apply (unfold subset_def)
+apply (erule bspec, assumption)
+done
+
+(*Classical elimination rule*)
+lemma subsetCE [elim]:
+ "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P"
+by (simp add: subset_def, blast)
+
+(*Sometimes useful with premises in this order*)
+lemma rev_subsetD: "[| c:A; A<=B |] ==> c:B"
+by blast
+
+lemma contra_subsetD: "[| A <= B; c ~: B |] ==> c ~: A"
+by blast
+
+lemma rev_contra_subsetD: "[| c ~: B; A <= B |] ==> c ~: A"
+by blast
+
+lemma subset_refl [simp]: "A <= A"
+by blast
+
+lemma subset_trans: "[| A<=B; B<=C |] ==> A<=C"
+by blast
+
+(*Useful for proving A<=B by rewriting in some cases*)
+lemma subset_iff:
+ "A<=B <-> (ALL x. x:A --> x:B)"
+apply (unfold subset_def Ball_def)
+apply (rule iff_refl)
+done
+
+
+subsection{*Rules for equality*}
+
+(*Anti-symmetry of the subset relation*)
+lemma equalityI [intro]: "[| A <= B; B <= A |] ==> A = B"
+by (rule extension [THEN iffD2], rule conjI)
+
+
+lemma equality_iffI: "(!!x. x:A <-> x:B) ==> A = B"
+by (rule equalityI, blast+)
+
+lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1, standard]
+lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2, standard]
+
+lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"
+by (blast dest: equalityD1 equalityD2)
+
+lemma equalityCE:
+ "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"
+by (erule equalityE, blast)
+
+(*Lemma for creating induction formulae -- for "pattern matching" on p
+ To make the induction hypotheses usable, apply "spec" or "bspec" to
+ put universal quantifiers over the free variables in p.
+ Would it be better to do subgoal_tac "ALL z. p = f(z) --> R(z)" ??*)
+lemma setup_induction: "[| p: A; !!z. z: A ==> p=z --> R |] ==> R"
+by auto
+
+
+
+subsection{*Rules for Replace -- the derived form of replacement*}
+
+lemma Replace_iff:
+ "b : {y. x:A, P(x,y)} <-> (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
+apply (unfold Replace_def)
+apply (rule replacement [THEN iff_trans], blast+)
+done
+
+(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
+lemma ReplaceI [intro]:
+ "[| P(x,b); x: A; !!y. P(x,y) ==> y=b |] ==>
+ b : {y. x:A, P(x,y)}"
+by (rule Replace_iff [THEN iffD2], blast)
+
+(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
+lemma ReplaceE:
+ "[| b : {y. x:A, P(x,y)};
+ !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R
+ |] ==> R"
+by (rule Replace_iff [THEN iffD1, THEN bexE], simp+)
+
+(*As above but without the (generally useless) 3rd assumption*)
+lemma ReplaceE2 [elim!]:
+ "[| b : {y. x:A, P(x,y)};
+ !!x. [| x: A; P(x,b) |] ==> R
+ |] ==> R"
+by (erule ReplaceE, blast)
+
+lemma Replace_cong [cong]:
+ "[| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==>
+ Replace(A,P) = Replace(B,Q)"
+apply (rule equality_iffI)
+apply (simp add: Replace_iff)
+done
+
+
+subsection{*Rules for RepFun*}
+
+lemma RepFunI: "a : A ==> f(a) : {f(x). x:A}"
+by (simp add: RepFun_def Replace_iff, blast)
+
+(*Useful for coinduction proofs*)
+lemma RepFun_eqI [intro]: "[| b=f(a); a : A |] ==> b : {f(x). x:A}"
+apply (erule ssubst)
+apply (erule RepFunI)
+done
+
+lemma RepFunE [elim!]:
+ "[| b : {f(x). x:A};
+ !!x.[| x:A; b=f(x) |] ==> P |] ==>
+ P"
+by (simp add: RepFun_def Replace_iff, blast)
+
+lemma RepFun_cong [cong]:
+ "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
+by (simp add: RepFun_def)
+
+lemma RepFun_iff [simp]: "b : {f(x). x:A} <-> (EX x:A. b=f(x))"
+by (unfold Bex_def, blast)
+
+lemma triv_RepFun [simp]: "{x. x:A} = A"
+by blast
+
+
+subsection{*Rules for Collect -- forming a subset by separation*}
+
+(*Separation is derivable from Replacement*)
+lemma separation [simp]: "a : {x:A. P(x)} <-> a:A & P(a)"
+by (unfold Collect_def, blast)
+
+lemma CollectI [intro!]: "[| a:A; P(a) |] ==> a : {x:A. P(x)}"
+by simp
+
+lemma CollectE [elim!]: "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> R |] ==> R"
+by simp
+
+lemma CollectD1: "a : {x:A. P(x)} ==> a:A"
+by (erule CollectE, assumption)
+
+lemma CollectD2: "a : {x:A. P(x)} ==> P(a)"
+by (erule CollectE, assumption)
+
+lemma Collect_cong [cong]:
+ "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |]
+ ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))"
+by (simp add: Collect_def)
+
+
+subsection{*Rules for Unions*}
+
+declare Union_iff [simp]
+
+(*The order of the premises presupposes that C is rigid; A may be flexible*)
+lemma UnionI [intro]: "[| B: C; A: B |] ==> A: Union(C)"
+by (simp, blast)
+
+lemma UnionE [elim!]: "[| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R"
+by (simp, blast)
+
+
+subsection{*Rules for Unions of families*}
+(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
+
+lemma UN_iff [simp]: "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))"
+by (simp add: Bex_def, blast)
+
+(*The order of the premises presupposes that A is rigid; b may be flexible*)
+lemma UN_I: "[| a: A; b: B(a) |] ==> b: (UN x:A. B(x))"
+by (simp, blast)
+
+
+lemma UN_E [elim!]:
+ "[| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R"
+by blast
+
+lemma UN_cong:
+ "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A. C(x)) = (UN x:B. D(x))"
+by simp
+
+
+(*No "Addcongs [UN_cong]" because UN is a combination of constants*)
+
+(* UN_E appears before UnionE so that it is tried first, to avoid expensive
+ calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: would enlarge
+ the search space.*)
+
+
+subsection{*Rules for Inter*}
+
+(*Not obviously useful for proving InterI, InterD, InterE*)
+lemma Inter_iff:
+ "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)"
+by (simp add: Inter_def Ball_def, blast)
+
+(* Intersection is well-behaved only if the family is non-empty! *)
+lemma InterI [intro!]:
+ "[| !!x. x: C ==> A: x; EX c. c:C |] ==> A : Inter(C)"
+by (simp add: Inter_iff)
+
+(*A "destruct" rule -- every B in C contains A as an element, but
+ A:B can hold when B:C does not! This rule is analogous to "spec". *)
+lemma InterD [elim]: "[| A : Inter(C); B : C |] ==> A : B"
+by (unfold Inter_def, blast)
+
+(*"Classical" elimination rule -- does not require exhibiting B:C *)
+lemma InterE [elim]:
+ "[| A : Inter(C); B~:C ==> R; A:B ==> R |] ==> R"
+by (simp add: Inter_def, blast)
+
+
+subsection{*Rules for Intersections of families*}
+(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
+
+lemma INT_iff: "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)"
+by (simp add: Inter_def, best)
+
+lemma INT_I:
+ "[| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x))"
+by blast
+
+lemma INT_E: "[| b : (INT x:A. B(x)); a: A |] ==> b : B(a)"
+by blast
+
+lemma INT_cong:
+ "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A. C(x)) = (INT x:B. D(x))"
+by simp
+
+(*No "Addcongs [INT_cong]" because INT is a combination of constants*)
+
+
+subsection{*Rules for the empty set*}
+
+(*The set {x:0.False} is empty; by foundation it equals 0
+ See Suppes, page 21.*)
+lemma not_mem_empty [simp]: "a ~: 0"
+apply (cut_tac foundation)
+apply (best dest: equalityD2)
+done
+
+lemmas emptyE [elim!] = not_mem_empty [THEN notE, standard]
+
+
+lemma empty_subsetI [simp]: "0 <= A"
+by blast
+
+lemma equals0I: "[| !!y. y:A ==> False |] ==> A=0"
+by blast
+
+lemma equals0D [dest]: "A=0 ==> a ~: A"
+by blast
+
+declare sym [THEN equals0D, dest]
+
+lemma not_emptyI: "a:A ==> A ~= 0"
+by blast
+
+lemma not_emptyE: "[| A ~= 0; !!x. x:A ==> R |] ==> R"
+by blast
+
+
+subsection{*Rules for Powersets*}
+
+lemma PowI: "A <= B ==> A : Pow(B)"
+by (erule Pow_iff [THEN iffD2])
+
+lemma PowD: "A : Pow(B) ==> A<=B"
+by (erule Pow_iff [THEN iffD1])
+
+declare Pow_iff [iff]
+
+lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *)
+lemmas Pow_top = subset_refl [THEN PowI] (* A : Pow(A) *)
+
+
+subsection{*Cantor's Theorem: There is no surjection from a set to its powerset.*}
+
+(*The search is undirected. Allowing redundant introduction rules may
+ make it diverge. Variable b represents ANY map, such as
+ (lam x:A.b(x)): A->Pow(A). *)
+lemma cantor: "EX S: Pow(A). ALL x:A. b(x) ~= S"
+by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
+
+ML
+{*
+val lam_def = thm "lam_def";
+val domain_def = thm "domain_def";
+val range_def = thm "range_def";
+val image_def = thm "image_def";
+val vimage_def = thm "vimage_def";
+val field_def = thm "field_def";
+val Inter_def = thm "Inter_def";
+val Ball_def = thm "Ball_def";
+val Bex_def = thm "Bex_def";
+
+val ballI = thm "ballI";
+val bspec = thm "bspec";
+val rev_ballE = thm "rev_ballE";
+val ballE = thm "ballE";
+val rev_bspec = thm "rev_bspec";
+val ball_triv = thm "ball_triv";
+val ball_cong = thm "ball_cong";
+val bexI = thm "bexI";
+val rev_bexI = thm "rev_bexI";
+val bexCI = thm "bexCI";
+val bexE = thm "bexE";
+val bex_triv = thm "bex_triv";
+val bex_cong = thm "bex_cong";
+val subst_elem = thm "subst_elem";
+val subsetI = thm "subsetI";
+val subsetD = thm "subsetD";
+val subsetCE = thm "subsetCE";
+val rev_subsetD = thm "rev_subsetD";
+val contra_subsetD = thm "contra_subsetD";
+val rev_contra_subsetD = thm "rev_contra_subsetD";
+val subset_refl = thm "subset_refl";
+val subset_trans = thm "subset_trans";
+val subset_iff = thm "subset_iff";
+val equalityI = thm "equalityI";
+val equality_iffI = thm "equality_iffI";
+val equalityD1 = thm "equalityD1";
+val equalityD2 = thm "equalityD2";
+val equalityE = thm "equalityE";
+val equalityCE = thm "equalityCE";
+val setup_induction = thm "setup_induction";
+val Replace_iff = thm "Replace_iff";
+val ReplaceI = thm "ReplaceI";
+val ReplaceE = thm "ReplaceE";
+val ReplaceE2 = thm "ReplaceE2";
+val Replace_cong = thm "Replace_cong";
+val RepFunI = thm "RepFunI";
+val RepFun_eqI = thm "RepFun_eqI";
+val RepFunE = thm "RepFunE";
+val RepFun_cong = thm "RepFun_cong";
+val RepFun_iff = thm "RepFun_iff";
+val triv_RepFun = thm "triv_RepFun";
+val separation = thm "separation";
+val CollectI = thm "CollectI";
+val CollectE = thm "CollectE";
+val CollectD1 = thm "CollectD1";
+val CollectD2 = thm "CollectD2";
+val Collect_cong = thm "Collect_cong";
+val UnionI = thm "UnionI";
+val UnionE = thm "UnionE";
+val UN_iff = thm "UN_iff";
+val UN_I = thm "UN_I";
+val UN_E = thm "UN_E";
+val UN_cong = thm "UN_cong";
+val Inter_iff = thm "Inter_iff";
+val InterI = thm "InterI";
+val InterD = thm "InterD";
+val InterE = thm "InterE";
+val INT_iff = thm "INT_iff";
+val INT_I = thm "INT_I";
+val INT_E = thm "INT_E";
+val INT_cong = thm "INT_cong";
+val PowI = thm "PowI";
+val PowD = thm "PowD";
+val Pow_bottom = thm "Pow_bottom";
+val Pow_top = thm "Pow_top";
+val not_mem_empty = thm "not_mem_empty";
+val emptyE = thm "emptyE";
+val empty_subsetI = thm "empty_subsetI";
+val equals0I = thm "equals0I";
+val equals0D = thm "equals0D";
+val not_emptyI = thm "not_emptyI";
+val not_emptyE = thm "not_emptyE";
+val cantor = thm "cantor";
+*}
+
+(*Functions for ML scripts*)
+ML
+{*
+(*Converts A<=B to x:A ==> x:B*)
+fun impOfSubs th = th RSN (2, rev_subsetD);
+
+(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
+val ball_tac = dtac bspec THEN' assume_tac
+*}
end
-
-ML
-
-(* Pattern-matching and 'Dependent' type operators *)
-
-val print_translation =
- [(*("split", split_tr'),*)
- ("Pi", dependent_tr' ("@PROD", "op ->")),
- ("Sigma", dependent_tr' ("@SUM", "op *"))];
--- a/src/ZF/simpdata.ML Wed Jan 15 16:44:21 2003 +0100
+++ b/src/ZF/simpdata.ML Wed Jan 15 16:45:32 2003 +0100
@@ -48,177 +48,9 @@
simpset_ref() :=
simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
addcongs [if_weak_cong]
- addsplits [split_if]
setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));
-(** Splitting IFs in the assumptions **)
-
-Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
-by (Simp_tac 1);
-qed "split_if_asm";
-
-bind_thms ("if_splits", [split_if, split_if_asm]);
-
-
-(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***)
-
-local
- (*For proving rewrite rules*)
- fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s
- (fn _ => [Simp_tac 1,
- ALLGOALS (blast_tac (claset() addSIs[equalityI]))]));
-
-in
-
-val ball_simps = map prover
- ["(ALL x:A. P(x) & Q) <-> (ALL x:A. P(x)) & (A=0 | Q)",
- "(ALL x:A. P & Q(x)) <-> (A=0 | P) & (ALL x:A. Q(x))",
- "(ALL x:A. P(x) | Q) <-> ((ALL x:A. P(x)) | Q)",
- "(ALL x:A. P | Q(x)) <-> (P | (ALL x:A. Q(x)))",
- "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
- "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
- "(ALL x:0.P(x)) <-> True",
- "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
- "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
- "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
- "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
- "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
- "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
-
-val ball_conj_distrib =
- prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
-
-val bex_simps = map prover
- ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
- "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
- "(EX x:A. P(x) | Q) <-> (EX x:A. P(x)) | (A~=0 & Q)",
- "(EX x:A. P | Q(x)) <-> (A~=0 & P) | (EX x:A. Q(x))",
- "(EX x:A. P --> Q(x)) <-> ((A=0 | P) --> (EX x:A. Q(x)))",
- "(EX x:A. P(x) --> Q) <-> ((ALL x:A. P(x)) --> (A~=0 & Q))",
- "(EX x:0.P(x)) <-> False",
- "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
- "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
- "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
- "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))",
- "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
- "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
-
-val bex_disj_distrib =
- prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
-
-val Rep_simps = map prover
- ["{x. y:0, R(x,y)} = 0", (*Replace*)
- "{x:0. P(x)} = 0", (*Collect*)
- "{x:A. P} = (if P then A else 0)",
- "RepFun(0,f) = 0", (*RepFun*)
- "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
- "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
-
-val misc_simps = map prover
- ["0 Un A = A", "A Un 0 = A",
- "0 Int A = 0", "A Int 0 = 0",
- "0 - A = 0", "A - 0 = A",
- "Union(0) = 0",
- "Union(cons(b,A)) = b Un Union(A)",
- "Inter({b}) = b"]
-
-
-val UN_simps = map prover
- ["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))",
- "(UN x:C. A(x) Un B) = (if C=0 then 0 else (UN x:C. A(x)) Un B)",
- "(UN x:C. A Un B(x)) = (if C=0 then 0 else A Un (UN x:C. B(x)))",
- "(UN x:C. A(x) Int B) = ((UN x:C. A(x)) Int B)",
- "(UN x:C. A Int B(x)) = (A Int (UN x:C. B(x)))",
- "(UN x:C. A(x) - B) = ((UN x:C. A(x)) - B)",
- "(UN x:C. A - B(x)) = (if C=0 then 0 else A - (INT x:C. B(x)))",
- "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))",
- "(UN z: (UN x:A. B(x)). C(z)) = (UN x:A. UN z: B(x). C(z))",
- "(UN x: RepFun(A,f). B(x)) = (UN a:A. B(f(a)))"];
-
-val INT_simps = map prover
- ["(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B",
- "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))",
- "(INT x:C. A(x) - B) = (INT x:C. A(x)) - B",
- "(INT x:C. A - B(x)) = (if C=0 then 0 else A - (UN x:C. B(x)))",
- "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))",
- "(INT x:C. A(x) Un B) = (if C=0 then 0 else (INT x:C. A(x)) Un B)",
- "(INT x:C. A Un B(x)) = (if C=0 then 0 else A Un (INT x:C. B(x)))"];
-
-(** The _extend_simps rules are oriented in the opposite direction, to
- pull UN and INT outwards. **)
-
-val UN_extend_simps = map prover
- ["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))",
- "(UN x:C. A(x)) Un B = (if C=0 then B else (UN x:C. A(x) Un B))",
- "A Un (UN x:C. B(x)) = (if C=0 then A else (UN x:C. A Un B(x)))",
- "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)",
- "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))",
- "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)",
- "A - (INT x:C. B(x)) = (if C=0 then A else (UN x:C. A - B(x)))",
- "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))",
- "(UN x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))",
- "(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"];
-
-val INT_extend_simps = map prover
- ["(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)",
- "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))",
- "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)",
- "A - (UN x:C. B(x)) = (if C=0 then A else (INT x:C. A - B(x)))",
- "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))",
- "(INT x:C. A(x)) Un B = (if C=0 then B else (INT x:C. A(x) Un B))",
- "A Un (INT x:C. B(x)) = (if C=0 then A else (INT x:C. A Un B(x)))"];
-
-end;
-
-bind_thms ("ball_simps", ball_simps);
-bind_thm ("ball_conj_distrib", ball_conj_distrib);
-bind_thms ("bex_simps", bex_simps);
-bind_thm ("bex_disj_distrib", bex_disj_distrib);
-bind_thms ("Rep_simps", Rep_simps);
-bind_thms ("misc_simps", misc_simps);
-
-Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
-
-bind_thms ("UN_simps", UN_simps);
-bind_thms ("INT_simps", INT_simps);
-
-Addsimps (UN_simps @ INT_simps);
-
-bind_thms ("UN_extend_simps", UN_extend_simps);
-bind_thms ("INT_extend_simps", INT_extend_simps);
-
-
-(** 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];
-
local
--- a/src/ZF/upair.thy Wed Jan 15 16:44:21 2003 +0100
+++ b/src/ZF/upair.thy Wed Jan 15 16:45:32 2003 +0100
@@ -16,13 +16,10 @@
files "Tools/typechk":
setup TypeCheck.setup
-declare atomize_ball [symmetric, rulify]
-(*belongs to theory ZF*)
-declare bspec [dest?]
-
-lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *)
-lemmas Pow_top = subset_refl [THEN PowI] (* A : Pow(A) *)
+lemma atomize_ball [symmetric, rulify]:
+ "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))"
+by (simp add: Ball_def atomize_all atomize_imp)
subsection{*Unordered Pairs: constant @{term Upair}*}
@@ -36,11 +33,8 @@
lemma UpairI2: "b : Upair(a,b)"
by simp
-lemma UpairE:
- "[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P"
-apply simp
-apply blast
-done
+lemma UpairE: "[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P"
+by (simp, blast)
subsection{*Rules for Binary Union, Defined via @{term Upair}*}
@@ -58,22 +52,15 @@
declare UnI1 [elim?] UnI2 [elim?]
lemma UnE [elim!]: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"
-apply simp
-apply blast
-done
+by (simp, blast)
(*Stronger version of the rule above*)
lemma UnE': "[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P"
-apply simp
-apply blast
-done
+by (simp, blast)
(*Classical introduction rule: no commitment to A vs B*)
lemma UnCI [intro!]: "(c ~: B ==> c : A) ==> c : A Un B"
-apply simp
-apply blast
-done
-
+by (simp, blast)
subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}
@@ -129,24 +116,17 @@
lemma consI2: "a : B ==> a : cons(b,B)"
by simp
-lemma consE [elim!]:
- "[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P"
-apply simp
-apply blast
-done
+lemma consE [elim!]: "[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P"
+by (simp, blast)
(*Stronger version of the rule above*)
lemma consE':
"[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P"
-apply simp
-apply blast
-done
+by (simp, blast)
(*Classical introduction rule*)
lemma consCI [intro!]: "(a~:B ==> a=b) ==> a: cons(b,B)"
-apply simp
-apply blast
-done
+by (simp, blast)
lemma cons_not_0 [simp]: "cons(a,B) ~= 0"
by (blast elim: equalityE)
@@ -213,6 +193,7 @@
lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a"
by blast
+
subsection{*Conditional Terms: @{text "if-then-else"}*}
lemma if_true [simp]: "(if True then a else b) = a"
@@ -240,10 +221,10 @@
lemma if_not_P: "~P ==> (if P then a else b) = b"
by (unfold if_def, blast)
-lemma split_if: "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
+lemma split_if [split]:
+ "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
(*no case_tac yet!*)
-apply (rule_tac P=Q in case_split_thm, simp_all)
-done
+by (rule_tac P=Q in case_split_thm, simp_all)
(** Rewrite rules for boolean case-splitting: faster than
addsplits[split_if]
@@ -259,11 +240,18 @@
(*Logically equivalent to split_if_mem2*)
lemma if_iff: "a: (if P then x else y) <-> P & a:x | ~P & a:y"
-by (simp split add: split_if)
+by simp
lemma if_type [TC]:
"[| P ==> a: A; ~P ==> b: A |] ==> (if P then a else b): A"
-by (simp split add: split_if)
+by simp
+
+(** Splitting IFs in the assumptions **)
+
+lemma split_if_asm: "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))"
+by simp
+
+lemmas if_splits = split_if split_if_asm
subsection{*Consequences of Foundation*}
@@ -333,10 +321,214 @@
lemmas succ_inject = succ_inject_iff [THEN iffD1, standard, dest!]
+
+subsection{*Miniscoping of the Bounded Universal Quantifier*}
+
+lemma ball_simps1:
+ "(ALL x:A. P(x) & Q) <-> (ALL x:A. P(x)) & (A=0 | Q)"
+ "(ALL x:A. P(x) | Q) <-> ((ALL x:A. P(x)) | Q)"
+ "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)"
+ "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"
+ "(ALL x:0.P(x)) <-> True"
+ "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))"
+ "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))"
+ "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))"
+ "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))"
+by blast+
+
+lemma ball_simps2:
+ "(ALL x:A. P & Q(x)) <-> (A=0 | P) & (ALL x:A. Q(x))"
+ "(ALL x:A. P | Q(x)) <-> (P | (ALL x:A. Q(x)))"
+ "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))"
+by blast+
+
+lemma ball_simps3:
+ "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"
+by blast+
+
+lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3
+
+lemma ball_conj_distrib:
+ "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"
+by blast
+
+
+subsection{*Miniscoping of the Bounded Existential Quantifier*}
+
+lemma bex_simps1:
+ "(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)"
+ "(EX x:A. P(x) | Q) <-> (EX x:A. P(x)) | (A~=0 & Q)"
+ "(EX x:A. P(x) --> Q) <-> ((ALL x:A. P(x)) --> (A~=0 & Q))"
+ "(EX x:0.P(x)) <-> False"
+ "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))"
+ "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))"
+ "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))"
+ "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y. P(x))"
+ "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"
+by blast+
+
+lemma bex_simps2:
+ "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))"
+ "(EX x:A. P | Q(x)) <-> (A~=0 & P) | (EX x:A. Q(x))"
+ "(EX x:A. P --> Q(x)) <-> ((A=0 | P) --> (EX x:A. Q(x)))"
+by blast+
+
+lemma bex_simps3:
+ "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"
+by blast
+
+lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3
+
+lemma bex_disj_distrib:
+ "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))"
+by blast
+
+
+(** One-point rule for bounded quantifiers: see HOL/Set.ML **)
+
+lemma bex_triv_one_point1 [simp]: "(EX x:A. x=a) <-> (a:A)"
+by blast
+
+lemma bex_triv_one_point2 [simp]: "(EX x:A. a=x) <-> (a:A)"
+by blast
+
+lemma bex_one_point1 [simp]: "(EX x:A. x=a & P(x)) <-> (a:A & P(a))"
+by blast
+
+lemma bex_one_point2 [simp]: "(EX x:A. a=x & P(x)) <-> (a:A & P(a))"
+by blast
+
+lemma ball_one_point1 [simp]: "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))"
+by blast
+
+lemma ball_one_point2 [simp]: "(ALL x:A. a=x --> P(x)) <-> (a:A --> P(a))"
+by blast
+
+
+subsection{*Miniscoping of the Replacement Operator*}
+
+text{*These cover both @{term Replace} and @{term Collect}*}
+lemma Rep_simps [simp]:
+ "{x. y:0, R(x,y)} = 0"
+ "{x:0. P(x)} = 0"
+ "{x:A. Q} = (if Q then A else 0)"
+ "RepFun(0,f) = 0"
+ "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))"
+ "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"
+by (simp_all, blast+)
+
+
+subsection{*Miniscoping of Unions*}
+
+lemma UN_simps1:
+ "(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))"
+ "(UN x:C. A(x) Un B') = (if C=0 then 0 else (UN x:C. A(x)) Un B')"
+ "(UN x:C. A' Un B(x)) = (if C=0 then 0 else A' Un (UN x:C. B(x)))"
+ "(UN x:C. A(x) Int B') = ((UN x:C. A(x)) Int B')"
+ "(UN x:C. A' Int B(x)) = (A' Int (UN x:C. B(x)))"
+ "(UN x:C. A(x) - B') = ((UN x:C. A(x)) - B')"
+ "(UN x:C. A' - B(x)) = (if C=0 then 0 else A' - (INT x:C. B(x)))"
+apply (simp_all add: Inter_def)
+apply (blast intro!: equalityI )+
+done
+
+lemma UN_simps2:
+ "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))"
+ "(UN z: (UN x:A. B(x)). C(z)) = (UN x:A. UN z: B(x). C(z))"
+ "(UN x: RepFun(A,f). B(x)) = (UN a:A. B(f(a)))"
+by blast+
+
+lemmas UN_simps [simp] = UN_simps1 UN_simps2
+
+text{*Opposite of miniscoping: pull the operator out*}
+
+lemma UN_extend_simps1:
+ "(UN x:C. A(x)) Un B = (if C=0 then B else (UN x:C. A(x) Un B))"
+ "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)"
+ "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)"
+apply simp_all
+apply blast+
+done
+
+lemma UN_extend_simps2:
+ "cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))"
+ "A Un (UN x:C. B(x)) = (if C=0 then A else (UN x:C. A Un B(x)))"
+ "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))"
+ "A - (INT x:C. B(x)) = (if C=0 then A else (UN x:C. A - B(x)))"
+ "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))"
+ "(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"
+apply (simp_all add: Inter_def)
+apply (blast intro!: equalityI)+
+done
+
+lemma UN_UN_extend:
+ "(UN x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))"
+by blast
+
+lemmas UN_extend_simps = UN_extend_simps1 UN_extend_simps2 UN_UN_extend
+
+
+subsection{*Miniscoping of Intersections*}
+
+lemma INT_simps1:
+ "(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B"
+ "(INT x:C. A(x) - B) = (INT x:C. A(x)) - B"
+ "(INT x:C. A(x) Un B) = (if C=0 then 0 else (INT x:C. A(x)) Un B)"
+by (simp_all add: Inter_def, blast+)
+
+lemma INT_simps2:
+ "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))"
+ "(INT x:C. A - B(x)) = (if C=0 then 0 else A - (UN x:C. B(x)))"
+ "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))"
+ "(INT x:C. A Un B(x)) = (if C=0 then 0 else A Un (INT x:C. B(x)))"
+apply (simp_all add: Inter_def)
+apply (blast intro!: equalityI)+
+done
+
+lemmas INT_simps [simp] = INT_simps1 INT_simps2
+
+text{*Opposite of miniscoping: pull the operator out*}
+
+
+lemma INT_extend_simps1:
+ "(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)"
+ "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)"
+ "(INT x:C. A(x)) Un B = (if C=0 then B else (INT x:C. A(x) Un B))"
+apply (simp_all add: Inter_def, blast+)
+done
+
+lemma INT_extend_simps2:
+ "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))"
+ "A - (UN x:C. B(x)) = (if C=0 then A else (INT x:C. A - B(x)))"
+ "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))"
+ "A Un (INT x:C. B(x)) = (if C=0 then A else (INT x:C. A Un B(x)))"
+apply (simp_all add: Inter_def)
+apply (blast intro!: equalityI)+
+done
+
+lemmas INT_extend_simps = INT_extend_simps1 INT_extend_simps2
+
+
+subsection{*Other simprules*}
+
+
+(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***)
+
+lemma misc_simps [simp]:
+ "0 Un A = A"
+ "A Un 0 = A"
+ "0 Int A = 0"
+ "A Int 0 = 0"
+ "0 - A = 0"
+ "A - 0 = A"
+ "Union(0) = 0"
+ "Union(cons(b,A)) = b Un Union(A)"
+ "Inter({b}) = b"
+by blast+
+
+
ML
{*
-val Pow_bottom = thm "Pow_bottom";
-val Pow_top = thm "Pow_top";
val Upair_iff = thm "Upair_iff";
val UpairI1 = thm "UpairI1";
val UpairI2 = thm "UpairI2";
@@ -403,6 +595,26 @@
val succ_inject = thm "succ_inject";
val split_ifs = thms "split_ifs";
+val ball_simps = thms "ball_simps";
+val bex_simps = thms "bex_simps";
+
+val ball_conj_distrib = thm "ball_conj_distrib";
+val bex_disj_distrib = thm "bex_disj_distrib";
+val bex_triv_one_point1 = thm "bex_triv_one_point1";
+val bex_triv_one_point2 = thm "bex_triv_one_point2";
+val bex_one_point1 = thm "bex_one_point1";
+val bex_one_point2 = thm "bex_one_point2";
+val ball_one_point1 = thm "ball_one_point1";
+val ball_one_point2 = thm "ball_one_point2";
+
+val Rep_simps = thms "Rep_simps";
+val misc_simps = thms "misc_simps";
+
+val UN_simps = thms "UN_simps";
+val INT_simps = thms "INT_simps";
+
+val UN_extend_simps = thms "UN_extend_simps";
+val INT_extend_simps = thms "INT_extend_simps";
*}
end