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