src/HOLCF/ssum0.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/ssum0.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Lemmas for theory ssum0.thy 
     7 *)
     8 
     9 open Ssum0;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* A non-emptyness result for Sssum                                         *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 val SsumIl = prove_goalw Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum"
    16  (fn prems =>
    17 	[
    18 	(rtac CollectI 1),
    19 	(rtac disjI1 1),
    20 	(rtac exI 1),
    21 	(rtac refl 1)
    22 	]);
    23 
    24 val SsumIr = prove_goalw Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum"
    25  (fn prems =>
    26 	[
    27 	(rtac CollectI 1),
    28 	(rtac disjI2 1),
    29 	(rtac exI 1),
    30 	(rtac refl 1)
    31 	]);
    32 
    33 val inj_onto_Abs_Ssum = prove_goal Ssum0.thy "inj_onto(Abs_Ssum,Ssum)"
    34 (fn prems =>
    35 	[
    36 	(rtac inj_onto_inverseI 1),
    37 	(etac Abs_Ssum_inverse 1)
    38 	]);
    39 
    40 (* ------------------------------------------------------------------------ *)
    41 (* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr                        *)
    42 (* ------------------------------------------------------------------------ *)
    43 
    44 val strict_SinlSinr_Rep = prove_goalw Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def]
    45  "Sinl_Rep(UU) = Sinr_Rep(UU)"
    46  (fn prems =>
    47 	[
    48 	(rtac ext 1),
    49 	(rtac ext 1),
    50 	(rtac ext 1),
    51 	(fast_tac HOL_cs 1)
    52 	]);
    53 
    54 val strict_IsinlIsinr = prove_goalw Ssum0.thy [Isinl_def,Isinr_def]
    55  "Isinl(UU) = Isinr(UU)"
    56  (fn prems =>
    57 	[
    58 	(rtac (strict_SinlSinr_Rep RS arg_cong) 1)
    59 	]);
    60 
    61 
    62 (* ------------------------------------------------------------------------ *)
    63 (* distinctness of  Sinl_Rep, Sinr_Rep and Isinl, Isinr                     *)
    64 (* ------------------------------------------------------------------------ *)
    65 
    66 val noteq_SinlSinr_Rep = prove_goalw Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
    67 	"(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
    68  (fn prems =>
    69 	[
    70 	(rtac conjI 1),
    71 	(res_inst_tac [("Q","a=UU")] classical2 1),
    72 	(atac 1),
    73 	(rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 
    74 	RS mp RS conjunct1 RS sym) 1),
    75 	(fast_tac HOL_cs 1),
    76 	(atac 1),
    77 	(res_inst_tac [("Q","b=UU")] classical2 1),
    78 	(atac 1),
    79 	(rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1 
    80 	RS mp RS conjunct1 RS sym) 1),
    81 	(fast_tac HOL_cs 1),
    82 	(atac 1)
    83 	]);
    84 
    85 
    86 val noteq_IsinlIsinr = prove_goalw Ssum0.thy [Isinl_def,Isinr_def]
    87 	"Isinl(a)=Isinr(b) ==> a=UU & b=UU"
    88  (fn prems =>
    89 	[
    90 	(cut_facts_tac prems 1),
    91 	(rtac noteq_SinlSinr_Rep 1),
    92 	(etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
    93 	(rtac SsumIl 1),
    94 	(rtac SsumIr 1)
    95 	]);
    96 
    97 
    98 
    99 (* ------------------------------------------------------------------------ *)
   100 (* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr                       *)
   101 (* ------------------------------------------------------------------------ *)
   102 
   103 val inject_Sinl_Rep1 = prove_goalw Ssum0.thy [Sinl_Rep_def]
   104  "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
   105  (fn prems =>
   106 	[
   107 	(res_inst_tac [("Q","a=UU")] classical2 1),
   108 	(atac 1),
   109 	(rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
   110 	RS iffD2 RS mp RS conjunct1 RS sym) 1),
   111 	(fast_tac HOL_cs 1),
   112 	(atac 1)
   113 	]);
   114 
   115 val inject_Sinr_Rep1 = prove_goalw Ssum0.thy [Sinr_Rep_def]
   116  "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
   117  (fn prems =>
   118 	[
   119 	(res_inst_tac [("Q","b=UU")] classical2 1),
   120 	(atac 1),
   121 	(rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
   122 	RS iffD2 RS mp RS conjunct1 RS sym) 1),
   123 	(fast_tac HOL_cs 1),
   124 	(atac 1)
   125 	]);
   126 
   127 val inject_Sinl_Rep2 = prove_goalw Ssum0.thy [Sinl_Rep_def]
   128 "[|~a1=UU ; ~a2=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2"
   129  (fn prems =>
   130 	[
   131 	(rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong 
   132 	RS iffD1 RS mp RS conjunct1) 1),
   133 	(fast_tac HOL_cs 1),
   134 	(resolve_tac prems 1)
   135 	]);
   136 
   137 val inject_Sinr_Rep2 = prove_goalw Ssum0.thy [Sinr_Rep_def]
   138 "[|~b1=UU ; ~b2=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2"
   139  (fn prems =>
   140 	[
   141 	(rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong 
   142 	RS iffD1 RS mp RS conjunct1) 1),
   143 	(fast_tac HOL_cs 1),
   144 	(resolve_tac prems 1)
   145 	]);
   146 
   147 val inject_Sinl_Rep = prove_goal Ssum0.thy 
   148 	"Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"
   149  (fn prems =>
   150 	[
   151 	(cut_facts_tac prems 1),
   152 	(res_inst_tac [("Q","a1=UU")] classical2 1),
   153 	(hyp_subst_tac 1),
   154 	(rtac (inject_Sinl_Rep1 RS sym) 1),
   155 	(etac sym 1),
   156 	(res_inst_tac [("Q","a2=UU")] classical2 1),
   157 	(hyp_subst_tac 1),
   158 	(etac inject_Sinl_Rep1 1),
   159 	(etac inject_Sinl_Rep2 1),
   160 	(atac 1),
   161 	(atac 1)
   162 	]);
   163 
   164 val inject_Sinr_Rep = prove_goal Ssum0.thy 
   165 	"Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2"
   166  (fn prems =>
   167 	[
   168 	(cut_facts_tac prems 1),
   169 	(res_inst_tac [("Q","b1=UU")] classical2 1),
   170 	(hyp_subst_tac 1),
   171 	(rtac (inject_Sinr_Rep1 RS sym) 1),
   172 	(etac sym 1),
   173 	(res_inst_tac [("Q","b2=UU")] classical2 1),
   174 	(hyp_subst_tac 1),
   175 	(etac inject_Sinr_Rep1 1),
   176 	(etac inject_Sinr_Rep2 1),
   177 	(atac 1),
   178 	(atac 1)
   179 	]);
   180 
   181 val inject_Isinl = prove_goalw Ssum0.thy [Isinl_def]
   182 "Isinl(a1)=Isinl(a2)==> a1=a2"
   183  (fn prems =>
   184 	[
   185 	(cut_facts_tac prems 1),
   186 	(rtac inject_Sinl_Rep 1),
   187 	(etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
   188 	(rtac SsumIl 1),
   189 	(rtac SsumIl 1)
   190 	]);
   191 
   192 val inject_Isinr = prove_goalw Ssum0.thy [Isinr_def]
   193 "Isinr(b1)=Isinr(b2) ==> b1=b2"
   194  (fn prems =>
   195 	[
   196 	(cut_facts_tac prems 1),
   197 	(rtac inject_Sinr_Rep 1),
   198 	(etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
   199 	(rtac SsumIr 1),
   200 	(rtac SsumIr 1)
   201 	]);
   202 
   203 val inject_Isinl_rev = prove_goal Ssum0.thy  
   204 "~a1=a2 ==> ~Isinl(a1) = Isinl(a2)"
   205  (fn prems =>
   206 	[
   207 	(cut_facts_tac prems 1),
   208 	(rtac contrapos 1),
   209 	(etac inject_Isinl 2),
   210 	(atac 1)
   211 	]);
   212 
   213 val inject_Isinr_rev = prove_goal Ssum0.thy  
   214 "~b1=b2 ==> ~Isinr(b1) = Isinr(b2)"
   215  (fn prems =>
   216 	[
   217 	(cut_facts_tac prems 1),
   218 	(rtac contrapos 1),
   219 	(etac inject_Isinr 2),
   220 	(atac 1)
   221 	]);
   222 
   223 (* ------------------------------------------------------------------------ *)
   224 (* Exhaustion of the strict sum ++                                          *)
   225 (* choice of the bottom representation is arbitrary                         *)
   226 (* ------------------------------------------------------------------------ *)
   227 
   228 val Exh_Ssum = prove_goalw Ssum0.thy [Isinl_def,Isinr_def]
   229 	"z=Isinl(UU) | (? a. z=Isinl(a) & ~a=UU) | (? b. z=Isinr(b) & ~b=UU)"
   230  (fn prems =>
   231 	[
   232 	(rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1),
   233 	(etac disjE 1),
   234 	(etac exE 1),
   235 	(res_inst_tac [("Q","z= Abs_Ssum(Sinl_Rep(UU))")] classical2 1),
   236 	(etac disjI1 1),
   237 	(rtac disjI2 1),
   238 	(rtac disjI1 1),
   239 	(rtac exI 1),
   240 	(rtac conjI 1),
   241 	(rtac (Rep_Ssum_inverse RS sym RS trans) 1),
   242 	(etac arg_cong 1),
   243 	(res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos 1),
   244 	(etac arg_cong 2),
   245 	(etac contrapos 1),
   246 	(rtac (Rep_Ssum_inverse RS sym RS trans) 1),
   247 	(rtac trans 1),
   248 	(etac arg_cong 1),
   249 	(etac arg_cong 1),
   250 	(etac exE 1),
   251 	(res_inst_tac [("Q","z= Abs_Ssum(Sinl_Rep(UU))")] classical2 1),
   252 	(etac disjI1 1),
   253 	(rtac disjI2 1),
   254 	(rtac disjI2 1),
   255 	(rtac exI 1),
   256 	(rtac conjI 1),
   257 	(rtac (Rep_Ssum_inverse RS sym RS trans) 1),
   258 	(etac arg_cong 1),
   259 	(res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos 1),
   260 	(hyp_subst_tac 2),
   261 	(rtac (strict_SinlSinr_Rep RS sym) 2),
   262 	(etac contrapos 1),
   263 	(rtac (Rep_Ssum_inverse RS sym RS trans) 1),
   264 	(rtac trans 1),
   265 	(etac arg_cong 1),
   266 	(etac arg_cong 1)
   267 	]);
   268 
   269 (* ------------------------------------------------------------------------ *)
   270 (* elimination rules for the strict sum ++                                  *)
   271 (* ------------------------------------------------------------------------ *)
   272 
   273 val IssumE = prove_goal Ssum0.thy
   274 	"[|p=Isinl(UU) ==> Q ;\
   275 \	!!x.[|p=Isinl(x); ~x=UU |] ==> Q;\
   276 \	!!y.[|p=Isinr(y); ~y=UU |] ==> Q|] ==> Q"
   277  (fn prems =>
   278 	[
   279 	(rtac (Exh_Ssum RS disjE) 1),
   280 	(etac disjE 2),
   281 	(eresolve_tac prems 1),
   282 	(etac exE 1),
   283 	(etac conjE 1),
   284 	(eresolve_tac prems 1),
   285 	(atac 1),
   286 	(etac exE 1),
   287 	(etac conjE 1),
   288 	(eresolve_tac prems 1),
   289 	(atac 1)
   290 	]);
   291 
   292 val IssumE2 = prove_goal Ssum0.thy 
   293 "[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q"
   294  (fn prems =>
   295 	[
   296 	(rtac IssumE 1),
   297 	(eresolve_tac prems 1), 
   298 	(eresolve_tac prems 1), 
   299 	(eresolve_tac prems 1)
   300 	]);
   301 
   302 
   303 
   304 
   305 (* ------------------------------------------------------------------------ *)
   306 (* rewrites for Iwhen                                                       *)
   307 (* ------------------------------------------------------------------------ *)
   308 
   309 val Iwhen1 = prove_goalw Ssum0.thy [Iwhen_def]
   310 	"Iwhen(f)(g)(Isinl(UU)) = UU"
   311  (fn prems =>
   312 	[
   313 	(rtac  select_equality 1),
   314 	(rtac conjI 1),
   315 	(fast_tac HOL_cs  1),
   316 	(rtac conjI 1),
   317 	(strip_tac 1),
   318 	(res_inst_tac [("P","a=UU")] notE 1),
   319 	(fast_tac HOL_cs  1),
   320 	(rtac inject_Isinl 1),
   321 	(rtac sym 1),
   322 	(fast_tac HOL_cs  1),
   323 	(strip_tac 1),
   324 	(res_inst_tac [("P","b=UU")] notE 1),
   325 	(fast_tac HOL_cs  1),
   326 	(rtac inject_Isinr 1),
   327 	(rtac sym 1),
   328 	(rtac (strict_IsinlIsinr RS subst) 1),
   329 	(fast_tac HOL_cs  1),
   330 	(fast_tac HOL_cs  1)
   331 	]);
   332 
   333 
   334 val Iwhen2 = prove_goalw Ssum0.thy [Iwhen_def]
   335 	"~x=UU ==> Iwhen(f)(g)(Isinl(x)) = f[x]"
   336  (fn prems =>
   337 	[
   338 	(cut_facts_tac prems 1),
   339 	(rtac  select_equality 1),
   340 	(fast_tac HOL_cs  2),
   341 	(rtac conjI 1),
   342 	(strip_tac 1),
   343 	(res_inst_tac [("P","x=UU")] notE 1),
   344 	(atac 1),
   345 	(rtac inject_Isinl 1),
   346 	(atac 1),
   347 	(rtac conjI 1),
   348 	(strip_tac 1),
   349 	(rtac cfun_arg_cong 1),
   350 	(rtac inject_Isinl 1),
   351 	(fast_tac HOL_cs  1),
   352 	(strip_tac 1),
   353 	(res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1),
   354 	(fast_tac HOL_cs  2),
   355 	(rtac contrapos 1),
   356 	(etac noteq_IsinlIsinr 2),
   357 	(fast_tac HOL_cs  1)
   358 	]);
   359 
   360 val Iwhen3 = prove_goalw Ssum0.thy [Iwhen_def]
   361 	"~y=UU ==> Iwhen(f)(g)(Isinr(y)) = g[y]"
   362  (fn prems =>
   363 	[
   364 	(cut_facts_tac prems 1),
   365 	(rtac  select_equality 1),
   366 	(fast_tac HOL_cs  2),
   367 	(rtac conjI 1),
   368 	(strip_tac 1),
   369 	(res_inst_tac [("P","y=UU")] notE 1),
   370 	(atac 1),
   371 	(rtac inject_Isinr 1),
   372 	(rtac (strict_IsinlIsinr RS subst) 1),
   373 	(atac 1),
   374 	(rtac conjI 1),
   375 	(strip_tac 1),
   376 	(res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1),
   377 	(fast_tac HOL_cs  2),
   378 	(rtac contrapos 1),
   379 	(etac (sym RS noteq_IsinlIsinr) 2),
   380 	(fast_tac HOL_cs  1),
   381 	(strip_tac 1),
   382 	(rtac cfun_arg_cong 1),
   383 	(rtac inject_Isinr 1),
   384 	(fast_tac HOL_cs  1)
   385 	]);
   386 
   387 (* ------------------------------------------------------------------------ *)
   388 (* instantiate the simplifier                                               *)
   389 (* ------------------------------------------------------------------------ *)
   390 
   391 val Ssum_ss = Cfun_ss addsimps 
   392 		[(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
   393 
   394