conversion of Sum, pair to Isar script
authorpaulson
Sun Jun 23 10:14:13 2002 +0200 (2002-06-23)
changeset 13240bb5f4faea1f3
parent 13239 f599984ec4c2
child 13241 0ffc4403f811
conversion of Sum, pair to Isar script
src/ZF/IsaMakefile
src/ZF/Sum.ML
src/ZF/Sum.thy
src/ZF/Trancl.thy
src/ZF/pair.ML
src/ZF/pair.thy
     1.1 --- a/src/ZF/IsaMakefile	Sat Jun 22 18:28:46 2002 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Sun Jun 23 10:14:13 2002 +0200
     1.3 @@ -39,13 +39,13 @@
     1.4    Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
     1.5    Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy	\
     1.6    OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy	\
     1.7 -  QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Sum.ML	\
     1.8 +  QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML	\
     1.9    Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
    1.10    Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
    1.11    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
    1.12    Trancl.thy Univ.thy Update.thy \
    1.13    WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy	\
    1.14 -  ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML		\
    1.15 +  ind_syntax.ML mono.ML mono.thy pair.thy simpdata.ML		\
    1.16    subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
    1.17  	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
    1.18  
     2.1 --- a/src/ZF/Sum.ML	Sat Jun 22 18:28:46 2002 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,211 +0,0 @@
     2.4 -(*  Title:      ZF/Sum
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1992  University of Cambridge
     2.8 -
     2.9 -Disjoint sums in Zermelo-Fraenkel Set Theory 
    2.10 -*)
    2.11 -
    2.12 -(*** Rules for the Part primitive ***)
    2.13 -
    2.14 -Goalw [Part_def]
    2.15 -    "a : Part(A,h) <-> a:A & (EX y. a=h(y))";
    2.16 -by (rtac separation 1);
    2.17 -qed "Part_iff";
    2.18 -
    2.19 -Goalw [Part_def]
    2.20 -    "[| a : A;  a=h(b) |] ==> a : Part(A,h)";
    2.21 -by (Blast_tac 1);
    2.22 -qed "Part_eqI";
    2.23 -
    2.24 -bind_thm ("PartI", refl RSN (2,Part_eqI));
    2.25 -
    2.26 -val major::prems = Goalw [Part_def]
    2.27 -    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
    2.28 -\    |] ==> P";
    2.29 -by (rtac (major RS CollectE) 1);
    2.30 -by (etac exE 1);
    2.31 -by (REPEAT (ares_tac prems 1));
    2.32 -qed "PartE";
    2.33 -
    2.34 -AddIs  [Part_eqI];
    2.35 -AddSEs [PartE];
    2.36 -
    2.37 -Goalw [Part_def] "Part(A,h) <= A";
    2.38 -by (rtac Collect_subset 1);
    2.39 -qed "Part_subset";
    2.40 -
    2.41 -
    2.42 -(*** Rules for Disjoint Sums ***)
    2.43 -
    2.44 -bind_thms ("sum_defs", [sum_def,Inl_def,Inr_def,case_def]);
    2.45 -
    2.46 -Goalw (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
    2.47 -by (Blast_tac 1);
    2.48 -qed "Sigma_bool";
    2.49 -
    2.50 -(** Introduction rules for the injections **)
    2.51 -
    2.52 -Goalw sum_defs "a : A ==> Inl(a) : A+B";
    2.53 -by (Blast_tac 1);
    2.54 -qed "InlI";
    2.55 -
    2.56 -Goalw sum_defs "b : B ==> Inr(b) : A+B";
    2.57 -by (Blast_tac 1);
    2.58 -qed "InrI";
    2.59 -
    2.60 -(** Elimination rules **)
    2.61 -
    2.62 -val major::prems = Goalw sum_defs
    2.63 -    "[| u: A+B;  \
    2.64 -\       !!x. [| x:A;  u=Inl(x) |] ==> P; \
    2.65 -\       !!y. [| y:B;  u=Inr(y) |] ==> P \
    2.66 -\    |] ==> P";
    2.67 -by (rtac (major RS UnE) 1);
    2.68 -by (REPEAT (rtac refl 1
    2.69 -     ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1));
    2.70 -qed "sumE";
    2.71 -
    2.72 -(** Injection and freeness equivalences, for rewriting **)
    2.73 -
    2.74 -Goalw sum_defs "Inl(a)=Inl(b) <-> a=b";
    2.75 -by (Simp_tac 1);
    2.76 -qed "Inl_iff";
    2.77 -
    2.78 -Goalw sum_defs "Inr(a)=Inr(b) <-> a=b";
    2.79 -by (Simp_tac 1);
    2.80 -qed "Inr_iff";
    2.81 -
    2.82 -Goalw sum_defs "Inl(a)=Inr(b) <-> False";
    2.83 -by (Simp_tac 1);
    2.84 -qed "Inl_Inr_iff";
    2.85 -
    2.86 -Goalw sum_defs "Inr(b)=Inl(a) <-> False";
    2.87 -by (Simp_tac 1);
    2.88 -qed "Inr_Inl_iff";
    2.89 -
    2.90 -Goalw sum_defs "0+0 = 0";
    2.91 -by (Simp_tac 1);
    2.92 -qed "sum_empty";
    2.93 -
    2.94 -(*Injection and freeness rules*)
    2.95 -
    2.96 -bind_thm ("Inl_inject", (Inl_iff RS iffD1));
    2.97 -bind_thm ("Inr_inject", (Inr_iff RS iffD1));
    2.98 -bind_thm ("Inl_neq_Inr", (Inl_Inr_iff RS iffD1 RS FalseE));
    2.99 -bind_thm ("Inr_neq_Inl", (Inr_Inl_iff RS iffD1 RS FalseE));
   2.100 -
   2.101 -AddSIs [InlI, InrI];
   2.102 -AddSEs [sumE, Inl_neq_Inr, Inr_neq_Inl];
   2.103 -AddSDs [Inl_inject, Inr_inject];
   2.104 -
   2.105 -Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty];
   2.106 -AddTCs   [InlI, InrI];
   2.107 -
   2.108 -Goal "Inl(a): A+B ==> a: A";
   2.109 -by (Blast_tac 1);
   2.110 -qed "InlD";
   2.111 -
   2.112 -Goal "Inr(b): A+B ==> b: B";
   2.113 -by (Blast_tac 1);
   2.114 -qed "InrD";
   2.115 -
   2.116 -Goal "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))";
   2.117 -by (Blast_tac 1);
   2.118 -qed "sum_iff";
   2.119 -
   2.120 -Goal "A+B <= C+D <-> A<=C & B<=D";
   2.121 -by (Blast_tac 1);
   2.122 -qed "sum_subset_iff";
   2.123 -
   2.124 -Goal "A+B = C+D <-> A=C & B=D";
   2.125 -by (simp_tac (simpset() addsimps [extension,sum_subset_iff]) 1);
   2.126 -by (Blast_tac 1);
   2.127 -qed "sum_equal_iff";
   2.128 -
   2.129 -Goalw [sum_def] "A+A = 2*A";
   2.130 -by (Blast_tac 1);
   2.131 -qed "sum_eq_2_times";
   2.132 -
   2.133 -
   2.134 -(*** Eliminator -- case ***)
   2.135 -
   2.136 -Goalw sum_defs "case(c, d, Inl(a)) = c(a)";
   2.137 -by (Simp_tac 1);
   2.138 -qed "case_Inl";
   2.139 -
   2.140 -Goalw sum_defs "case(c, d, Inr(b)) = d(b)";
   2.141 -by (Simp_tac 1);
   2.142 -qed "case_Inr";
   2.143 -
   2.144 -Addsimps [case_Inl, case_Inr];
   2.145 -
   2.146 -val major::prems = Goal
   2.147 -    "[| u: A+B; \
   2.148 -\       !!x. x: A ==> c(x): C(Inl(x));   \
   2.149 -\       !!y. y: B ==> d(y): C(Inr(y)) \
   2.150 -\    |] ==> case(c,d,u) : C(u)";
   2.151 -by (rtac (major RS sumE) 1);
   2.152 -by (ALLGOALS (etac ssubst));
   2.153 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   2.154 -qed "case_type";
   2.155 -AddTCs [case_type];
   2.156 -
   2.157 -Goal "u: A+B ==>   \
   2.158 -\       R(case(c,d,u)) <-> \
   2.159 -\       ((ALL x:A. u = Inl(x) --> R(c(x))) & \
   2.160 -\       (ALL y:B. u = Inr(y) --> R(d(y))))";
   2.161 -by Auto_tac;
   2.162 -qed "expand_case";
   2.163 -
   2.164 -val major::prems = Goal
   2.165 -  "[| z: A+B;   \
   2.166 -\     !!x. x:A ==> c(x)=c'(x);  \
   2.167 -\     !!y. y:B ==> d(y)=d'(y)   \
   2.168 -\  |] ==> case(c,d,z) = case(c',d',z)";
   2.169 -by (resolve_tac [major RS sumE] 1);
   2.170 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   2.171 -qed "case_cong";
   2.172 -
   2.173 -Goal "z: A+B ==>   \
   2.174 -\       case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \
   2.175 -\       case(%x. c(c'(x)), %y. d(d'(y)), z)";
   2.176 -by Auto_tac;
   2.177 -qed "case_case";
   2.178 -
   2.179 -
   2.180 -(*** More rules for Part(A,h) ***)
   2.181 -
   2.182 -Goal "A<=B ==> Part(A,h)<=Part(B,h)";
   2.183 -by (Blast_tac 1);
   2.184 -qed "Part_mono";
   2.185 -
   2.186 -Goal "Part(Collect(A,P), h) = Collect(Part(A,h), P)";
   2.187 -by (Blast_tac 1);
   2.188 -qed "Part_Collect";
   2.189 -
   2.190 -bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE);
   2.191 -
   2.192 -Goal "Part(A+B,Inl) = {Inl(x). x: A}";
   2.193 -by (Blast_tac 1);
   2.194 -qed "Part_Inl";
   2.195 -
   2.196 -Goal "Part(A+B,Inr) = {Inr(y). y: B}";
   2.197 -by (Blast_tac 1);
   2.198 -qed "Part_Inr";
   2.199 -
   2.200 -Goalw [Part_def] "a : Part(A,h) ==> a : A";
   2.201 -by (etac CollectD1 1);
   2.202 -qed "PartD1";
   2.203 -
   2.204 -Goal "Part(A,%x. x) = A";
   2.205 -by (Blast_tac 1);
   2.206 -qed "Part_id";
   2.207 -
   2.208 -Goal "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}";
   2.209 -by (Blast_tac 1);
   2.210 -qed "Part_Inr2";
   2.211 -
   2.212 -Goal "C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
   2.213 -by (Blast_tac 1);
   2.214 -qed "Part_sum_equality";
     3.1 --- a/src/ZF/Sum.thy	Sat Jun 22 18:28:46 2002 +0200
     3.2 +++ b/src/ZF/Sum.thy	Sun Jun 23 10:14:13 2002 +0200
     3.3 @@ -7,25 +7,270 @@
     3.4  "Part" primitive for simultaneous recursive type definitions
     3.5  *)
     3.6  
     3.7 -Sum = Bool + equalities + 
     3.8 +theory Sum = Bool + equalities:
     3.9  
    3.10  global
    3.11  
    3.12 -consts
    3.13 -    "+"     :: "[i,i]=>i"                     (infixr 65)
    3.14 -    Inl     :: "i=>i"
    3.15 -    Inr     :: "i=>i"
    3.16 -    "case"  :: "[i=>i, i=>i, i]=>i"
    3.17 -    Part    :: "[i,i=>i] => i"
    3.18 +constdefs
    3.19 +  sum     :: "[i,i]=>i"                     (infixr "+" 65)
    3.20 +     "A+B == {0}*A Un {1}*B"
    3.21 +
    3.22 +  Inl     :: "i=>i"
    3.23 +     "Inl(a) == <0,a>"
    3.24 +
    3.25 +  Inr     :: "i=>i"
    3.26 +     "Inr(b) == <1,b>"
    3.27 +
    3.28 +  "case"  :: "[i=>i, i=>i, i]=>i"
    3.29 +     "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"
    3.30 +
    3.31 +  (*operator for selecting out the various summands*)
    3.32 +  Part    :: "[i,i=>i] => i"
    3.33 +     "Part(A,h) == {x: A. EX z. x = h(z)}"
    3.34  
    3.35  local
    3.36  
    3.37 -defs
    3.38 -    sum_def     "A+B == {0}*A Un {1}*B"
    3.39 -    Inl_def     "Inl(a) == <0,a>"
    3.40 -    Inr_def     "Inr(b) == <1,b>"
    3.41 -    case_def    "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"
    3.42 +(*** Rules for the Part primitive ***)
    3.43 +
    3.44 +lemma Part_iff: 
    3.45 +    "a : Part(A,h) <-> a:A & (EX y. a=h(y))"
    3.46 +apply (unfold Part_def)
    3.47 +apply (rule separation)
    3.48 +done
    3.49 +
    3.50 +lemma Part_eqI [intro]: 
    3.51 +    "[| a : A;  a=h(b) |] ==> a : Part(A,h)"
    3.52 +apply (unfold Part_def)
    3.53 +apply blast
    3.54 +done
    3.55 +
    3.56 +lemmas PartI = refl [THEN [2] Part_eqI]
    3.57 +
    3.58 +lemma PartE [elim!]: 
    3.59 +    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P   
    3.60 +     |] ==> P"
    3.61 +apply (unfold Part_def)
    3.62 +apply blast
    3.63 +done
    3.64 +
    3.65 +lemma Part_subset: "Part(A,h) <= A"
    3.66 +apply (unfold Part_def)
    3.67 +apply (rule Collect_subset)
    3.68 +done
    3.69 +
    3.70 +
    3.71 +(*** Rules for Disjoint Sums ***)
    3.72 +
    3.73 +lemmas sum_defs = sum_def Inl_def Inr_def case_def
    3.74 +
    3.75 +lemma Sigma_bool: "Sigma(bool,C) = C(0) + C(1)"
    3.76 +apply (unfold bool_def sum_def)
    3.77 +apply blast
    3.78 +done
    3.79 +
    3.80 +(** Introduction rules for the injections **)
    3.81 +
    3.82 +lemma InlI [intro!,simp,TC]: "a : A ==> Inl(a) : A+B"
    3.83 +apply (unfold sum_defs)
    3.84 +apply blast
    3.85 +done
    3.86 +
    3.87 +lemma InrI [intro!,simp,TC]: "b : B ==> Inr(b) : A+B"
    3.88 +apply (unfold sum_defs)
    3.89 +apply blast
    3.90 +done
    3.91 +
    3.92 +(** Elimination rules **)
    3.93 +
    3.94 +lemma sumE [elim!]:
    3.95 +    "[| u: A+B;   
    3.96 +        !!x. [| x:A;  u=Inl(x) |] ==> P;  
    3.97 +        !!y. [| y:B;  u=Inr(y) |] ==> P  
    3.98 +     |] ==> P"
    3.99 +apply (unfold sum_defs)
   3.100 +apply (blast intro: elim:); 
   3.101 +done
   3.102 +
   3.103 +(** Injection and freeness equivalences, for rewriting **)
   3.104 +
   3.105 +lemma Inl_iff [iff]: "Inl(a)=Inl(b) <-> a=b"
   3.106 +apply (simp add: sum_defs)
   3.107 +done
   3.108 +
   3.109 +lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
   3.110 +apply (simp add: sum_defs)
   3.111 +done
   3.112 +
   3.113 +lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) <-> False"
   3.114 +apply (simp add: sum_defs)
   3.115 +done
   3.116 +
   3.117 +lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) <-> False"
   3.118 +apply (simp add: sum_defs)
   3.119 +done
   3.120 +
   3.121 +lemma sum_empty [simp]: "0+0 = 0"
   3.122 +apply (simp add: sum_defs)
   3.123 +done
   3.124 +
   3.125 +(*Injection and freeness rules*)
   3.126 +
   3.127 +lemmas Inl_inject = Inl_iff [THEN iffD1, standard]
   3.128 +lemmas Inr_inject = Inr_iff [THEN iffD1, standard]
   3.129 +lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE]
   3.130 +lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE]
   3.131 +
   3.132 +
   3.133 +lemma InlD: "Inl(a): A+B ==> a: A"
   3.134 +apply blast
   3.135 +done
   3.136 +
   3.137 +lemma InrD: "Inr(b): A+B ==> b: B"
   3.138 +apply blast
   3.139 +done
   3.140 +
   3.141 +lemma sum_iff: "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"
   3.142 +apply blast
   3.143 +done
   3.144 +
   3.145 +lemma sum_subset_iff: "A+B <= C+D <-> A<=C & B<=D"
   3.146 +apply blast
   3.147 +done
   3.148 +
   3.149 +lemma sum_equal_iff: "A+B = C+D <-> A=C & B=D"
   3.150 +apply (simp add: extension sum_subset_iff)
   3.151 +apply blast
   3.152 +done
   3.153 +
   3.154 +lemma sum_eq_2_times: "A+A = 2*A"
   3.155 +apply (simp add: sum_def)
   3.156 +apply blast
   3.157 +done
   3.158 +
   3.159 +
   3.160 +(*** Eliminator -- case ***)
   3.161  
   3.162 -  (*operator for selecting out the various summands*)
   3.163 -    Part_def    "Part(A,h) == {x: A. EX z. x = h(z)}"
   3.164 +lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)"
   3.165 +apply (simp add: sum_defs)
   3.166 +done
   3.167 +
   3.168 +lemma case_Inr [simp]: "case(c, d, Inr(b)) = d(b)"
   3.169 +apply (simp add: sum_defs)
   3.170 +done
   3.171 +
   3.172 +lemma case_type [TC]:
   3.173 +    "[| u: A+B;  
   3.174 +        !!x. x: A ==> c(x): C(Inl(x));    
   3.175 +        !!y. y: B ==> d(y): C(Inr(y))  
   3.176 +     |] ==> case(c,d,u) : C(u)"
   3.177 +apply (auto );  
   3.178 +done
   3.179 +
   3.180 +lemma expand_case: "u: A+B ==>    
   3.181 +        R(case(c,d,u)) <->  
   3.182 +        ((ALL x:A. u = Inl(x) --> R(c(x))) &  
   3.183 +        (ALL y:B. u = Inr(y) --> R(d(y))))"
   3.184 +by auto
   3.185 +
   3.186 +lemma case_cong:
   3.187 +  "[| z: A+B;    
   3.188 +      !!x. x:A ==> c(x)=c'(x);   
   3.189 +      !!y. y:B ==> d(y)=d'(y)    
   3.190 +   |] ==> case(c,d,z) = case(c',d',z)"
   3.191 +by (auto ); 
   3.192 +
   3.193 +lemma case_case: "z: A+B ==>    
   3.194 +        case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) =  
   3.195 +        case(%x. c(c'(x)), %y. d(d'(y)), z)"
   3.196 +by auto
   3.197 +
   3.198 +
   3.199 +(*** More rules for Part(A,h) ***)
   3.200 +
   3.201 +lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)"
   3.202 +apply blast
   3.203 +done
   3.204 +
   3.205 +lemma Part_Collect: "Part(Collect(A,P), h) = Collect(Part(A,h), P)"
   3.206 +apply blast
   3.207 +done
   3.208 +
   3.209 +lemmas Part_CollectE =
   3.210 +     Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE, standard]
   3.211 +
   3.212 +lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x: A}"
   3.213 +apply blast
   3.214 +done
   3.215 +
   3.216 +lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y: B}"
   3.217 +apply blast
   3.218 +done
   3.219 +
   3.220 +lemma PartD1: "a : Part(A,h) ==> a : A"
   3.221 +apply (simp add: Part_def)
   3.222 +done
   3.223 +
   3.224 +lemma Part_id: "Part(A,%x. x) = A"
   3.225 +apply blast
   3.226 +done
   3.227 +
   3.228 +lemma Part_Inr2: "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}"
   3.229 +apply blast
   3.230 +done
   3.231 +
   3.232 +lemma Part_sum_equality: "C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"
   3.233 +apply blast
   3.234 +done
   3.235 +
   3.236 +ML
   3.237 +{*
   3.238 +val sum_def = thm "sum_def";
   3.239 +val Inl_def = thm "Inl_def";
   3.240 +val Inr_def = thm "Inr_def";
   3.241 +val sum_defs = thms "sum_defs";
   3.242 +
   3.243 +val Part_iff = thm "Part_iff";
   3.244 +val Part_eqI = thm "Part_eqI";
   3.245 +val PartI = thm "PartI";
   3.246 +val PartE = thm "PartE";
   3.247 +val Part_subset = thm "Part_subset";
   3.248 +val Sigma_bool = thm "Sigma_bool";
   3.249 +val InlI = thm "InlI";
   3.250 +val InrI = thm "InrI";
   3.251 +val sumE = thm "sumE";
   3.252 +val Inl_iff = thm "Inl_iff";
   3.253 +val Inr_iff = thm "Inr_iff";
   3.254 +val Inl_Inr_iff = thm "Inl_Inr_iff";
   3.255 +val Inr_Inl_iff = thm "Inr_Inl_iff";
   3.256 +val sum_empty = thm "sum_empty";
   3.257 +val Inl_inject = thm "Inl_inject";
   3.258 +val Inr_inject = thm "Inr_inject";
   3.259 +val Inl_neq_Inr = thm "Inl_neq_Inr";
   3.260 +val Inr_neq_Inl = thm "Inr_neq_Inl";
   3.261 +val InlD = thm "InlD";
   3.262 +val InrD = thm "InrD";
   3.263 +val sum_iff = thm "sum_iff";
   3.264 +val sum_subset_iff = thm "sum_subset_iff";
   3.265 +val sum_equal_iff = thm "sum_equal_iff";
   3.266 +val sum_eq_2_times = thm "sum_eq_2_times";
   3.267 +val case_Inl = thm "case_Inl";
   3.268 +val case_Inr = thm "case_Inr";
   3.269 +val case_type = thm "case_type";
   3.270 +val expand_case = thm "expand_case";
   3.271 +val case_cong = thm "case_cong";
   3.272 +val case_case = thm "case_case";
   3.273 +val Part_mono = thm "Part_mono";
   3.274 +val Part_Collect = thm "Part_Collect";
   3.275 +val Part_CollectE = thm "Part_CollectE";
   3.276 +val Part_Inl = thm "Part_Inl";
   3.277 +val Part_Inr = thm "Part_Inr";
   3.278 +val PartD1 = thm "PartD1";
   3.279 +val Part_id = thm "Part_id";
   3.280 +val Part_Inr2 = thm "Part_Inr2";
   3.281 +val Part_sum_equality = thm "Part_sum_equality";
   3.282 +
   3.283 +*}
   3.284 +
   3.285 +
   3.286 +
   3.287  end
     4.1 --- a/src/ZF/Trancl.thy	Sat Jun 22 18:28:46 2002 +0200
     4.2 +++ b/src/ZF/Trancl.thy	Sun Jun 23 10:14:13 2002 +0200
     4.3 @@ -47,64 +47,53 @@
     4.4  
     4.5  lemma irreflI:
     4.6      "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)"
     4.7 -by (simp add: irrefl_def); 
     4.8 +by (simp add: irrefl_def) 
     4.9  
    4.10  lemma symI: "[| irrefl(A,r);  x:A |] ==>  <x,x> ~: r"
    4.11 -apply (simp add: irrefl_def)
    4.12 -done
    4.13 +by (simp add: irrefl_def)
    4.14  
    4.15  subsubsection{*symmetry*}
    4.16  
    4.17  lemma symI:
    4.18       "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"
    4.19 -apply (unfold sym_def); 
    4.20 -apply (blast intro: elim:); 
    4.21 +apply (unfold sym_def, blast) 
    4.22  done
    4.23  
    4.24  lemma antisymI: "[| sym(r); <x,y>: r |]  ==>  <y,x>: r"
    4.25 -apply (unfold sym_def)
    4.26 -apply blast
    4.27 -done
    4.28 +by (unfold sym_def, blast)
    4.29  
    4.30  subsubsection{*antisymmetry*}
    4.31  
    4.32  lemma antisymI:
    4.33       "[| !!x y.[| <x,y>: r;  <y,x>: r |] ==> x=y |] ==> antisym(r)"
    4.34 -apply (simp add: antisym_def) 
    4.35 -apply (blast intro: elim:); 
    4.36 +apply (simp add: antisym_def, blast) 
    4.37  done
    4.38  
    4.39  lemma antisymE: "[| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y"
    4.40 -apply (simp add: antisym_def)
    4.41 -apply blast
    4.42 -done
    4.43 +by (simp add: antisym_def, blast)
    4.44  
    4.45  subsubsection{*transitivity*}
    4.46  
    4.47  lemma transD: "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r"
    4.48 -apply (unfold trans_def)
    4.49 -apply blast
    4.50 -done
    4.51 +by (unfold trans_def, blast)
    4.52  
    4.53  lemma trans_onD: 
    4.54      "[| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>:r"
    4.55 -apply (unfold trans_on_def)
    4.56 -apply blast
    4.57 +apply (unfold trans_on_def, blast)
    4.58  done
    4.59  
    4.60  subsection{*Transitive closure of a relation*}
    4.61  
    4.62  lemma rtrancl_bnd_mono:
    4.63       "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))"
    4.64 -apply (rule bnd_monoI)
    4.65 -apply (blast intro: elim:)+
    4.66 +apply (rule bnd_monoI, blast+)
    4.67  done
    4.68  
    4.69  lemma rtrancl_mono: "r<=s ==> r^* <= s^*"
    4.70  apply (unfold rtrancl_def)
    4.71  apply (rule lfp_mono)
    4.72  apply (rule rtrancl_bnd_mono)+
    4.73 -apply (blast intro: elim:); 
    4.74 +apply blast 
    4.75  done
    4.76  
    4.77  (* r^* = id(field(r)) Un ( r O r^* )    *)
    4.78 @@ -125,25 +114,20 @@
    4.79  (*Closure under composition with r  *)
    4.80  lemma rtrancl_into_rtrancl: "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*"
    4.81  apply (rule rtrancl_unfold [THEN ssubst])
    4.82 -apply (rule compI [THEN UnI2])
    4.83 -apply assumption
    4.84 +apply (rule compI [THEN UnI2], assumption)
    4.85  apply assumption
    4.86  done
    4.87  
    4.88  (*rtrancl of r contains all pairs in r  *)
    4.89  lemma r_into_rtrancl: "<a,b> : r ==> <a,b> : r^*"
    4.90 -apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
    4.91 -apply (blast intro: elim:)+
    4.92 -done
    4.93 +by (rule rtrancl_refl [THEN rtrancl_into_rtrancl], blast+)
    4.94  
    4.95  (*The premise ensures that r consists entirely of pairs*)
    4.96  lemma r_subset_rtrancl: "r <= Sigma(A,B) ==> r <= r^*"
    4.97 -apply (blast intro: r_into_rtrancl)
    4.98 -done
    4.99 +by (blast intro: r_into_rtrancl)
   4.100  
   4.101  lemma rtrancl_field: "field(r^*) = field(r)"
   4.102 -apply (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD])
   4.103 -done
   4.104 +by (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD])
   4.105  
   4.106  
   4.107  (** standard induction rule **)
   4.108 @@ -153,8 +137,7 @@
   4.109        !!x. x: field(r) ==> P(<x,x>);  
   4.110        !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |]  
   4.111     ==>  P(<a,b>)"
   4.112 -apply (erule def_induct [OF rtrancl_def rtrancl_bnd_mono])
   4.113 -apply (blast intro: elim:); 
   4.114 +apply (erule def_induct [OF rtrancl_def rtrancl_bnd_mono], blast) 
   4.115  done
   4.116  
   4.117  (*nice induction rule.
   4.118 @@ -170,16 +153,14 @@
   4.119  (*now solve first subgoal: this formula is sufficient*)
   4.120  apply (erule spec [THEN mp], rule refl)
   4.121  (*now do the induction*)
   4.122 -apply (erule rtrancl_full_induct)
   4.123 -apply (blast)+
   4.124 +apply (erule rtrancl_full_induct, blast+)
   4.125  done
   4.126  
   4.127  (*transitivity of transitive closure!! -- by induction.*)
   4.128  lemma trans_rtrancl: "trans(r^*)"
   4.129  apply (unfold trans_def)
   4.130  apply (intro allI impI)
   4.131 -apply (erule_tac b = "z" in rtrancl_induct)
   4.132 -apply assumption; 
   4.133 +apply (erule_tac b = "z" in rtrancl_induct, assumption)
   4.134  apply (blast intro: rtrancl_into_rtrancl) 
   4.135  done
   4.136  
   4.137 @@ -192,9 +173,8 @@
   4.138       ==> P"
   4.139  apply (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r) ")
   4.140  (*see HOL/trancl*)
   4.141 -apply (blast intro: elim:); 
   4.142 -apply (erule rtrancl_induct)
   4.143 -apply (blast intro: elim:)+
   4.144 +apply blast 
   4.145 +apply (erule rtrancl_induct, blast+)
   4.146  done
   4.147  
   4.148  
   4.149 @@ -224,14 +204,11 @@
   4.150  
   4.151  (*The premise ensures that r consists entirely of pairs*)
   4.152  lemma r_subset_trancl: "r <= Sigma(A,B) ==> r <= r^+"
   4.153 -apply (blast intro: r_into_trancl)
   4.154 -done
   4.155 +by (blast intro: r_into_trancl)
   4.156  
   4.157  (*intro rule by definition: from r^* and r  *)
   4.158  lemma rtrancl_into_trancl1: "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+"
   4.159 -apply (unfold trancl_def)
   4.160 -apply blast
   4.161 -done
   4.162 +by (unfold trancl_def, blast)
   4.163  
   4.164  (*intro rule from r and r^*  *)
   4.165  lemma rtrancl_into_trancl2:
   4.166 @@ -264,7 +241,7 @@
   4.167          !!y.[| <a,y> : r^+; <y,b> : r |] ==> P   
   4.168       |] ==> P"
   4.169  apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r) ")
   4.170 -apply (blast intro: elim:); 
   4.171 +apply blast 
   4.172  apply (rule compEpair)
   4.173  apply (unfold trancl_def, assumption)
   4.174  apply (erule rtranclE)
   4.175 @@ -283,14 +260,12 @@
   4.176  (** Suggested by Sidi Ould Ehmety **)
   4.177  
   4.178  lemma rtrancl_idemp [simp]: "(r^*)^* = r^*"
   4.179 -apply (rule equalityI)
   4.180 -apply auto
   4.181 +apply (rule equalityI, auto)
   4.182   prefer 2
   4.183   apply (frule rtrancl_type [THEN subsetD])
   4.184 - apply (blast intro: r_into_rtrancl elim:); 
   4.185 + apply (blast intro: r_into_rtrancl ) 
   4.186  txt{*converse direction*}
   4.187 -apply (frule rtrancl_type [THEN subsetD])
   4.188 -apply (clarify ); 
   4.189 +apply (frule rtrancl_type [THEN subsetD], clarify) 
   4.190  apply (erule rtrancl_induct)
   4.191  apply (simp add: rtrancl_refl rtrancl_field)
   4.192  apply (blast intro: rtrancl_trans)
   4.193 @@ -298,8 +273,7 @@
   4.194  
   4.195  lemma rtrancl_subset: "[| R <= S; S <= R^* |] ==> S^* = R^*"
   4.196  apply (drule rtrancl_mono)
   4.197 -apply (drule rtrancl_mono)
   4.198 -apply simp_all
   4.199 +apply (drule rtrancl_mono, simp_all)
   4.200  apply blast
   4.201  done
   4.202  
     5.1 --- a/src/ZF/pair.ML	Sat Jun 22 18:28:46 2002 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,191 +0,0 @@
     5.4 -(*  Title:      ZF/pair
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1992  University of Cambridge
     5.8 -
     5.9 -Ordered pairs in Zermelo-Fraenkel Set Theory 
    5.10 -*)
    5.11 -
    5.12 -(** Lemmas for showing that <a,b> uniquely determines a and b **)
    5.13 -
    5.14 -Goal "{a} = {b} <-> a=b";
    5.15 -by (resolve_tac [extension RS iff_trans] 1);
    5.16 -by (Blast_tac 1) ;
    5.17 -qed "singleton_eq_iff";
    5.18 -AddIffs [singleton_eq_iff];
    5.19 -
    5.20 -Goal "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)";
    5.21 -by (resolve_tac [extension RS iff_trans] 1);
    5.22 -by (Blast_tac 1) ;
    5.23 -qed "doubleton_eq_iff";
    5.24 -
    5.25 -Goalw [Pair_def] "<a,b> = <c,d> <-> a=c & b=d";
    5.26 -by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1);
    5.27 -by (Blast_tac 1) ;
    5.28 -qed "Pair_iff";
    5.29 -
    5.30 -Addsimps [Pair_iff];
    5.31 -
    5.32 -bind_thm ("Pair_inject", Pair_iff RS iffD1 RS conjE);
    5.33 -
    5.34 -AddSEs [Pair_inject];
    5.35 -
    5.36 -bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1);
    5.37 -bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2);
    5.38 -
    5.39 -Goalw [Pair_def]  "<a,b> ~= 0";
    5.40 -by (blast_tac (claset() addEs [equalityE]) 1) ;
    5.41 -qed "Pair_not_0";
    5.42 -
    5.43 -bind_thm ("Pair_neq_0", Pair_not_0 RS notE);
    5.44 -
    5.45 -AddSEs [Pair_neq_0, sym RS Pair_neq_0];
    5.46 -
    5.47 -Goalw [Pair_def]  "<a,b>=a ==> P";
    5.48 -by (rtac (consI1 RS mem_asym RS FalseE) 1);
    5.49 -by (etac subst 1);
    5.50 -by (rtac consI1 1) ;
    5.51 -qed "Pair_neq_fst";
    5.52 -
    5.53 -Goalw [Pair_def]  "<a,b>=b ==> P";
    5.54 -by (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1);
    5.55 -by (etac subst 1);
    5.56 -by (rtac (consI1 RS consI2) 1) ;
    5.57 -qed "Pair_neq_snd";
    5.58 -
    5.59 -
    5.60 -(*** Sigma: Disjoint union of a family of sets
    5.61 -     Generalizes Cartesian product ***)
    5.62 -
    5.63 -Goalw [Sigma_def]  "<a,b>: Sigma(A,B) <-> a:A & b:B(a)";
    5.64 -by (Blast_tac 1) ;
    5.65 -qed "Sigma_iff";
    5.66 -
    5.67 -Addsimps [Sigma_iff];
    5.68 -
    5.69 -Goal "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)";
    5.70 -by (Asm_simp_tac 1);
    5.71 -qed "SigmaI";
    5.72 -
    5.73 -AddTCs [SigmaI];
    5.74 -
    5.75 -bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1);
    5.76 -bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);
    5.77 -
    5.78 -(*The general elimination rule*)
    5.79 -val major::prems= Goalw [Sigma_def] 
    5.80 -    "[| c: Sigma(A,B);  \
    5.81 -\       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \
    5.82 -\    |] ==> P";
    5.83 -by (cut_facts_tac [major] 1);
    5.84 -by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
    5.85 -qed "SigmaE";
    5.86 -
    5.87 -val [major,minor]= Goal
    5.88 -    "[| <a,b> : Sigma(A,B);    \
    5.89 -\       [| a:A;  b:B(a) |] ==> P   \
    5.90 -\    |] ==> P";
    5.91 -by (rtac minor 1);
    5.92 -by (rtac (major RS SigmaD1) 1);
    5.93 -by (rtac (major RS SigmaD2) 1) ;
    5.94 -qed "SigmaE2";
    5.95 -
    5.96 -val prems= Goalw [Sigma_def] 
    5.97 -    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
    5.98 -\    Sigma(A,B) = Sigma(A',B')";
    5.99 -by (simp_tac (simpset() addsimps prems) 1) ;
   5.100 -qed "Sigma_cong";
   5.101 -
   5.102 -
   5.103 -(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
   5.104 -  flex-flex pairs and the "Check your prover" error.  Most
   5.105 -  Sigmas and Pis are abbreviated as * or -> *)
   5.106 -
   5.107 -AddSIs [SigmaI];
   5.108 -AddSEs [SigmaE2, SigmaE];
   5.109 -
   5.110 -Goal "Sigma(0,B) = 0";
   5.111 -by (Blast_tac 1) ;
   5.112 -qed "Sigma_empty1";
   5.113 -
   5.114 -Goal "A*0 = 0";
   5.115 -by (Blast_tac 1) ;
   5.116 -qed "Sigma_empty2";
   5.117 -
   5.118 -Addsimps [Sigma_empty1, Sigma_empty2];
   5.119 -
   5.120 -Goal "A*B=0 <-> A=0 | B=0";
   5.121 -by (Blast_tac 1);
   5.122 -qed "Sigma_empty_iff";
   5.123 -
   5.124 -
   5.125 -(*** Projections: fst, snd ***)
   5.126 -
   5.127 -Goalw [fst_def]  "fst(<a,b>) = a";
   5.128 -by (Blast_tac 1) ;
   5.129 -qed "fst_conv";
   5.130 -
   5.131 -Goalw [snd_def]  "snd(<a,b>) = b";
   5.132 -by (Blast_tac 1) ;
   5.133 -qed "snd_conv";
   5.134 -
   5.135 -Addsimps [fst_conv,snd_conv];
   5.136 -
   5.137 -Goal "p:Sigma(A,B) ==> fst(p) : A";
   5.138 -by (Auto_tac) ;
   5.139 -qed "fst_type";
   5.140 -AddTCs [fst_type];
   5.141 -
   5.142 -Goal "p:Sigma(A,B) ==> snd(p) : B(fst(p))";
   5.143 -by (Auto_tac) ;
   5.144 -qed "snd_type";
   5.145 -AddTCs [snd_type];
   5.146 -
   5.147 -Goal "a: Sigma(A,B) ==> <fst(a),snd(a)> = a";
   5.148 -by (Auto_tac) ;
   5.149 -qed "Pair_fst_snd_eq";
   5.150 -
   5.151 -
   5.152 -(*** Eliminator - split ***)
   5.153 -
   5.154 -(*A META-equality, so that it applies to higher types as well...*)
   5.155 -Goalw [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)";
   5.156 -by (Simp_tac 1);
   5.157 -qed "split";
   5.158 -Addsimps [split];
   5.159 -
   5.160 -val major::prems= Goal
   5.161 -    "[|  p:Sigma(A,B);   \
   5.162 -\        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
   5.163 -\    |] ==> split(%x y. c(x,y), p) : C(p)";
   5.164 -by (rtac (major RS SigmaE) 1);
   5.165 -by (asm_simp_tac (simpset() addsimps prems) 1);
   5.166 -qed "split_type";
   5.167 -AddTCs [split_type];
   5.168 -
   5.169 -Goalw [split_def]
   5.170 -  "u: A*B ==>   \
   5.171 -\       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
   5.172 -by Auto_tac;
   5.173 -qed "expand_split";
   5.174 -
   5.175 -
   5.176 -(*** split for predicates: result type o ***)
   5.177 -
   5.178 -Goalw [split_def] "R(a,b) ==> split(R, <a,b>)";
   5.179 -by (Asm_simp_tac 1);
   5.180 -qed "splitI";
   5.181 -
   5.182 -val major::sigma::prems = Goalw [split_def]
   5.183 -    "[| split(R,z);  z:Sigma(A,B);                      \
   5.184 -\       !!x y. [| z = <x,y>;  R(x,y) |] ==> P           \
   5.185 -\    |] ==> P";
   5.186 -by (rtac (sigma RS SigmaE) 1);
   5.187 -by (cut_facts_tac [major] 1);
   5.188 -by (REPEAT (ares_tac prems 1));
   5.189 -by (Asm_full_simp_tac 1);
   5.190 -qed "splitE";
   5.191 -
   5.192 -Goalw [split_def] "split(R,<a,b>) ==> R(a,b)";
   5.193 -by (Full_simp_tac 1);
   5.194 -qed "splitD";
     6.1 --- a/src/ZF/pair.thy	Sat Jun 22 18:28:46 2002 +0200
     6.2 +++ b/src/ZF/pair.thy	Sun Jun 23 10:14:13 2002 +0200
     6.3 @@ -1,5 +1,189 @@
     6.4 +(*  Title:      ZF/pair
     6.5 +    ID:         $Id$
     6.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 +    Copyright   1992  University of Cambridge
     6.8 +
     6.9 +Ordered pairs in Zermelo-Fraenkel Set Theory 
    6.10 +*)
    6.11 +
    6.12  theory pair = upair
    6.13  files "simpdata.ML":
    6.14 +
    6.15 +(** Lemmas for showing that <a,b> uniquely determines a and b **)
    6.16 +
    6.17 +lemma singleton_eq_iff [iff]: "{a} = {b} <-> a=b"
    6.18 +by (rule extension [THEN iff_trans], blast)
    6.19 +
    6.20 +lemma doubleton_eq_iff: "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
    6.21 +by (rule extension [THEN iff_trans], blast)
    6.22 +
    6.23 +lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
    6.24 +by (simp add: Pair_def doubleton_eq_iff, blast)
    6.25 +
    6.26 +lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, standard, elim!]
    6.27 +
    6.28 +lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1, standard]
    6.29 +lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2, standard]
    6.30 +
    6.31 +lemma Pair_not_0: "<a,b> ~= 0"
    6.32 +apply (unfold Pair_def)
    6.33 +apply (blast elim: equalityE)
    6.34 +done
    6.35 +
    6.36 +lemmas Pair_neq_0 = Pair_not_0 [THEN notE, standard, elim!]
    6.37 +
    6.38 +declare sym [THEN Pair_neq_0, elim!]
    6.39 +
    6.40 +lemma Pair_neq_fst: "<a,b>=a ==> P"
    6.41 +apply (unfold Pair_def)
    6.42 +apply (rule consI1 [THEN mem_asym, THEN FalseE])
    6.43 +apply (erule subst)
    6.44 +apply (rule consI1)
    6.45 +done
    6.46 +
    6.47 +lemma Pair_neq_snd: "<a,b>=b ==> P"
    6.48 +apply (unfold Pair_def)
    6.49 +apply (rule consI1 [THEN consI2, THEN mem_asym, THEN FalseE])
    6.50 +apply (erule subst)
    6.51 +apply (rule consI1 [THEN consI2])
    6.52 +done
    6.53 +
    6.54 +
    6.55 +(*** Sigma: Disjoint union of a family of sets
    6.56 +     Generalizes Cartesian product ***)
    6.57 +
    6.58 +lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
    6.59 +by (simp add: Sigma_def)
    6.60 +
    6.61 +lemma SigmaI [TC,intro!]: "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
    6.62 +by simp
    6.63 +
    6.64 +lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1, standard]
    6.65 +lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2, standard]
    6.66 +
    6.67 +(*The general elimination rule*)
    6.68 +lemma SigmaE [elim!]:
    6.69 +    "[| c: Sigma(A,B);   
    6.70 +        !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P  
    6.71 +     |] ==> P"
    6.72 +apply (unfold Sigma_def, blast) 
    6.73 +done
    6.74 +
    6.75 +lemma SigmaE2 [elim!]:
    6.76 +    "[| <a,b> : Sigma(A,B);     
    6.77 +        [| a:A;  b:B(a) |] ==> P    
    6.78 +     |] ==> P"
    6.79 +apply (unfold Sigma_def, blast) 
    6.80 +done
    6.81 +
    6.82 +lemma Sigma_cong:
    6.83 +    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>  
    6.84 +     Sigma(A,B) = Sigma(A',B')"
    6.85 +by (simp add: Sigma_def)
    6.86 +
    6.87 +(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
    6.88 +  flex-flex pairs and the "Check your prover" error.  Most
    6.89 +  Sigmas and Pis are abbreviated as * or -> *)
    6.90 +
    6.91 +lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
    6.92 +by blast
    6.93 +
    6.94 +lemma Sigma_empty2 [simp]: "A*0 = 0"
    6.95 +by blast
    6.96 +
    6.97 +lemma Sigma_empty_iff: "A*B=0 <-> A=0 | B=0"
    6.98 +by blast
    6.99 +
   6.100 +
   6.101 +(*** Projections: fst, snd ***)
   6.102 +
   6.103 +lemma fst_conv [simp]: "fst(<a,b>) = a"
   6.104 +by (simp add: fst_def, blast)
   6.105 +
   6.106 +lemma snd_conv [simp]: "snd(<a,b>) = b"
   6.107 +by (simp add: snd_def, blast)
   6.108 +
   6.109 +lemma fst_type [TC]: "p:Sigma(A,B) ==> fst(p) : A"
   6.110 +by auto
   6.111 +
   6.112 +lemma snd_type [TC]: "p:Sigma(A,B) ==> snd(p) : B(fst(p))"
   6.113 +by auto
   6.114 +
   6.115 +lemma Pair_fst_snd_eq: "a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
   6.116 +by auto
   6.117 +
   6.118 +
   6.119 +(*** Eliminator - split ***)
   6.120 +
   6.121 +(*A META-equality, so that it applies to higher types as well...*)
   6.122 +lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
   6.123 +by (simp add: split_def)
   6.124 +
   6.125 +lemma split_type [TC]:
   6.126 +    "[|  p:Sigma(A,B);    
   6.127 +         !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>)  
   6.128 +     |] ==> split(%x y. c(x,y), p) : C(p)"
   6.129 +apply (erule SigmaE, auto) 
   6.130 +done
   6.131 +
   6.132 +lemma expand_split: 
   6.133 +  "u: A*B ==>    
   6.134 +        R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"
   6.135 +apply (simp add: split_def, auto)
   6.136 +done
   6.137 +
   6.138 +
   6.139 +(*** split for predicates: result type o ***)
   6.140 +
   6.141 +lemma splitI: "R(a,b) ==> split(R, <a,b>)"
   6.142 +by (simp add: split_def)
   6.143 +
   6.144 +lemma splitE:
   6.145 +    "[| split(R,z);  z:Sigma(A,B);                       
   6.146 +        !!x y. [| z = <x,y>;  R(x,y) |] ==> P            
   6.147 +     |] ==> P"
   6.148 +apply (simp add: split_def)
   6.149 +apply (erule SigmaE, force) 
   6.150 +done
   6.151 +
   6.152 +lemma splitD: "split(R,<a,b>) ==> R(a,b)"
   6.153 +by (simp add: split_def)
   6.154 +
   6.155 +ML
   6.156 +{*
   6.157 +val singleton_eq_iff = thm "singleton_eq_iff";
   6.158 +val doubleton_eq_iff = thm "doubleton_eq_iff";
   6.159 +val Pair_iff = thm "Pair_iff";
   6.160 +val Pair_inject = thm "Pair_inject";
   6.161 +val Pair_inject1 = thm "Pair_inject1";
   6.162 +val Pair_inject2 = thm "Pair_inject2";
   6.163 +val Pair_not_0 = thm "Pair_not_0";
   6.164 +val Pair_neq_0 = thm "Pair_neq_0";
   6.165 +val Pair_neq_fst = thm "Pair_neq_fst";
   6.166 +val Pair_neq_snd = thm "Pair_neq_snd";
   6.167 +val Sigma_iff = thm "Sigma_iff";
   6.168 +val SigmaI = thm "SigmaI";
   6.169 +val SigmaD1 = thm "SigmaD1";
   6.170 +val SigmaD2 = thm "SigmaD2";
   6.171 +val SigmaE = thm "SigmaE";
   6.172 +val SigmaE2 = thm "SigmaE2";
   6.173 +val Sigma_cong = thm "Sigma_cong";
   6.174 +val Sigma_empty1 = thm "Sigma_empty1";
   6.175 +val Sigma_empty2 = thm "Sigma_empty2";
   6.176 +val Sigma_empty_iff = thm "Sigma_empty_iff";
   6.177 +val fst_conv = thm "fst_conv";
   6.178 +val snd_conv = thm "snd_conv";
   6.179 +val fst_type = thm "fst_type";
   6.180 +val snd_type = thm "snd_type";
   6.181 +val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
   6.182 +val split = thm "split";
   6.183 +val split_type = thm "split_type";
   6.184 +val expand_split = thm "expand_split";
   6.185 +val splitI = thm "splitI";
   6.186 +val splitE = thm "splitE";
   6.187 +val splitD = thm "splitD";
   6.188 +*}
   6.189 +
   6.190  end
   6.191  
   6.192