Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Sprod0.ML
changeset 9245 428385c4bc50
parent 4833 2e53109d4bc8
child 9248 e1dee89de037
equal deleted inserted replaced
9244:7edd3e5f26d4 9245:428385c4bc50 
     1 (*  Title:      HOLCF/sprod0.thy
 
     1 (*  Title:      HOLCF/Sprod0
 
     2     ID:         $Id$
 
     2     ID:         $Id$
 
     3     Author:     Franz Regensburger
 
     3     Author:     Franz Regensburger
 
     4     Copyright   1993  Technische Universitaet Muenchen
 
     4     Copyright   1993  Technische Universitaet Muenchen
 
     5 
     5 
     6 Lemmas for theory sprod0.thy
 
     6 Strict product with typedef.
 
     7 *)
 
     7 *)
 
     8 
     8 
     9 open Sprod0;
 
       
    10 
       
    11 (* ------------------------------------------------------------------------ *)
 
     9 (* ------------------------------------------------------------------------ *)
 
    12 (* A non-emptyness result for Sprod                                         *)
 
    10 (* A non-emptyness result for Sprod                                         *)
 
    13 (* ------------------------------------------------------------------------ *)
 
    11 (* ------------------------------------------------------------------------ *)
 
    14 
    12 
    15 qed_goalw "SprodI" Sprod0.thy [Sprod_def]
 
    13 val prems = goalw Sprod0.thy [Sprod_def]
 
    16         "(Spair_Rep a b):Sprod"
 
    14         "(Spair_Rep a b):Sprod";
 
    17 (fn prems =>
 
    15 by (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl]);
 
    18         [
 
    16 qed "SprodI";
 
    19         (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl])
 
    17 
    20         ]);
 
    18 val prems = goal Sprod0.thy 
    21 
    19         "inj_on Abs_Sprod Sprod";
 
    22 qed_goal "inj_on_Abs_Sprod" Sprod0.thy 
    20 by (rtac inj_on_inverseI 1);
 
    23         "inj_on Abs_Sprod Sprod"
 
    21 by (etac Abs_Sprod_inverse 1);
 
    24 (fn prems =>
 
    22 qed "inj_on_Abs_Sprod";
 
    25         [
 
       
    26         (rtac inj_on_inverseI 1),
 
       
    27         (etac Abs_Sprod_inverse 1)
 
       
    28         ]);
 
       
    29 
    23 
    30 (* ------------------------------------------------------------------------ *)
 
    24 (* ------------------------------------------------------------------------ *)
 
    31 (* Strictness and definedness of Spair_Rep                                  *)
 
    25 (* Strictness and definedness of Spair_Rep                                  *)
 
    32 (* ------------------------------------------------------------------------ *)
 
    26 (* ------------------------------------------------------------------------ *)
 
    33 
    27 
    34 qed_goalw "strict_Spair_Rep" Sprod0.thy [Spair_Rep_def]
 
    28 val prems = goalw Sprod0.thy [Spair_Rep_def]
 
    35  "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
 
    29  "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)";
 
    36  (fn prems =>
 
    30 by (cut_facts_tac prems 1);
 
    37         [
 
    31 by (rtac ext 1);
 
    38         (cut_facts_tac prems 1),
 
    32 by (rtac ext 1);
 
    39         (rtac ext 1),
 
    33 by (rtac iffI 1);
 
    40         (rtac ext 1),
 
    34 by (fast_tac HOL_cs 1);
 
    41         (rtac iffI 1),
 
    35 by (fast_tac HOL_cs 1);
 
    42         (fast_tac HOL_cs 1),
 
    36 qed "strict_Spair_Rep";
 
    43         (fast_tac HOL_cs 1)
 
    37 
    44         ]);
 
    38 val prems = goalw Sprod0.thy [Spair_Rep_def]
 
    45 
    39  "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)";
 
    46 qed_goalw "defined_Spair_Rep_rev" Sprod0.thy [Spair_Rep_def]
 
    40 by (case_tac "a=UU|b=UU" 1);
 
    47  "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
 
    41 by (atac 1);
 
    48  (fn prems =>
 
    42 by (rtac disjI1 1);
 
    49         [
 
    43 by (rtac ((hd prems) RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1);
 
    50         (case_tac "a=UU|b=UU" 1),
 
    44 by (fast_tac HOL_cs 1);
 
    51         (atac 1),
 
    45 by (fast_tac HOL_cs 1);
 
    52         (rtac disjI1 1),
 
    46 qed "defined_Spair_Rep_rev";
 
    53         (rtac ((hd prems) RS fun_cong RS fun_cong RS iffD2 RS mp RS 
       
    54         conjunct1 RS sym) 1),
 
       
    55         (fast_tac HOL_cs 1),
 
       
    56         (fast_tac HOL_cs 1)
 
       
    57         ]);
 
       
    58 
       
    59 
    47 
    60 (* ------------------------------------------------------------------------ *)
 
    48 (* ------------------------------------------------------------------------ *)
 
    61 (* injectivity of Spair_Rep and Ispair                                      *)
 
    49 (* injectivity of Spair_Rep and Ispair                                      *)
 
    62 (* ------------------------------------------------------------------------ *)
 
    50 (* ------------------------------------------------------------------------ *)
 
    63 
    51 
    64 qed_goalw "inject_Spair_Rep" Sprod0.thy [Spair_Rep_def]
 
    52 val prems = goalw Sprod0.thy [Spair_Rep_def]
 
    65 "[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
 
    53 "[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba";
 
    66  (fn prems =>
 
    54 by (cut_facts_tac prems 1);
 
    67         [
 
    55 by (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS iffD1 RS mp) 1);
 
    68         (cut_facts_tac prems 1),
 
    56 by (fast_tac HOL_cs 1);
 
    69         (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong 
    57 by (fast_tac HOL_cs 1);
 
    70                 RS iffD1 RS mp) 1),
 
    58 qed "inject_Spair_Rep";
 
    71         (fast_tac HOL_cs 1),
 
    59 
    72         (fast_tac HOL_cs 1)
 
    60 
    73         ]);
 
    61 val prems = goalw Sprod0.thy [Ispair_def]
 
    74 
    62         "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba";
 
    75 
    63 by (cut_facts_tac prems 1);
 
    76 qed_goalw "inject_Ispair" Sprod0.thy [Ispair_def]
 
    64 by (etac inject_Spair_Rep 1);
 
    77         "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"
 
    65 by (atac 1);
 
    78 (fn prems =>
 
    66 by (etac (inj_on_Abs_Sprod  RS inj_onD) 1);
 
    79         [
 
    67 by (rtac SprodI 1);
 
    80         (cut_facts_tac prems 1),
 
    68 by (rtac SprodI 1);
 
    81         (etac inject_Spair_Rep 1),
 
    69 qed "inject_Ispair";
 
    82         (atac 1),
 
       
    83         (etac (inj_on_Abs_Sprod  RS inj_onD) 1),
 
       
    84         (rtac SprodI 1),
 
       
    85         (rtac SprodI 1)
 
       
    86         ]);
 
       
    87 
    70 
    88 
    71 
    89 (* ------------------------------------------------------------------------ *)
 
    72 (* ------------------------------------------------------------------------ *)
 
    90 (* strictness and definedness of Ispair                                     *)
 
    73 (* strictness and definedness of Ispair                                     *)
 
    91 (* ------------------------------------------------------------------------ *)
 
    74 (* ------------------------------------------------------------------------ *)
 
    92 
    75 
    93 qed_goalw "strict_Ispair" Sprod0.thy [Ispair_def] 
    76 val prems = goalw Sprod0.thy [Ispair_def] 
    94  "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
 
    77  "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU";
 
    95 (fn prems =>
 
    78 by (cut_facts_tac prems 1);
 
    96         [
 
    79 by (etac (strict_Spair_Rep RS arg_cong) 1);
 
    97         (cut_facts_tac prems 1),
 
    80 qed "strict_Ispair";
 
    98         (etac (strict_Spair_Rep RS arg_cong) 1)
 
    81 
    99         ]);
 
    82 val prems = goalw Sprod0.thy [Ispair_def]
 
   100 
    83         "Ispair UU b  = Ispair UU UU";
 
   101 qed_goalw "strict_Ispair1" Sprod0.thy [Ispair_def]
 
    84 by (rtac (strict_Spair_Rep RS arg_cong) 1);
 
   102         "Ispair UU b  = Ispair UU UU"
 
    85 by (rtac disjI1 1);
 
   103 (fn prems =>
 
    86 by (rtac refl 1);
 
   104         [
 
    87 qed "strict_Ispair1";
 
   105         (rtac (strict_Spair_Rep RS arg_cong) 1),
 
    88 
   106         (rtac disjI1 1),
 
    89 val prems = goalw Sprod0.thy [Ispair_def]
 
   107         (rtac refl 1)
 
    90         "Ispair a UU = Ispair UU UU";
 
   108         ]);
 
    91 by (rtac (strict_Spair_Rep RS arg_cong) 1);
 
   109 
    92 by (rtac disjI2 1);
 
   110 qed_goalw "strict_Ispair2" Sprod0.thy [Ispair_def]
 
    93 by (rtac refl 1);
 
   111         "Ispair a UU = Ispair UU UU"
 
    94 qed "strict_Ispair2";
 
   112 (fn prems =>
 
    95 
   113         [
 
    96 val prems = goal Sprod0.thy 
   114         (rtac (strict_Spair_Rep RS arg_cong) 1),
 
    97         "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU";
 
   115         (rtac disjI2 1),
 
    98 by (cut_facts_tac prems 1);
 
   116         (rtac refl 1)
 
    99 by (rtac (de_Morgan_disj RS subst) 1);
 
   117         ]);
 
   100 by (etac contrapos 1);
 
   118 
   101 by (etac strict_Ispair 1);
 
   119 qed_goal "strict_Ispair_rev" Sprod0.thy 
   102 qed "strict_Ispair_rev";
 
   120         "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
 
   103 
   121 (fn prems =>
 
   104 val prems = goalw Sprod0.thy [Ispair_def]
 
   122         [
 
   105         "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)";
 
   123         (cut_facts_tac prems 1),
 
   106 by (cut_facts_tac prems 1);
 
   124         (rtac (de_Morgan_disj RS subst) 1),
 
   107 by (rtac defined_Spair_Rep_rev 1);
 
   125         (etac contrapos 1),
 
   108 by (rtac (inj_on_Abs_Sprod  RS inj_onD) 1);
 
   126         (etac strict_Ispair 1)
 
   109 by (atac 1);
 
   127         ]);
 
   110 by (rtac SprodI 1);
 
   128 
   111 by (rtac SprodI 1);
 
   129 qed_goalw "defined_Ispair_rev" Sprod0.thy [Ispair_def]
 
   112 qed "defined_Ispair_rev";
 
   130         "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)"
 
   113 
   131 (fn prems =>
 
   114 val prems = goal Sprod0.thy  
   132         [
 
   115 "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)";
 
   133         (cut_facts_tac prems 1),
 
   116 by (cut_facts_tac prems 1);
 
   134         (rtac defined_Spair_Rep_rev 1),
 
   117 by (rtac contrapos 1);
 
   135         (rtac (inj_on_Abs_Sprod  RS inj_onD) 1),
 
   118 by (etac defined_Ispair_rev 2);
 
   136         (atac 1),
 
   119 by (rtac (de_Morgan_disj RS iffD2) 1);
 
   137         (rtac SprodI 1),
 
   120 by (etac conjI 1);
 
   138         (rtac SprodI 1)
 
   121 by (atac 1);
 
   139         ]);
 
   122 qed "defined_Ispair";
 
   140 
       
   141 qed_goal "defined_Ispair" Sprod0.thy  
       
   142 "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)" 
       
   143 (fn prems =>
 
       
   144         [
 
       
   145         (cut_facts_tac prems 1),
 
       
   146         (rtac contrapos 1),
 
       
   147         (etac defined_Ispair_rev 2),
 
       
   148         (rtac (de_Morgan_disj RS iffD2) 1),
 
       
   149         (etac conjI 1),
 
       
   150         (atac 1)
 
       
   151         ]);
 
       
   152 
   123 
   153 
   124 
   154 (* ------------------------------------------------------------------------ *)
 
   125 (* ------------------------------------------------------------------------ *)
 
   155 (* Exhaustion of the strict product **                                      *)
 
   126 (* Exhaustion of the strict product **                                      *)
 
   156 (* ------------------------------------------------------------------------ *)
 
   127 (* ------------------------------------------------------------------------ *)
 
   157 
   128 
   158 qed_goalw "Exh_Sprod" Sprod0.thy [Ispair_def]
 
   129 val prems = goalw Sprod0.thy [Ispair_def]
 
   159         "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
 
   130         "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)";
 
   160 (fn prems =>
 
   131 by (rtac (rewrite_rule [Sprod_def] Rep_Sprod RS CollectE) 1);
 
   161         [
 
   132 by (etac exE 1);
 
   162         (rtac (rewrite_rule [Sprod_def] Rep_Sprod RS CollectE) 1),
 
   133 by (etac exE 1);
 
   163         (etac exE 1),
 
   134 by (rtac (excluded_middle RS disjE) 1);
 
   164         (etac exE 1),
 
   135 by (rtac disjI2 1);
 
   165         (rtac (excluded_middle RS disjE) 1),
 
   136 by (rtac exI 1);
 
   166         (rtac disjI2 1),
 
   137 by (rtac exI 1);
 
   167         (rtac exI 1),
 
   138 by (rtac conjI 1);
 
   168         (rtac exI 1),
 
   139 by (rtac (Rep_Sprod_inverse RS sym RS trans) 1);
 
   169         (rtac conjI 1),
 
   140 by (etac arg_cong 1);
 
   170         (rtac (Rep_Sprod_inverse RS sym RS trans) 1),
 
   141 by (rtac (de_Morgan_disj RS subst) 1);
 
   171         (etac arg_cong 1),
 
   142 by (atac 1);
 
   172         (rtac (de_Morgan_disj RS subst) 1),
 
   143 by (rtac disjI1 1);
 
   173         (atac 1),
 
   144 by (rtac (Rep_Sprod_inverse RS sym RS trans) 1);
 
   174         (rtac disjI1 1),
 
   145 by (res_inst_tac [("f","Abs_Sprod")] arg_cong 1);
 
   175         (rtac (Rep_Sprod_inverse RS sym RS trans) 1),
 
   146 by (etac trans 1);
 
   176         (res_inst_tac [("f","Abs_Sprod")] arg_cong 1),
 
   147 by (etac strict_Spair_Rep 1);
 
   177         (etac trans 1),
 
   148 qed "Exh_Sprod";
 
   178         (etac strict_Spair_Rep 1)
 
       
   179         ]);
 
       
   180 
   149 
   181 (* ------------------------------------------------------------------------ *)
 
   150 (* ------------------------------------------------------------------------ *)
 
   182 (* general elimination rule for strict product                              *)
 
   151 (* general elimination rule for strict product                              *)
 
   183 (* ------------------------------------------------------------------------ *)
 
   152 (* ------------------------------------------------------------------------ *)
 
   184 
   153 
   185 qed_goal "IsprodE" Sprod0.thy
 
   154 val prems = goal Sprod0.thy
 
   186 "[|p=Ispair UU UU ==> Q ;!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q|] ==> Q"
 
   155 "[|p=Ispair UU UU ==> Q ;!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q|] ==> Q";
 
   187 (fn prems =>
 
   156 by (rtac (Exh_Sprod RS disjE) 1);
 
   188         [
 
   157 by (etac (hd prems) 1);
 
   189         (rtac (Exh_Sprod RS disjE) 1),
 
   158 by (etac exE 1);
 
   190         (etac (hd prems) 1),
 
   159 by (etac exE 1);
 
   191         (etac exE 1),
 
   160 by (etac conjE 1);
 
   192         (etac exE 1),
 
   161 by (etac conjE 1);
 
   193         (etac conjE 1),
 
   162 by (etac (hd (tl prems)) 1);
 
   194         (etac conjE 1),
 
   163 by (atac 1);
 
   195         (etac (hd (tl prems)) 1),
 
   164 by (atac 1);
 
   196         (atac 1),
 
   165 qed "IsprodE";
 
   197         (atac 1)
 
       
   198         ]);
 
       
   199 
   166 
   200 
   167 
   201 (* ------------------------------------------------------------------------ *)
 
   168 (* ------------------------------------------------------------------------ *)
 
   202 (* some results about the selectors Isfst, Issnd                            *)
 
   169 (* some results about the selectors Isfst, Issnd                            *)
 
   203 (* ------------------------------------------------------------------------ *)
 
   170 (* ------------------------------------------------------------------------ *)
 
   204 
   171 
   205 qed_goalw "strict_Isfst" Sprod0.thy [Isfst_def] 
   172 val prems = goalw Sprod0.thy [Isfst_def] 
   206         "p=Ispair UU UU ==> Isfst p = UU"
 
   173         "p=Ispair UU UU ==> Isfst p = UU";
 
   207 (fn prems =>
 
   174 by (cut_facts_tac prems 1);
 
   208         [
 
   175 by (rtac select_equality 1);
 
   209         (cut_facts_tac prems 1),
 
   176 by (rtac conjI 1);
 
   210         (rtac select_equality 1),
 
   177 by (fast_tac HOL_cs  1);
 
   211         (rtac conjI 1),
 
   178 by (strip_tac 1);
 
   212         (fast_tac HOL_cs  1),
 
   179 by (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1);
 
   213         (strip_tac 1),
 
   180 by (rtac not_sym 1);
 
   214         (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1),
 
   181 by (rtac defined_Ispair 1);
 
   215         (rtac not_sym 1),
 
   182 by (REPEAT (fast_tac HOL_cs  1));
 
   216         (rtac defined_Ispair 1),
 
   183 qed "strict_Isfst";
 
   217         (REPEAT (fast_tac HOL_cs  1))
 
   184 
   218         ]);
 
   185 
   219 
   186 val prems = goal Sprod0.thy
 
   220 
   187         "Isfst(Ispair UU y) = UU";
 
   221 qed_goal "strict_Isfst1" Sprod0.thy
 
   188 by (stac strict_Ispair1 1);
 
   222         "Isfst(Ispair UU y) = UU"
 
   189 by (rtac strict_Isfst 1);
 
   223 (fn prems =>
 
   190 by (rtac refl 1);
 
   224         [
 
   191 qed "strict_Isfst1";
 
   225         (stac strict_Ispair1 1),
 
   192 
   226         (rtac strict_Isfst 1),
 
   193 val prems = goal Sprod0.thy
 
   227         (rtac refl 1)
 
   194         "Isfst(Ispair x UU) = UU";
 
   228         ]);
 
   195 by (stac strict_Ispair2 1);
 
   229 
   196 by (rtac strict_Isfst 1);
 
   230 qed_goal "strict_Isfst2" Sprod0.thy
 
   197 by (rtac refl 1);
 
   231         "Isfst(Ispair x UU) = UU"
 
   198 qed "strict_Isfst2";
 
   232 (fn prems =>
 
   199 
   233         [
 
   200 
   234         (stac strict_Ispair2 1),
 
   201 val prems = goalw Sprod0.thy [Issnd_def] 
   235         (rtac strict_Isfst 1),
 
   202         "p=Ispair UU UU ==>Issnd p=UU";
 
   236         (rtac refl 1)
 
   203 by (cut_facts_tac prems 1);
 
   237         ]);
 
   204 by (rtac select_equality 1);
 
   238 
   205 by (rtac conjI 1);
 
   239 
   206 by (fast_tac HOL_cs  1);
 
   240 qed_goalw "strict_Issnd" Sprod0.thy [Issnd_def] 
   207 by (strip_tac 1);
 
   241         "p=Ispair UU UU ==>Issnd p=UU"
 
   208 by (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1);
 
   242 (fn prems =>
 
   209 by (rtac not_sym 1);
 
   243         [
 
   210 by (rtac defined_Ispair 1);
 
   244         (cut_facts_tac prems 1),
 
   211 by (REPEAT (fast_tac HOL_cs  1));
 
   245         (rtac select_equality 1),
 
   212 qed "strict_Issnd";
 
   246         (rtac conjI 1),
 
   213 
   247         (fast_tac HOL_cs  1),
 
   214 val prems = goal Sprod0.thy
 
   248         (strip_tac 1),
 
   215         "Issnd(Ispair UU y) = UU";
 
   249         (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1),
 
   216 by (stac strict_Ispair1 1);
 
   250         (rtac not_sym 1),
 
   217 by (rtac strict_Issnd 1);
 
   251         (rtac defined_Ispair 1),
 
   218 by (rtac refl 1);
 
   252         (REPEAT (fast_tac HOL_cs  1))
 
   219 qed "strict_Issnd1";
 
   253         ]);
 
   220 
   254 
   221 val prems = goal Sprod0.thy
 
   255 qed_goal "strict_Issnd1" Sprod0.thy
 
   222         "Issnd(Ispair x UU) = UU";
 
   256         "Issnd(Ispair UU y) = UU"
 
   223 by (stac strict_Ispair2 1);
 
   257 (fn prems =>
 
   224 by (rtac strict_Issnd 1);
 
   258         [
 
   225 by (rtac refl 1);
 
   259         (stac strict_Ispair1 1),
 
   226 qed "strict_Issnd2";
 
   260         (rtac strict_Issnd 1),
 
   227 
   261         (rtac refl 1)
 
   228 val prems = goalw Sprod0.thy [Isfst_def]
 
   262         ]);
 
   229         "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x";
 
   263 
   230 by (cut_facts_tac prems 1);
 
   264 qed_goal "strict_Issnd2" Sprod0.thy
 
   231 by (rtac select_equality 1);
 
   265         "Issnd(Ispair x UU) = UU"
 
   232 by (rtac conjI 1);
 
   266 (fn prems =>
 
   233 by (strip_tac 1);
 
   267         [
 
   234 by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1);
 
   268         (stac strict_Ispair2 1),
 
   235 by (etac defined_Ispair 1);
 
   269         (rtac strict_Issnd 1),
 
   236 by (atac 1);
 
   270         (rtac refl 1)
 
   237 by (atac 1);
 
   271         ]);
 
   238 by (strip_tac 1);
 
   272 
   239 by (rtac (inject_Ispair RS conjunct1) 1);
 
   273 qed_goalw "Isfst" Sprod0.thy [Isfst_def]
 
   240 by (fast_tac HOL_cs  3);
 
   274         "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
 
   241 by (fast_tac HOL_cs  1);
 
   275 (fn prems =>
 
   242 by (fast_tac HOL_cs  1);
 
   276         [
 
   243 by (fast_tac HOL_cs  1);
 
   277         (cut_facts_tac prems 1),
 
   244 qed "Isfst";
 
   278         (rtac select_equality 1),
 
   245 
   279         (rtac conjI 1),
 
   246 val prems = goalw Sprod0.thy [Issnd_def]
 
   280         (strip_tac 1),
 
   247         "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y";
 
   281         (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
 
   248 by (cut_facts_tac prems 1);
 
   282         (etac defined_Ispair 1),
 
   249 by (rtac select_equality 1);
 
   283         (atac 1),
 
   250 by (rtac conjI 1);
 
   284         (atac 1),
 
   251 by (strip_tac 1);
 
   285         (strip_tac 1),
 
   252 by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1);
 
   286         (rtac (inject_Ispair RS conjunct1) 1),
 
   253 by (etac defined_Ispair 1);
 
   287         (fast_tac HOL_cs  3),
 
   254 by (atac 1);
 
   288         (fast_tac HOL_cs  1),
 
   255 by (atac 1);
 
   289         (fast_tac HOL_cs  1),
 
   256 by (strip_tac 1);
 
   290         (fast_tac HOL_cs  1)
 
   257 by (rtac (inject_Ispair RS conjunct2) 1);
 
   291         ]);
 
   258 by (fast_tac HOL_cs  3);
 
   292 
   259 by (fast_tac HOL_cs  1);
 
   293 qed_goalw "Issnd" Sprod0.thy [Issnd_def]
 
   260 by (fast_tac HOL_cs  1);
 
   294         "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
 
   261 by (fast_tac HOL_cs  1);
 
   295 (fn prems =>
 
   262 qed "Issnd";
 
   296         [
 
   263 
   297         (cut_facts_tac prems 1),
 
   264 val prems = goal Sprod0.thy "y~=UU ==>Isfst(Ispair x y)=x";
 
   298         (rtac select_equality 1),
 
   265 by (cut_facts_tac prems 1);
 
   299         (rtac conjI 1),
 
   266 by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1);
 
   300         (strip_tac 1),
 
   267 by (etac Isfst 1);
 
   301         (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
 
   268 by (atac 1);
 
   302         (etac defined_Ispair 1),
 
   269 by (hyp_subst_tac 1);
 
   303         (atac 1),
 
   270 by (rtac strict_Isfst1 1);
 
   304         (atac 1),
 
   271 qed "Isfst2";
 
   305         (strip_tac 1),
 
   272 
   306         (rtac (inject_Ispair RS conjunct2) 1),
 
   273 val prems = goal Sprod0.thy "~x=UU ==>Issnd(Ispair x y)=y";
 
   307         (fast_tac HOL_cs  3),
 
   274 by (cut_facts_tac prems 1);
 
   308         (fast_tac HOL_cs  1),
 
   275 by (res_inst_tac [("Q","y=UU")] (excluded_middle RS disjE) 1);
 
   309         (fast_tac HOL_cs  1),
 
   276 by (etac Issnd 1);
 
   310         (fast_tac HOL_cs  1)
 
   277 by (atac 1);
 
   311         ]);
 
   278 by (hyp_subst_tac 1);
 
   312 
   279 by (rtac strict_Issnd2 1);
 
   313 qed_goal "Isfst2" Sprod0.thy "y~=UU ==>Isfst(Ispair x y)=x"
 
   280 qed "Issnd2";
 
   314 (fn prems =>
 
       
   315         [
 
       
   316         (cut_facts_tac prems 1),
 
       
   317         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
 
       
   318         (etac Isfst 1),
 
       
   319         (atac 1),
 
       
   320         (hyp_subst_tac 1),
 
       
   321         (rtac strict_Isfst1 1)
 
       
   322         ]);
 
       
   323 
       
   324 qed_goal "Issnd2" Sprod0.thy "~x=UU ==>Issnd(Ispair x y)=y"
 
       
   325 (fn prems =>
 
       
   326         [
 
       
   327         (cut_facts_tac prems 1),
 
       
   328         (res_inst_tac [("Q","y=UU")] (excluded_middle RS disjE) 1),
 
       
   329         (etac Issnd 1),
 
       
   330         (atac 1),
 
       
   331         (hyp_subst_tac 1),
 
       
   332         (rtac strict_Issnd2 1)
 
       
   333         ]);
 
       
   334 
   281 
   335 
   282 
   336 (* ------------------------------------------------------------------------ *)
 
   283 (* ------------------------------------------------------------------------ *)
 
   337 (* instantiate the simplifier                                               *)
 
   284 (* instantiate the simplifier                                               *)
 
   338 (* ------------------------------------------------------------------------ *)
 
   285 (* ------------------------------------------------------------------------ *)
 
   340 val Sprod0_ss = 
   287 val Sprod0_ss = 
   341         HOL_ss 
   288         HOL_ss 
   342         addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
 
   289         addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
 
   343                  Isfst2,Issnd2];
 
   290                  Isfst2,Issnd2];
 
   344 
   291 
   345 qed_goal "defined_IsfstIssnd" Sprod0.thy 
   292 val prems = goal Sprod0.thy 
   346         "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
 
   293         "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU";
 
   347  (fn prems =>
 
   294 by (cut_facts_tac prems 1);
 
   348         [
 
   295 by (res_inst_tac [("p","p")] IsprodE 1);
 
   349         (cut_facts_tac prems 1),
 
   296 by (contr_tac 1);
 
   350         (res_inst_tac [("p","p")] IsprodE 1),
 
   297 by (hyp_subst_tac 1);
 
   351         (contr_tac 1),
 
   298 by (rtac conjI 1);
 
   352         (hyp_subst_tac 1),
 
   299 by (asm_simp_tac Sprod0_ss 1);
 
   353         (rtac conjI 1),
 
   300 by (asm_simp_tac Sprod0_ss 1);
 
   354         (asm_simp_tac Sprod0_ss 1),
 
   301 qed "defined_IsfstIssnd";
 
   355         (asm_simp_tac Sprod0_ss 1)
 
       
   356         ]);
 
       
   357 
   302 
   358 
   303 
   359 (* ------------------------------------------------------------------------ *)
 
   304 (* ------------------------------------------------------------------------ *)
 
   360 (* Surjective pairing: equivalent to Exh_Sprod                              *)
 
   305 (* Surjective pairing: equivalent to Exh_Sprod                              *)
 
   361 (* ------------------------------------------------------------------------ *)
 
   306 (* ------------------------------------------------------------------------ *)
 
   362 
   307 
   363 qed_goal "surjective_pairing_Sprod" Sprod0.thy 
   308 val prems = goal Sprod0.thy 
   364         "z = Ispair(Isfst z)(Issnd z)"
 
   309         "z = Ispair(Isfst z)(Issnd z)";
 
   365 (fn prems =>
 
   310 by (res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1);
 
   366         [
 
   311 by (asm_simp_tac Sprod0_ss 1);
 
   367         (res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1),
 
   312 by (etac exE 1);
 
   368         (asm_simp_tac Sprod0_ss 1),
 
   313 by (etac exE 1);
 
   369         (etac exE 1),
 
   314 by (asm_simp_tac Sprod0_ss 1);
 
   370         (etac exE 1),
 
   315 qed "surjective_pairing_Sprod";
 
   371         (asm_simp_tac Sprod0_ss 1)
 
   316 
   372         ]);
 
   317 val prems = goal thy 
   373 
   318         "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y";
 
   374 qed_goal "Sel_injective_Sprod" thy 
   319 by (cut_facts_tac prems 1);
 
   375         "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
 
   320 by (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1);
 
   376 (fn prems =>
 
   321 by (rotate_tac ~1 1);
 
   377         [
 
   322 by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1);
 
   378         (cut_facts_tac prems 1),
 
   323 by (Asm_simp_tac 1);
 
   379         (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1),
 
   324 qed "Sel_injective_Sprod";
 
   380         (rotate_tac ~1 1),
 
       
   381         (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1),
 
       
   382         (Asm_simp_tac 1)
 
       
   383         ]);
isabelle