author | huffman |
Thu, 19 Nov 2009 08:00:42 -0800 | |
changeset 33782 | cdb3ca1a765d |
parent 33778 | 9121ea165a40 |
child 33784 | 7e434813752f |
permissions | -rw-r--r-- |
33774 | 1 |
(* Title: HOLCF/Tools/domain/domain_isomorphism.ML |
2 |
Author: Brian Huffman |
|
3 |
||
4 |
Defines new types satisfying the given domain equations. |
|
5 |
*) |
|
6 |
||
7 |
signature DOMAIN_ISOMORPHISM = |
|
8 |
sig |
|
9 |
val domain_isomorphism: |
|
10 |
(string list * binding * mixfix * typ) list -> theory -> theory |
|
11 |
val domain_isomorphism_cmd: |
|
12 |
(string list * binding * mixfix * string) list -> theory -> theory |
|
13 |
end; |
|
14 |
||
15 |
structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM = |
|
16 |
struct |
|
17 |
||
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
18 |
val beta_ss = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
19 |
HOL_basic_ss |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
20 |
addsimps simp_thms |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
21 |
addsimps [@{thm beta_cfun}] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
22 |
addsimprocs [@{simproc cont_proc}]; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
23 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
24 |
val beta_tac = simp_tac beta_ss; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
25 |
|
33774 | 26 |
(******************************************************************************) |
27 |
(******************************* building types *******************************) |
|
28 |
(******************************************************************************) |
|
29 |
||
30 |
(* ->> is taken from holcf_logic.ML *) |
|
31 |
fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]); |
|
32 |
||
33 |
infixr 6 ->>; val (op ->>) = cfunT; |
|
34 |
||
35 |
fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) |
|
36 |
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); |
|
37 |
||
38 |
fun tupleT [] = HOLogic.unitT |
|
39 |
| tupleT [T] = T |
|
40 |
| tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts); |
|
41 |
||
42 |
val deflT = @{typ "udom alg_defl"}; |
|
43 |
||
44 |
(******************************************************************************) |
|
45 |
(******************************* building terms *******************************) |
|
46 |
(******************************************************************************) |
|
47 |
||
48 |
(* builds the expression (v1,v2,..,vn) *) |
|
49 |
fun mk_tuple [] = HOLogic.unit |
|
50 |
| mk_tuple (t::[]) = t |
|
51 |
| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts); |
|
52 |
||
53 |
(* builds the expression (%(v1,v2,..,vn). rhs) *) |
|
54 |
fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs |
|
55 |
| lambda_tuple (v::[]) rhs = Term.lambda v rhs |
|
56 |
| lambda_tuple (v::vs) rhs = |
|
57 |
HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)); |
|
58 |
||
59 |
(* continuous application and abstraction *) |
|
60 |
||
61 |
fun capply_const (S, T) = |
|
62 |
Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T)); |
|
63 |
||
64 |
fun cabs_const (S, T) = |
|
65 |
Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T)); |
|
66 |
||
67 |
fun mk_cabs t = |
|
68 |
let val T = Term.fastype_of t |
|
69 |
in cabs_const (Term.domain_type T, Term.range_type T) $ t end |
|
70 |
||
71 |
(* builds the expression (LAM v. rhs) *) |
|
72 |
fun big_lambda v rhs = |
|
73 |
cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs; |
|
74 |
||
75 |
(* builds the expression (LAM v1 v2 .. vn. rhs) *) |
|
76 |
fun big_lambdas [] rhs = rhs |
|
77 |
| big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); |
|
78 |
||
79 |
fun mk_capply (t, u) = |
|
80 |
let val (S, T) = |
|
81 |
case Term.fastype_of t of |
|
82 |
Type(@{type_name "->"}, [S, T]) => (S, T) |
|
83 |
| _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); |
|
84 |
in capply_const (S, T) $ t $ u end; |
|
85 |
||
86 |
(* miscellaneous term constructions *) |
|
87 |
||
88 |
val mk_trp = HOLogic.mk_Trueprop; |
|
89 |
||
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
90 |
val mk_fst = HOLogic.mk_fst; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
91 |
val mk_snd = HOLogic.mk_snd; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
92 |
|
33774 | 93 |
fun mk_cont t = |
94 |
let val T = Term.fastype_of t |
|
95 |
in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end; |
|
96 |
||
97 |
fun mk_fix t = |
|
98 |
let val (T, _) = dest_cfunT (Term.fastype_of t) |
|
99 |
in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end; |
|
100 |
||
101 |
fun mk_Rep_of T = |
|
102 |
Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T; |
|
103 |
||
33778 | 104 |
fun coerce_const T = Const (@{const_name coerce}, T); |
105 |
||
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
106 |
(* splits a cterm into the right and lefthand sides of equality *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
107 |
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
108 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
109 |
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
110 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
111 |
(******************************************************************************) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
112 |
(*************** fixed-point definitions and unfolding theorems ***************) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
113 |
(******************************************************************************) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
114 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
115 |
fun add_fixdefs |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
116 |
(spec : (binding * term) list) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
117 |
(thy : theory) : thm list * theory = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
118 |
let |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
119 |
val binds = map fst spec; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
120 |
val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
121 |
val functional = lambda_tuple lhss (mk_tuple rhss); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
122 |
val fixpoint = mk_fix (mk_cabs functional); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
123 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
124 |
(* project components of fixpoint *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
125 |
fun mk_projs (x::[]) t = [(x, t)] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
126 |
| mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
127 |
val projs = mk_projs lhss fixpoint; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
128 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
129 |
(* convert parameters to lambda abstractions *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
130 |
fun mk_eqn (lhs, rhs) = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
131 |
case lhs of |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
132 |
Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) => |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
133 |
mk_eqn (f, big_lambda x rhs) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
134 |
| Const _ => Logic.mk_equals (lhs, rhs) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
135 |
| _ => raise TERM ("lhs not of correct form", [lhs, rhs]); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
136 |
val eqns = map mk_eqn projs; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
137 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
138 |
(* register constant definitions *) |
33777 | 139 |
val (fixdef_thms, thy) = |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
140 |
(PureThy.add_defs false o map Thm.no_attributes) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
141 |
(map (Binding.suffix_name "_def") binds ~~ eqns) thy; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
142 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
143 |
(* prove applied version of definitions *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
144 |
fun prove_proj (lhs, rhs) = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
145 |
let |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
146 |
val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
147 |
val goal = Logic.mk_equals (lhs, rhs); |
33777 | 148 |
in Goal.prove_global thy [] [] goal (K tac) end; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
149 |
val proj_thms = map prove_proj projs; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
150 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
151 |
(* mk_tuple lhss == fixpoint *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
152 |
fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
153 |
val tuple_fixdef_thm = foldr1 pair_equalI proj_thms; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
154 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
155 |
val cont_thm = |
33777 | 156 |
Goal.prove_global thy [] [] (mk_trp (mk_cont functional)) |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
157 |
(K (beta_tac 1)); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
158 |
val tuple_unfold_thm = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
159 |
(@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm]) |
33777 | 160 |
|> LocalDefs.unfold (ProofContext.init thy) @{thms split_conv}; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
161 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
162 |
fun mk_unfold_thms [] thm = [] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
163 |
| mk_unfold_thms (n::[]) thm = [(n, thm)] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
164 |
| mk_unfold_thms (n::ns) thm = let |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
165 |
val thmL = thm RS @{thm Pair_eqD1}; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
166 |
val thmR = thm RS @{thm Pair_eqD2}; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
167 |
in (n, thmL) :: mk_unfold_thms ns thmR end; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
168 |
val unfold_binds = map (Binding.suffix_name "_unfold") binds; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
169 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
170 |
(* register unfold theorems *) |
33777 | 171 |
val (unfold_thms, thy) = |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
172 |
(PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard)) |
33777 | 173 |
(mk_unfold_thms unfold_binds tuple_unfold_thm) thy; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
174 |
in |
33777 | 175 |
(unfold_thms, thy) |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
176 |
end; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
177 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
178 |
|
33774 | 179 |
(******************************************************************************) |
180 |
||
181 |
fun typ_of_dtyp |
|
182 |
(descr : (string * string list) list) |
|
183 |
(sorts : (string * sort) list) |
|
184 |
: DatatypeAux.dtyp -> typ = |
|
185 |
let |
|
186 |
fun tfree a = TFree (a, the (AList.lookup (op =) sorts a)) |
|
187 |
fun typ_of (DatatypeAux.DtTFree a) = tfree a |
|
188 |
| typ_of (DatatypeAux.DtType (s, ds)) = Type (s, map typ_of ds) |
|
189 |
| typ_of (DatatypeAux.DtRec i) = |
|
190 |
let val (s, vs) = nth descr i |
|
191 |
in Type (s, map tfree vs) end |
|
192 |
in typ_of end; |
|
193 |
||
194 |
fun is_closed_dtyp (DatatypeAux.DtTFree a) = false |
|
195 |
| is_closed_dtyp (DatatypeAux.DtRec i) = false |
|
196 |
| is_closed_dtyp (DatatypeAux.DtType (s, ds)) = forall is_closed_dtyp ds; |
|
197 |
||
198 |
(* FIXME: use theory data for this *) |
|
199 |
val defl_tab : term Symtab.table = |
|
200 |
Symtab.make [(@{type_name "->"}, @{term "cfun_typ"}), |
|
201 |
(@{type_name "++"}, @{term "ssum_typ"}), |
|
202 |
(@{type_name "**"}, @{term "sprod_typ"}), |
|
203 |
(@{type_name "*"}, @{term "cprod_typ"}), |
|
204 |
(@{type_name "u"}, @{term "u_typ"}), |
|
205 |
(@{type_name "upper_pd"}, @{term "upper_typ"}), |
|
206 |
(@{type_name "lower_pd"}, @{term "lower_typ"}), |
|
207 |
(@{type_name "convex_pd"}, @{term "convex_typ"})]; |
|
208 |
||
209 |
fun defl_of_typ |
|
210 |
(tab : term Symtab.table) |
|
211 |
(free : string -> term) |
|
212 |
(T : typ) : term = |
|
213 |
let |
|
214 |
fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts |
|
215 |
| is_closed_typ _ = false; |
|
216 |
fun defl_of (TFree (a, _)) = free a |
|
217 |
| defl_of (TVar _) = error ("defl_of_typ: TVar") |
|
218 |
| defl_of (T as Type (c, Ts)) = |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
219 |
case Symtab.lookup tab c of |
33774 | 220 |
SOME t => Library.foldl mk_capply (t, map defl_of Ts) |
221 |
| NONE => if is_closed_typ T |
|
222 |
then mk_Rep_of T |
|
223 |
else error ("defl_of_typ: type variable under unsupported type constructor " ^ c); |
|
224 |
in defl_of T end; |
|
225 |
||
226 |
fun defl_of_dtyp |
|
227 |
(descr : (string * string list) list) |
|
228 |
(sorts : (string * sort) list) |
|
229 |
(f : string -> term) |
|
230 |
(r : int -> term) |
|
231 |
(dt : DatatypeAux.dtyp) : term = |
|
232 |
let |
|
233 |
fun tfree a = TFree (a, the (AList.lookup (op =) sorts a)) |
|
234 |
fun defl_of (DatatypeAux.DtTFree a) = f a |
|
235 |
| defl_of (DatatypeAux.DtRec i) = r i |
|
236 |
| defl_of (dt as DatatypeAux.DtType (s, ds)) = |
|
237 |
case Symtab.lookup defl_tab s of |
|
238 |
SOME t => Library.foldl mk_capply (t, map defl_of ds) |
|
239 |
| NONE => if DatatypeAux.is_rec_type dt |
|
240 |
then error ("defl_of_dtyp: recursion under unsupported type constructor " ^ s) |
|
241 |
else if is_closed_dtyp dt |
|
242 |
then mk_Rep_of (typ_of_dtyp descr sorts dt) |
|
243 |
else error ("defl_of_dtyp: type variable under unsupported type constructor " ^ s); |
|
244 |
in defl_of dt end; |
|
245 |
||
246 |
(******************************************************************************) |
|
247 |
(* prepare datatype specifications *) |
|
248 |
||
249 |
fun read_typ thy str sorts = |
|
250 |
let |
|
251 |
val ctxt = ProofContext.init thy |
|
252 |
|> fold (Variable.declare_typ o TFree) sorts; |
|
253 |
val T = Syntax.read_typ ctxt str; |
|
254 |
in (T, Term.add_tfreesT T sorts) end; |
|
255 |
||
256 |
fun cert_typ sign raw_T sorts = |
|
257 |
let |
|
258 |
val T = Type.no_tvars (Sign.certify_typ sign raw_T) |
|
259 |
handle TYPE (msg, _, _) => error msg; |
|
260 |
val sorts' = Term.add_tfreesT T sorts; |
|
261 |
val _ = |
|
262 |
case duplicates (op =) (map fst sorts') of |
|
263 |
[] => () |
|
264 |
| dups => error ("Inconsistent sort constraints for " ^ commas dups) |
|
265 |
in (T, sorts') end; |
|
266 |
||
267 |
fun gen_domain_isomorphism |
|
268 |
(prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list) |
|
269 |
(doms_raw: (string list * binding * mixfix * 'a) list) |
|
270 |
(thy: theory) |
|
271 |
: theory = |
|
272 |
let |
|
273 |
val _ = Theory.requires thy "Domain" "domain definitions"; |
|
274 |
||
275 |
(* this theory is used just for parsing *) |
|
276 |
val tmp_thy = thy |> |
|
277 |
Theory.copy |> |
|
278 |
Sign.add_types (map (fn (tvs, tname, mx, _) => |
|
279 |
(tname, length tvs, mx)) doms_raw); |
|
280 |
||
281 |
fun prep_dom thy (vs, t, mx, typ_raw) sorts = |
|
282 |
let val (typ, sorts') = prep_typ thy typ_raw sorts |
|
283 |
in ((vs, t, mx, typ), sorts') end; |
|
284 |
||
285 |
val (doms : (string list * binding * mixfix * typ) list, |
|
286 |
sorts : (string * sort) list) = |
|
287 |
fold_map (prep_dom tmp_thy) doms_raw []; |
|
288 |
||
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
289 |
(* domain equations *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
290 |
fun mk_dom_eqn (vs, tbind, mx, rhs) = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
291 |
let fun arg v = TFree (v, the (AList.lookup (op =) sorts v)); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
292 |
in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
293 |
val dom_eqns = map mk_dom_eqn doms; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
294 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
295 |
(* check for valid type parameters *) |
33774 | 296 |
val (tyvars, _, _, _)::_ = doms; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
297 |
val new_doms = map (fn (tvs, tname, mx, _) => |
33774 | 298 |
let val full_tname = Sign.full_name tmp_thy tname |
299 |
in |
|
300 |
(case duplicates (op =) tvs of |
|
301 |
[] => |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
302 |
if eq_set (op =) (tyvars, tvs) then (full_tname, tvs) |
33774 | 303 |
else error ("Mutually recursive domains must have same type parameters") |
304 |
| dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^ |
|
305 |
" : " ^ commas dups)) |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
306 |
end) doms; |
33782 | 307 |
val dom_binds = map (fn (_, tbind, _, _) => tbind) doms; |
33774 | 308 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
309 |
(* declare type combinator constants *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
310 |
fun declare_typ_const (vs, tbind, mx, rhs) thy = |
33774 | 311 |
let |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
312 |
val typ_type = Library.foldr cfunT (map (K deflT) vs, deflT); |
33774 | 313 |
val typ_bind = Binding.suffix_name "_typ" tbind; |
314 |
in |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
315 |
Sign.declare_const ((typ_bind, typ_type), NoSyn) thy |
33774 | 316 |
end; |
33777 | 317 |
val (typ_consts, thy) = fold_map declare_typ_const doms thy; |
33774 | 318 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
319 |
(* defining equations for type combinators *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
320 |
val defl_tab1 = defl_tab; (* FIXME: use theory data *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
321 |
val defl_tab2 = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
322 |
Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ typ_consts); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
323 |
val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
324 |
fun free a = Free (Library.unprefix "'" a, deflT); |
33776 | 325 |
fun mk_defl_spec (lhsT, rhsT) = |
326 |
mk_eqs (defl_of_typ defl_tab' free lhsT, |
|
327 |
defl_of_typ defl_tab' free rhsT); |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
328 |
val defl_specs = map mk_defl_spec dom_eqns; |
33774 | 329 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
330 |
(* register recursive definition of type combinators *) |
33782 | 331 |
val typ_binds = map (Binding.suffix_name "_typ") dom_binds; |
33777 | 332 |
val (typ_unfold_thms, thy) = add_fixdefs (typ_binds ~~ defl_specs) thy; |
33774 | 333 |
|
33776 | 334 |
(* define types using deflation combinators *) |
33774 | 335 |
fun make_repdef ((vs, tbind, mx, _), typ_const) thy = |
336 |
let |
|
337 |
fun tfree a = TFree (a, the (AList.lookup (op =) sorts a)) |
|
338 |
val reps = map (mk_Rep_of o tfree) vs; |
|
339 |
val defl = Library.foldl mk_capply (typ_const, reps); |
|
33777 | 340 |
val ((_, _, _, {REP, ...}), thy) = |
33774 | 341 |
Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy; |
342 |
in |
|
33777 | 343 |
(REP, thy) |
33774 | 344 |
end; |
33782 | 345 |
val (REP_thms, thy) = fold_map make_repdef (doms ~~ typ_consts) thy; |
33774 | 346 |
|
33776 | 347 |
(* FIXME: use theory data for this *) |
348 |
val REP_simps = REP_thms @ |
|
349 |
@{thms REP_cfun REP_ssum REP_sprod REP_cprod REP_up |
|
350 |
REP_upper REP_lower REP_convex}; |
|
351 |
||
352 |
(* prove REP equations *) |
|
33782 | 353 |
fun mk_REP_eq_thm (lhsT, rhsT) = |
33776 | 354 |
let |
355 |
val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT); |
|
356 |
val tac = |
|
357 |
simp_tac (HOL_basic_ss addsimps REP_simps) 1 |
|
358 |
THEN resolve_tac typ_unfold_thms 1; |
|
359 |
in |
|
33777 | 360 |
Goal.prove_global thy [] [] goal (K tac) |
33776 | 361 |
end; |
33782 | 362 |
val REP_eq_thms = map mk_REP_eq_thm dom_eqns; |
363 |
||
364 |
(* register REP equations *) |
|
365 |
val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dom_binds; |
|
366 |
val (_, thy) = thy |> |
|
367 |
(PureThy.add_thms o map Thm.no_attributes) |
|
368 |
(REP_eq_binds ~~ REP_eq_thms); |
|
33776 | 369 |
|
33778 | 370 |
(* define rep/abs functions *) |
33782 | 371 |
fun mk_rep_abs (tbind, (lhsT, rhsT)) thy = |
33778 | 372 |
let |
373 |
val rep_type = cfunT (lhsT, rhsT); |
|
33782 | 374 |
val abs_type = cfunT (rhsT, lhsT); |
33778 | 375 |
val rep_bind = Binding.suffix_name "_rep" tbind; |
376 |
val abs_bind = Binding.suffix_name "_abs" tbind; |
|
377 |
val (rep_const, thy) = thy |> |
|
378 |
Sign.declare_const ((rep_bind, rep_type), NoSyn); |
|
379 |
val (abs_const, thy) = thy |> |
|
380 |
Sign.declare_const ((abs_bind, abs_type), NoSyn); |
|
381 |
val rep_eqn = Logic.mk_equals (rep_const, coerce_const rep_type); |
|
382 |
val abs_eqn = Logic.mk_equals (abs_const, coerce_const abs_type); |
|
383 |
val ([rep_def, abs_def], thy) = thy |> |
|
384 |
(PureThy.add_defs false o map Thm.no_attributes) |
|
385 |
[(Binding.suffix_name "_rep_def" tbind, rep_eqn), |
|
386 |
(Binding.suffix_name "_abs_def" tbind, abs_eqn)]; |
|
387 |
in |
|
388 |
((rep_def, abs_def), thy) |
|
389 |
end; |
|
390 |
val (rep_abs_defs, thy) = thy |> |
|
33782 | 391 |
fold_map mk_rep_abs (dom_binds ~~ dom_eqns); |
392 |
||
393 |
(* prove isomorphism and isodefl rules *) |
|
394 |
fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy = |
|
395 |
let |
|
396 |
fun make thm = Drule.standard (thm OF [REP_eq, abs_def, rep_def]); |
|
397 |
val rep_iso_thm = make @{thm domain_rep_iso}; |
|
398 |
val abs_iso_thm = make @{thm domain_abs_iso}; |
|
399 |
val isodefl_thm = make @{thm isodefl_abs_rep}; |
|
400 |
val rep_iso_bind = Binding.suffix_name "_rep_iso" tbind; |
|
401 |
val abs_iso_bind = Binding.suffix_name "_abs_iso" tbind; |
|
402 |
val isodefl_bind = Binding.prefix_name "isodefl_abs_rep_" tbind; |
|
403 |
val (_, thy) = thy |> |
|
404 |
(PureThy.add_thms o map Thm.no_attributes) |
|
405 |
[(rep_iso_bind, rep_iso_thm), |
|
406 |
(abs_iso_bind, abs_iso_thm), |
|
407 |
(isodefl_bind, isodefl_thm)]; |
|
408 |
in |
|
409 |
(((rep_iso_thm, abs_iso_thm), isodefl_thm), thy) |
|
410 |
end; |
|
411 |
val ((iso_thms, isodefl_abs_rep_thms), thy) = thy |
|
412 |
|> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs) |
|
413 |
|>> ListPair.unzip; |
|
33778 | 414 |
|
33774 | 415 |
in |
33777 | 416 |
thy |
33774 | 417 |
end; |
418 |
||
419 |
val domain_isomorphism = gen_domain_isomorphism cert_typ; |
|
420 |
val domain_isomorphism_cmd = gen_domain_isomorphism read_typ; |
|
421 |
||
422 |
(******************************************************************************) |
|
423 |
(******************************** outer syntax ********************************) |
|
424 |
(******************************************************************************) |
|
425 |
||
426 |
local |
|
427 |
||
428 |
structure P = OuterParse and K = OuterKeyword |
|
429 |
||
430 |
val parse_domain_iso : (string list * binding * mixfix * string) parser = |
|
431 |
(P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ)) |
|
432 |
>> (fn (((vs, t), mx), rhs) => (vs, t, mx, rhs)); |
|
433 |
||
434 |
val parse_domain_isos = P.and_list1 parse_domain_iso; |
|
435 |
||
436 |
in |
|
437 |
||
438 |
val _ = |
|
439 |
OuterSyntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" K.thy_decl |
|
440 |
(parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd)); |
|
441 |
||
442 |
end; |
|
443 |
||
444 |
end; |