src/HOLCF/Sprod2.ML
author clasohm
Tue Jan 30 13:42:57 1996 +0100 (1996-01-30)
changeset 1461 6bcb44e4d6e5
parent 1168 74be52691d62
child 1779 1155c06fa956
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      HOLCF/sprod2.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for sprod2.thy
     7 *)
     8 
     9 
    10 open Sprod2;
    11 
    12 (* ------------------------------------------------------------------------ *)
    13 (* access to less_sprod in class po                                         *)
    14 (* ------------------------------------------------------------------------ *)
    15 
    16 qed_goal "less_sprod3a" Sprod2.thy 
    17         "p1=Ispair UU UU ==> p1 << p2"
    18 (fn prems =>
    19         [
    20         (cut_facts_tac prems 1),
    21         (rtac (inst_sprod_po RS ssubst) 1),
    22         (etac less_sprod1a 1)
    23         ]);
    24 
    25 
    26 qed_goal "less_sprod3b" Sprod2.thy
    27  "p1~=Ispair UU UU ==>\
    28 \       (p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))" 
    29 (fn prems =>
    30         [
    31         (cut_facts_tac prems 1),
    32         (rtac (inst_sprod_po RS ssubst) 1),
    33         (etac less_sprod1b 1)
    34         ]);
    35 
    36 qed_goal "less_sprod4b" Sprod2.thy 
    37         "p << Ispair UU UU ==> p = Ispair UU UU"
    38 (fn prems =>
    39         [
    40         (cut_facts_tac prems 1),
    41         (rtac less_sprod2b 1),
    42         (etac (inst_sprod_po RS subst) 1)
    43         ]);
    44 
    45 val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
    46 (* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *)
    47 
    48 qed_goal "less_sprod4c" Sprod2.thy
    49  "[|Ispair xa ya << Ispair x y; xa~=UU; ya~=UU; x~=UU; y~=UU|] ==>\
    50 \               xa<<x & ya << y"
    51 (fn prems =>
    52         [
    53         (cut_facts_tac prems 1),
    54         (rtac less_sprod2c 1),
    55         (etac (inst_sprod_po RS subst) 1),
    56         (REPEAT (atac 1))
    57         ]);
    58 
    59 (* ------------------------------------------------------------------------ *)
    60 (* type sprod is pointed                                                    *)
    61 (* ------------------------------------------------------------------------ *)
    62 
    63 qed_goal "minimal_sprod" Sprod2.thy  "Ispair UU UU << p"
    64 (fn prems =>
    65         [
    66         (rtac less_sprod3a 1),
    67         (rtac refl 1)
    68         ]);
    69 
    70 (* ------------------------------------------------------------------------ *)
    71 (* Ispair is monotone in both arguments                                     *)
    72 (* ------------------------------------------------------------------------ *)
    73 
    74 qed_goalw "monofun_Ispair1" Sprod2.thy [monofun] "monofun(Ispair)"
    75 (fn prems =>
    76         [
    77         (strip_tac 1),
    78         (rtac (less_fun RS iffD2) 1),
    79         (strip_tac 1),
    80         (res_inst_tac [("Q",
    81         " Ispair y xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
    82         (res_inst_tac [("Q",
    83         " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
    84         (rtac (less_sprod3b RS iffD2) 1),
    85         (atac 1),
    86         (rtac conjI 1),
    87         (rtac (Isfst RS ssubst) 1),
    88         (etac (strict_Ispair_rev RS conjunct1) 1),
    89         (etac (strict_Ispair_rev RS conjunct2) 1),
    90         (rtac (Isfst RS ssubst) 1),
    91         (etac (strict_Ispair_rev RS conjunct1) 1),
    92         (etac (strict_Ispair_rev RS conjunct2) 1),
    93         (atac 1),
    94         (rtac (Issnd RS ssubst) 1),
    95         (etac (strict_Ispair_rev RS conjunct1) 1),
    96         (etac (strict_Ispair_rev RS conjunct2) 1),
    97         (rtac (Issnd RS ssubst) 1),
    98         (etac (strict_Ispair_rev RS conjunct1) 1),
    99         (etac (strict_Ispair_rev RS conjunct2) 1),
   100         (rtac refl_less 1),
   101         (etac less_sprod3a 1),
   102         (res_inst_tac [("Q",
   103         " Ispair x xa  = Ispair UU UU")] (excluded_middle RS disjE) 1),
   104         (etac less_sprod3a 2),
   105         (res_inst_tac [("P","Ispair y xa = Ispair UU UU")] notE 1),
   106         (atac 2),
   107         (rtac defined_Ispair 1),
   108         (etac notUU_I 1),
   109         (etac (strict_Ispair_rev RS  conjunct1) 1),
   110         (etac (strict_Ispair_rev RS  conjunct2) 1)
   111         ]);
   112 
   113 
   114 qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))"
   115 (fn prems =>
   116         [
   117         (strip_tac 1),
   118         (res_inst_tac [("Q",
   119         " Ispair x y = Ispair UU UU")] (excluded_middle RS disjE) 1),
   120         (res_inst_tac [("Q",
   121         " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   122         (rtac (less_sprod3b RS iffD2) 1),
   123         (atac 1),
   124         (rtac conjI 1),
   125         (rtac (Isfst RS ssubst) 1),
   126         (etac (strict_Ispair_rev RS conjunct1) 1),
   127         (etac (strict_Ispair_rev RS conjunct2) 1),
   128         (rtac (Isfst RS ssubst) 1),
   129         (etac (strict_Ispair_rev RS conjunct1) 1),
   130         (etac (strict_Ispair_rev RS conjunct2) 1),
   131         (rtac refl_less 1),
   132         (rtac (Issnd RS ssubst) 1),
   133         (etac (strict_Ispair_rev RS conjunct1) 1),
   134         (etac (strict_Ispair_rev RS conjunct2) 1),
   135         (rtac (Issnd RS ssubst) 1),
   136         (etac (strict_Ispair_rev RS conjunct1) 1),
   137         (etac (strict_Ispair_rev RS conjunct2) 1),
   138         (atac 1),
   139         (etac less_sprod3a 1),
   140         (res_inst_tac [("Q",
   141         " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   142         (etac less_sprod3a 2),
   143         (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
   144         (atac 2),
   145         (rtac defined_Ispair 1),
   146         (etac (strict_Ispair_rev RS  conjunct1) 1),
   147         (etac notUU_I 1),
   148         (etac (strict_Ispair_rev RS  conjunct2) 1)
   149         ]);
   150 
   151 qed_goal " monofun_Ispair" Sprod2.thy 
   152  "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
   153 (fn prems =>
   154         [
   155         (cut_facts_tac prems 1),
   156         (rtac trans_less 1),
   157         (rtac (monofun_Ispair1 RS monofunE RS spec RS spec RS mp RS 
   158         (less_fun RS iffD1 RS spec)) 1),
   159         (rtac (monofun_Ispair2 RS monofunE RS spec RS spec RS mp) 2),
   160         (atac 1),
   161         (atac 1)
   162         ]);
   163 
   164 
   165 (* ------------------------------------------------------------------------ *)
   166 (* Isfst and Issnd are monotone                                             *)
   167 (* ------------------------------------------------------------------------ *)
   168 
   169 qed_goalw " monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
   170 (fn prems =>
   171         [
   172         (strip_tac 1),
   173         (res_inst_tac [("p","x")] IsprodE 1),
   174         (hyp_subst_tac 1),
   175         (rtac trans_less 1),
   176         (rtac minimal 2),
   177         (rtac (strict_Isfst1 RS ssubst) 1),
   178         (rtac refl_less 1),
   179         (hyp_subst_tac 1),
   180         (res_inst_tac [("p","y")] IsprodE 1),
   181         (hyp_subst_tac 1),
   182         (res_inst_tac [("t","Isfst(Ispair xa ya)")] subst 1),
   183         (rtac refl_less 2),
   184         (etac (less_sprod4b RS sym RS arg_cong) 1),
   185         (hyp_subst_tac 1),
   186         (rtac (Isfst RS ssubst) 1),
   187         (atac 1),
   188         (atac 1),
   189         (rtac (Isfst RS ssubst) 1),
   190         (atac 1),
   191         (atac 1),
   192         (etac (less_sprod4c RS  conjunct1) 1),
   193         (REPEAT (atac 1))
   194         ]);
   195 
   196 qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)"
   197 (fn prems =>
   198         [
   199         (strip_tac 1),
   200         (res_inst_tac [("p","x")] IsprodE 1),
   201         (hyp_subst_tac 1),
   202         (rtac trans_less 1),
   203         (rtac minimal 2),
   204         (rtac (strict_Issnd1 RS ssubst) 1),
   205         (rtac refl_less 1),
   206         (hyp_subst_tac 1),
   207         (res_inst_tac [("p","y")] IsprodE 1),
   208         (hyp_subst_tac 1),
   209         (res_inst_tac [("t","Issnd(Ispair xa ya)")] subst 1),
   210         (rtac refl_less 2),
   211         (etac (less_sprod4b RS sym RS arg_cong) 1),
   212         (hyp_subst_tac 1),
   213         (rtac (Issnd RS ssubst) 1),
   214         (atac 1),
   215         (atac 1),
   216         (rtac (Issnd RS ssubst) 1),
   217         (atac 1),
   218         (atac 1),
   219         (etac (less_sprod4c RS  conjunct2) 1),
   220         (REPEAT (atac 1))
   221         ]);
   222 
   223 
   224 (* ------------------------------------------------------------------------ *)
   225 (* the type 'a ** 'b is a cpo                                               *)
   226 (* ------------------------------------------------------------------------ *)
   227 
   228 qed_goal "lub_sprod" Sprod2.thy 
   229 "[|is_chain(S)|] ==> range(S) <<| \
   230 \ Ispair (lub(range(%i.Isfst(S i)))) (lub(range(%i.Issnd(S i))))"
   231 (fn prems =>
   232         [
   233         (cut_facts_tac prems 1),
   234         (rtac is_lubI 1),
   235         (rtac conjI 1),
   236         (rtac ub_rangeI 1),
   237         (rtac allI 1),
   238         (res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1),
   239         (rtac monofun_Ispair 1),
   240         (rtac is_ub_thelub 1),
   241         (etac (monofun_Isfst RS ch2ch_monofun) 1),
   242         (rtac is_ub_thelub 1),
   243         (etac (monofun_Issnd RS ch2ch_monofun) 1),
   244         (strip_tac 1),
   245         (res_inst_tac [("t","u")] (surjective_pairing_Sprod RS ssubst) 1),
   246         (rtac monofun_Ispair 1),
   247         (rtac is_lub_thelub 1),
   248         (etac (monofun_Isfst RS ch2ch_monofun) 1),
   249         (etac (monofun_Isfst RS ub2ub_monofun) 1),
   250         (rtac is_lub_thelub 1),
   251         (etac (monofun_Issnd RS ch2ch_monofun) 1),
   252         (etac (monofun_Issnd RS ub2ub_monofun) 1)
   253         ]);
   254 
   255 val thelub_sprod = (lub_sprod RS thelubI);
   256 
   257 
   258 qed_goal "cpo_sprod" Sprod2.thy 
   259         "is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
   260 (fn prems =>
   261         [
   262         (cut_facts_tac prems 1),
   263         (rtac exI 1),
   264         (etac lub_sprod 1)
   265         ]);
   266 
   267 
   268 
   269 
   270 
   271 
   272 
   273