src/HOLCF/ssum2.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/ssum2.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for ssum2.thy
     7 *)
     8 
     9 open Ssum2;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* access to less_ssum in class po                                          *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 val less_ssum3a = prove_goal Ssum2.thy 
    16 	"(Isinl(x) << Isinl(y)) = (x << y)"
    17  (fn prems =>
    18 	[
    19 	(rtac (inst_ssum_po RS ssubst) 1),
    20 	(rtac less_ssum2a 1)
    21 	]);
    22 
    23 val less_ssum3b = prove_goal Ssum2.thy 
    24 	"(Isinr(x) << Isinr(y)) = (x << y)"
    25  (fn prems =>
    26 	[
    27 	(rtac (inst_ssum_po RS ssubst) 1),
    28 	(rtac less_ssum2b 1)
    29 	]);
    30 
    31 val less_ssum3c = prove_goal Ssum2.thy 
    32 	"(Isinl(x) << Isinr(y)) = (x = UU)"
    33  (fn prems =>
    34 	[
    35 	(rtac (inst_ssum_po RS ssubst) 1),
    36 	(rtac less_ssum2c 1)
    37 	]);
    38 
    39 val less_ssum3d = prove_goal Ssum2.thy 
    40 	"(Isinr(x) << Isinl(y)) = (x = UU)"
    41  (fn prems =>
    42 	[
    43 	(rtac (inst_ssum_po RS ssubst) 1),
    44 	(rtac less_ssum2d 1)
    45 	]);
    46 
    47 
    48 (* ------------------------------------------------------------------------ *)
    49 (* type ssum ++ is pointed                                                  *)
    50 (* ------------------------------------------------------------------------ *)
    51 
    52 val minimal_ssum = prove_goal Ssum2.thy "Isinl(UU) << s"
    53  (fn prems =>
    54 	[
    55 	(res_inst_tac [("p","s")] IssumE2 1),
    56 	(hyp_subst_tac 1),
    57 	(rtac (less_ssum3a RS iffD2) 1),
    58 	(rtac minimal 1),
    59 	(hyp_subst_tac 1),
    60 	(rtac (strict_IsinlIsinr RS ssubst) 1),
    61 	(rtac (less_ssum3b RS iffD2) 1),
    62 	(rtac minimal 1)
    63 	]);
    64 
    65 
    66 (* ------------------------------------------------------------------------ *)
    67 (* Isinl, Isinr are monotone                                                *)
    68 (* ------------------------------------------------------------------------ *)
    69 
    70 val monofun_Isinl = prove_goalw Ssum2.thy [monofun] "monofun(Isinl)"
    71  (fn prems =>
    72 	[
    73 	(strip_tac 1),
    74 	(etac (less_ssum3a RS iffD2) 1)
    75 	]);
    76 
    77 val monofun_Isinr = prove_goalw Ssum2.thy [monofun] "monofun(Isinr)"
    78  (fn prems =>
    79 	[
    80 	(strip_tac 1),
    81 	(etac (less_ssum3b RS iffD2) 1)
    82 	]);
    83 
    84 
    85 (* ------------------------------------------------------------------------ *)
    86 (* Iwhen is monotone in all arguments                                       *)
    87 (* ------------------------------------------------------------------------ *)
    88 
    89 
    90 val monofun_Iwhen1 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen)"
    91  (fn prems =>
    92 	[
    93 	(strip_tac 1),
    94 	(rtac (less_fun RS iffD2) 1),
    95 	(strip_tac 1),
    96 	(rtac (less_fun RS iffD2) 1),
    97 	(strip_tac 1),
    98 	(res_inst_tac [("p","xb")] IssumE 1),
    99 	(hyp_subst_tac 1),
   100 	(asm_simp_tac Ssum_ss 1),
   101 	(asm_simp_tac Ssum_ss 1),
   102 	(etac monofun_cfun_fun 1),
   103 	(asm_simp_tac Ssum_ss 1)
   104 	]);
   105 
   106 val monofun_Iwhen2 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen(f))"
   107  (fn prems =>
   108 	[
   109 	(strip_tac 1),
   110 	(rtac (less_fun RS iffD2) 1),
   111 	(strip_tac 1),
   112 	(res_inst_tac [("p","xa")] IssumE 1),
   113 	(hyp_subst_tac 1),
   114 	(asm_simp_tac Ssum_ss 1),
   115 	(asm_simp_tac Ssum_ss 1),
   116 	(asm_simp_tac Ssum_ss 1),
   117 	(etac monofun_cfun_fun 1)
   118 	]);
   119 
   120 val monofun_Iwhen3 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen(f)(g))"
   121  (fn prems =>
   122 	[
   123 	(strip_tac 1),
   124 	(res_inst_tac [("p","x")] IssumE 1),
   125 	(hyp_subst_tac 1),
   126 	(asm_simp_tac Ssum_ss 1),
   127 	(hyp_subst_tac 1),
   128 	(res_inst_tac [("p","y")] IssumE 1),
   129 	(hyp_subst_tac 1),
   130 	(asm_simp_tac Ssum_ss 1),
   131 	(res_inst_tac  [("P","xa=UU")] notE 1),
   132 	(atac 1),
   133 	(rtac UU_I 1),
   134 	(rtac (less_ssum3a  RS iffD1) 1),
   135 	(atac 1),
   136 	(hyp_subst_tac 1),
   137 	(asm_simp_tac Ssum_ss 1),
   138 	(rtac monofun_cfun_arg 1),
   139 	(etac (less_ssum3a  RS iffD1) 1),
   140 	(hyp_subst_tac 1),
   141 	(res_inst_tac [("s","UU"),("t","xa")] subst 1),
   142 	(etac (less_ssum3c  RS iffD1 RS sym) 1),
   143 	(asm_simp_tac Ssum_ss 1),
   144 	(hyp_subst_tac 1),
   145 	(res_inst_tac [("p","y")] IssumE 1),
   146 	(hyp_subst_tac 1),
   147 	(res_inst_tac [("s","UU"),("t","ya")] subst 1),
   148 	(etac (less_ssum3d  RS iffD1 RS sym) 1),
   149 	(asm_simp_tac Ssum_ss 1),
   150 	(hyp_subst_tac 1),
   151 	(res_inst_tac [("s","UU"),("t","ya")] subst 1),
   152 	(etac (less_ssum3d  RS iffD1 RS sym) 1),
   153 	(asm_simp_tac Ssum_ss 1),
   154 	(hyp_subst_tac 1),
   155 	(asm_simp_tac Ssum_ss 1),
   156 	(rtac monofun_cfun_arg 1),
   157 	(etac (less_ssum3b  RS iffD1) 1)
   158 	]);
   159 
   160 
   161 
   162 
   163 (* ------------------------------------------------------------------------ *)
   164 (* some kind of exhaustion rules for chains in 'a ++ 'b                     *)
   165 (* ------------------------------------------------------------------------ *)
   166 
   167 
   168 val ssum_lemma1 = prove_goal Ssum2.thy 
   169 "[|~(!i.? x.Y(i::nat)=Isinl(x))|] ==> (? i.! x.~Y(i)=Isinl(x))"
   170  (fn prems =>
   171 	[
   172 	(cut_facts_tac prems 1),
   173 	(fast_tac HOL_cs 1)
   174 	]);
   175 
   176 val ssum_lemma2 = prove_goal Ssum2.thy 
   177 "[|(? i.!x.~(Y::nat => 'a++'b)(i::nat)=Isinl(x::'a))|] ==>\
   178 \   (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & ~y=UU)"
   179  (fn prems =>
   180 	[
   181 	(cut_facts_tac prems 1),
   182 	(etac exE 1),
   183 	(res_inst_tac [("p","Y(i)")] IssumE 1),
   184 	(dtac spec 1),
   185 	(contr_tac 1),
   186 	(dtac spec 1),
   187 	(contr_tac 1),
   188 	(fast_tac HOL_cs 1)
   189 	]);
   190 
   191 
   192 val ssum_lemma3 = prove_goal Ssum2.thy 
   193 "[|is_chain(Y);(? i x. Y(i)=Isinr(x) & ~x=UU)|] ==> (!i.? y.Y(i)=Isinr(y))"
   194  (fn prems =>
   195 	[
   196 	(cut_facts_tac prems 1),
   197 	(etac exE 1),
   198 	(etac exE 1),
   199 	(rtac allI 1),
   200 	(res_inst_tac [("p","Y(ia)")] IssumE 1),
   201 	(rtac exI 1),
   202 	(rtac trans 1),
   203 	(rtac strict_IsinlIsinr 2),
   204 	(atac 1),
   205 	(etac exI 2),
   206 	(etac conjE 1),
   207 	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
   208 	(hyp_subst_tac 2),
   209 	(etac exI 2),
   210 	(res_inst_tac [("P","x=UU")] notE 1),
   211 	(atac 1),
   212 	(rtac (less_ssum3d RS iffD1) 1),
   213 	(res_inst_tac [("s","Y(i)"),("t","Isinr(x)")] subst 1),
   214 	(atac 1),
   215 	(res_inst_tac [("s","Y(ia)"),("t","Isinl(xa)")] subst 1),
   216 	(atac 1),
   217 	(etac (chain_mono RS mp) 1),
   218 	(atac 1),
   219 	(res_inst_tac [("P","xa=UU")] notE 1),
   220 	(atac 1),
   221 	(rtac (less_ssum3c RS iffD1) 1),
   222 	(res_inst_tac [("s","Y(i)"),("t","Isinr(x)")] subst 1),
   223 	(atac 1),
   224 	(res_inst_tac [("s","Y(ia)"),("t","Isinl(xa)")] subst 1),
   225 	(atac 1),
   226 	(etac (chain_mono RS mp) 1),
   227 	(atac 1)
   228 	]);
   229 
   230 val ssum_lemma4 = prove_goal Ssum2.thy 
   231 "is_chain(Y) ==> (!i.? x.Y(i)=Isinl(x))|(!i.? y.Y(i)=Isinr(y))"
   232  (fn prems =>
   233 	[
   234 	(cut_facts_tac prems 1),
   235 	(rtac classical2 1),
   236 	(etac disjI1 1),
   237 	(rtac disjI2 1),
   238 	(etac ssum_lemma3 1),
   239 	(rtac ssum_lemma2 1),
   240 	(etac ssum_lemma1 1)
   241 	]);
   242 
   243 
   244 (* ------------------------------------------------------------------------ *)
   245 (* restricted surjectivity of Isinl                                         *)
   246 (* ------------------------------------------------------------------------ *)
   247 
   248 val ssum_lemma5 = prove_goal Ssum2.thy 
   249 "z=Isinl(x)==> Isinl((Iwhen (LAM x.x) (LAM y.UU))(z)) = z"
   250  (fn prems =>
   251 	[
   252 	(cut_facts_tac prems 1),
   253 	(hyp_subst_tac 1),
   254 	(res_inst_tac [("Q","x=UU")] classical2 1),
   255 	(asm_simp_tac Ssum_ss 1),
   256 	(asm_simp_tac Ssum_ss 1)
   257 	]);
   258 
   259 (* ------------------------------------------------------------------------ *)
   260 (* restricted surjectivity of Isinr                                         *)
   261 (* ------------------------------------------------------------------------ *)
   262 
   263 val ssum_lemma6 = prove_goal Ssum2.thy 
   264 "z=Isinr(x)==> Isinr((Iwhen (LAM y.UU) (LAM x.x))(z)) = z"
   265  (fn prems =>
   266 	[
   267 	(cut_facts_tac prems 1),
   268 	(hyp_subst_tac 1),
   269 	(res_inst_tac [("Q","x=UU")] classical2 1),
   270 	(asm_simp_tac Ssum_ss 1),
   271 	(asm_simp_tac Ssum_ss 1)
   272 	]);
   273 
   274 (* ------------------------------------------------------------------------ *)
   275 (* technical lemmas                                                         *)
   276 (* ------------------------------------------------------------------------ *)
   277 
   278 val ssum_lemma7 = prove_goal Ssum2.thy 
   279 "[|Isinl(x) << z; ~x=UU|] ==> ? y.z=Isinl(y) & ~y=UU"
   280  (fn prems =>
   281 	[
   282 	(cut_facts_tac prems 1),
   283 	(res_inst_tac [("p","z")] IssumE 1),
   284 	(hyp_subst_tac 1),
   285 	(etac notE 1),
   286 	(rtac antisym_less 1),
   287 	(etac (less_ssum3a RS iffD1) 1),
   288 	(rtac minimal 1),
   289 	(fast_tac HOL_cs 1),
   290 	(hyp_subst_tac 1),
   291 	(rtac notE 1),
   292 	(etac (less_ssum3c RS iffD1) 2),
   293 	(atac 1)
   294 	]);
   295 
   296 val ssum_lemma8 = prove_goal Ssum2.thy 
   297 "[|Isinr(x) << z; ~x=UU|] ==> ? y.z=Isinr(y) & ~y=UU"
   298  (fn prems =>
   299 	[
   300 	(cut_facts_tac prems 1),
   301 	(res_inst_tac [("p","z")] IssumE 1),
   302 	(hyp_subst_tac 1),
   303 	(etac notE 1),
   304 	(etac (less_ssum3d RS iffD1) 1),
   305 	(hyp_subst_tac 1),
   306 	(rtac notE 1),
   307 	(etac (less_ssum3d RS iffD1) 2),
   308 	(atac 1),
   309 	(fast_tac HOL_cs 1)
   310 	]);
   311 
   312 (* ------------------------------------------------------------------------ *)
   313 (* the type 'a ++ 'b is a cpo in three steps                                *)
   314 (* ------------------------------------------------------------------------ *)
   315 
   316 val lub_ssum1a = prove_goal Ssum2.thy 
   317 "[|is_chain(Y);(!i.? x.Y(i)=Isinl(x))|] ==>\
   318 \ range(Y) <<|\
   319 \ Isinl(lub(range(%i.(Iwhen (LAM x.x) (LAM y.UU))(Y(i)))))"
   320  (fn prems =>
   321 	[
   322 	(cut_facts_tac prems 1),
   323 	(rtac is_lubI 1),
   324 	(rtac conjI 1),
   325 	(rtac ub_rangeI 1),
   326 	(rtac allI 1),
   327 	(etac allE 1),
   328 	(etac exE 1),
   329 	(res_inst_tac [("t","Y(i)")] (ssum_lemma5 RS subst) 1),
   330 	(atac 1),
   331 	(rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1),
   332 	(rtac is_ub_thelub 1),
   333 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   334 	(strip_tac 1),
   335 	(res_inst_tac [("p","u")] IssumE2 1),
   336 	(res_inst_tac [("t","u")] (ssum_lemma5 RS subst) 1),
   337 	(atac 1),
   338 	(rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1),
   339 	(rtac is_lub_thelub 1),
   340 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   341 	(etac (monofun_Iwhen3 RS ub2ub_monofun) 1),
   342 	(hyp_subst_tac 1),
   343 	(rtac (less_ssum3c RS iffD2) 1),
   344 	(rtac chain_UU_I_inverse 1),
   345 	(rtac allI 1),
   346 	(res_inst_tac [("p","Y(i)")] IssumE 1),
   347 	(asm_simp_tac Ssum_ss 1),
   348 	(asm_simp_tac Ssum_ss 2),
   349 	(etac notE 1),
   350 	(rtac (less_ssum3c RS iffD1) 1),
   351 	(res_inst_tac [("t","Isinl(x)")] subst 1),
   352 	(atac 1),
   353 	(etac (ub_rangeE RS spec) 1)
   354 	]);
   355 
   356 
   357 val lub_ssum1b = prove_goal Ssum2.thy 
   358 "[|is_chain(Y);(!i.? x.Y(i)=Isinr(x))|] ==>\
   359 \ range(Y) <<|\
   360 \ Isinr(lub(range(%i.(Iwhen (LAM y.UU) (LAM x.x))(Y(i)))))"
   361  (fn prems =>
   362 	[
   363 	(cut_facts_tac prems 1),
   364 	(rtac is_lubI 1),
   365 	(rtac conjI 1),
   366 	(rtac ub_rangeI 1),
   367 	(rtac allI 1),
   368 	(etac allE 1),
   369 	(etac exE 1),
   370 	(res_inst_tac [("t","Y(i)")] (ssum_lemma6 RS subst) 1),
   371 	(atac 1),
   372 	(rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1),
   373 	(rtac is_ub_thelub 1),
   374 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   375 	(strip_tac 1),
   376 	(res_inst_tac [("p","u")] IssumE2 1),
   377 	(hyp_subst_tac 1),
   378 	(rtac (less_ssum3d RS iffD2) 1),
   379 	(rtac chain_UU_I_inverse 1),
   380 	(rtac allI 1),
   381 	(res_inst_tac [("p","Y(i)")] IssumE 1),
   382 	(asm_simp_tac Ssum_ss 1),
   383 	(asm_simp_tac Ssum_ss 1),
   384 	(etac notE 1),
   385 	(rtac (less_ssum3d RS iffD1) 1),
   386 	(res_inst_tac [("t","Isinr(y)")] subst 1),
   387 	(atac 1),
   388 	(etac (ub_rangeE RS spec) 1),
   389 	(res_inst_tac [("t","u")] (ssum_lemma6 RS subst) 1),
   390 	(atac 1),
   391 	(rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1),
   392 	(rtac is_lub_thelub 1),
   393 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   394 	(etac (monofun_Iwhen3 RS ub2ub_monofun) 1)
   395 	]);
   396 
   397 
   398 val thelub_ssum1a = lub_ssum1a RS thelubI;
   399 (* [| is_chain(?Y1); ! i. ? x. ?Y1(i) = Isinl(x) |] ==>                     *)
   400 (* lub(range(?Y1)) = Isinl(lub(range(%i. Iwhen(LAM x. x,LAM y. UU,?Y1(i)))))*)
   401 
   402 val thelub_ssum1b = lub_ssum1b RS thelubI;
   403 (* [| is_chain(?Y1); ! i. ? x. ?Y1(i) = Isinr(x) |] ==>                     *)
   404 (* lub(range(?Y1)) = Isinr(lub(range(%i. Iwhen(LAM y. UU,LAM x. x,?Y1(i)))))*)
   405 
   406 val cpo_ssum = prove_goal Ssum2.thy 
   407 	"is_chain(Y::nat=>'a ++'b) ==> ? x.range(Y) <<|x"
   408  (fn prems =>
   409 	[
   410 	(cut_facts_tac prems 1),
   411 	(rtac (ssum_lemma4 RS disjE) 1),
   412 	(atac 1),
   413 	(rtac exI 1),
   414 	(etac lub_ssum1a 1),
   415 	(atac 1),
   416 	(rtac exI 1),
   417 	(etac lub_ssum1b 1),
   418 	(atac 1)
   419 	]);