src/HOLCF/Sprod3.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5033 06f03dc5a1dc
child 9245 428385c4bc50
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/Sprod3.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for Sprod.thy 
     7 *)
     8 
     9 open Sprod3;
    10 
    11 (* for compatibility with old HOLCF-Version *)
    12 qed_goal "inst_sprod_pcpo" thy "UU = Ispair UU UU"
    13  (fn prems => 
    14         [
    15         (simp_tac (HOL_ss addsimps [UU_def,UU_sprod_def]) 1)
    16         ]);
    17 (* ------------------------------------------------------------------------ *)
    18 (* continuity of Ispair, Isfst, Issnd                                       *)
    19 (* ------------------------------------------------------------------------ *)
    20 
    21 qed_goal "sprod3_lemma1" thy 
    22 "[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==>\
    23 \ Ispair (lub(range Y)) x =\
    24 \ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \
    25 \        (lub(range(%i. Issnd(Ispair(Y i) x))))"
    26  (fn prems =>
    27         [
    28         (cut_facts_tac prems 1),
    29         (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
    30         (rtac lub_equal 1),
    31         (atac 1),
    32         (rtac (monofun_Isfst RS ch2ch_monofun) 1),
    33         (rtac ch2ch_fun 1),
    34         (rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
    35         (atac 1),
    36         (rtac allI 1),
    37         (asm_simp_tac Sprod0_ss 1),
    38         (rtac sym 1),
    39         (rtac lub_chain_maxelem 1),
    40         (res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
    41         (rtac (not_all RS iffD1) 1),
    42         (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
    43         (atac 1),
    44         (rtac chain_UU_I_inverse 1),
    45         (atac 1),
    46         (rtac exI 1),
    47         (etac Issnd2 1),
    48         (rtac allI 1),
    49         (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
    50         (asm_simp_tac Sprod0_ss 1),
    51         (rtac refl_less 1),
    52         (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
    53         (etac sym 1),
    54         (asm_simp_tac Sprod0_ss  1),
    55         (rtac minimal 1)
    56         ]);
    57 
    58 qed_goal "sprod3_lemma2" thy 
    59 "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
    60 \   Ispair (lub(range Y)) x =\
    61 \   Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\
    62 \          (lub(range(%i. Issnd(Ispair(Y i) x))))"
    63  (fn prems =>
    64         [
    65         (cut_facts_tac prems 1),
    66         (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
    67         (atac 1),
    68         (rtac trans 1),
    69         (rtac strict_Ispair1 1),
    70         (rtac (strict_Ispair RS sym) 1),
    71         (rtac disjI1 1),
    72         (rtac chain_UU_I_inverse 1),
    73         (rtac allI 1),
    74         (asm_simp_tac Sprod0_ss  1),
    75         (etac (chain_UU_I RS spec) 1),
    76         (atac 1)
    77         ]);
    78 
    79 
    80 qed_goal "sprod3_lemma3" thy 
    81 "[| chain(Y); x = UU |] ==>\
    82 \          Ispair (lub(range Y)) x =\
    83 \          Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\
    84 \                 (lub(range(%i. Issnd(Ispair (Y i) x))))"
    85  (fn prems =>
    86         [
    87         (cut_facts_tac prems 1),
    88         (res_inst_tac [("s","UU"),("t","x")] ssubst 1),
    89         (atac 1),
    90         (rtac trans 1),
    91         (rtac strict_Ispair2 1),
    92         (rtac (strict_Ispair RS sym) 1),
    93         (rtac disjI1 1),
    94         (rtac chain_UU_I_inverse 1),
    95         (rtac allI 1),
    96         (simp_tac Sprod0_ss  1)
    97         ]);
    98 
    99 
   100 qed_goal "contlub_Ispair1" thy "contlub(Ispair)"
   101 (fn prems =>
   102         [
   103         (rtac contlubI 1),
   104         (strip_tac 1),
   105         (rtac (expand_fun_eq RS iffD2) 1),
   106         (strip_tac 1),
   107         (stac (lub_fun RS thelubI) 1),
   108         (etac (monofun_Ispair1 RS ch2ch_monofun) 1),
   109         (rtac trans 1),
   110         (rtac (thelub_sprod RS sym) 2),
   111         (rtac ch2ch_fun 2),
   112         (etac (monofun_Ispair1 RS ch2ch_monofun) 2),
   113         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   114         (res_inst_tac 
   115                 [("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1),
   116         (etac sprod3_lemma1 1),
   117         (atac 1),
   118         (atac 1),
   119         (etac sprod3_lemma2 1),
   120         (atac 1),
   121         (atac 1),
   122         (etac sprod3_lemma3 1),
   123         (atac 1)
   124         ]);
   125 
   126 qed_goal "sprod3_lemma4" thy 
   127 "[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
   128 \         Ispair x (lub(range Y)) =\
   129 \         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
   130 \                (lub(range(%i. Issnd (Ispair x (Y i)))))"
   131  (fn prems =>
   132         [
   133         (cut_facts_tac prems 1),
   134         (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
   135         (rtac sym 1),
   136         (rtac lub_chain_maxelem 1),
   137         (res_inst_tac [("P","%j. Y(j)~=UU")] exE 1),
   138         (rtac (not_all RS iffD1) 1),
   139         (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
   140         (atac 1),
   141         (rtac chain_UU_I_inverse 1),
   142         (atac 1),
   143         (rtac exI 1),
   144         (etac Isfst2 1),
   145         (rtac allI 1),
   146         (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
   147         (asm_simp_tac Sprod0_ss 1),
   148         (rtac refl_less 1),
   149         (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
   150         (etac sym 1),
   151         (asm_simp_tac Sprod0_ss  1),
   152         (rtac minimal 1),
   153         (rtac lub_equal 1),
   154         (atac 1),
   155         (rtac (monofun_Issnd RS ch2ch_monofun) 1),
   156         (rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
   157         (atac 1),
   158         (rtac allI 1),
   159         (asm_simp_tac Sprod0_ss 1)
   160         ]);
   161 
   162 qed_goal "sprod3_lemma5" thy 
   163 "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
   164 \         Ispair x (lub(range Y)) =\
   165 \         Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\
   166 \                (lub(range(%i. Issnd(Ispair x (Y i)))))"
   167  (fn prems =>
   168         [
   169         (cut_facts_tac prems 1),
   170         (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
   171         (atac 1),
   172         (rtac trans 1),
   173         (rtac strict_Ispair2 1),
   174         (rtac (strict_Ispair RS sym) 1),
   175         (rtac disjI2 1),
   176         (rtac chain_UU_I_inverse 1),
   177         (rtac allI 1),
   178         (asm_simp_tac Sprod0_ss  1),
   179         (etac (chain_UU_I RS spec) 1),
   180         (atac 1)
   181         ]);
   182 
   183 qed_goal "sprod3_lemma6" thy 
   184 "[| chain(Y); x = UU |] ==>\
   185 \         Ispair x (lub(range Y)) =\
   186 \         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
   187 \                (lub(range(%i. Issnd (Ispair x (Y i)))))"
   188 (fn prems =>
   189         [
   190         (cut_facts_tac prems 1),
   191         (res_inst_tac [("s","UU"),("t","x")] ssubst 1),
   192         (atac 1),
   193         (rtac trans 1),
   194         (rtac strict_Ispair1 1),
   195         (rtac (strict_Ispair RS sym) 1),
   196         (rtac disjI1 1),
   197         (rtac chain_UU_I_inverse 1),
   198         (rtac allI 1),
   199         (simp_tac Sprod0_ss  1)
   200         ]);
   201 
   202 qed_goal "contlub_Ispair2" thy "contlub(Ispair(x))"
   203 (fn prems =>
   204         [
   205         (rtac contlubI 1),
   206         (strip_tac 1),
   207         (rtac trans 1),
   208         (rtac (thelub_sprod RS sym) 2),
   209         (etac (monofun_Ispair2 RS ch2ch_monofun) 2),
   210         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   211         (res_inst_tac [("Q","lub(range(Y))=UU")] 
   212                 (excluded_middle RS disjE) 1),
   213         (etac sprod3_lemma4 1),
   214         (atac 1),
   215         (atac 1),
   216         (etac sprod3_lemma5 1),
   217         (atac 1),
   218         (atac 1),
   219         (etac sprod3_lemma6 1),
   220         (atac 1)
   221         ]);
   222 
   223 
   224 qed_goal "cont_Ispair1" thy "cont(Ispair)"
   225 (fn prems =>
   226         [
   227         (rtac monocontlub2cont 1),
   228         (rtac monofun_Ispair1 1),
   229         (rtac contlub_Ispair1 1)
   230         ]);
   231 
   232 
   233 qed_goal "cont_Ispair2" thy "cont(Ispair(x))"
   234 (fn prems =>
   235         [
   236         (rtac monocontlub2cont 1),
   237         (rtac monofun_Ispair2 1),
   238         (rtac contlub_Ispair2 1)
   239         ]);
   240 
   241 qed_goal "contlub_Isfst" thy "contlub(Isfst)"
   242  (fn prems =>
   243         [
   244         (rtac contlubI 1),
   245         (strip_tac 1),
   246         (stac (lub_sprod RS thelubI) 1),
   247         (atac 1),
   248         (res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]  
   249                 (excluded_middle RS disjE) 1),
   250         (asm_simp_tac Sprod0_ss  1),
   251         (res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")]
   252                 ssubst 1),
   253         (atac 1),
   254         (rtac trans 1),
   255         (asm_simp_tac Sprod0_ss  1),
   256         (rtac sym 1),
   257         (rtac chain_UU_I_inverse 1),
   258         (rtac allI 1),
   259         (rtac strict_Isfst 1),
   260         (rtac swap 1),
   261         (etac (defined_IsfstIssnd RS conjunct2) 2),
   262         (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS 
   263                                   chain_UU_I RS spec]) 1)
   264         ]);
   265 
   266 qed_goal "contlub_Issnd" thy "contlub(Issnd)"
   267 (fn prems =>
   268         [
   269         (rtac contlubI 1),
   270         (strip_tac 1),
   271         (stac (lub_sprod RS thelubI) 1),
   272         (atac 1),
   273         (res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
   274          (excluded_middle RS disjE) 1),
   275         (asm_simp_tac Sprod0_ss  1),
   276         (res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] 
   277                 ssubst 1),
   278         (atac 1),
   279         (asm_simp_tac Sprod0_ss  1),
   280         (rtac sym 1),
   281         (rtac chain_UU_I_inverse 1),
   282         (rtac allI 1),
   283         (rtac strict_Issnd 1),
   284         (rtac swap 1),
   285         (etac (defined_IsfstIssnd RS conjunct1) 2),
   286         (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS
   287                                   chain_UU_I RS spec]) 1)
   288         ]);
   289 
   290 qed_goal "cont_Isfst" thy "cont(Isfst)"
   291 (fn prems =>
   292         [
   293         (rtac monocontlub2cont 1),
   294         (rtac monofun_Isfst 1),
   295         (rtac contlub_Isfst 1)
   296         ]);
   297 
   298 qed_goal "cont_Issnd" thy "cont(Issnd)"
   299 (fn prems =>
   300         [
   301         (rtac monocontlub2cont 1),
   302         (rtac monofun_Issnd 1),
   303         (rtac contlub_Issnd 1)
   304         ]);
   305 
   306 qed_goal "spair_eq" thy "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)"
   307  (fn prems =>
   308         [
   309         (cut_facts_tac prems 1),
   310         (fast_tac HOL_cs 1)
   311         ]);
   312 
   313 (* ------------------------------------------------------------------------ *)
   314 (* convert all lemmas to the continuous versions                            *)
   315 (* ------------------------------------------------------------------------ *)
   316 
   317 qed_goalw "beta_cfun_sprod" thy [spair_def]
   318         "(LAM x y. Ispair x y)`a`b = Ispair a b"
   319  (fn prems =>
   320         [
   321         (stac beta_cfun 1),
   322         (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1,
   323 					cont2cont_CF1L]) 1),
   324         (stac beta_cfun 1),
   325         (rtac cont_Ispair2 1),
   326         (rtac refl 1)
   327         ]);
   328 
   329 qed_goalw "inject_spair" thy [spair_def]
   330         "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba"
   331  (fn prems =>
   332         [
   333         (cut_facts_tac prems 1),
   334         (etac inject_Ispair 1),
   335         (atac 1),
   336         (etac box_equals 1),
   337         (rtac beta_cfun_sprod 1),
   338         (rtac beta_cfun_sprod 1)
   339         ]);
   340 
   341 qed_goalw "inst_sprod_pcpo2" thy [spair_def] "UU = (:UU,UU:)"
   342  (fn prems =>
   343         [
   344         (rtac sym 1),
   345         (rtac trans 1),
   346         (rtac beta_cfun_sprod 1),
   347         (rtac sym 1),
   348         (rtac inst_sprod_pcpo 1)
   349         ]);
   350 
   351 qed_goalw "strict_spair" thy [spair_def] 
   352         "(a=UU | b=UU) ==> (:a,b:)=UU"
   353  (fn prems =>
   354         [
   355         (cut_facts_tac prems 1),
   356         (rtac trans 1),
   357         (rtac beta_cfun_sprod 1),
   358         (rtac trans 1),
   359         (rtac (inst_sprod_pcpo RS sym) 2),
   360         (etac strict_Ispair 1)
   361         ]);
   362 
   363 qed_goalw "strict_spair1" thy [spair_def] "(:UU,b:) = UU"
   364  (fn prems =>
   365         [
   366         (stac beta_cfun_sprod 1),
   367         (rtac trans 1),
   368         (rtac (inst_sprod_pcpo RS sym) 2),
   369         (rtac strict_Ispair1 1)
   370         ]);
   371 
   372 qed_goalw "strict_spair2" thy [spair_def] "(:a,UU:) = UU"
   373  (fn prems =>
   374         [
   375         (stac beta_cfun_sprod 1),
   376         (rtac trans 1),
   377         (rtac (inst_sprod_pcpo RS sym) 2),
   378         (rtac strict_Ispair2 1)
   379         ]);
   380 
   381 qed_goalw "strict_spair_rev" thy [spair_def]
   382         "(:x,y:)~=UU ==> ~x=UU & ~y=UU"
   383  (fn prems =>
   384         [
   385         (cut_facts_tac prems 1),
   386         (rtac strict_Ispair_rev 1),
   387         (rtac (beta_cfun_sprod RS subst) 1),
   388         (rtac (inst_sprod_pcpo RS subst) 1),
   389         (atac 1)
   390         ]);
   391 
   392 qed_goalw "defined_spair_rev" thy [spair_def]
   393  "(:a,b:) = UU ==> (a = UU | b = UU)"
   394  (fn prems =>
   395         [
   396         (cut_facts_tac prems 1),
   397         (rtac defined_Ispair_rev 1),
   398         (rtac (beta_cfun_sprod RS subst) 1),
   399         (rtac (inst_sprod_pcpo RS subst) 1),
   400         (atac 1)
   401         ]);
   402 
   403 qed_goalw "defined_spair" thy [spair_def]
   404         "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
   405  (fn prems =>
   406         [
   407         (cut_facts_tac prems 1),
   408         (stac beta_cfun_sprod 1),
   409         (stac inst_sprod_pcpo 1),
   410         (etac defined_Ispair 1),
   411         (atac 1)
   412         ]);
   413 
   414 qed_goalw "Exh_Sprod2" thy [spair_def]
   415         "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)"
   416  (fn prems =>
   417         [
   418         (rtac (Exh_Sprod RS disjE) 1),
   419         (rtac disjI1 1),
   420         (stac inst_sprod_pcpo 1),
   421         (atac 1),
   422         (rtac disjI2 1),
   423         (etac exE 1),
   424         (etac exE 1),
   425         (rtac exI 1),
   426         (rtac exI 1),
   427         (rtac conjI 1),
   428         (stac beta_cfun_sprod 1),
   429         (fast_tac HOL_cs 1),
   430         (fast_tac HOL_cs 1)
   431         ]);
   432 
   433 
   434 qed_goalw "sprodE" thy [spair_def]
   435 "[|p=UU ==> Q;!!x y. [|p=(:x,y:);x~=UU ; y~=UU|] ==> Q|] ==> Q"
   436 (fn prems =>
   437         [
   438         (rtac IsprodE 1),
   439         (resolve_tac prems 1),
   440         (stac inst_sprod_pcpo 1),
   441         (atac 1),
   442         (resolve_tac prems 1),
   443         (atac 2),
   444         (atac 2),
   445         (stac beta_cfun_sprod 1),
   446         (atac 1)
   447         ]);
   448 
   449 
   450 qed_goalw "strict_sfst" thy [sfst_def] 
   451         "p=UU==>sfst`p=UU"
   452  (fn prems =>
   453         [
   454         (cut_facts_tac prems 1),
   455         (stac beta_cfun 1),
   456         (rtac cont_Isfst 1),
   457         (rtac strict_Isfst 1),
   458         (rtac (inst_sprod_pcpo RS subst) 1),
   459         (atac 1)
   460         ]);
   461 
   462 qed_goalw "strict_sfst1" thy [sfst_def,spair_def] 
   463         "sfst`(:UU,y:) = UU"
   464  (fn prems =>
   465         [
   466         (stac beta_cfun_sprod 1),
   467         (stac beta_cfun 1),
   468         (rtac cont_Isfst 1),
   469         (rtac strict_Isfst1 1)
   470         ]);
   471  
   472 qed_goalw "strict_sfst2" thy [sfst_def,spair_def] 
   473         "sfst`(:x,UU:) = UU"
   474  (fn prems =>
   475         [
   476         (stac beta_cfun_sprod 1),
   477         (stac beta_cfun 1),
   478         (rtac cont_Isfst 1),
   479         (rtac strict_Isfst2 1)
   480         ]);
   481 
   482 qed_goalw "strict_ssnd" thy [ssnd_def] 
   483         "p=UU==>ssnd`p=UU"
   484  (fn prems =>
   485         [
   486         (cut_facts_tac prems 1),
   487         (stac beta_cfun 1),
   488         (rtac cont_Issnd 1),
   489         (rtac strict_Issnd 1),
   490         (rtac (inst_sprod_pcpo RS subst) 1),
   491         (atac 1)
   492         ]);
   493 
   494 qed_goalw "strict_ssnd1" thy [ssnd_def,spair_def] 
   495         "ssnd`(:UU,y:) = UU"
   496  (fn prems =>
   497         [
   498         (stac beta_cfun_sprod 1),
   499         (stac beta_cfun 1),
   500         (rtac cont_Issnd 1),
   501         (rtac strict_Issnd1 1)
   502         ]);
   503 
   504 qed_goalw "strict_ssnd2" thy [ssnd_def,spair_def] 
   505         "ssnd`(:x,UU:) = UU"
   506  (fn prems =>
   507         [
   508         (stac beta_cfun_sprod 1),
   509         (stac beta_cfun 1),
   510         (rtac cont_Issnd 1),
   511         (rtac strict_Issnd2 1)
   512         ]);
   513 
   514 qed_goalw "sfst2" thy [sfst_def,spair_def] 
   515         "y~=UU ==>sfst`(:x,y:)=x"
   516  (fn prems =>
   517         [
   518         (cut_facts_tac prems 1),
   519         (stac beta_cfun_sprod 1),
   520         (stac beta_cfun 1),
   521         (rtac cont_Isfst 1),
   522         (etac Isfst2 1)
   523         ]);
   524 
   525 qed_goalw "ssnd2" thy [ssnd_def,spair_def] 
   526         "x~=UU ==>ssnd`(:x,y:)=y"
   527  (fn prems =>
   528         [
   529         (cut_facts_tac prems 1),
   530         (stac beta_cfun_sprod 1),
   531         (stac beta_cfun 1),
   532         (rtac cont_Issnd 1),
   533         (etac Issnd2 1)
   534         ]);
   535 
   536 
   537 qed_goalw "defined_sfstssnd" thy [sfst_def,ssnd_def,spair_def]
   538         "p~=UU ==> sfst`p ~=UU & ssnd`p ~=UU"
   539  (fn prems =>
   540         [
   541         (cut_facts_tac prems 1),
   542         (stac beta_cfun 1),
   543         (rtac cont_Issnd 1),
   544         (stac beta_cfun 1),
   545         (rtac cont_Isfst 1),
   546         (rtac defined_IsfstIssnd 1),
   547         (rtac (inst_sprod_pcpo RS subst) 1),
   548         (atac 1)
   549         ]);
   550  
   551 
   552 qed_goalw "surjective_pairing_Sprod2" thy 
   553         [sfst_def,ssnd_def,spair_def] "(:sfst`p , ssnd`p:) = p"
   554  (fn prems =>
   555         [
   556         (stac beta_cfun_sprod 1),
   557         (stac beta_cfun 1),
   558         (rtac cont_Issnd 1),
   559         (stac beta_cfun 1),
   560         (rtac cont_Isfst 1),
   561         (rtac (surjective_pairing_Sprod RS sym) 1)
   562         ]);
   563 
   564 
   565 qed_goalw "lub_sprod2" thy [sfst_def,ssnd_def,spair_def]
   566 "[|chain(S)|] ==> range(S) <<| \
   567 \ (: lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) :)"
   568  (fn prems =>
   569         [
   570         (cut_facts_tac prems 1),
   571         (stac beta_cfun_sprod 1),
   572         (stac (beta_cfun RS ext) 1),
   573         (rtac cont_Issnd 1),
   574         (stac (beta_cfun RS ext) 1),
   575         (rtac cont_Isfst 1),
   576         (rtac lub_sprod 1),
   577         (resolve_tac prems 1)
   578         ]);
   579 
   580 
   581 bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI);
   582 (*
   583  "chain ?S1 ==>
   584  lub (range ?S1) =
   585  (:lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i))):)" : thm
   586 *)
   587 
   588 qed_goalw "ssplit1" thy [ssplit_def]
   589         "ssplit`f`UU=UU"
   590  (fn prems =>
   591         [
   592         (stac beta_cfun 1),
   593         (Simp_tac 1),
   594         (stac strictify1 1),
   595         (rtac refl 1)
   596         ]);
   597 
   598 qed_goalw "ssplit2" thy [ssplit_def]
   599         "[|x~=UU;y~=UU|] ==> ssplit`f`(:x,y:)= f`x`y"
   600  (fn prems =>
   601         [
   602         (stac beta_cfun 1),
   603         (Simp_tac 1),
   604         (stac strictify2 1),
   605         (rtac defined_spair 1),
   606         (resolve_tac prems 1),
   607         (resolve_tac prems 1),
   608         (stac beta_cfun 1),
   609         (Simp_tac 1),
   610         (stac sfst2 1),
   611         (resolve_tac prems 1),
   612         (stac ssnd2 1),
   613         (resolve_tac prems 1),
   614         (rtac refl 1)
   615         ]);
   616 
   617 
   618 qed_goalw "ssplit3" thy [ssplit_def]
   619   "ssplit`spair`z=z"
   620  (fn prems =>
   621         [
   622         (stac beta_cfun 1),
   623         (Simp_tac 1),
   624         (case_tac "z=UU" 1),
   625         (hyp_subst_tac 1),
   626         (rtac strictify1 1),
   627         (rtac trans 1),
   628         (rtac strictify2 1),
   629         (atac 1),
   630         (stac beta_cfun 1),
   631         (Simp_tac 1),
   632         (rtac surjective_pairing_Sprod2 1)
   633         ]);
   634 
   635 (* ------------------------------------------------------------------------ *)
   636 (* install simplifier for Sprod                                             *)
   637 (* ------------------------------------------------------------------------ *)
   638 
   639 val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
   640                 strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair,
   641                 ssplit1,ssplit2];
   642 Addsimps Sprod_rews;
   643