src/ZF/pair.ML
 changeset 5325 f7a5e06adea1 parent 5264 7538fce1fe37 child 5505 b0856ff6fc69
equal inserted replaced
`     6 Ordered pairs in Zermelo-Fraenkel Set Theory `
`     6 Ordered pairs in Zermelo-Fraenkel Set Theory `
`     7 *)`
`     7 *)`
`     8 `
`     8 `
`     9 (** Lemmas for showing that <a,b> uniquely determines a and b **)`
`     9 (** Lemmas for showing that <a,b> uniquely determines a and b **)`
`    10 `
`    10 `
`    11 qed_goal "singleton_eq_iff" ZF.thy`
`    11 qed_goal "singleton_eq_iff" thy`
`    12     "{a} = {b} <-> a=b"`
`    12     "{a} = {b} <-> a=b"`
`    13  (fn _=> [ (resolve_tac [extension RS iff_trans] 1),`
`    13  (fn _=> [ (resolve_tac [extension RS iff_trans] 1),`
`    14            (Blast_tac 1) ]);`
`    14            (Blast_tac 1) ]);`
`    15 `
`    15 `
`    16 qed_goal "doubleton_eq_iff" ZF.thy`
`    16 qed_goal "doubleton_eq_iff" thy`
`    17     "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"`
`    17     "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"`
`    18  (fn _=> [ (resolve_tac [extension RS iff_trans] 1),`
`    18  (fn _=> [ (resolve_tac [extension RS iff_trans] 1),`
`    19            (Blast_tac 1) ]);`
`    19            (Blast_tac 1) ]);`
`    20 `
`    20 `
`    21 qed_goalw "Pair_iff" ZF.thy [Pair_def]`
`    21 qed_goalw "Pair_iff" thy [Pair_def]`
`    22     "<a,b> = <c,d> <-> a=c & b=d"`
`    22     "<a,b> = <c,d> <-> a=c & b=d"`
`    23  (fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1),`
`    23  (fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1),`
`    24            (Blast_tac 1) ]);`
`    24            (Blast_tac 1) ]);`
`    25 `
`    25 `
`    26 Addsimps [Pair_iff];`
`    26 Addsimps [Pair_iff];`
`    30 AddSEs [Pair_inject];`
`    30 AddSEs [Pair_inject];`
`    31 `
`    31 `
`    32 bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1);`
`    32 bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1);`
`    33 bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2);`
`    33 bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2);`
`    34 `
`    34 `
`    35 qed_goalw "Pair_not_0" ZF.thy [Pair_def] "<a,b> ~= 0"`
`    35 qed_goalw "Pair_not_0" thy [Pair_def] "<a,b> ~= 0"`
`    36  (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);`
`    36  (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);`
`    37 `
`    37 `
`    38 bind_thm ("Pair_neq_0", Pair_not_0 RS notE);`
`    38 bind_thm ("Pair_neq_0", Pair_not_0 RS notE);`
`    39 `
`    39 `
`    40 AddSEs [Pair_neq_0, sym RS Pair_neq_0];`
`    40 AddSEs [Pair_neq_0, sym RS Pair_neq_0];`
`    41 `
`    41 `
`    42 qed_goalw "Pair_neq_fst" ZF.thy [Pair_def] "<a,b>=a ==> P"`
`    42 qed_goalw "Pair_neq_fst" thy [Pair_def] "<a,b>=a ==> P"`
`    43  (fn [major]=>`
`    43  (fn [major]=>`
`    44   [ (rtac (consI1 RS mem_asym RS FalseE) 1),`
`    44   [ (rtac (consI1 RS mem_asym RS FalseE) 1),`
`    45     (rtac (major RS subst) 1),`
`    45     (rtac (major RS subst) 1),`
`    46     (rtac consI1 1) ]);`
`    46     (rtac consI1 1) ]);`
`    47 `
`    47 `
`    48 qed_goalw "Pair_neq_snd" ZF.thy [Pair_def] "<a,b>=b ==> P"`
`    48 qed_goalw "Pair_neq_snd" thy [Pair_def] "<a,b>=b ==> P"`
`    49  (fn [major]=>`
`    49  (fn [major]=>`
`    50   [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),`
`    50   [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),`
`    51     (rtac (major RS subst) 1),`
`    51     (rtac (major RS subst) 1),`
`    52     (rtac (consI1 RS consI2) 1) ]);`
`    52     (rtac (consI1 RS consI2) 1) ]);`
`    53 `
`    53 `
`    54 `
`    54 `
`    55 (*** Sigma: Disjoint union of a family of sets`
`    55 (*** Sigma: Disjoint union of a family of sets`
`    56      Generalizes Cartesian product ***)`
`    56      Generalizes Cartesian product ***)`
`    57 `
`    57 `
`    58 qed_goalw "Sigma_iff" ZF.thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"`
`    58 qed_goalw "Sigma_iff" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"`
`    59  (fn _ => [ Blast_tac 1 ]);`
`    59  (fn _ => [ Blast_tac 1 ]);`
`    60 `
`    60 `
`    61 Addsimps [Sigma_iff];`
`    61 Addsimps [Sigma_iff];`
`    62 `
`    62 `
`    63 qed_goal "SigmaI" ZF.thy`
`    63 qed_goal "SigmaI" thy`
`    64     "!!a b. [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"`
`    64     "!!a b. [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"`
`    65  (fn _ => [ Asm_simp_tac 1 ]);`
`    65  (fn _ => [ Asm_simp_tac 1 ]);`
`    66 `
`    66 `
`    67 bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1);`
`    67 bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1);`
`    68 bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);`
`    68 bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);`
`    69 `
`    69 `
`    70 (*The general elimination rule*)`
`    70 (*The general elimination rule*)`
`    71 qed_goalw "SigmaE" ZF.thy [Sigma_def]`
`    71 qed_goalw "SigmaE" thy [Sigma_def]`
`    72     "[| c: Sigma(A,B);  \`
`    72     "[| c: Sigma(A,B);  \`
`    73 \       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \`
`    73 \       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \`
`    74 \    |] ==> P"`
`    74 \    |] ==> P"`
`    75  (fn major::prems=>`
`    75  (fn major::prems=>`
`    76   [ (cut_facts_tac [major] 1),`
`    76   [ (cut_facts_tac [major] 1),`
`    77     (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);`
`    77     (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);`
`    78 `
`    78 `
`    79 qed_goal "SigmaE2" ZF.thy`
`    79 qed_goal "SigmaE2" thy`
`    80     "[| <a,b> : Sigma(A,B);    \`
`    80     "[| <a,b> : Sigma(A,B);    \`
`    81 \       [| a:A;  b:B(a) |] ==> P   \`
`    81 \       [| a:A;  b:B(a) |] ==> P   \`
`    82 \    |] ==> P"`
`    82 \    |] ==> P"`
`    83  (fn [major,minor]=>`
`    83  (fn [major,minor]=>`
`    84   [ (rtac minor 1),`
`    84   [ (rtac minor 1),`
`    85     (rtac (major RS SigmaD1) 1),`
`    85     (rtac (major RS SigmaD1) 1),`
`    86     (rtac (major RS SigmaD2) 1) ]);`
`    86     (rtac (major RS SigmaD2) 1) ]);`
`    87 `
`    87 `
`    88 qed_goalw "Sigma_cong" ZF.thy [Sigma_def]`
`    88 qed_goalw "Sigma_cong" thy [Sigma_def]`
`    89     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \`
`    89     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \`
`    90 \    Sigma(A,B) = Sigma(A',B')"`
`    90 \    Sigma(A,B) = Sigma(A',B')"`
`    91  (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);`
`    91  (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);`
`    92 `
`    92 `
`    93 `
`    93 `
`    96   Sigmas and Pis are abbreviated as * or -> *)`
`    96   Sigmas and Pis are abbreviated as * or -> *)`
`    97 `
`    97 `
`    98 AddSIs [SigmaI];`
`    98 AddSIs [SigmaI];`
`    99 AddSEs [SigmaE2, SigmaE];`
`    99 AddSEs [SigmaE2, SigmaE];`
`   100 `
`   100 `
`   101 qed_goal "Sigma_empty1" ZF.thy "Sigma(0,B) = 0"`
`   101 qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0"`
`   102  (fn _ => [ (Blast_tac 1) ]);`
`   102  (fn _ => [ (Blast_tac 1) ]);`
`   103 `
`   103 `
`   104 qed_goal "Sigma_empty2" ZF.thy "A*0 = 0"`
`   104 qed_goal "Sigma_empty2" thy "A*0 = 0"`
`   105  (fn _ => [ (Blast_tac 1) ]);`
`   105  (fn _ => [ (Blast_tac 1) ]);`
`   106 `
`   106 `
`   107 Addsimps [Sigma_empty1, Sigma_empty2];`
`   107 Addsimps [Sigma_empty1, Sigma_empty2];`
`   108 `
`   108 `
`   109 Goal "A*B=0 <-> A=0 | B=0";`
`   109 Goal "A*B=0 <-> A=0 | B=0";`
`   111 qed "Sigma_empty_iff";`
`   111 qed "Sigma_empty_iff";`
`   112 `
`   112 `
`   113 `
`   113 `
`   114 (*** Projections: fst, snd ***)`
`   114 (*** Projections: fst, snd ***)`
`   115 `
`   115 `
`   116 qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a"`
`   116 qed_goalw "fst_conv" thy [fst_def] "fst(<a,b>) = a"`
`   117  (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);`
`   117  (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);`
`   118 `
`   118 `
`   119 qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b"`
`   119 qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b"`
`   120  (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);`
`   120  (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);`
`   121 `
`   121 `
`   122 Addsimps [fst_conv,snd_conv];`
`   122 Addsimps [fst_conv,snd_conv];`
`   123 `
`   123 `
`   124 qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"`
`   124 qed_goal "fst_type" thy "!!p. p:Sigma(A,B) ==> fst(p) : A"`
`   125  (fn _=> [ Auto_tac ]);`
`   125  (fn _=> [ Auto_tac ]);`
`   126 `
`   126 `
`   127 qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"`
`   127 qed_goal "snd_type" thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"`
`   128  (fn _=> [ Auto_tac ]);`
`   128  (fn _=> [ Auto_tac ]);`
`   129 `
`   129 `
`   130 qed_goal "Pair_fst_snd_eq" ZF.thy`
`   130 qed_goal "Pair_fst_snd_eq" thy`
`   131     "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"`
`   131     "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"`
`   132  (fn _=> [ Auto_tac ]);`
`   132  (fn _=> [ Auto_tac ]);`
`   133 `
`   133 `
`   134 `
`   134 `
`   135 (*** Eliminator - split ***)`
`   135 (*** Eliminator - split ***)`
`   136 `
`   136 `
`   137 (*A META-equality, so that it applies to higher types as well...*)`
`   137 (*A META-equality, so that it applies to higher types as well...*)`
`   138 qed_goalw "split" ZF.thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"`
`   138 qed_goalw "split" thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"`
`   139  (fn _ => [ (Simp_tac 1),`
`   139  (fn _ => [ (Simp_tac 1),`
`   140             (rtac reflexive_thm 1) ]);`
`   140             (rtac reflexive_thm 1) ]);`
`   141 `
`   141 `
`   142 Addsimps [split];`
`   142 Addsimps [split];`
`   143 `
`   143 `
`   144 qed_goal "split_type" ZF.thy`
`   144 qed_goal "split_type" thy`
`   145     "[|  p:Sigma(A,B);   \`
`   145     "[|  p:Sigma(A,B);   \`
`   146 \        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \`
`   146 \        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \`
`   147 \    |] ==> split(%x y. c(x,y), p) : C(p)"`
`   147 \    |] ==> split(%x y. c(x,y), p) : C(p)"`
`   148  (fn major::prems=>`
`   148  (fn major::prems=>`
`   149   [ (rtac (major RS SigmaE) 1),`
`   149   [ (rtac (major RS SigmaE) 1),`
`   150     (asm_simp_tac (simpset() addsimps prems) 1) ]);`
`   150     (asm_simp_tac (simpset() addsimps prems) 1) ]);`
`   151 `
`   151 `
`   152 goalw ZF.thy [split_def]`
`   152 Goalw [split_def]`
`   153   "!!u. u: A*B ==>   \`
`   153   "u: A*B ==>   \`
`   154 \       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";`
`   154 \       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";`
`   155 by Auto_tac;`
`   155 by Auto_tac;`
`   156 qed "expand_split";`
`   156 qed "expand_split";`
`   157 `
`   157 `
`   158 `
`   158 `
`   159 (*** split for predicates: result type o ***)`
`   159 (*** split for predicates: result type o ***)`
`   160 `
`   160 `
`   161 goalw ZF.thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)";`
`   161 Goalw [split_def] "R(a,b) ==> split(R, <a,b>)";`
`   162 by (Asm_simp_tac 1);`
`   162 by (Asm_simp_tac 1);`
`   163 qed "splitI";`
`   163 qed "splitI";`
`   164 `
`   164 `
`   165 val major::sigma::prems = goalw ZF.thy [split_def]`
`   165 val major::sigma::prems = Goalw [split_def]`
`   166     "[| split(R,z);  z:Sigma(A,B);                      \`
`   166     "[| split(R,z);  z:Sigma(A,B);                      \`
`   167 \       !!x y. [| z = <x,y>;  R(x,y) |] ==> P           \`
`   167 \       !!x y. [| z = <x,y>;  R(x,y) |] ==> P           \`
`   168 \    |] ==> P";`
`   168 \    |] ==> P";`
`   169 by (rtac (sigma RS SigmaE) 1);`
`   169 by (rtac (sigma RS SigmaE) 1);`
`   170 by (cut_facts_tac [major] 1);`
`   170 by (cut_facts_tac [major] 1);`
`   171 by (REPEAT (ares_tac prems 1));`
`   171 by (REPEAT (ares_tac prems 1));`
`   172 by (Asm_full_simp_tac 1);`
`   172 by (Asm_full_simp_tac 1);`
`   173 qed "splitE";`
`   173 qed "splitE";`
`   174 `
`   174 `
`   175 goalw ZF.thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)";`
`   175 Goalw [split_def] "split(R,<a,b>) ==> R(a,b)";`
`   176 by (Full_simp_tac 1);`
`   176 by (Full_simp_tac 1);`
`   177 qed "splitD";`
`   177 qed "splitD";`
`   178 `
`   178 `
`   179 `
`   179 `
`   180 `
`   180 `