src/HOLCF/Cprod2.ML
author clasohm
Tue Jan 30 13:42:57 1996 +0100 (1996-01-30)
changeset 1461 6bcb44e4d6e5
parent 1267 bca91b4e1710
child 1779 1155c06fa956
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      HOLCF/cprod2.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for cprod2.thy 
     7 *)
     8 
     9 open Cprod2;
    10 
    11 qed_goal "less_cprod3a" Cprod2.thy 
    12         "p1=(UU,UU) ==> p1 << p2"
    13  (fn prems =>
    14         [
    15         (cut_facts_tac prems 1),
    16         (rtac (inst_cprod_po RS ssubst) 1),
    17         (rtac (less_cprod1b RS ssubst) 1),
    18         (hyp_subst_tac 1),
    19         (Asm_simp_tac  1)
    20         ]);
    21 
    22 qed_goal "less_cprod3b" Cprod2.thy
    23  "(p1 << p2) = (fst(p1)<<fst(p2) & snd(p1)<<snd(p2))"
    24  (fn prems =>
    25         [
    26         (rtac (inst_cprod_po RS ssubst) 1),
    27         (rtac less_cprod1b 1)
    28         ]);
    29 
    30 qed_goal "less_cprod4a" Cprod2.thy 
    31         "(x1,x2) << (UU,UU) ==> x1=UU & x2=UU"
    32  (fn prems =>
    33         [
    34         (cut_facts_tac prems 1),
    35         (rtac less_cprod2a 1),
    36         (etac (inst_cprod_po RS subst) 1)
    37         ]);
    38 
    39 qed_goal "less_cprod4b" Cprod2.thy 
    40         "p << (UU,UU) ==> p = (UU,UU)"
    41 (fn prems =>
    42         [
    43         (cut_facts_tac prems 1),
    44         (rtac less_cprod2b 1),
    45         (etac (inst_cprod_po RS subst) 1)
    46         ]);
    47 
    48 qed_goal "less_cprod4c" Cprod2.thy
    49  " (xa,ya) << (x,y) ==> xa<<x & ya << y"
    50 (fn prems =>
    51         [
    52         (cut_facts_tac prems 1),
    53         (rtac less_cprod2c 1),
    54         (etac (inst_cprod_po RS subst) 1),
    55         (REPEAT (atac 1))
    56         ]);
    57 
    58 (* ------------------------------------------------------------------------ *)
    59 (* type cprod is pointed                                                    *)
    60 (* ------------------------------------------------------------------------ *)
    61 
    62 qed_goal "minimal_cprod" Cprod2.thy  "(UU,UU)<<p"
    63 (fn prems =>
    64         [
    65         (rtac less_cprod3a 1),
    66         (rtac refl 1)
    67         ]);
    68 
    69 (* ------------------------------------------------------------------------ *)
    70 (* Pair <_,_>  is monotone in both arguments                                *)
    71 (* ------------------------------------------------------------------------ *)
    72 
    73 qed_goalw "monofun_pair1" Cprod2.thy [monofun] "monofun(Pair)"
    74  (fn prems =>
    75         [
    76         (strip_tac 1),
    77         (rtac (less_fun RS iffD2) 1),
    78         (strip_tac 1),
    79         (rtac (less_cprod3b RS iffD2) 1),
    80         (Simp_tac 1)
    81         ]);
    82 
    83 qed_goalw "monofun_pair2" Cprod2.thy [monofun] "monofun(Pair(x))"
    84  (fn prems =>
    85         [
    86         (strip_tac 1),
    87         (rtac (less_cprod3b RS iffD2) 1),
    88         (Simp_tac 1)
    89         ]);
    90 
    91 qed_goal "monofun_pair" Cprod2.thy 
    92  "[|x1<<x2; y1<<y2|] ==> (x1,y1) << (x2,y2)"
    93  (fn prems =>
    94         [
    95         (cut_facts_tac prems 1),
    96         (rtac trans_less 1),
    97         (rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS 
    98         (less_fun RS iffD1 RS spec)) 1),
    99         (rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2),
   100         (atac 1),
   101         (atac 1)
   102         ]);
   103 
   104 (* ------------------------------------------------------------------------ *)
   105 (* fst and snd are monotone                                                 *)
   106 (* ------------------------------------------------------------------------ *)
   107 
   108 qed_goalw "monofun_fst" Cprod2.thy [monofun] "monofun(fst)"
   109  (fn prems =>
   110         [
   111         (strip_tac 1),
   112         (res_inst_tac [("p","x")] PairE 1),
   113         (hyp_subst_tac 1),
   114         (res_inst_tac [("p","y")] PairE 1),
   115         (hyp_subst_tac 1),
   116         (Asm_simp_tac  1),
   117         (etac (less_cprod4c RS conjunct1) 1)
   118         ]);
   119 
   120 qed_goalw "monofun_snd" Cprod2.thy [monofun] "monofun(snd)"
   121  (fn prems =>
   122         [
   123         (strip_tac 1),
   124         (res_inst_tac [("p","x")] PairE 1),
   125         (hyp_subst_tac 1),
   126         (res_inst_tac [("p","y")] PairE 1),
   127         (hyp_subst_tac 1),
   128         (Asm_simp_tac  1),
   129         (etac (less_cprod4c RS conjunct2) 1)
   130         ]);
   131 
   132 (* ------------------------------------------------------------------------ *)
   133 (* the type 'a * 'b is a cpo                                                *)
   134 (* ------------------------------------------------------------------------ *)
   135 
   136 qed_goal "lub_cprod" Cprod2.thy 
   137 " is_chain(S) ==> range(S) <<| \
   138 \   (lub(range(%i.fst(S i))),lub(range(%i.snd(S i)))) "
   139  (fn prems =>
   140         [
   141         (cut_facts_tac prems 1),
   142         (rtac is_lubI 1),
   143         (rtac conjI 1),
   144         (rtac ub_rangeI 1),
   145         (rtac allI 1),
   146         (res_inst_tac [("t","S(i)")] (surjective_pairing RS ssubst) 1),
   147         (rtac monofun_pair 1),
   148         (rtac is_ub_thelub 1),
   149         (etac (monofun_fst RS ch2ch_monofun) 1),
   150         (rtac is_ub_thelub 1),
   151         (etac (monofun_snd RS ch2ch_monofun) 1),
   152         (strip_tac 1),
   153         (res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1),
   154         (rtac monofun_pair 1),
   155         (rtac is_lub_thelub 1),
   156         (etac (monofun_fst RS ch2ch_monofun) 1),
   157         (etac (monofun_fst RS ub2ub_monofun) 1),
   158         (rtac is_lub_thelub 1),
   159         (etac (monofun_snd RS ch2ch_monofun) 1),
   160         (etac (monofun_snd RS ub2ub_monofun) 1)
   161         ]);
   162 
   163 val thelub_cprod = (lub_cprod RS thelubI);
   164 (*
   165 "is_chain ?S1 ==>
   166  lub (range ?S1) =
   167  (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
   168 
   169 *)
   170 
   171 qed_goal "cpo_cprod" Cprod2.thy 
   172         "is_chain(S::nat=>'a*'b)==>? x.range(S)<<| x"
   173 (fn prems =>
   174         [
   175         (cut_facts_tac prems 1),
   176         (rtac exI 1),
   177         (etac lub_cprod 1)
   178         ]);
   179 
   180