src/HOLCF/Cprod2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4721 c8a8482a8124
child 9245 428385c4bc50
permissions -rw-r--r--
made tutorial first;
     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 (* for compatibility with old HOLCF-Version *)
    12 qed_goal "inst_cprod_po" thy "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
    13  (fn prems => 
    14         [
    15         (fold_goals_tac [less_cprod_def]),
    16         (rtac refl 1)
    17         ]);
    18 
    19 qed_goalw "less_cprod4c" thy [inst_cprod_po RS eq_reflection]
    20  "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"
    21  (fn prems =>
    22         [
    23         (cut_facts_tac prems 1),
    24         (etac conjE 1),
    25         (dtac (fst_conv RS subst) 1),
    26         (dtac (fst_conv RS subst) 1),
    27         (dtac (fst_conv RS subst) 1),
    28         (dtac (snd_conv RS subst) 1),
    29         (dtac (snd_conv RS subst) 1),
    30         (dtac (snd_conv RS subst) 1),
    31         (rtac conjI 1),
    32         (atac 1),
    33         (atac 1)
    34         ]);
    35 
    36 (* ------------------------------------------------------------------------ *)
    37 (* type cprod is pointed                                                    *)
    38 (* ------------------------------------------------------------------------ *)
    39 
    40 qed_goal "minimal_cprod" thy  "(UU,UU)<<p"
    41 (fn prems =>
    42         [
    43         (simp_tac(simpset() addsimps[inst_cprod_po])1)
    44         ]);
    45 
    46 bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym);
    47 
    48 qed_goal "least_cprod" thy "? x::'a*'b.!y. x<<y"
    49 (fn prems =>
    50         [
    51         (res_inst_tac [("x","(UU,UU)")] exI 1),
    52         (rtac (minimal_cprod RS allI) 1)
    53         ]);
    54 
    55 (* ------------------------------------------------------------------------ *)
    56 (* Pair <_,_>  is monotone in both arguments                                *)
    57 (* ------------------------------------------------------------------------ *)
    58 
    59 qed_goalw "monofun_pair1" thy [monofun] "monofun Pair"
    60  (fn prems =>
    61         [
    62         (strip_tac 1),
    63         (rtac (less_fun RS iffD2) 1),
    64         (strip_tac 1),
    65         (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1)
    66         ]);
    67 
    68 qed_goalw "monofun_pair2" thy [monofun] "monofun(Pair x)"
    69  (fn prems =>
    70         [
    71         (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1)
    72         ]);
    73 
    74 qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
    75  (fn prems =>
    76         [
    77         (cut_facts_tac prems 1),
    78         (rtac trans_less 1),
    79         (rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS 
    80         (less_fun RS iffD1 RS spec)) 1),
    81         (rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2),
    82         (atac 1),
    83         (atac 1)
    84         ]);
    85 
    86 (* ------------------------------------------------------------------------ *)
    87 (* fst and snd are monotone                                                 *)
    88 (* ------------------------------------------------------------------------ *)
    89 
    90 qed_goalw "monofun_fst" thy [monofun] "monofun fst"
    91  (fn prems =>
    92         [
    93         (strip_tac 1),
    94         (res_inst_tac [("p","x")] PairE 1),
    95         (hyp_subst_tac 1),
    96         (res_inst_tac [("p","y")] PairE 1),
    97         (hyp_subst_tac 1),
    98         (Asm_simp_tac  1),
    99         (etac (less_cprod4c RS conjunct1) 1)
   100         ]);
   101 
   102 qed_goalw "monofun_snd" thy [monofun] "monofun snd"
   103  (fn prems =>
   104         [
   105         (strip_tac 1),
   106         (res_inst_tac [("p","x")] PairE 1),
   107         (hyp_subst_tac 1),
   108         (res_inst_tac [("p","y")] PairE 1),
   109         (hyp_subst_tac 1),
   110         (Asm_simp_tac  1),
   111         (etac (less_cprod4c RS conjunct2) 1)
   112         ]);
   113 
   114 (* ------------------------------------------------------------------------ *)
   115 (* the type 'a * 'b is a cpo                                                *)
   116 (* ------------------------------------------------------------------------ *)
   117 
   118 qed_goal "lub_cprod" thy 
   119 "chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
   120  (fn prems =>
   121         [
   122         (cut_facts_tac prems 1),
   123         (rtac (conjI RS is_lubI) 1),
   124         (rtac (allI RS ub_rangeI) 1),
   125         (res_inst_tac [("t","S i")] (surjective_pairing RS ssubst) 1),
   126         (rtac monofun_pair 1),
   127         (rtac is_ub_thelub 1),
   128         (etac (monofun_fst RS ch2ch_monofun) 1),
   129         (rtac is_ub_thelub 1),
   130         (etac (monofun_snd RS ch2ch_monofun) 1),
   131         (strip_tac 1),
   132         (res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1),
   133         (rtac monofun_pair 1),
   134         (rtac is_lub_thelub 1),
   135         (etac (monofun_fst RS ch2ch_monofun) 1),
   136         (etac (monofun_fst RS ub2ub_monofun) 1),
   137         (rtac is_lub_thelub 1),
   138         (etac (monofun_snd RS ch2ch_monofun) 1),
   139         (etac (monofun_snd RS ub2ub_monofun) 1)
   140         ]);
   141 
   142 bind_thm ("thelub_cprod", lub_cprod RS thelubI);
   143 (*
   144 "chain ?S1 ==>
   145  lub (range ?S1) =
   146  (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
   147 
   148 *)
   149 
   150 qed_goal "cpo_cprod" thy "chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"
   151 (fn prems =>
   152         [
   153         (cut_facts_tac prems 1),
   154         (rtac exI 1),
   155         (etac lub_cprod 1)
   156         ]);
   157 
   158