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