src/HOLCF/Sprod0.ML
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 10230 5eb935d6cc69
child 13601 fd3e3d6b37b2
permissions -rw-r--r--
GPLed;
     1 (*  Title:      HOLCF/Sprod0
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Strict product with typedef.
     7 *)
     8 
     9 (* ------------------------------------------------------------------------ *)
    10 (* A non-emptyness result for Sprod                                         *)
    11 (* ------------------------------------------------------------------------ *)
    12 
    13 Goalw [Sprod_def] "(Spair_Rep a b):Sprod";
    14 by (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl]);
    15 qed "SprodI";
    16 
    17 Goal "inj_on Abs_Sprod Sprod";
    18 by (rtac inj_on_inverseI 1);
    19 by (etac Abs_Sprod_inverse 1);
    20 qed "inj_on_Abs_Sprod";
    21 
    22 (* ------------------------------------------------------------------------ *)
    23 (* Strictness and definedness of Spair_Rep                                  *)
    24 (* ------------------------------------------------------------------------ *)
    25 
    26 Goalw [Spair_Rep_def]
    27  "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)";
    28 by (rtac ext 1);
    29 by (rtac ext 1);
    30 by (rtac iffI 1);
    31 by (fast_tac HOL_cs 1);
    32 by (fast_tac HOL_cs 1);
    33 qed "strict_Spair_Rep";
    34 
    35 Goalw [Spair_Rep_def]
    36  "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)";
    37 by (case_tac "a=UU|b=UU" 1);
    38 by (atac 1);
    39 by (fast_tac (claset() addDs [fun_cong]) 1);
    40 qed "defined_Spair_Rep_rev";
    41 
    42 (* ------------------------------------------------------------------------ *)
    43 (* injectivity of Spair_Rep and Ispair                                      *)
    44 (* ------------------------------------------------------------------------ *)
    45 
    46 Goalw [Spair_Rep_def]
    47 "[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba";
    48 by (dtac fun_cong 1);
    49 by (dtac fun_cong 1);
    50 by (etac (iffD1 RS mp) 1);
    51 by Auto_tac;  
    52 qed "inject_Spair_Rep";
    53 
    54 
    55 Goalw [Ispair_def]
    56         "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba";
    57 by (etac inject_Spair_Rep 1);
    58 by (atac 1);
    59 by (etac (inj_on_Abs_Sprod  RS inj_onD) 1);
    60 by (rtac SprodI 1);
    61 by (rtac SprodI 1);
    62 qed "inject_Ispair";
    63 
    64 
    65 (* ------------------------------------------------------------------------ *)
    66 (* strictness and definedness of Ispair                                     *)
    67 (* ------------------------------------------------------------------------ *)
    68 
    69 Goalw [Ispair_def] 
    70  "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU";
    71 by (etac (strict_Spair_Rep RS arg_cong) 1);
    72 qed "strict_Ispair";
    73 
    74 Goalw [Ispair_def]
    75         "Ispair UU b  = Ispair UU UU";
    76 by (rtac (strict_Spair_Rep RS arg_cong) 1);
    77 by (rtac disjI1 1);
    78 by (rtac refl 1);
    79 qed "strict_Ispair1";
    80 
    81 Goalw [Ispair_def]
    82         "Ispair a UU = Ispair UU UU";
    83 by (rtac (strict_Spair_Rep RS arg_cong) 1);
    84 by (rtac disjI2 1);
    85 by (rtac refl 1);
    86 qed "strict_Ispair2";
    87 
    88 Goal "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU";
    89 by (rtac (de_Morgan_disj RS subst) 1);
    90 by (etac contrapos_nn 1);
    91 by (etac strict_Ispair 1);
    92 qed "strict_Ispair_rev";
    93 
    94 Goalw [Ispair_def]
    95         "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)";
    96 by (rtac defined_Spair_Rep_rev 1);
    97 by (rtac (inj_on_Abs_Sprod  RS inj_onD) 1);
    98 by (atac 1);
    99 by (rtac SprodI 1);
   100 by (rtac SprodI 1);
   101 qed "defined_Ispair_rev";
   102 
   103 Goal "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)";
   104 by (rtac contrapos_nn 1);
   105 by (etac defined_Ispair_rev 2);
   106 by (rtac (de_Morgan_disj RS iffD2) 1);
   107 by (etac conjI 1);
   108 by (atac 1);
   109 qed "defined_Ispair";
   110 
   111 
   112 (* ------------------------------------------------------------------------ *)
   113 (* Exhaustion of the strict product **                                      *)
   114 (* ------------------------------------------------------------------------ *)
   115 
   116 Goalw [Ispair_def]
   117         "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)";
   118 by (rtac (rewrite_rule [Sprod_def] Rep_Sprod RS CollectE) 1);
   119 by (etac exE 1);
   120 by (etac exE 1);
   121 by (rtac (excluded_middle RS disjE) 1);
   122 by (rtac disjI2 1);
   123 by (rtac exI 1);
   124 by (rtac exI 1);
   125 by (rtac conjI 1);
   126 by (rtac (Rep_Sprod_inverse RS sym RS trans) 1);
   127 by (etac arg_cong 1);
   128 by (rtac (de_Morgan_disj RS subst) 1);
   129 by (atac 1);
   130 by (rtac disjI1 1);
   131 by (rtac (Rep_Sprod_inverse RS sym RS trans) 1);
   132 by (res_inst_tac [("f","Abs_Sprod")] arg_cong 1);
   133 by (etac trans 1);
   134 by (etac strict_Spair_Rep 1);
   135 qed "Exh_Sprod";
   136 
   137 (* ------------------------------------------------------------------------ *)
   138 (* general elimination rule for strict product                              *)
   139 (* ------------------------------------------------------------------------ *)
   140 
   141 val [prem1,prem2] = Goal
   142 "  [| p=Ispair UU UU ==> Q ; !!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q|] \
   143 \  ==> Q";
   144 by (rtac (Exh_Sprod RS disjE) 1);
   145 by (etac prem1 1);
   146 by (etac exE 1);
   147 by (etac exE 1);
   148 by (etac conjE 1);
   149 by (etac conjE 1);
   150 by (etac prem2 1);
   151 by (atac 1);
   152 by (atac 1);
   153 qed "IsprodE";
   154 
   155 
   156 (* ------------------------------------------------------------------------ *)
   157 (* some results about the selectors Isfst, Issnd                            *)
   158 (* ------------------------------------------------------------------------ *)
   159 
   160 Goalw [Isfst_def] "p=Ispair UU UU ==> Isfst p = UU";
   161 by (rtac some_equality 1);
   162 by (rtac conjI 1);
   163 by (fast_tac HOL_cs  1);
   164 by (strip_tac 1);
   165 by (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1);
   166 by (rtac not_sym 1);
   167 by (rtac defined_Ispair 1);
   168 by (REPEAT (fast_tac HOL_cs  1));
   169 qed "strict_Isfst";
   170 
   171 
   172 Goal "Isfst(Ispair UU y) = UU";
   173 by (stac strict_Ispair1 1);
   174 by (rtac strict_Isfst 1);
   175 by (rtac refl 1);
   176 qed "strict_Isfst1";
   177 
   178 Addsimps [strict_Isfst1];
   179 
   180 Goal "Isfst(Ispair x UU) = UU";
   181 by (stac strict_Ispair2 1);
   182 by (rtac strict_Isfst 1);
   183 by (rtac refl 1);
   184 qed "strict_Isfst2";
   185 
   186 Addsimps [strict_Isfst2];
   187 
   188 
   189 Goalw [Issnd_def] "p=Ispair UU UU ==>Issnd p=UU";
   190 by (rtac some_equality 1);
   191 by (rtac conjI 1);
   192 by (fast_tac HOL_cs  1);
   193 by (strip_tac 1);
   194 by (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1);
   195 by (rtac not_sym 1);
   196 by (rtac defined_Ispair 1);
   197 by (REPEAT (fast_tac HOL_cs  1));
   198 qed "strict_Issnd";
   199 
   200 Goal "Issnd(Ispair UU y) = UU";
   201 by (stac strict_Ispair1 1);
   202 by (rtac strict_Issnd 1);
   203 by (rtac refl 1);
   204 qed "strict_Issnd1";
   205 
   206 Addsimps [strict_Issnd1];
   207 
   208 Goal "Issnd(Ispair x UU) = UU";
   209 by (stac strict_Ispair2 1);
   210 by (rtac strict_Issnd 1);
   211 by (rtac refl 1);
   212 qed "strict_Issnd2";
   213 
   214 Addsimps [strict_Issnd2];
   215 
   216 Goalw [Isfst_def] "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x";
   217 by (rtac some_equality 1);
   218 by (rtac conjI 1);
   219 by (strip_tac 1);
   220 by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1);
   221 by (etac defined_Ispair 1);
   222 by (atac 1);
   223 by (atac 1);
   224 by (strip_tac 1);
   225 by (rtac (inject_Ispair RS conjunct1) 1);
   226 by (fast_tac HOL_cs  3);
   227 by (fast_tac HOL_cs  1);
   228 by (fast_tac HOL_cs  1);
   229 by (fast_tac HOL_cs  1);
   230 qed "Isfst";
   231 
   232 Goalw [Issnd_def] "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y";
   233 by (rtac some_equality 1);
   234 by (rtac conjI 1);
   235 by (strip_tac 1);
   236 by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1);
   237 by (etac defined_Ispair 1);
   238 by (atac 1);
   239 by (atac 1);
   240 by (strip_tac 1);
   241 by (rtac (inject_Ispair RS conjunct2) 1);
   242 by (fast_tac HOL_cs  3);
   243 by (fast_tac HOL_cs  1);
   244 by (fast_tac HOL_cs  1);
   245 by (fast_tac HOL_cs  1);
   246 qed "Issnd";
   247 
   248 Goal "y~=UU ==>Isfst(Ispair x y)=x";
   249 by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1);
   250 by (etac Isfst 1);
   251 by (atac 1);
   252 by (hyp_subst_tac 1);
   253 by (rtac strict_Isfst1 1);
   254 qed "Isfst2";
   255 
   256 Goal "~x=UU ==>Issnd(Ispair x y)=y";
   257 by (res_inst_tac [("Q","y=UU")] (excluded_middle RS disjE) 1);
   258 by (etac Issnd 1);
   259 by (atac 1);
   260 by (hyp_subst_tac 1);
   261 by (rtac strict_Issnd2 1);
   262 qed "Issnd2";
   263 
   264 
   265 (* ------------------------------------------------------------------------ *)
   266 (* instantiate the simplifier                                               *)
   267 (* ------------------------------------------------------------------------ *)
   268 
   269 val Sprod0_ss = 
   270         HOL_ss 
   271         addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
   272                  Isfst2,Issnd2];
   273 
   274 Addsimps [Isfst2,Issnd2];
   275 
   276 Goal "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU";
   277 by (res_inst_tac [("p","p")] IsprodE 1);
   278 by (contr_tac 1);
   279 by (hyp_subst_tac 1);
   280 by (rtac conjI 1);
   281 by (asm_simp_tac Sprod0_ss 1);
   282 by (asm_simp_tac Sprod0_ss 1);
   283 qed "defined_IsfstIssnd";
   284 
   285 
   286 (* ------------------------------------------------------------------------ *)
   287 (* Surjective pairing: equivalent to Exh_Sprod                              *)
   288 (* ------------------------------------------------------------------------ *)
   289 
   290 Goal "z = Ispair(Isfst z)(Issnd z)";
   291 by (res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1);
   292 by (asm_simp_tac Sprod0_ss 1);
   293 by (etac exE 1);
   294 by (etac exE 1);
   295 by (asm_simp_tac Sprod0_ss 1);
   296 qed "surjective_pairing_Sprod";
   297 
   298 Goal "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y";
   299 by (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1);
   300 by (rotate_tac ~1 1);
   301 by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1);
   302 by (Asm_simp_tac 1);
   303 qed "Sel_injective_Sprod";