src/HOLCF/Up2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4721 c8a8482a8124
child 9169 85a47aa21f74
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/Up2.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for Up2.thy 
     7 *)
     8 
     9 open Up2;
    10 
    11 (* for compatibility with old HOLCF-Version *)
    12 qed_goal "inst_up_po" thy "(op <<)=(%x1 x2. case Rep_Up(x1) of \               
    13 \               Inl(y1) => True \
    14 \             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False \
    15 \                                            | Inr(z2) => y2<<z2))"
    16  (fn prems => 
    17         [
    18         (fold_goals_tac [less_up_def]),
    19         (rtac refl 1)
    20         ]);
    21 
    22 (* -------------------------------------------------------------------------*)
    23 (* type ('a)u is pointed                                                    *)
    24 (* ------------------------------------------------------------------------ *)
    25 
    26 qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"
    27  (fn prems =>
    28         [
    29         (simp_tac (simpset() addsimps [less_up1a]) 1)
    30         ]);
    31 
    32 bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
    33 
    34 qed_goal "least_up" thy "? x::'a u.!y. x<<y"
    35 (fn prems =>
    36         [
    37         (res_inst_tac [("x","Abs_Up(Inl ())")] exI 1),
    38         (rtac (minimal_up RS allI) 1)
    39         ]);
    40 
    41 (* -------------------------------------------------------------------------*)
    42 (* access to less_up in class po                                          *)
    43 (* ------------------------------------------------------------------------ *)
    44 
    45 qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"
    46  (fn prems =>
    47         [
    48         (simp_tac (simpset() addsimps [less_up1b]) 1)
    49         ]);
    50 
    51 qed_goal "less_up2c" thy "(Iup(x)<<Iup(y)) = (x<<y)"
    52  (fn prems =>
    53         [
    54         (simp_tac (simpset() addsimps [less_up1c]) 1)
    55         ]);
    56 
    57 (* ------------------------------------------------------------------------ *)
    58 (* Iup and Ifup are monotone                                               *)
    59 (* ------------------------------------------------------------------------ *)
    60 
    61 qed_goalw "monofun_Iup" thy [monofun] "monofun(Iup)"
    62  (fn prems =>
    63         [
    64         (strip_tac 1),
    65         (etac (less_up2c RS iffD2) 1)
    66         ]);
    67 
    68 qed_goalw "monofun_Ifup1" thy [monofun] "monofun(Ifup)"
    69  (fn prems =>
    70         [
    71         (strip_tac 1),
    72         (rtac (less_fun RS iffD2) 1),
    73         (strip_tac 1),
    74         (res_inst_tac [("p","xa")] upE 1),
    75         (asm_simp_tac Up0_ss 1),
    76         (asm_simp_tac Up0_ss 1),
    77         (etac monofun_cfun_fun 1)
    78         ]);
    79 
    80 qed_goalw "monofun_Ifup2" thy [monofun] "monofun(Ifup(f))"
    81  (fn prems =>
    82         [
    83         (strip_tac 1),
    84         (res_inst_tac [("p","x")] upE 1),
    85         (asm_simp_tac Up0_ss 1),
    86         (asm_simp_tac Up0_ss 1),
    87         (res_inst_tac [("p","y")] upE 1),
    88         (hyp_subst_tac 1),
    89         (rtac notE 1),
    90         (rtac less_up2b 1),
    91         (atac 1),
    92         (asm_simp_tac Up0_ss 1),
    93         (rtac monofun_cfun_arg 1),
    94         (hyp_subst_tac 1),
    95         (etac (less_up2c  RS iffD1) 1)
    96         ]);
    97 
    98 (* ------------------------------------------------------------------------ *)
    99 (* Some kind of surjectivity lemma                                          *)
   100 (* ------------------------------------------------------------------------ *)
   101 
   102 qed_goal "up_lemma1" thy  "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
   103  (fn prems =>
   104         [
   105         (cut_facts_tac prems 1),
   106         (asm_simp_tac Up0_ss 1)
   107         ]);
   108 
   109 (* ------------------------------------------------------------------------ *)
   110 (* ('a)u is a cpo                                                           *)
   111 (* ------------------------------------------------------------------------ *)
   112 
   113 qed_goal "lub_up1a" thy 
   114 "[|chain(Y);? i x. Y(i)=Iup(x)|] ==>\
   115 \ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
   116  (fn prems =>
   117         [
   118         (cut_facts_tac prems 1),
   119         (rtac is_lubI 1),
   120         (rtac conjI 1),
   121         (rtac ub_rangeI 1),
   122         (rtac allI 1),
   123         (res_inst_tac [("p","Y(i)")] upE 1),
   124         (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] subst 1),
   125         (etac sym 1),
   126         (rtac minimal_up 1),
   127         (res_inst_tac [("t","Y(i)")] (up_lemma1 RS subst) 1),
   128         (atac 1),
   129         (rtac (less_up2c RS iffD2) 1),
   130         (rtac is_ub_thelub 1),
   131         (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
   132         (strip_tac 1),
   133         (res_inst_tac [("p","u")] upE 1),
   134         (etac exE 1),
   135         (etac exE 1),
   136         (res_inst_tac [("P","Y(i)<<Abs_Up (Inl ())")] notE 1),
   137         (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
   138         (atac 1),
   139         (rtac less_up2b 1),
   140         (hyp_subst_tac 1),
   141         (etac (ub_rangeE RS spec) 1),
   142         (res_inst_tac [("t","u")] (up_lemma1 RS subst) 1),
   143         (atac 1),
   144         (rtac (less_up2c RS iffD2) 1),
   145         (rtac is_lub_thelub 1),
   146         (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
   147         (etac (monofun_Ifup2 RS ub2ub_monofun) 1)
   148         ]);
   149 
   150 qed_goal "lub_up1b" thy 
   151 "[|chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
   152 \ range(Y) <<| Abs_Up (Inl ())"
   153  (fn prems =>
   154         [
   155         (cut_facts_tac prems 1),
   156         (rtac is_lubI 1),
   157         (rtac conjI 1),
   158         (rtac ub_rangeI 1),
   159         (rtac allI 1),
   160         (res_inst_tac [("p","Y(i)")] upE 1),
   161         (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] ssubst 1),
   162         (atac 1),
   163         (rtac refl_less 1),
   164         (rtac notE 1),
   165         (dtac spec 1),
   166         (dtac spec 1),
   167         (atac 1),
   168         (atac 1),
   169         (strip_tac 1),
   170         (rtac minimal_up 1)
   171         ]);
   172 
   173 bind_thm ("thelub_up1a", lub_up1a RS thelubI);
   174 (*
   175 [| chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
   176  lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
   177 *)
   178 
   179 bind_thm ("thelub_up1b", lub_up1b RS thelubI);
   180 (*
   181 [| chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
   182  lub (range ?Y1) = UU_up
   183 *)
   184 
   185 qed_goal "cpo_up" thy 
   186         "chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
   187  (fn prems =>
   188         [
   189         (cut_facts_tac prems 1),
   190         (rtac disjE 1),
   191         (rtac exI 2),
   192         (etac lub_up1a 2),
   193         (atac 2),
   194         (rtac exI 2),
   195         (etac lub_up1b 2),
   196         (atac 2),
   197         (fast_tac HOL_cs 1)
   198         ]);
   199