1 (* Title: HOLCF/Up2.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 |
|
5 Class Instance u::(pcpo)po |
|
6 *) |
|
7 |
|
8 (* for compatibility with old HOLCF-Version *) |
|
9 Goal "(op <<)=(%x1 x2. case Rep_Up(x1) of \ |
|
10 \ Inl(y1) => True \ |
|
11 \ | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False \ |
|
12 \ | Inr(z2) => y2<<z2))"; |
|
13 by (fold_goals_tac [less_up_def]); |
|
14 by (rtac refl 1); |
|
15 qed "inst_up_po"; |
|
16 |
|
17 (* -------------------------------------------------------------------------*) |
|
18 (* type ('a)u is pointed *) |
|
19 (* ------------------------------------------------------------------------ *) |
|
20 |
|
21 Goal "Abs_Up(Inl ()) << z"; |
|
22 by (simp_tac (simpset() addsimps [less_up1a]) 1); |
|
23 qed "minimal_up"; |
|
24 |
|
25 bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym); |
|
26 |
|
27 Goal "EX x::'a u. ALL y. x<<y"; |
|
28 by (res_inst_tac [("x","Abs_Up(Inl ())")] exI 1); |
|
29 by (rtac (minimal_up RS allI) 1); |
|
30 qed "least_up"; |
|
31 |
|
32 (* -------------------------------------------------------------------------*) |
|
33 (* access to less_up in class po *) |
|
34 (* ------------------------------------------------------------------------ *) |
|
35 |
|
36 Goal "~ Iup(x) << Abs_Up(Inl ())"; |
|
37 by (simp_tac (simpset() addsimps [less_up1b]) 1); |
|
38 qed "less_up2b"; |
|
39 |
|
40 Goal "(Iup(x)<<Iup(y)) = (x<<y)"; |
|
41 by (simp_tac (simpset() addsimps [less_up1c]) 1); |
|
42 qed "less_up2c"; |
|
43 |
|
44 (* ------------------------------------------------------------------------ *) |
|
45 (* Iup and Ifup are monotone *) |
|
46 (* ------------------------------------------------------------------------ *) |
|
47 |
|
48 Goalw [monofun] "monofun(Iup)"; |
|
49 by (strip_tac 1); |
|
50 by (etac (less_up2c RS iffD2) 1); |
|
51 qed "monofun_Iup"; |
|
52 |
|
53 Goalw [monofun] "monofun(Ifup)"; |
|
54 by (strip_tac 1); |
|
55 by (rtac (less_fun RS iffD2) 1); |
|
56 by (strip_tac 1); |
|
57 by (res_inst_tac [("p","xa")] upE 1); |
|
58 by (asm_simp_tac Up0_ss 1); |
|
59 by (asm_simp_tac Up0_ss 1); |
|
60 by (etac monofun_cfun_fun 1); |
|
61 qed "monofun_Ifup1"; |
|
62 |
|
63 Goalw [monofun] "monofun(Ifup(f))"; |
|
64 by (strip_tac 1); |
|
65 by (res_inst_tac [("p","x")] upE 1); |
|
66 by (asm_simp_tac Up0_ss 1); |
|
67 by (asm_simp_tac Up0_ss 1); |
|
68 by (res_inst_tac [("p","y")] upE 1); |
|
69 by (hyp_subst_tac 1); |
|
70 by (rtac notE 1); |
|
71 by (rtac less_up2b 1); |
|
72 by (atac 1); |
|
73 by (asm_simp_tac Up0_ss 1); |
|
74 by (rtac monofun_cfun_arg 1); |
|
75 by (hyp_subst_tac 1); |
|
76 by (etac (less_up2c RS iffD1) 1); |
|
77 qed "monofun_Ifup2"; |
|
78 |
|
79 (* ------------------------------------------------------------------------ *) |
|
80 (* SOME kind of surjectivity lemma *) |
|
81 (* ------------------------------------------------------------------------ *) |
|
82 |
|
83 Goal "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"; |
|
84 by (asm_simp_tac Up0_ss 1); |
|
85 qed "up_lemma1"; |
|
86 |
|
87 (* ------------------------------------------------------------------------ *) |
|
88 (* ('a)u is a cpo *) |
|
89 (* ------------------------------------------------------------------------ *) |
|
90 |
|
91 Goal "[|chain(Y);EX i x. Y(i)=Iup(x)|] \ |
|
92 \ ==> range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"; |
|
93 by (rtac is_lubI 1); |
|
94 by (rtac ub_rangeI 1); |
|
95 by (res_inst_tac [("p","Y(i)")] upE 1); |
|
96 by (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] subst 1); |
|
97 by (etac sym 1); |
|
98 by (rtac minimal_up 1); |
|
99 by (res_inst_tac [("t","Y(i)")] (up_lemma1 RS subst) 1); |
|
100 by (atac 1); |
|
101 by (rtac (less_up2c RS iffD2) 1); |
|
102 by (rtac is_ub_thelub 1); |
|
103 by (etac (monofun_Ifup2 RS ch2ch_monofun) 1); |
|
104 by (strip_tac 1); |
|
105 by (res_inst_tac [("p","u")] upE 1); |
|
106 by (etac exE 1); |
|
107 by (etac exE 1); |
|
108 by (res_inst_tac [("P","Y(i)<<Abs_Up (Inl ())")] notE 1); |
|
109 by (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1); |
|
110 by (atac 1); |
|
111 by (rtac less_up2b 1); |
|
112 by (hyp_subst_tac 1); |
|
113 by (etac ub_rangeD 1); |
|
114 by (res_inst_tac [("t","u")] (up_lemma1 RS subst) 1); |
|
115 by (atac 1); |
|
116 by (rtac (less_up2c RS iffD2) 1); |
|
117 by (rtac is_lub_thelub 1); |
|
118 by (etac (monofun_Ifup2 RS ch2ch_monofun) 1); |
|
119 by (etac (monofun_Ifup2 RS ub2ub_monofun) 1); |
|
120 qed "lub_up1a"; |
|
121 |
|
122 Goal "[|chain(Y); ALL i x. Y(i)~=Iup(x)|] ==> range(Y) <<| Abs_Up (Inl ())"; |
|
123 by (rtac is_lubI 1); |
|
124 by (rtac ub_rangeI 1); |
|
125 by (res_inst_tac [("p","Y(i)")] upE 1); |
|
126 by (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] ssubst 1); |
|
127 by (atac 1); |
|
128 by (rtac refl_less 1); |
|
129 by (rtac notE 1); |
|
130 by (dtac spec 1); |
|
131 by (dtac spec 1); |
|
132 by (atac 1); |
|
133 by (atac 1); |
|
134 by (strip_tac 1); |
|
135 by (rtac minimal_up 1); |
|
136 qed "lub_up1b"; |
|
137 |
|
138 bind_thm ("thelub_up1a", lub_up1a RS thelubI); |
|
139 (* |
|
140 [| chain ?Y1; EX i x. ?Y1 i = Iup x |] ==> |
|
141 lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i)))) |
|
142 *) |
|
143 |
|
144 bind_thm ("thelub_up1b", lub_up1b RS thelubI); |
|
145 (* |
|
146 [| chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==> |
|
147 lub (range ?Y1) = UU_up |
|
148 *) |
|
149 |
|
150 Goal "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<|x"; |
|
151 by (rtac disjE 1); |
|
152 by (rtac exI 2); |
|
153 by (etac lub_up1a 2); |
|
154 by (atac 2); |
|
155 by (rtac exI 2); |
|
156 by (etac lub_up1b 2); |
|
157 by (atac 2); |
|
158 by (fast_tac HOL_cs 1); |
|
159 qed "cpo_up"; |
|
160 |
|