isabelle: src/HOLCF/Up2.ML@645f46a24c72

     1 (*  Title:      HOLCF/Up2.ML

     2     ID:         $Id$

     3     Author:     Franz Regensburger

     4     Copyright   1993 Technische Universitaet Muenchen

     6 Lemmas for Up2.thy

     7 *)

     9 open Up2;

    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         ]);

    22 (* -------------------------------------------------------------------------*)

    23 (* type ('a)u is pointed                                                    *)

    24 (* ------------------------------------------------------------------------ *)

    26 qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"

    27  (fn prems =>

    28         [

    29         (simp_tac (simpset() addsimps [less_up1a]) 1)

    30         ]);

    32 bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);

    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         ]);

    41 (* -------------------------------------------------------------------------*)

    42 (* access to less_up in class po                                          *)

    43 (* ------------------------------------------------------------------------ *)

    45 qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"

    46  (fn prems =>

    47         [

    48         (simp_tac (simpset() addsimps [less_up1b]) 1)

    49         ]);

    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         ]);

    57 (* ------------------------------------------------------------------------ *)

    58 (* Iup and Ifup are monotone                                               *)

    59 (* ------------------------------------------------------------------------ *)

    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         ]);

    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         ]);

    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         ]);

    98 (* ------------------------------------------------------------------------ *)

    99 (* Some kind of surjectivity lemma                                          *)

   100 (* ------------------------------------------------------------------------ *)

   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         ]);

   109 (* ------------------------------------------------------------------------ *)

   110 (* ('a)u is a cpo                                                           *)

   111 (* ------------------------------------------------------------------------ *)

   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         ]);

   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         ]);

   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 *)

   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 *)

   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         ]);

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--