author | wenzelm |
Sun, 21 Aug 2022 15:00:14 +0200 | |
changeset 75952 | 864b10457a7d |
parent 74375 | ba880f3a4e52 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tools/holcf_library.ML |
35475 | 2 |
Author: Brian Huffman |
3 |
||
4 |
Functions for constructing HOLCF types and terms. |
|
5 |
*) |
|
6 |
||
7 |
structure HOLCF_Library = |
|
8 |
struct |
|
9 |
||
40832 | 10 |
infixr 6 ->> |
11 |
infixr -->> |
|
12 |
infix 9 ` |
|
35476 | 13 |
|
35475 | 14 |
(*** Operations from Isabelle/HOL ***) |
15 |
||
40832 | 16 |
val mk_equals = Logic.mk_equals |
17 |
val mk_eq = HOLogic.mk_eq |
|
18 |
val mk_trp = HOLogic.mk_Trueprop |
|
19 |
val mk_fst = HOLogic.mk_fst |
|
20 |
val mk_snd = HOLogic.mk_snd |
|
21 |
val mk_not = HOLogic.mk_not |
|
22 |
val mk_conj = HOLogic.mk_conj |
|
23 |
val mk_disj = HOLogic.mk_disj |
|
24 |
val mk_imp = HOLogic.mk_imp |
|
35475 | 25 |
|
40832 | 26 |
fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t |
27 |
fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t |
|
35475 | 28 |
|
29 |
||
30 |
(*** Basic HOLCF concepts ***) |
|
31 |
||
74305 | 32 |
fun mk_bottom T = \<^Const>\<open>bottom T\<close> |
35475 | 33 |
|
74305 | 34 |
fun below_const T = \<^Const>\<open>below T\<close> |
40832 | 35 |
fun mk_below (t, u) = below_const (fastype_of t) $ t $ u |
35475 | 36 |
|
40832 | 37 |
fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t)) |
35475 | 38 |
|
40832 | 39 |
fun mk_defined t = mk_not (mk_undef t) |
35475 | 40 |
|
40021 | 41 |
fun mk_adm t = |
74305 | 42 |
let val T = Term.domain_type (fastype_of t) |
43 |
in \<^Const>\<open>adm T for t\<close> end |
|
40021 | 44 |
|
35475 | 45 |
fun mk_compact t = |
74305 | 46 |
let val T = fastype_of t |
47 |
in \<^Const>\<open>compact T for t\<close> end |
|
35475 | 48 |
|
49 |
fun mk_cont t = |
|
74305 | 50 |
let val \<^Type>\<open>fun A B\<close> = fastype_of t |
51 |
in \<^Const>\<open>cont A B for t\<close> end |
|
35475 | 52 |
|
35489 | 53 |
fun mk_chain t = |
74305 | 54 |
let val T = Term.range_type (Term.fastype_of t) |
55 |
in \<^Const>\<open>chain T for t\<close> end |
|
35489 | 56 |
|
35555 | 57 |
fun mk_lub t = |
58 |
let |
|
40832 | 59 |
val T = Term.range_type (Term.fastype_of t) |
69597 | 60 |
val UNIV_const = \<^term>\<open>UNIV :: nat set\<close> |
74375 | 61 |
in \<^Const>\<open>lub T for \<^Const>\<open>image \<^Type>\<open>nat\<close> T for t UNIV_const\<close>\<close> end |
35555 | 62 |
|
35475 | 63 |
|
64 |
(*** Continuous function space ***) |
|
65 |
||
74305 | 66 |
fun mk_cfunT (T, U) = \<^Type>\<open>cfun T U\<close> |
35475 | 67 |
|
40832 | 68 |
val (op ->>) = mk_cfunT |
69 |
val (op -->>) = Library.foldr mk_cfunT |
|
35475 | 70 |
|
74305 | 71 |
fun dest_cfunT \<^Type>\<open>cfun T U\<close> = (T, U) |
40832 | 72 |
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []) |
35475 | 73 |
|
74305 | 74 |
fun capply_const (S, T) = \<^Const>\<open>Rep_cfun S T\<close> |
75 |
fun cabs_const (S, T) = \<^Const>\<open>Abs_cfun S T\<close> |
|
35475 | 76 |
|
77 |
fun mk_cabs t = |
|
78 |
let val T = fastype_of t |
|
40840 | 79 |
in cabs_const (Term.dest_funT T) $ t end |
35475 | 80 |
|
81 |
(* builds the expression (% v1 v2 .. vn. rhs) *) |
|
82 |
fun lambdas [] rhs = rhs |
|
40832 | 83 |
| lambdas (v::vs) rhs = Term.lambda v (lambdas vs rhs) |
35475 | 84 |
|
85 |
(* builds the expression (LAM v. rhs) *) |
|
86 |
fun big_lambda v rhs = |
|
40832 | 87 |
cabs_const (fastype_of v, fastype_of rhs) $ Term.lambda v rhs |
35475 | 88 |
|
89 |
(* builds the expression (LAM v1 v2 .. vn. rhs) *) |
|
90 |
fun big_lambdas [] rhs = rhs |
|
40832 | 91 |
| big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs) |
35475 | 92 |
|
93 |
fun mk_capply (t, u) = |
|
94 |
let val (S, T) = |
|
95 |
case fastype_of t of |
|
74305 | 96 |
\<^Type>\<open>cfun S T\<close> => (S, T) |
40832 | 97 |
| _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]) |
98 |
in capply_const (S, T) $ t $ u end |
|
35475 | 99 |
|
40832 | 100 |
val (op `) = mk_capply |
35475 | 101 |
|
40832 | 102 |
val list_ccomb : term * term list -> term = Library.foldl mk_capply |
35475 | 103 |
|
74305 | 104 |
fun mk_ID T = \<^Const>\<open>ID T\<close> |
35475 | 105 |
|
106 |
fun mk_cfcomp (f, g) = |
|
107 |
let |
|
40832 | 108 |
val (U, V) = dest_cfunT (fastype_of f) |
109 |
val (T, U') = dest_cfunT (fastype_of g) |
|
35475 | 110 |
in |
111 |
if U = U' |
|
74305 | 112 |
then mk_capply (mk_capply (\<^Const>\<open>cfcomp U V T\<close>, f), g) |
35475 | 113 |
else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) |
40832 | 114 |
end |
35475 | 115 |
|
74305 | 116 |
fun mk_strictify t = |
117 |
let val (T, U) = dest_cfunT (fastype_of t) |
|
118 |
in \<^Const>\<open>strictify T U\<close> ` t end; |
|
35785 | 119 |
|
35475 | 120 |
fun mk_strict t = |
40832 | 121 |
let val (T, U) = dest_cfunT (fastype_of t) |
122 |
in mk_eq (t ` mk_bottom T, mk_bottom U) end |
|
35475 | 123 |
|
124 |
||
125 |
(*** Product type ***) |
|
126 |
||
127 |
val mk_prodT = HOLogic.mk_prodT |
|
128 |
||
129 |
fun mk_tupleT [] = HOLogic.unitT |
|
130 |
| mk_tupleT [T] = T |
|
40832 | 131 |
| mk_tupleT (T :: Ts) = mk_prodT (T, mk_tupleT Ts) |
35475 | 132 |
|
133 |
(* builds the expression (v1,v2,..,vn) *) |
|
134 |
fun mk_tuple [] = HOLogic.unit |
|
135 |
| mk_tuple (t::[]) = t |
|
40832 | 136 |
| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts) |
35475 | 137 |
|
138 |
(* builds the expression (%(v1,v2,..,vn). rhs) *) |
|
139 |
fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs |
|
140 |
| lambda_tuple (v::[]) rhs = Term.lambda v rhs |
|
141 |
| lambda_tuple (v::vs) rhs = |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
44169
diff
changeset
|
142 |
HOLogic.mk_case_prod (Term.lambda v (lambda_tuple vs rhs)) |
35475 | 143 |
|
144 |
||
145 |
(*** Lifted cpo type ***) |
|
146 |
||
74305 | 147 |
fun mk_upT T = \<^Type>\<open>u T\<close> |
35475 | 148 |
|
74305 | 149 |
fun dest_upT \<^Type>\<open>u T\<close> = T |
40832 | 150 |
| dest_upT T = raise TYPE ("dest_upT", [T], []) |
35475 | 151 |
|
74305 | 152 |
fun up_const T = \<^Const>\<open>up T\<close> |
35475 | 153 |
|
40832 | 154 |
fun mk_up t = up_const (fastype_of t) ` t |
35475 | 155 |
|
74305 | 156 |
fun fup_const (T, U) = \<^Const>\<open>fup T U\<close> |
35475 | 157 |
|
40832 | 158 |
fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t |
35785 | 159 |
|
40832 | 160 |
fun from_up T = fup_const (T, T) ` mk_ID T |
35475 | 161 |
|
162 |
||
35785 | 163 |
(*** Lifted unit type ***) |
35475 | 164 |
|
69597 | 165 |
val oneT = \<^typ>\<open>one\<close> |
35475 | 166 |
|
74305 | 167 |
fun one_case_const T = \<^Const>\<open>one_case T\<close> |
40832 | 168 |
fun mk_one_case t = one_case_const (fastype_of t) ` t |
35785 | 169 |
|
170 |
||
171 |
(*** Strict product type ***) |
|
172 |
||
74305 | 173 |
fun mk_sprodT (T, U) = \<^Type>\<open>sprod T U\<close> |
35475 | 174 |
|
74305 | 175 |
fun dest_sprodT \<^Type>\<open>sprod T U\<close> = (T, U) |
40832 | 176 |
| dest_sprodT T = raise TYPE ("dest_sprodT", [T], []) |
35475 | 177 |
|
74305 | 178 |
fun spair_const (T, U) = \<^Const>\<open>spair T U\<close> |
35475 | 179 |
|
180 |
(* builds the expression (:t, u:) *) |
|
181 |
fun mk_spair (t, u) = |
|
40832 | 182 |
spair_const (fastype_of t, fastype_of u) ` t ` u |
35475 | 183 |
|
184 |
(* builds the expression (:t1,t2,..,tn:) *) |
|
69597 | 185 |
fun mk_stuple [] = \<^term>\<open>ONE\<close> |
35475 | 186 |
| mk_stuple (t::[]) = t |
40832 | 187 |
| mk_stuple (t::ts) = mk_spair (t, mk_stuple ts) |
35475 | 188 |
|
74305 | 189 |
fun sfst_const (T, U) = \<^Const>\<open>sfst T U\<close> |
35475 | 190 |
|
74305 | 191 |
fun ssnd_const (T, U) = \<^Const>\<open>ssnd T U\<close> |
35475 | 192 |
|
74305 | 193 |
fun ssplit_const (T, U, V) = \<^Const>\<open>ssplit T U V\<close> |
35785 | 194 |
|
195 |
fun mk_ssplit t = |
|
40832 | 196 |
let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t)) |
197 |
in ssplit_const (T, U, V) ` t end |
|
35785 | 198 |
|
35475 | 199 |
|
200 |
(*** Strict sum type ***) |
|
201 |
||
74305 | 202 |
fun mk_ssumT (T, U) = \<^Type>\<open>ssum T U\<close> |
35475 | 203 |
|
74305 | 204 |
fun dest_ssumT \<^Type>\<open>ssum T U\<close> = (T, U) |
40832 | 205 |
| dest_ssumT T = raise TYPE ("dest_ssumT", [T], []) |
35475 | 206 |
|
74305 | 207 |
fun sinl_const (T, U) = \<^Const>\<open>sinl T U\<close> |
208 |
fun sinr_const (T, U) = \<^Const>\<open>sinr U T\<close> |
|
35475 | 209 |
|
210 |
(* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *) |
|
211 |
fun mk_sinjects ts = |
|
212 |
let |
|
40832 | 213 |
val Ts = map fastype_of ts |
35475 | 214 |
fun combine (t, T) (us, U) = |
215 |
let |
|
40832 | 216 |
val v = sinl_const (T, U) ` t |
217 |
val vs = map (fn u => sinr_const (T, U) ` u) us |
|
35475 | 218 |
in |
219 |
(v::vs, mk_ssumT (T, U)) |
|
220 |
end |
|
35912 | 221 |
fun inj [] = raise Fail "mk_sinjects: empty list" |
35475 | 222 |
| inj ((t, T)::[]) = ([t], T) |
40832 | 223 |
| inj ((t, T)::ts) = combine (t, T) (inj ts) |
35475 | 224 |
in |
225 |
fst (inj (ts ~~ Ts)) |
|
40832 | 226 |
end |
35475 | 227 |
|
74305 | 228 |
fun sscase_const (T, U, V) = \<^Const>\<open>sscase T V U\<close> |
35475 | 229 |
|
35785 | 230 |
fun mk_sscase (t, u) = |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42151
diff
changeset
|
231 |
let val (T, _) = dest_cfunT (fastype_of t) |
40832 | 232 |
val (U, V) = dest_cfunT (fastype_of u) |
233 |
in sscase_const (T, U, V) ` t ` u end |
|
35785 | 234 |
|
35475 | 235 |
fun from_sinl (T, U) = |
40832 | 236 |
sscase_const (T, U, T) ` mk_ID T ` mk_bottom (U ->> T) |
35475 | 237 |
|
238 |
fun from_sinr (T, U) = |
|
40832 | 239 |
sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U |
35475 | 240 |
|
241 |
||
242 |
(*** pattern match monad type ***) |
|
243 |
||
74305 | 244 |
fun mk_matchT T = \<^Type>\<open>match T\<close> |
35475 | 245 |
|
74305 | 246 |
fun dest_matchT \<^Type>\<open>match T\<close> = T |
40832 | 247 |
| dest_matchT T = raise TYPE ("dest_matchT", [T], []) |
35475 | 248 |
|
74305 | 249 |
fun mk_fail T = \<^Const>\<open>Fixrec.fail T\<close> |
35475 | 250 |
|
74305 | 251 |
fun succeed_const T = \<^Const>\<open>Fixrec.succeed T\<close> |
40832 | 252 |
fun mk_succeed t = succeed_const (fastype_of t) ` t |
35475 | 253 |
|
254 |
||
255 |
(*** lifted boolean type ***) |
|
256 |
||
69597 | 257 |
val trT = \<^typ>\<open>tr\<close> |
35475 | 258 |
|
259 |
||
260 |
(*** theory of fixed points ***) |
|
261 |
||
262 |
fun mk_fix t = |
|
263 |
let val (T, _) = dest_cfunT (fastype_of t) |
|
74305 | 264 |
in mk_capply (\<^Const>\<open>fix T\<close>, t) end |
35475 | 265 |
|
74305 | 266 |
fun iterate_const T = \<^Const>\<open>iterate T\<close> |
35489 | 267 |
|
268 |
fun mk_iterate (n, f) = |
|
40832 | 269 |
let val (T, _) = dest_cfunT (Term.fastype_of f) |
270 |
in (iterate_const T $ n) ` f ` mk_bottom T end |
|
35475 | 271 |
|
40832 | 272 |
end |