# HG changeset patch # User paulson # Date 1042645532 -3600 # Node ID af7b792713647d2e7ac39441b0d717c1b1bf695e # Parent 2a34dc5cf79e0a9998e99b0c307cc260ead231f4 more new-style theories diff -r 2a34dc5cf79e -r af7b79271364 src/ZF/Constructible/Wellorderings.thy --- 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 \ 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 diff -r 2a34dc5cf79e -r af7b79271364 src/ZF/Datatype.ML --- 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; diff -r 2a34dc5cf79e -r af7b79271364 src/ZF/IsaMakefile --- 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 diff -r 2a34dc5cf79e -r af7b79271364 src/ZF/Let.ML --- 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"; diff -r 2a34dc5cf79e -r af7b79271364 src/ZF/Let.thy --- 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 diff -r 2a34dc5cf79e -r af7b79271364 src/ZF/WF.thy --- 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) diff -r 2a34dc5cf79e -r af7b79271364 src/ZF/ZF.ML --- 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"; diff -r 2a34dc5cf79e -r af7b79271364 src/ZF/ZF.thy --- 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\*) "<=" :: "[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 "\\" 80) - "op Int" :: "[i, i] => i" (infixl "\\" 70) - "op Un" :: "[i, i] => i" (infixl "\\" 65) - "op ->" :: "[i, i] => i" (infixr "\\" 60) - "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]) - "@UNION" :: "[pttrn, i, i] => i" ("(3\\_\\_./ _)" 10) - "@INTER" :: "[pttrn, i, i] => i" ("(3\\_\\_./ _)" 10) - Union :: "i =>i" ("\\_" [90] 90) - Inter :: "i =>i" ("\\_" [90] 90) - "@PROD" :: "[pttrn, i, i] => i" ("(3\\_\\_./ _)" 10) - "@SUM" :: "[pttrn, i, i] => i" ("(3\\_\\_./ _)" 10) - "@lam" :: "[pttrn, i, i] => i" ("(3\\_\\_./ _)" 10) - "@Ball" :: "[pttrn, i, o] => o" ("(3\\_\\_./ _)" 10) - "@Bex" :: "[pttrn, i, o] => o" ("(3\\_\\_./ _)" 10) - "@Tuple" :: "[i, is] => i" ("\\(_,/ _)\\") - "@pattern" :: "patterns => pttrn" ("\\_\\") + "op *" :: "[i, i] => i" (infixr "\" 80) + "op Int" :: "[i, i] => i" (infixl "\" 70) + "op Un" :: "[i, i] => i" (infixl "\" 65) + "op ->" :: "[i, i] => i" (infixr "\" 60) + "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]) + "@UNION" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) + "@INTER" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) + Union :: "i =>i" ("\_" [90] 90) + Inter :: "i =>i" ("\_" [90] 90) + "@PROD" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) + "@SUM" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) + "@lam" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) + "@Ball" :: "[pttrn, i, o] => o" ("(3\_\_./ _)" 10) + "@Bex" :: "[pttrn, i, o] => o" ("(3\_\_./ _)" 10) + "@Tuple" :: "[i, is] => i" ("\(_,/ _)\") + "@pattern" :: "patterns => pttrn" ("\_\") syntax (HTML output) - "op *" :: "[i, i] => i" (infixr "\\" 80) + "op *" :: "[i, i] => i" (infixr "\" 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,a}, {a,b}}" - fst_def "fst(p) == THE a. EX b. p=" - snd_def "snd(p) == THE b. EX a. p=" - split_def "split(c) == %p. c(fst(p), snd(p))" - Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {}" + Pair_def: " == {{a,a}, {a,b}}" + fst_def: "fst(p) == THE a. EX b. p=" + snd_def: "snd(p) == THE b. EX a. p=" + split_def: "split(c) == %p. c(fst(p), snd(p))" + Sigma_def: "Sigma(A,B) == UN x:A. UN y:B(x). {}" (* Operations on relations *) (*converse of relation r, inverse of function*) - converse_def "converse(r) == {z. w:r, EX x y. w= & z=}" + converse_def: "converse(r) == {z. w:r, EX x y. w= & z=}" - domain_def "domain(r) == {x. w:r, EX y. w=}" - 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 = " - function_def "function(r) == + domain_def: "domain(r) == {x. w:r, EX y. w=}" + 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 = " + function_def: "function(r) == ALL x y. :r --> (ALL y'. :r --> y=y')" - image_def "r `` A == {y : range(r) . EX x:A. : r}" - vimage_def "r -`` A == converse(r)``A" + image_def: "r `` A == {y : range(r) . EX x:A. : r}" + vimage_def: "r -`` A == converse(r)``A" (* Abstraction, application and Cartesian product of a family of sets *) - lam_def "Lambda(A,b) == { . 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: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 = }" + restrict_def: "restrict(r,A) == {z : r. EX x:A. EX y. z = }" + +(* 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 *"))]; diff -r 2a34dc5cf79e -r af7b79271364 src/ZF/simpdata.ML --- 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 diff -r 2a34dc5cf79e -r af7b79271364 src/ZF/upair.thy --- 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