# HG changeset patch # User paulson # Date 1024820053 -7200 # Node ID bb5f4faea1f39f510d7798e1147ed5e8699c2aae # Parent f599984ec4c2a72f0541ccc50bdf6fa5118a9c14 conversion of Sum, pair to Isar script diff -r f599984ec4c2 -r bb5f4faea1f3 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Sat Jun 22 18:28:46 2002 +0200 +++ b/src/ZF/IsaMakefile Sun Jun 23 10:14:13 2002 +0200 @@ -39,13 +39,13 @@ Integ/twos_compl.ML Let.ML Let.thy List.ML 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.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Sum.ML \ + QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML \ Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \ 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 Update.thy \ WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \ - ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML \ + ind_syntax.ML mono.ML mono.thy pair.thy simpdata.ML \ subset.ML subset.thy thy_syntax.ML upair.ML upair.thy @$(ISATOOL) usedir -b -r $(OUT)/FOL ZF diff -r f599984ec4c2 -r bb5f4faea1f3 src/ZF/Sum.ML --- a/src/ZF/Sum.ML Sat Jun 22 18:28:46 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,211 +0,0 @@ -(* Title: ZF/Sum - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Disjoint sums in Zermelo-Fraenkel Set Theory -*) - -(*** Rules for the Part primitive ***) - -Goalw [Part_def] - "a : Part(A,h) <-> a:A & (EX y. a=h(y))"; -by (rtac separation 1); -qed "Part_iff"; - -Goalw [Part_def] - "[| a : A; a=h(b) |] ==> a : Part(A,h)"; -by (Blast_tac 1); -qed "Part_eqI"; - -bind_thm ("PartI", refl RSN (2,Part_eqI)); - -val major::prems = Goalw [Part_def] - "[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \ -\ |] ==> P"; -by (rtac (major RS CollectE) 1); -by (etac exE 1); -by (REPEAT (ares_tac prems 1)); -qed "PartE"; - -AddIs [Part_eqI]; -AddSEs [PartE]; - -Goalw [Part_def] "Part(A,h) <= A"; -by (rtac Collect_subset 1); -qed "Part_subset"; - - -(*** Rules for Disjoint Sums ***) - -bind_thms ("sum_defs", [sum_def,Inl_def,Inr_def,case_def]); - -Goalw (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)"; -by (Blast_tac 1); -qed "Sigma_bool"; - -(** Introduction rules for the injections **) - -Goalw sum_defs "a : A ==> Inl(a) : A+B"; -by (Blast_tac 1); -qed "InlI"; - -Goalw sum_defs "b : B ==> Inr(b) : A+B"; -by (Blast_tac 1); -qed "InrI"; - -(** Elimination rules **) - -val major::prems = Goalw sum_defs - "[| u: A+B; \ -\ !!x. [| x:A; u=Inl(x) |] ==> P; \ -\ !!y. [| y:B; u=Inr(y) |] ==> P \ -\ |] ==> P"; -by (rtac (major RS UnE) 1); -by (REPEAT (rtac refl 1 - ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1)); -qed "sumE"; - -(** Injection and freeness equivalences, for rewriting **) - -Goalw sum_defs "Inl(a)=Inl(b) <-> a=b"; -by (Simp_tac 1); -qed "Inl_iff"; - -Goalw sum_defs "Inr(a)=Inr(b) <-> a=b"; -by (Simp_tac 1); -qed "Inr_iff"; - -Goalw sum_defs "Inl(a)=Inr(b) <-> False"; -by (Simp_tac 1); -qed "Inl_Inr_iff"; - -Goalw sum_defs "Inr(b)=Inl(a) <-> False"; -by (Simp_tac 1); -qed "Inr_Inl_iff"; - -Goalw sum_defs "0+0 = 0"; -by (Simp_tac 1); -qed "sum_empty"; - -(*Injection and freeness rules*) - -bind_thm ("Inl_inject", (Inl_iff RS iffD1)); -bind_thm ("Inr_inject", (Inr_iff RS iffD1)); -bind_thm ("Inl_neq_Inr", (Inl_Inr_iff RS iffD1 RS FalseE)); -bind_thm ("Inr_neq_Inl", (Inr_Inl_iff RS iffD1 RS FalseE)); - -AddSIs [InlI, InrI]; -AddSEs [sumE, Inl_neq_Inr, Inr_neq_Inl]; -AddSDs [Inl_inject, Inr_inject]; - -Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty]; -AddTCs [InlI, InrI]; - -Goal "Inl(a): A+B ==> a: A"; -by (Blast_tac 1); -qed "InlD"; - -Goal "Inr(b): A+B ==> b: B"; -by (Blast_tac 1); -qed "InrD"; - -Goal "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"; -by (Blast_tac 1); -qed "sum_iff"; - -Goal "A+B <= C+D <-> A<=C & B<=D"; -by (Blast_tac 1); -qed "sum_subset_iff"; - -Goal "A+B = C+D <-> A=C & B=D"; -by (simp_tac (simpset() addsimps [extension,sum_subset_iff]) 1); -by (Blast_tac 1); -qed "sum_equal_iff"; - -Goalw [sum_def] "A+A = 2*A"; -by (Blast_tac 1); -qed "sum_eq_2_times"; - - -(*** Eliminator -- case ***) - -Goalw sum_defs "case(c, d, Inl(a)) = c(a)"; -by (Simp_tac 1); -qed "case_Inl"; - -Goalw sum_defs "case(c, d, Inr(b)) = d(b)"; -by (Simp_tac 1); -qed "case_Inr"; - -Addsimps [case_Inl, case_Inr]; - -val major::prems = Goal - "[| u: A+B; \ -\ !!x. x: A ==> c(x): C(Inl(x)); \ -\ !!y. y: B ==> d(y): C(Inr(y)) \ -\ |] ==> case(c,d,u) : C(u)"; -by (rtac (major RS sumE) 1); -by (ALLGOALS (etac ssubst)); -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); -qed "case_type"; -AddTCs [case_type]; - -Goal "u: A+B ==> \ -\ R(case(c,d,u)) <-> \ -\ ((ALL x:A. u = Inl(x) --> R(c(x))) & \ -\ (ALL y:B. u = Inr(y) --> R(d(y))))"; -by Auto_tac; -qed "expand_case"; - -val major::prems = Goal - "[| z: A+B; \ -\ !!x. x:A ==> c(x)=c'(x); \ -\ !!y. y:B ==> d(y)=d'(y) \ -\ |] ==> case(c,d,z) = case(c',d',z)"; -by (resolve_tac [major RS sumE] 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); -qed "case_cong"; - -Goal "z: A+B ==> \ -\ case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \ -\ case(%x. c(c'(x)), %y. d(d'(y)), z)"; -by Auto_tac; -qed "case_case"; - - -(*** More rules for Part(A,h) ***) - -Goal "A<=B ==> Part(A,h)<=Part(B,h)"; -by (Blast_tac 1); -qed "Part_mono"; - -Goal "Part(Collect(A,P), h) = Collect(Part(A,h), P)"; -by (Blast_tac 1); -qed "Part_Collect"; - -bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE); - -Goal "Part(A+B,Inl) = {Inl(x). x: A}"; -by (Blast_tac 1); -qed "Part_Inl"; - -Goal "Part(A+B,Inr) = {Inr(y). y: B}"; -by (Blast_tac 1); -qed "Part_Inr"; - -Goalw [Part_def] "a : Part(A,h) ==> a : A"; -by (etac CollectD1 1); -qed "PartD1"; - -Goal "Part(A,%x. x) = A"; -by (Blast_tac 1); -qed "Part_id"; - -Goal "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}"; -by (Blast_tac 1); -qed "Part_Inr2"; - -Goal "C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"; -by (Blast_tac 1); -qed "Part_sum_equality"; diff -r f599984ec4c2 -r bb5f4faea1f3 src/ZF/Sum.thy --- a/src/ZF/Sum.thy Sat Jun 22 18:28:46 2002 +0200 +++ b/src/ZF/Sum.thy Sun Jun 23 10:14:13 2002 +0200 @@ -7,25 +7,270 @@ "Part" primitive for simultaneous recursive type definitions *) -Sum = Bool + equalities + +theory Sum = Bool + equalities: global -consts - "+" :: "[i,i]=>i" (infixr 65) - Inl :: "i=>i" - Inr :: "i=>i" - "case" :: "[i=>i, i=>i, i]=>i" - Part :: "[i,i=>i] => i" +constdefs + sum :: "[i,i]=>i" (infixr "+" 65) + "A+B == {0}*A Un {1}*B" + + Inl :: "i=>i" + "Inl(a) == <0,a>" + + Inr :: "i=>i" + "Inr(b) == <1,b>" + + "case" :: "[i=>i, i=>i, i]=>i" + "case(c,d) == (%. cond(y, d(z), c(z)))" + + (*operator for selecting out the various summands*) + Part :: "[i,i=>i] => i" + "Part(A,h) == {x: A. EX z. x = h(z)}" local -defs - sum_def "A+B == {0}*A Un {1}*B" - Inl_def "Inl(a) == <0,a>" - Inr_def "Inr(b) == <1,b>" - case_def "case(c,d) == (%. cond(y, d(z), c(z)))" +(*** Rules for the Part primitive ***) + +lemma Part_iff: + "a : Part(A,h) <-> a:A & (EX y. a=h(y))" +apply (unfold Part_def) +apply (rule separation) +done + +lemma Part_eqI [intro]: + "[| a : A; a=h(b) |] ==> a : Part(A,h)" +apply (unfold Part_def) +apply blast +done + +lemmas PartI = refl [THEN [2] Part_eqI] + +lemma PartE [elim!]: + "[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P + |] ==> P" +apply (unfold Part_def) +apply blast +done + +lemma Part_subset: "Part(A,h) <= A" +apply (unfold Part_def) +apply (rule Collect_subset) +done + + +(*** Rules for Disjoint Sums ***) + +lemmas sum_defs = sum_def Inl_def Inr_def case_def + +lemma Sigma_bool: "Sigma(bool,C) = C(0) + C(1)" +apply (unfold bool_def sum_def) +apply blast +done + +(** Introduction rules for the injections **) + +lemma InlI [intro!,simp,TC]: "a : A ==> Inl(a) : A+B" +apply (unfold sum_defs) +apply blast +done + +lemma InrI [intro!,simp,TC]: "b : B ==> Inr(b) : A+B" +apply (unfold sum_defs) +apply blast +done + +(** Elimination rules **) + +lemma sumE [elim!]: + "[| u: A+B; + !!x. [| x:A; u=Inl(x) |] ==> P; + !!y. [| y:B; u=Inr(y) |] ==> P + |] ==> P" +apply (unfold sum_defs) +apply (blast intro: elim:); +done + +(** Injection and freeness equivalences, for rewriting **) + +lemma Inl_iff [iff]: "Inl(a)=Inl(b) <-> a=b" +apply (simp add: sum_defs) +done + +lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b" +apply (simp add: sum_defs) +done + +lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) <-> False" +apply (simp add: sum_defs) +done + +lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) <-> False" +apply (simp add: sum_defs) +done + +lemma sum_empty [simp]: "0+0 = 0" +apply (simp add: sum_defs) +done + +(*Injection and freeness rules*) + +lemmas Inl_inject = Inl_iff [THEN iffD1, standard] +lemmas Inr_inject = Inr_iff [THEN iffD1, standard] +lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE] +lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE] + + +lemma InlD: "Inl(a): A+B ==> a: A" +apply blast +done + +lemma InrD: "Inr(b): A+B ==> b: B" +apply blast +done + +lemma sum_iff: "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))" +apply blast +done + +lemma sum_subset_iff: "A+B <= C+D <-> A<=C & B<=D" +apply blast +done + +lemma sum_equal_iff: "A+B = C+D <-> A=C & B=D" +apply (simp add: extension sum_subset_iff) +apply blast +done + +lemma sum_eq_2_times: "A+A = 2*A" +apply (simp add: sum_def) +apply blast +done + + +(*** Eliminator -- case ***) - (*operator for selecting out the various summands*) - Part_def "Part(A,h) == {x: A. EX z. x = h(z)}" +lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)" +apply (simp add: sum_defs) +done + +lemma case_Inr [simp]: "case(c, d, Inr(b)) = d(b)" +apply (simp add: sum_defs) +done + +lemma case_type [TC]: + "[| u: A+B; + !!x. x: A ==> c(x): C(Inl(x)); + !!y. y: B ==> d(y): C(Inr(y)) + |] ==> case(c,d,u) : C(u)" +apply (auto ); +done + +lemma expand_case: "u: A+B ==> + R(case(c,d,u)) <-> + ((ALL x:A. u = Inl(x) --> R(c(x))) & + (ALL y:B. u = Inr(y) --> R(d(y))))" +by auto + +lemma case_cong: + "[| z: A+B; + !!x. x:A ==> c(x)=c'(x); + !!y. y:B ==> d(y)=d'(y) + |] ==> case(c,d,z) = case(c',d',z)" +by (auto ); + +lemma case_case: "z: A+B ==> + case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = + case(%x. c(c'(x)), %y. d(d'(y)), z)" +by auto + + +(*** More rules for Part(A,h) ***) + +lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)" +apply blast +done + +lemma Part_Collect: "Part(Collect(A,P), h) = Collect(Part(A,h), P)" +apply blast +done + +lemmas Part_CollectE = + Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE, standard] + +lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x: A}" +apply blast +done + +lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y: B}" +apply blast +done + +lemma PartD1: "a : Part(A,h) ==> a : A" +apply (simp add: Part_def) +done + +lemma Part_id: "Part(A,%x. x) = A" +apply blast +done + +lemma Part_Inr2: "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}" +apply blast +done + +lemma Part_sum_equality: "C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C" +apply blast +done + +ML +{* +val sum_def = thm "sum_def"; +val Inl_def = thm "Inl_def"; +val Inr_def = thm "Inr_def"; +val sum_defs = thms "sum_defs"; + +val Part_iff = thm "Part_iff"; +val Part_eqI = thm "Part_eqI"; +val PartI = thm "PartI"; +val PartE = thm "PartE"; +val Part_subset = thm "Part_subset"; +val Sigma_bool = thm "Sigma_bool"; +val InlI = thm "InlI"; +val InrI = thm "InrI"; +val sumE = thm "sumE"; +val Inl_iff = thm "Inl_iff"; +val Inr_iff = thm "Inr_iff"; +val Inl_Inr_iff = thm "Inl_Inr_iff"; +val Inr_Inl_iff = thm "Inr_Inl_iff"; +val sum_empty = thm "sum_empty"; +val Inl_inject = thm "Inl_inject"; +val Inr_inject = thm "Inr_inject"; +val Inl_neq_Inr = thm "Inl_neq_Inr"; +val Inr_neq_Inl = thm "Inr_neq_Inl"; +val InlD = thm "InlD"; +val InrD = thm "InrD"; +val sum_iff = thm "sum_iff"; +val sum_subset_iff = thm "sum_subset_iff"; +val sum_equal_iff = thm "sum_equal_iff"; +val sum_eq_2_times = thm "sum_eq_2_times"; +val case_Inl = thm "case_Inl"; +val case_Inr = thm "case_Inr"; +val case_type = thm "case_type"; +val expand_case = thm "expand_case"; +val case_cong = thm "case_cong"; +val case_case = thm "case_case"; +val Part_mono = thm "Part_mono"; +val Part_Collect = thm "Part_Collect"; +val Part_CollectE = thm "Part_CollectE"; +val Part_Inl = thm "Part_Inl"; +val Part_Inr = thm "Part_Inr"; +val PartD1 = thm "PartD1"; +val Part_id = thm "Part_id"; +val Part_Inr2 = thm "Part_Inr2"; +val Part_sum_equality = thm "Part_sum_equality"; + +*} + + + end diff -r f599984ec4c2 -r bb5f4faea1f3 src/ZF/Trancl.thy --- a/src/ZF/Trancl.thy Sat Jun 22 18:28:46 2002 +0200 +++ b/src/ZF/Trancl.thy Sun Jun 23 10:14:13 2002 +0200 @@ -47,64 +47,53 @@ lemma irreflI: "[| !!x. x:A ==> ~: r |] ==> irrefl(A,r)" -by (simp add: irrefl_def); +by (simp add: irrefl_def) lemma symI: "[| irrefl(A,r); x:A |] ==> ~: r" -apply (simp add: irrefl_def) -done +by (simp add: irrefl_def) subsubsection{*symmetry*} lemma symI: "[| !!x y.: r ==> : r |] ==> sym(r)" -apply (unfold sym_def); -apply (blast intro: elim:); +apply (unfold sym_def, blast) done lemma antisymI: "[| sym(r); : r |] ==> : r" -apply (unfold sym_def) -apply blast -done +by (unfold sym_def, blast) subsubsection{*antisymmetry*} lemma antisymI: "[| !!x y.[| : r; : r |] ==> x=y |] ==> antisym(r)" -apply (simp add: antisym_def) -apply (blast intro: elim:); +apply (simp add: antisym_def, blast) done lemma antisymE: "[| antisym(r); : r; : r |] ==> x=y" -apply (simp add: antisym_def) -apply blast -done +by (simp add: antisym_def, blast) subsubsection{*transitivity*} lemma transD: "[| trans(r); :r; :r |] ==> :r" -apply (unfold trans_def) -apply blast -done +by (unfold trans_def, blast) lemma trans_onD: "[| trans[A](r); :r; :r; a:A; b:A; c:A |] ==> :r" -apply (unfold trans_on_def) -apply blast +apply (unfold trans_on_def, blast) done subsection{*Transitive closure of a relation*} lemma rtrancl_bnd_mono: "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))" -apply (rule bnd_monoI) -apply (blast intro: elim:)+ +apply (rule bnd_monoI, blast+) done lemma rtrancl_mono: "r<=s ==> r^* <= s^*" apply (unfold rtrancl_def) apply (rule lfp_mono) apply (rule rtrancl_bnd_mono)+ -apply (blast intro: elim:); +apply blast done (* r^* = id(field(r)) Un ( r O r^* ) *) @@ -125,25 +114,20 @@ (*Closure under composition with r *) lemma rtrancl_into_rtrancl: "[| : r^*; : r |] ==> : r^*" apply (rule rtrancl_unfold [THEN ssubst]) -apply (rule compI [THEN UnI2]) -apply assumption +apply (rule compI [THEN UnI2], assumption) apply assumption done (*rtrancl of r contains all pairs in r *) lemma r_into_rtrancl: " : r ==> : r^*" -apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl]) -apply (blast intro: elim:)+ -done +by (rule rtrancl_refl [THEN rtrancl_into_rtrancl], blast+) (*The premise ensures that r consists entirely of pairs*) lemma r_subset_rtrancl: "r <= Sigma(A,B) ==> r <= r^*" -apply (blast intro: r_into_rtrancl) -done +by (blast intro: r_into_rtrancl) lemma rtrancl_field: "field(r^*) = field(r)" -apply (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD]) -done +by (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD]) (** standard induction rule **) @@ -153,8 +137,7 @@ !!x. x: field(r) ==> P(); !!x y z.[| P(); : r^*; : r |] ==> P() |] ==> P()" -apply (erule def_induct [OF rtrancl_def rtrancl_bnd_mono]) -apply (blast intro: elim:); +apply (erule def_induct [OF rtrancl_def rtrancl_bnd_mono], blast) done (*nice induction rule. @@ -170,16 +153,14 @@ (*now solve first subgoal: this formula is sufficient*) apply (erule spec [THEN mp], rule refl) (*now do the induction*) -apply (erule rtrancl_full_induct) -apply (blast)+ +apply (erule rtrancl_full_induct, blast+) done (*transitivity of transitive closure!! -- by induction.*) lemma trans_rtrancl: "trans(r^*)" apply (unfold trans_def) apply (intro allI impI) -apply (erule_tac b = "z" in rtrancl_induct) -apply assumption; +apply (erule_tac b = "z" in rtrancl_induct, assumption) apply (blast intro: rtrancl_into_rtrancl) done @@ -192,9 +173,8 @@ ==> P" apply (subgoal_tac "a = b | (EX y. : r^* & : r) ") (*see HOL/trancl*) -apply (blast intro: elim:); -apply (erule rtrancl_induct) -apply (blast intro: elim:)+ +apply blast +apply (erule rtrancl_induct, blast+) done @@ -224,14 +204,11 @@ (*The premise ensures that r consists entirely of pairs*) lemma r_subset_trancl: "r <= Sigma(A,B) ==> r <= r^+" -apply (blast intro: r_into_trancl) -done +by (blast intro: r_into_trancl) (*intro rule by definition: from r^* and r *) lemma rtrancl_into_trancl1: "[| : r^*; : r |] ==> : r^+" -apply (unfold trancl_def) -apply blast -done +by (unfold trancl_def, blast) (*intro rule from r and r^* *) lemma rtrancl_into_trancl2: @@ -264,7 +241,7 @@ !!y.[| : r^+; : r |] ==> P |] ==> P" apply (subgoal_tac " : r | (EX y. : r^+ & : r) ") -apply (blast intro: elim:); +apply blast apply (rule compEpair) apply (unfold trancl_def, assumption) apply (erule rtranclE) @@ -283,14 +260,12 @@ (** Suggested by Sidi Ould Ehmety **) lemma rtrancl_idemp [simp]: "(r^*)^* = r^*" -apply (rule equalityI) -apply auto +apply (rule equalityI, auto) prefer 2 apply (frule rtrancl_type [THEN subsetD]) - apply (blast intro: r_into_rtrancl elim:); + apply (blast intro: r_into_rtrancl ) txt{*converse direction*} -apply (frule rtrancl_type [THEN subsetD]) -apply (clarify ); +apply (frule rtrancl_type [THEN subsetD], clarify) apply (erule rtrancl_induct) apply (simp add: rtrancl_refl rtrancl_field) apply (blast intro: rtrancl_trans) @@ -298,8 +273,7 @@ lemma rtrancl_subset: "[| R <= S; S <= R^* |] ==> S^* = R^*" apply (drule rtrancl_mono) -apply (drule rtrancl_mono) -apply simp_all +apply (drule rtrancl_mono, simp_all) apply blast done diff -r f599984ec4c2 -r bb5f4faea1f3 src/ZF/pair.ML --- a/src/ZF/pair.ML Sat Jun 22 18:28:46 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,191 +0,0 @@ -(* Title: ZF/pair - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Ordered pairs in Zermelo-Fraenkel Set Theory -*) - -(** Lemmas for showing that uniquely determines a and b **) - -Goal "{a} = {b} <-> a=b"; -by (resolve_tac [extension RS iff_trans] 1); -by (Blast_tac 1) ; -qed "singleton_eq_iff"; -AddIffs [singleton_eq_iff]; - -Goal "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"; -by (resolve_tac [extension RS iff_trans] 1); -by (Blast_tac 1) ; -qed "doubleton_eq_iff"; - -Goalw [Pair_def] " = <-> a=c & b=d"; -by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1); -by (Blast_tac 1) ; -qed "Pair_iff"; - -Addsimps [Pair_iff]; - -bind_thm ("Pair_inject", Pair_iff RS iffD1 RS conjE); - -AddSEs [Pair_inject]; - -bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1); -bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2); - -Goalw [Pair_def] " ~= 0"; -by (blast_tac (claset() addEs [equalityE]) 1) ; -qed "Pair_not_0"; - -bind_thm ("Pair_neq_0", Pair_not_0 RS notE); - -AddSEs [Pair_neq_0, sym RS Pair_neq_0]; - -Goalw [Pair_def] "=a ==> P"; -by (rtac (consI1 RS mem_asym RS FalseE) 1); -by (etac subst 1); -by (rtac consI1 1) ; -qed "Pair_neq_fst"; - -Goalw [Pair_def] "=b ==> P"; -by (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1); -by (etac subst 1); -by (rtac (consI1 RS consI2) 1) ; -qed "Pair_neq_snd"; - - -(*** Sigma: Disjoint union of a family of sets - Generalizes Cartesian product ***) - -Goalw [Sigma_def] ": Sigma(A,B) <-> a:A & b:B(a)"; -by (Blast_tac 1) ; -qed "Sigma_iff"; - -Addsimps [Sigma_iff]; - -Goal "[| a:A; b:B(a) |] ==> : Sigma(A,B)"; -by (Asm_simp_tac 1); -qed "SigmaI"; - -AddTCs [SigmaI]; - -bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1); -bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2); - -(*The general elimination rule*) -val major::prems= Goalw [Sigma_def] - "[| c: Sigma(A,B); \ -\ !!x y.[| x:A; y:B(x); c= |] ==> P \ -\ |] ==> P"; -by (cut_facts_tac [major] 1); -by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ; -qed "SigmaE"; - -val [major,minor]= Goal - "[| : Sigma(A,B); \ -\ [| a:A; b:B(a) |] ==> P \ -\ |] ==> P"; -by (rtac minor 1); -by (rtac (major RS SigmaD1) 1); -by (rtac (major RS SigmaD2) 1) ; -qed "SigmaE2"; - -val prems= Goalw [Sigma_def] - "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ -\ Sigma(A,B) = Sigma(A',B')"; -by (simp_tac (simpset() addsimps prems) 1) ; -qed "Sigma_cong"; - - -(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause - flex-flex pairs and the "Check your prover" error. Most - Sigmas and Pis are abbreviated as * or -> *) - -AddSIs [SigmaI]; -AddSEs [SigmaE2, SigmaE]; - -Goal "Sigma(0,B) = 0"; -by (Blast_tac 1) ; -qed "Sigma_empty1"; - -Goal "A*0 = 0"; -by (Blast_tac 1) ; -qed "Sigma_empty2"; - -Addsimps [Sigma_empty1, Sigma_empty2]; - -Goal "A*B=0 <-> A=0 | B=0"; -by (Blast_tac 1); -qed "Sigma_empty_iff"; - - -(*** Projections: fst, snd ***) - -Goalw [fst_def] "fst() = a"; -by (Blast_tac 1) ; -qed "fst_conv"; - -Goalw [snd_def] "snd() = b"; -by (Blast_tac 1) ; -qed "snd_conv"; - -Addsimps [fst_conv,snd_conv]; - -Goal "p:Sigma(A,B) ==> fst(p) : A"; -by (Auto_tac) ; -qed "fst_type"; -AddTCs [fst_type]; - -Goal "p:Sigma(A,B) ==> snd(p) : B(fst(p))"; -by (Auto_tac) ; -qed "snd_type"; -AddTCs [snd_type]; - -Goal "a: Sigma(A,B) ==> = a"; -by (Auto_tac) ; -qed "Pair_fst_snd_eq"; - - -(*** Eliminator - split ***) - -(*A META-equality, so that it applies to higher types as well...*) -Goalw [split_def] "split(%x y. c(x,y), ) == c(a,b)"; -by (Simp_tac 1); -qed "split"; -Addsimps [split]; - -val major::prems= Goal - "[| p:Sigma(A,B); \ -\ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C() \ -\ |] ==> split(%x y. c(x,y), p) : C(p)"; -by (rtac (major RS SigmaE) 1); -by (asm_simp_tac (simpset() addsimps prems) 1); -qed "split_type"; -AddTCs [split_type]; - -Goalw [split_def] - "u: A*B ==> \ -\ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = --> R(c(x,y)))"; -by Auto_tac; -qed "expand_split"; - - -(*** split for predicates: result type o ***) - -Goalw [split_def] "R(a,b) ==> split(R, )"; -by (Asm_simp_tac 1); -qed "splitI"; - -val major::sigma::prems = Goalw [split_def] - "[| split(R,z); z:Sigma(A,B); \ -\ !!x y. [| z = ; R(x,y) |] ==> P \ -\ |] ==> P"; -by (rtac (sigma RS SigmaE) 1); -by (cut_facts_tac [major] 1); -by (REPEAT (ares_tac prems 1)); -by (Asm_full_simp_tac 1); -qed "splitE"; - -Goalw [split_def] "split(R,) ==> R(a,b)"; -by (Full_simp_tac 1); -qed "splitD"; diff -r f599984ec4c2 -r bb5f4faea1f3 src/ZF/pair.thy --- a/src/ZF/pair.thy Sat Jun 22 18:28:46 2002 +0200 +++ b/src/ZF/pair.thy Sun Jun 23 10:14:13 2002 +0200 @@ -1,5 +1,189 @@ +(* Title: ZF/pair + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Ordered pairs in Zermelo-Fraenkel Set Theory +*) + theory pair = upair files "simpdata.ML": + +(** Lemmas for showing that uniquely determines a and b **) + +lemma singleton_eq_iff [iff]: "{a} = {b} <-> a=b" +by (rule extension [THEN iff_trans], blast) + +lemma doubleton_eq_iff: "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)" +by (rule extension [THEN iff_trans], blast) + +lemma Pair_iff [simp]: " = <-> a=c & b=d" +by (simp add: Pair_def doubleton_eq_iff, blast) + +lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, standard, elim!] + +lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1, standard] +lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2, standard] + +lemma Pair_not_0: " ~= 0" +apply (unfold Pair_def) +apply (blast elim: equalityE) +done + +lemmas Pair_neq_0 = Pair_not_0 [THEN notE, standard, elim!] + +declare sym [THEN Pair_neq_0, elim!] + +lemma Pair_neq_fst: "=a ==> P" +apply (unfold Pair_def) +apply (rule consI1 [THEN mem_asym, THEN FalseE]) +apply (erule subst) +apply (rule consI1) +done + +lemma Pair_neq_snd: "=b ==> P" +apply (unfold Pair_def) +apply (rule consI1 [THEN consI2, THEN mem_asym, THEN FalseE]) +apply (erule subst) +apply (rule consI1 [THEN consI2]) +done + + +(*** Sigma: Disjoint union of a family of sets + Generalizes Cartesian product ***) + +lemma Sigma_iff [simp]: ": Sigma(A,B) <-> a:A & b:B(a)" +by (simp add: Sigma_def) + +lemma SigmaI [TC,intro!]: "[| a:A; b:B(a) |] ==> : Sigma(A,B)" +by simp + +lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1, standard] +lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2, standard] + +(*The general elimination rule*) +lemma SigmaE [elim!]: + "[| c: Sigma(A,B); + !!x y.[| x:A; y:B(x); c= |] ==> P + |] ==> P" +apply (unfold Sigma_def, blast) +done + +lemma SigmaE2 [elim!]: + "[| : Sigma(A,B); + [| a:A; b:B(a) |] ==> P + |] ==> P" +apply (unfold Sigma_def, blast) +done + +lemma Sigma_cong: + "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> + Sigma(A,B) = Sigma(A',B')" +by (simp add: Sigma_def) + +(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause + flex-flex pairs and the "Check your prover" error. Most + Sigmas and Pis are abbreviated as * or -> *) + +lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0" +by blast + +lemma Sigma_empty2 [simp]: "A*0 = 0" +by blast + +lemma Sigma_empty_iff: "A*B=0 <-> A=0 | B=0" +by blast + + +(*** Projections: fst, snd ***) + +lemma fst_conv [simp]: "fst() = a" +by (simp add: fst_def, blast) + +lemma snd_conv [simp]: "snd() = b" +by (simp add: snd_def, blast) + +lemma fst_type [TC]: "p:Sigma(A,B) ==> fst(p) : A" +by auto + +lemma snd_type [TC]: "p:Sigma(A,B) ==> snd(p) : B(fst(p))" +by auto + +lemma Pair_fst_snd_eq: "a: Sigma(A,B) ==> = a" +by auto + + +(*** Eliminator - split ***) + +(*A META-equality, so that it applies to higher types as well...*) +lemma split [simp]: "split(%x y. c(x,y), ) == c(a,b)" +by (simp add: split_def) + +lemma split_type [TC]: + "[| p:Sigma(A,B); + !!x y.[| x:A; y:B(x) |] ==> c(x,y):C() + |] ==> split(%x y. c(x,y), p) : C(p)" +apply (erule SigmaE, auto) +done + +lemma expand_split: + "u: A*B ==> + R(split(c,u)) <-> (ALL x:A. ALL y:B. u = --> R(c(x,y)))" +apply (simp add: split_def, auto) +done + + +(*** split for predicates: result type o ***) + +lemma splitI: "R(a,b) ==> split(R, )" +by (simp add: split_def) + +lemma splitE: + "[| split(R,z); z:Sigma(A,B); + !!x y. [| z = ; R(x,y) |] ==> P + |] ==> P" +apply (simp add: split_def) +apply (erule SigmaE, force) +done + +lemma splitD: "split(R,) ==> R(a,b)" +by (simp add: split_def) + +ML +{* +val singleton_eq_iff = thm "singleton_eq_iff"; +val doubleton_eq_iff = thm "doubleton_eq_iff"; +val Pair_iff = thm "Pair_iff"; +val Pair_inject = thm "Pair_inject"; +val Pair_inject1 = thm "Pair_inject1"; +val Pair_inject2 = thm "Pair_inject2"; +val Pair_not_0 = thm "Pair_not_0"; +val Pair_neq_0 = thm "Pair_neq_0"; +val Pair_neq_fst = thm "Pair_neq_fst"; +val Pair_neq_snd = thm "Pair_neq_snd"; +val Sigma_iff = thm "Sigma_iff"; +val SigmaI = thm "SigmaI"; +val SigmaD1 = thm "SigmaD1"; +val SigmaD2 = thm "SigmaD2"; +val SigmaE = thm "SigmaE"; +val SigmaE2 = thm "SigmaE2"; +val Sigma_cong = thm "Sigma_cong"; +val Sigma_empty1 = thm "Sigma_empty1"; +val Sigma_empty2 = thm "Sigma_empty2"; +val Sigma_empty_iff = thm "Sigma_empty_iff"; +val fst_conv = thm "fst_conv"; +val snd_conv = thm "snd_conv"; +val fst_type = thm "fst_type"; +val snd_type = thm "snd_type"; +val Pair_fst_snd_eq = thm "Pair_fst_snd_eq"; +val split = thm "split"; +val split_type = thm "split_type"; +val expand_split = thm "expand_split"; +val splitI = thm "splitI"; +val splitE = thm "splitE"; +val splitD = thm "splitD"; +*} + end