author | huffman |
Sat, 19 Dec 2009 09:07:04 -0800 | |
changeset 34149 | a0efb4754cb7 |
parent 33971 | 9c7fa7f76950 |
child 35021 | c839a4c670c6 |
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: |
|
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
10 |
(string list * binding * mixfix * typ * (binding * binding) option) list |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
11 |
-> theory -> theory |
33774 | 12 |
val domain_isomorphism_cmd: |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
13 |
(string list * binding * mixfix * string * (binding * binding) option) list |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
14 |
-> theory -> theory |
33791 | 15 |
val add_type_constructor: |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
16 |
(string * term * string * thm * thm * thm) -> theory -> theory |
33801 | 17 |
val get_map_tab: |
18 |
theory -> string Symtab.table |
|
33774 | 19 |
end; |
20 |
||
21 |
structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM = |
|
22 |
struct |
|
23 |
||
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
24 |
val beta_ss = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
25 |
HOL_basic_ss |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
26 |
addsimps simp_thms |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
27 |
addsimps [@{thm beta_cfun}] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
28 |
addsimprocs [@{simproc cont_proc}]; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
29 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
30 |
val beta_tac = simp_tac beta_ss; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
31 |
|
33774 | 32 |
(******************************************************************************) |
33791 | 33 |
(******************************** theory data *********************************) |
34 |
(******************************************************************************) |
|
35 |
||
36 |
structure DeflData = Theory_Data |
|
37 |
( |
|
38 |
type T = term Symtab.table; |
|
39 |
val empty = Symtab.empty; |
|
40 |
val extend = I; |
|
41 |
fun merge data = Symtab.merge (K true) data; |
|
42 |
); |
|
43 |
||
44 |
structure MapData = Theory_Data |
|
45 |
( |
|
46 |
type T = string Symtab.table; |
|
47 |
val empty = Symtab.empty; |
|
48 |
val extend = I; |
|
49 |
fun merge data = Symtab.merge (K true) data; |
|
50 |
); |
|
51 |
||
52 |
structure RepData = Theory_Data |
|
53 |
( |
|
54 |
type T = thm list; |
|
55 |
val empty = []; |
|
56 |
val extend = I; |
|
57 |
val merge = Thm.merge_thms; |
|
58 |
); |
|
59 |
||
60 |
structure IsodeflData = Theory_Data |
|
61 |
( |
|
62 |
type T = thm list; |
|
63 |
val empty = []; |
|
64 |
val extend = I; |
|
65 |
val merge = Thm.merge_thms; |
|
66 |
); |
|
67 |
||
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
68 |
structure MapIdData = Theory_Data |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
69 |
( |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
70 |
type T = thm list; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
71 |
val empty = []; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
72 |
val extend = I; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
73 |
val merge = Thm.merge_thms; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
74 |
); |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
75 |
|
33791 | 76 |
fun add_type_constructor |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
77 |
(tname, defl_const, map_name, REP_thm, isodefl_thm, map_ID_thm) = |
33791 | 78 |
DeflData.map (Symtab.insert (K true) (tname, defl_const)) |
79 |
#> MapData.map (Symtab.insert (K true) (tname, map_name)) |
|
80 |
#> RepData.map (Thm.add_thm REP_thm) |
|
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
81 |
#> IsodeflData.map (Thm.add_thm isodefl_thm) |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
82 |
#> MapIdData.map (Thm.add_thm map_ID_thm); |
33791 | 83 |
|
33801 | 84 |
val get_map_tab = MapData.get; |
85 |
||
33791 | 86 |
|
87 |
(******************************************************************************) |
|
33774 | 88 |
(******************************* building types *******************************) |
89 |
(******************************************************************************) |
|
90 |
||
91 |
(* ->> is taken from holcf_logic.ML *) |
|
92 |
fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]); |
|
93 |
||
94 |
infixr 6 ->>; val (op ->>) = cfunT; |
|
95 |
||
96 |
fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) |
|
97 |
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); |
|
98 |
||
99 |
fun tupleT [] = HOLogic.unitT |
|
100 |
| tupleT [T] = T |
|
101 |
| tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts); |
|
102 |
||
103 |
val deflT = @{typ "udom alg_defl"}; |
|
104 |
||
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
105 |
fun mapT (T as Type (_, Ts)) = |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
106 |
Library.foldr cfunT (map (fn T => T ->> T) Ts, T ->> T); |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
107 |
|
33774 | 108 |
(******************************************************************************) |
109 |
(******************************* building terms *******************************) |
|
110 |
(******************************************************************************) |
|
111 |
||
112 |
(* builds the expression (v1,v2,..,vn) *) |
|
113 |
fun mk_tuple [] = HOLogic.unit |
|
114 |
| mk_tuple (t::[]) = t |
|
115 |
| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts); |
|
116 |
||
117 |
(* builds the expression (%(v1,v2,..,vn). rhs) *) |
|
118 |
fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs |
|
119 |
| lambda_tuple (v::[]) rhs = Term.lambda v rhs |
|
120 |
| lambda_tuple (v::vs) rhs = |
|
121 |
HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)); |
|
122 |
||
123 |
(* continuous application and abstraction *) |
|
124 |
||
125 |
fun capply_const (S, T) = |
|
126 |
Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T)); |
|
127 |
||
128 |
fun cabs_const (S, T) = |
|
129 |
Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T)); |
|
130 |
||
131 |
fun mk_cabs t = |
|
132 |
let val T = Term.fastype_of t |
|
133 |
in cabs_const (Term.domain_type T, Term.range_type T) $ t end |
|
134 |
||
135 |
(* builds the expression (LAM v. rhs) *) |
|
136 |
fun big_lambda v rhs = |
|
137 |
cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs; |
|
138 |
||
139 |
(* builds the expression (LAM v1 v2 .. vn. rhs) *) |
|
140 |
fun big_lambdas [] rhs = rhs |
|
141 |
| big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); |
|
142 |
||
143 |
fun mk_capply (t, u) = |
|
144 |
let val (S, T) = |
|
145 |
case Term.fastype_of t of |
|
146 |
Type(@{type_name "->"}, [S, T]) => (S, T) |
|
147 |
| _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); |
|
148 |
in capply_const (S, T) $ t $ u end; |
|
149 |
||
150 |
(* miscellaneous term constructions *) |
|
151 |
||
152 |
val mk_trp = HOLogic.mk_Trueprop; |
|
153 |
||
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
154 |
val mk_fst = HOLogic.mk_fst; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
155 |
val mk_snd = HOLogic.mk_snd; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
156 |
|
33774 | 157 |
fun mk_cont t = |
158 |
let val T = Term.fastype_of t |
|
159 |
in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end; |
|
160 |
||
161 |
fun mk_fix t = |
|
162 |
let val (T, _) = dest_cfunT (Term.fastype_of t) |
|
163 |
in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end; |
|
164 |
||
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
165 |
fun ID_const T = Const (@{const_name ID}, cfunT (T, T)); |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
166 |
|
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
167 |
fun cfcomp_const (T, U, V) = |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
168 |
Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V)); |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
169 |
|
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
170 |
fun mk_cfcomp (f, g) = |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
171 |
let |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
172 |
val (U, V) = dest_cfunT (Term.fastype_of f); |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
173 |
val (T, U') = dest_cfunT (Term.fastype_of g); |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
174 |
in |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
175 |
if U = U' |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
176 |
then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g) |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
177 |
else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
178 |
end; |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
179 |
|
33774 | 180 |
fun mk_Rep_of T = |
181 |
Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T; |
|
182 |
||
33778 | 183 |
fun coerce_const T = Const (@{const_name coerce}, T); |
184 |
||
33788 | 185 |
fun isodefl_const T = |
186 |
Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT); |
|
187 |
||
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
188 |
(* 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
|
189 |
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
|
190 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
191 |
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
|
192 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
193 |
(******************************************************************************) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
194 |
(*************** fixed-point definitions and unfolding theorems ***************) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
195 |
(******************************************************************************) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
196 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
197 |
fun add_fixdefs |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
198 |
(spec : (binding * term) list) |
33788 | 199 |
(thy : theory) : (thm list * thm list) * theory = |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
200 |
let |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
201 |
val binds = map fst spec; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
202 |
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
|
203 |
val functional = lambda_tuple lhss (mk_tuple rhss); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
204 |
val fixpoint = mk_fix (mk_cabs functional); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
205 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
206 |
(* project components of fixpoint *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
207 |
fun mk_projs (x::[]) t = [(x, t)] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
208 |
| 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
|
209 |
val projs = mk_projs lhss fixpoint; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
210 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
211 |
(* convert parameters to lambda abstractions *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
212 |
fun mk_eqn (lhs, rhs) = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
213 |
case lhs of |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
214 |
Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) => |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
215 |
mk_eqn (f, big_lambda x rhs) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
216 |
| Const _ => Logic.mk_equals (lhs, rhs) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
217 |
| _ => raise TERM ("lhs not of correct form", [lhs, rhs]); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
218 |
val eqns = map mk_eqn projs; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
219 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
220 |
(* register constant definitions *) |
33777 | 221 |
val (fixdef_thms, thy) = |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
222 |
(PureThy.add_defs false o map Thm.no_attributes) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
223 |
(map (Binding.suffix_name "_def") binds ~~ eqns) thy; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
224 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
225 |
(* prove applied version of definitions *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
226 |
fun prove_proj (lhs, rhs) = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
227 |
let |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
228 |
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
|
229 |
val goal = Logic.mk_equals (lhs, rhs); |
33777 | 230 |
in Goal.prove_global thy [] [] goal (K tac) end; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
231 |
val proj_thms = map prove_proj projs; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
232 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
233 |
(* mk_tuple lhss == fixpoint *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
234 |
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
|
235 |
val tuple_fixdef_thm = foldr1 pair_equalI proj_thms; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
236 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
237 |
val cont_thm = |
33777 | 238 |
Goal.prove_global thy [] [] (mk_trp (mk_cont functional)) |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
239 |
(K (beta_tac 1)); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
240 |
val tuple_unfold_thm = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
241 |
(@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm]) |
33777 | 242 |
|> LocalDefs.unfold (ProofContext.init thy) @{thms split_conv}; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
243 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
244 |
fun mk_unfold_thms [] thm = [] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
245 |
| mk_unfold_thms (n::[]) thm = [(n, thm)] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
246 |
| mk_unfold_thms (n::ns) thm = let |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
247 |
val thmL = thm RS @{thm Pair_eqD1}; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
248 |
val thmR = thm RS @{thm Pair_eqD2}; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
249 |
in (n, thmL) :: mk_unfold_thms ns thmR end; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
250 |
val unfold_binds = map (Binding.suffix_name "_unfold") binds; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
251 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
252 |
(* register unfold theorems *) |
33777 | 253 |
val (unfold_thms, thy) = |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
254 |
(PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard)) |
33777 | 255 |
(mk_unfold_thms unfold_binds tuple_unfold_thm) thy; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
256 |
in |
33788 | 257 |
((proj_thms, unfold_thms), thy) |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
258 |
end; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
259 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
260 |
|
33774 | 261 |
(******************************************************************************) |
33790 | 262 |
(****************** deflation combinators and map functions *******************) |
263 |
(******************************************************************************) |
|
33774 | 264 |
|
265 |
fun defl_of_typ |
|
266 |
(tab : term Symtab.table) |
|
267 |
(T : typ) : term = |
|
268 |
let |
|
269 |
fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts |
|
270 |
| is_closed_typ _ = false; |
|
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
271 |
fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT) |
33774 | 272 |
| defl_of (TVar _) = error ("defl_of_typ: TVar") |
273 |
| defl_of (T as Type (c, Ts)) = |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
274 |
case Symtab.lookup tab c of |
33774 | 275 |
SOME t => Library.foldl mk_capply (t, map defl_of Ts) |
276 |
| NONE => if is_closed_typ T |
|
277 |
then mk_Rep_of T |
|
278 |
else error ("defl_of_typ: type variable under unsupported type constructor " ^ c); |
|
279 |
in defl_of T end; |
|
280 |
||
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
281 |
fun map_of_typ |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
282 |
(tab : string Symtab.table) |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
283 |
(T : typ) : term = |
33774 | 284 |
let |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
285 |
fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
286 |
| is_closed_typ _ = false; |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
287 |
fun map_of (T as TFree (a, _)) = Free (Library.unprefix "'" a, T ->> T) |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
288 |
| map_of (T as TVar _) = error ("map_of_typ: TVar") |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
289 |
| map_of (T as Type (c, Ts)) = |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
290 |
case Symtab.lookup tab c of |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
291 |
SOME t => Library.foldl mk_capply (Const (t, mapT T), map map_of Ts) |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
292 |
| NONE => if is_closed_typ T |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
293 |
then ID_const T |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
294 |
else error ("map_of_typ: type variable under unsupported type constructor " ^ c); |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
295 |
in map_of T end; |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
296 |
|
33774 | 297 |
|
298 |
(******************************************************************************) |
|
299 |
(* prepare datatype specifications *) |
|
300 |
||
301 |
fun read_typ thy str sorts = |
|
302 |
let |
|
303 |
val ctxt = ProofContext.init thy |
|
304 |
|> fold (Variable.declare_typ o TFree) sorts; |
|
305 |
val T = Syntax.read_typ ctxt str; |
|
306 |
in (T, Term.add_tfreesT T sorts) end; |
|
307 |
||
308 |
fun cert_typ sign raw_T sorts = |
|
309 |
let |
|
310 |
val T = Type.no_tvars (Sign.certify_typ sign raw_T) |
|
311 |
handle TYPE (msg, _, _) => error msg; |
|
312 |
val sorts' = Term.add_tfreesT T sorts; |
|
313 |
val _ = |
|
314 |
case duplicates (op =) (map fst sorts') of |
|
315 |
[] => () |
|
316 |
| dups => error ("Inconsistent sort constraints for " ^ commas dups) |
|
317 |
in (T, sorts') end; |
|
318 |
||
319 |
fun gen_domain_isomorphism |
|
320 |
(prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list) |
|
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
321 |
(doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list) |
33774 | 322 |
(thy: theory) |
323 |
: theory = |
|
324 |
let |
|
33792 | 325 |
val _ = Theory.requires thy "Representable" "domain isomorphisms"; |
33774 | 326 |
|
327 |
(* this theory is used just for parsing *) |
|
328 |
val tmp_thy = thy |> |
|
329 |
Theory.copy |> |
|
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
330 |
Sign.add_types (map (fn (tvs, tname, mx, _, morphs) => |
33774 | 331 |
(tname, length tvs, mx)) doms_raw); |
332 |
||
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
333 |
fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts = |
33774 | 334 |
let val (typ, sorts') = prep_typ thy typ_raw sorts |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
335 |
in ((vs, t, mx, typ, morphs), sorts') end; |
33774 | 336 |
|
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
337 |
val (doms : (string list * binding * mixfix * typ * (binding * binding) option) list, |
33774 | 338 |
sorts : (string * sort) list) = |
339 |
fold_map (prep_dom tmp_thy) doms_raw []; |
|
340 |
||
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
341 |
(* domain equations *) |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
342 |
fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) = |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
343 |
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
|
344 |
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
|
345 |
val dom_eqns = map mk_dom_eqn doms; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
346 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
347 |
(* check for valid type parameters *) |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
348 |
val (tyvars, _, _, _, _)::_ = doms; |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
349 |
val new_doms = map (fn (tvs, tname, mx, _, _) => |
33774 | 350 |
let val full_tname = Sign.full_name tmp_thy tname |
351 |
in |
|
352 |
(case duplicates (op =) tvs of |
|
353 |
[] => |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
354 |
if eq_set (op =) (tyvars, tvs) then (full_tname, tvs) |
33774 | 355 |
else error ("Mutually recursive domains must have same type parameters") |
356 |
| dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^ |
|
357 |
" : " ^ commas dups)) |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
358 |
end) doms; |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
359 |
val dom_binds = map (fn (_, tbind, _, _, _) => tbind) doms; |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
360 |
val morphs = map (fn (_, _, _, _, morphs) => morphs) doms; |
33774 | 361 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
362 |
(* declare deflation combinator constants *) |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
363 |
fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy = |
33774 | 364 |
let |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
365 |
val defl_type = Library.foldr cfunT (map (K deflT) vs, deflT); |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
366 |
val defl_bind = Binding.suffix_name "_defl" tbind; |
33774 | 367 |
in |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
368 |
Sign.declare_const ((defl_bind, defl_type), NoSyn) thy |
33774 | 369 |
end; |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
370 |
val (defl_consts, thy) = fold_map declare_defl_const doms thy; |
33774 | 371 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
372 |
(* defining equations for type combinators *) |
33790 | 373 |
val defl_tab1 = DeflData.get thy; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
374 |
val defl_tab2 = |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
375 |
Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts); |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
376 |
val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2); |
33790 | 377 |
val thy = DeflData.put defl_tab' thy; |
33776 | 378 |
fun mk_defl_spec (lhsT, rhsT) = |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
379 |
mk_eqs (defl_of_typ defl_tab' lhsT, |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
380 |
defl_of_typ defl_tab' rhsT); |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
381 |
val defl_specs = map mk_defl_spec dom_eqns; |
33774 | 382 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
383 |
(* register recursive definition of deflation combinators *) |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
384 |
val defl_binds = map (Binding.suffix_name "_defl") dom_binds; |
33788 | 385 |
val ((defl_apply_thms, defl_unfold_thms), thy) = |
386 |
add_fixdefs (defl_binds ~~ defl_specs) thy; |
|
33774 | 387 |
|
33776 | 388 |
(* define types using deflation combinators *) |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
389 |
fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy = |
33774 | 390 |
let |
391 |
fun tfree a = TFree (a, the (AList.lookup (op =) sorts a)) |
|
392 |
val reps = map (mk_Rep_of o tfree) vs; |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
393 |
val defl = Library.foldl mk_capply (defl_const, reps); |
33777 | 394 |
val ((_, _, _, {REP, ...}), thy) = |
33774 | 395 |
Repdef.add_repdef false NONE (tbind, vs, mx) defl NONE thy; |
396 |
in |
|
33777 | 397 |
(REP, thy) |
33774 | 398 |
end; |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
399 |
val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy; |
33791 | 400 |
val thy = RepData.map (fold Thm.add_thm REP_thms) thy; |
33776 | 401 |
|
402 |
(* prove REP equations *) |
|
33782 | 403 |
fun mk_REP_eq_thm (lhsT, rhsT) = |
33776 | 404 |
let |
405 |
val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT); |
|
33791 | 406 |
val REP_simps = RepData.get thy; |
33776 | 407 |
val tac = |
408 |
simp_tac (HOL_basic_ss addsimps REP_simps) 1 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
409 |
THEN resolve_tac defl_unfold_thms 1; |
33776 | 410 |
in |
33777 | 411 |
Goal.prove_global thy [] [] goal (K tac) |
33776 | 412 |
end; |
33782 | 413 |
val REP_eq_thms = map mk_REP_eq_thm dom_eqns; |
414 |
||
415 |
(* register REP equations *) |
|
416 |
val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dom_binds; |
|
417 |
val (_, thy) = thy |> |
|
418 |
(PureThy.add_thms o map Thm.no_attributes) |
|
419 |
(REP_eq_binds ~~ REP_eq_thms); |
|
33776 | 420 |
|
33778 | 421 |
(* define rep/abs functions *) |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
422 |
fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy = |
33778 | 423 |
let |
424 |
val rep_type = cfunT (lhsT, rhsT); |
|
33782 | 425 |
val abs_type = cfunT (rhsT, lhsT); |
33778 | 426 |
val rep_bind = Binding.suffix_name "_rep" tbind; |
427 |
val abs_bind = Binding.suffix_name "_abs" tbind; |
|
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
428 |
val (rep_bind, abs_bind) = the_default (rep_bind, abs_bind) morphs; |
33778 | 429 |
val (rep_const, thy) = thy |> |
430 |
Sign.declare_const ((rep_bind, rep_type), NoSyn); |
|
431 |
val (abs_const, thy) = thy |> |
|
432 |
Sign.declare_const ((abs_bind, abs_type), NoSyn); |
|
433 |
val rep_eqn = Logic.mk_equals (rep_const, coerce_const rep_type); |
|
434 |
val abs_eqn = Logic.mk_equals (abs_const, coerce_const abs_type); |
|
435 |
val ([rep_def, abs_def], thy) = thy |> |
|
436 |
(PureThy.add_defs false o map Thm.no_attributes) |
|
437 |
[(Binding.suffix_name "_rep_def" tbind, rep_eqn), |
|
438 |
(Binding.suffix_name "_abs_def" tbind, abs_eqn)]; |
|
439 |
in |
|
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
440 |
(((rep_const, abs_const), (rep_def, abs_def)), thy) |
33778 | 441 |
end; |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
442 |
val ((rep_abs_consts, rep_abs_defs), thy) = thy |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
443 |
|> fold_map mk_rep_abs (dom_binds ~~ morphs ~~ dom_eqns) |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
444 |
|>> ListPair.unzip; |
33782 | 445 |
|
446 |
(* prove isomorphism and isodefl rules *) |
|
447 |
fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy = |
|
448 |
let |
|
449 |
fun make thm = Drule.standard (thm OF [REP_eq, abs_def, rep_def]); |
|
450 |
val rep_iso_thm = make @{thm domain_rep_iso}; |
|
451 |
val abs_iso_thm = make @{thm domain_abs_iso}; |
|
452 |
val isodefl_thm = make @{thm isodefl_abs_rep}; |
|
33797 | 453 |
val rep_iso_bind = Binding.name "rep_iso"; |
454 |
val abs_iso_bind = Binding.name "abs_iso"; |
|
455 |
val isodefl_bind = Binding.name "isodefl_abs_rep"; |
|
456 |
val (_, thy) = thy |
|
457 |
|> Sign.add_path (Binding.name_of tbind) |
|
458 |
|> (PureThy.add_thms o map Thm.no_attributes) |
|
459 |
[(rep_iso_bind, rep_iso_thm), |
|
460 |
(abs_iso_bind, abs_iso_thm), |
|
461 |
(isodefl_bind, isodefl_thm)] |
|
462 |
||> Sign.parent_path; |
|
33782 | 463 |
in |
464 |
(((rep_iso_thm, abs_iso_thm), isodefl_thm), thy) |
|
465 |
end; |
|
466 |
val ((iso_thms, isodefl_abs_rep_thms), thy) = thy |
|
467 |
|> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs) |
|
468 |
|>> ListPair.unzip; |
|
33778 | 469 |
|
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
470 |
(* declare map functions *) |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
471 |
fun declare_map_const (tbind, (lhsT, rhsT)) thy = |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
472 |
let |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
473 |
val map_type = mapT lhsT; |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
474 |
val map_bind = Binding.suffix_name "_map" tbind; |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
475 |
in |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
476 |
Sign.declare_const ((map_bind, map_type), NoSyn) thy |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
477 |
end; |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
478 |
val (map_consts, thy) = thy |> |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
479 |
fold_map declare_map_const (dom_binds ~~ dom_eqns); |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
480 |
|
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
481 |
(* defining equations for map functions *) |
33790 | 482 |
val map_tab1 = MapData.get thy; |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
483 |
val map_tab2 = |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
484 |
Symtab.make (map (fst o dest_Type o fst) dom_eqns |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
485 |
~~ map (fst o dest_Const) map_consts); |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
486 |
val map_tab' = Symtab.merge (K true) (map_tab1, map_tab2); |
33790 | 487 |
val thy = MapData.put map_tab' thy; |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
488 |
fun mk_map_spec ((rep_const, abs_const), (lhsT, rhsT)) = |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
489 |
let |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
490 |
val lhs = map_of_typ map_tab' lhsT; |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
491 |
val body = map_of_typ map_tab' rhsT; |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
492 |
val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)); |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
493 |
in mk_eqs (lhs, rhs) end; |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
494 |
val map_specs = map mk_map_spec (rep_abs_consts ~~ dom_eqns); |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
495 |
|
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
496 |
(* register recursive definition of map functions *) |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
497 |
val map_binds = map (Binding.suffix_name "_map") dom_binds; |
33788 | 498 |
val ((map_apply_thms, map_unfold_thms), thy) = |
499 |
add_fixdefs (map_binds ~~ map_specs) thy; |
|
500 |
||
501 |
(* prove isodefl rules for map functions *) |
|
502 |
val isodefl_thm = |
|
503 |
let |
|
504 |
fun unprime a = Library.unprefix "'" a; |
|
505 |
fun mk_d (TFree (a, _)) = Free ("d" ^ unprime a, deflT); |
|
506 |
fun mk_f (T as TFree (a, _)) = Free ("f" ^ unprime a, T ->> T); |
|
507 |
fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T); |
|
508 |
fun mk_goal ((map_const, defl_const), (T as Type (c, Ts), rhsT)) = |
|
509 |
let |
|
510 |
val map_term = Library.foldl mk_capply (map_const, map mk_f Ts); |
|
511 |
val defl_term = Library.foldl mk_capply (defl_const, map mk_d Ts); |
|
512 |
in isodefl_const T $ map_term $ defl_term end; |
|
513 |
val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns; |
|
514 |
val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns); |
|
515 |
val goal = mk_trp (foldr1 HOLogic.mk_conj goals); |
|
516 |
val start_thms = |
|
517 |
@{thm split_def} :: defl_apply_thms @ map_apply_thms; |
|
518 |
val adm_rules = |
|
519 |
@{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id}; |
|
520 |
val bottom_rules = |
|
521 |
@{thms fst_strict snd_strict isodefl_bottom simp_thms}; |
|
522 |
val isodefl_rules = |
|
33791 | 523 |
@{thms conjI isodefl_ID_REP} |
524 |
@ isodefl_abs_rep_thms |
|
525 |
@ IsodeflData.get thy; |
|
33845 | 526 |
in |
527 |
Goal.prove_global thy [] assms goal (fn {prems, ...} => |
|
528 |
EVERY |
|
33788 | 529 |
[simp_tac (HOL_basic_ss addsimps start_thms) 1, |
33791 | 530 |
(* FIXME: how reliable is unification here? *) |
531 |
(* Maybe I should instantiate the rule. *) |
|
33788 | 532 |
rtac @{thm parallel_fix_ind} 1, |
533 |
REPEAT (resolve_tac adm_rules 1), |
|
534 |
simp_tac (HOL_basic_ss addsimps bottom_rules) 1, |
|
535 |
simp_tac beta_ss 1, |
|
536 |
simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1, |
|
537 |
REPEAT (etac @{thm conjE} 1), |
|
33845 | 538 |
REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)]) |
33788 | 539 |
end; |
33789 | 540 |
val isodefl_binds = map (Binding.prefix_name "isodefl_") dom_binds; |
541 |
fun conjuncts [] thm = [] |
|
542 |
| conjuncts (n::[]) thm = [(n, thm)] |
|
543 |
| conjuncts (n::ns) thm = let |
|
544 |
val thmL = thm RS @{thm conjunct1}; |
|
545 |
val thmR = thm RS @{thm conjunct2}; |
|
546 |
in (n, thmL):: conjuncts ns thmR end; |
|
547 |
val (isodefl_thms, thy) = thy |> |
|
548 |
(PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard)) |
|
549 |
(conjuncts isodefl_binds isodefl_thm); |
|
33791 | 550 |
val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy; |
33793 | 551 |
|
552 |
(* prove map_ID theorems *) |
|
553 |
fun prove_map_ID_thm |
|
554 |
(((map_const, (lhsT, _)), REP_thm), isodefl_thm) = |
|
555 |
let |
|
556 |
val Ts = snd (dest_Type lhsT); |
|
557 |
val lhs = Library.foldl mk_capply (map_const, map ID_const Ts); |
|
558 |
val goal = mk_eqs (lhs, ID_const lhsT); |
|
559 |
val tac = EVERY |
|
560 |
[rtac @{thm isodefl_REP_imp_ID} 1, |
|
561 |
stac REP_thm 1, |
|
562 |
rtac isodefl_thm 1, |
|
563 |
REPEAT (rtac @{thm isodefl_ID_REP} 1)]; |
|
564 |
in |
|
565 |
Goal.prove_global thy [] [] goal (K tac) |
|
566 |
end; |
|
567 |
val map_ID_binds = map (Binding.suffix_name "_map_ID") dom_binds; |
|
568 |
val map_ID_thms = |
|
569 |
map prove_map_ID_thm |
|
570 |
(map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms); |
|
571 |
val (_, thy) = thy |> |
|
572 |
(PureThy.add_thms o map Thm.no_attributes) |
|
573 |
(map_ID_binds ~~ map_ID_thms); |
|
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
574 |
val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy; |
33802
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
575 |
|
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
576 |
(* define copy combinators *) |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
577 |
val new_dts = |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
578 |
map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns; |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
579 |
val copy_arg_type = tupleT (map (fn (T, _) => T ->> T) dom_eqns); |
33807
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
580 |
val copy_arg = Free ("f", copy_arg_type); |
33802
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
581 |
val copy_args = |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
582 |
let fun mk_copy_args [] t = [] |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
583 |
| mk_copy_args (_::[]) t = [t] |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
584 |
| mk_copy_args (_::xs) t = |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
585 |
mk_fst t :: mk_copy_args xs (mk_snd t); |
33807
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
586 |
in mk_copy_args doms copy_arg end; |
33802
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
587 |
fun copy_of_dtyp (T, dt) = |
33971 | 588 |
if Datatype_Aux.is_rec_type dt |
33802
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
589 |
then copy_of_dtyp' (T, dt) |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
590 |
else ID_const T |
33971 | 591 |
and copy_of_dtyp' (T, Datatype_Aux.DtRec i) = nth copy_args i |
592 |
| copy_of_dtyp' (T, Datatype_Aux.DtTFree a) = ID_const T |
|
593 |
| copy_of_dtyp' (T as Type (_, Ts), Datatype_Aux.DtType (c, ds)) = |
|
33802
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
594 |
case Symtab.lookup map_tab' c of |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
595 |
SOME f => |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
596 |
Library.foldl mk_capply |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
597 |
(Const (f, mapT T), map copy_of_dtyp (Ts ~~ ds)) |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
598 |
| NONE => |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
599 |
(warning ("copy_of_dtyp: unknown type constructor " ^ c); ID_const T); |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
600 |
fun define_copy ((tbind, (rep_const, abs_const)), (lhsT, rhsT)) thy = |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
601 |
let |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
602 |
val copy_type = copy_arg_type ->> (lhsT ->> lhsT); |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
603 |
val copy_bind = Binding.suffix_name "_copy" tbind; |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
604 |
val (copy_const, thy) = thy |> |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
605 |
Sign.declare_const ((copy_bind, copy_type), NoSyn); |
33971 | 606 |
val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT; |
33802
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
607 |
val body = copy_of_dtyp (rhsT, dtyp); |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
608 |
val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)); |
33807
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
609 |
val rhs = big_lambda copy_arg comp; |
33802
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
610 |
val eqn = Logic.mk_equals (copy_const, rhs); |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
611 |
val ([copy_def], thy) = |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
612 |
thy |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
613 |
|> Sign.add_path (Binding.name_of tbind) |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
614 |
|> (PureThy.add_defs false o map Thm.no_attributes) |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
615 |
[(Binding.name "copy_def", eqn)] |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
616 |
||> Sign.parent_path; |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
617 |
in ((copy_const, copy_def), thy) end; |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
618 |
val ((copy_consts, copy_defs), thy) = thy |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
619 |
|> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns) |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
620 |
|>> ListPair.unzip; |
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
621 |
|
33807
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
622 |
(* define combined copy combinator *) |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
623 |
val ((c_const, c_def_thms), thy) = |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
624 |
if length doms = 1 |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
625 |
then ((hd copy_consts, []), thy) |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
626 |
else |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
627 |
let |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
628 |
val c_type = copy_arg_type ->> copy_arg_type; |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
629 |
val c_name = space_implode "_" (map Binding.name_of dom_binds); |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
630 |
val c_bind = Binding.name (c_name ^ "_copy"); |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
631 |
val c_body = |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
632 |
mk_tuple (map (mk_capply o rpair copy_arg) copy_consts); |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
633 |
val c_rhs = big_lambda copy_arg c_body; |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
634 |
val (c_const, thy) = |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
635 |
Sign.declare_const ((c_bind, c_type), NoSyn) thy; |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
636 |
val c_eqn = Logic.mk_equals (c_const, c_rhs); |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
637 |
val (c_def_thms, thy) = |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
638 |
thy |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
639 |
|> Sign.add_path c_name |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
640 |
|> (PureThy.add_defs false o map Thm.no_attributes) |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
641 |
[(Binding.name "copy_def", c_eqn)] |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
642 |
||> Sign.parent_path; |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
643 |
in ((c_const, c_def_thms), thy) end; |
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
644 |
|
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
645 |
(* fixed-point lemma for combined copy combinator *) |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
646 |
val fix_copy_lemma = |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
647 |
let |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
648 |
fun mk_map_ID (map_const, (Type (c, Ts), rhsT)) = |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
649 |
Library.foldl mk_capply (map_const, map ID_const Ts); |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
650 |
val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns)); |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
651 |
val goal = mk_eqs (mk_fix c_const, rhs); |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
652 |
val rules = |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
653 |
[@{thm pair_collapse}, @{thm split_def}] |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
654 |
@ map_apply_thms |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
655 |
@ c_def_thms @ copy_defs |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
656 |
@ MapIdData.get thy; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
657 |
val tac = simp_tac (beta_ss addsimps rules) 1; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
658 |
in |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
659 |
Goal.prove_global thy [] [] goal (K tac) |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
660 |
end; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
661 |
|
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
662 |
(* prove reach lemmas *) |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
663 |
val reach_thm_projs = |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
664 |
let fun mk_projs (x::[]) t = [(x, t)] |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
665 |
| mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
666 |
in mk_projs dom_binds (mk_fix c_const) end; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
667 |
fun prove_reach_thm (((bind, t), map_ID_thm), (lhsT, rhsT)) thy = |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
668 |
let |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
669 |
val x = Free ("x", lhsT); |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
670 |
val goal = mk_eqs (mk_capply (t, x), x); |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
671 |
val rules = |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
672 |
fix_copy_lemma :: map_ID_thm :: @{thms fst_conv snd_conv ID1}; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
673 |
val tac = simp_tac (HOL_basic_ss addsimps rules) 1; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
674 |
val reach_thm = Goal.prove_global thy [] [] goal (K tac); |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
675 |
in |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
676 |
thy |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
677 |
|> Sign.add_path (Binding.name_of bind) |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
678 |
|> yield_singleton (PureThy.add_thms o map Thm.no_attributes) |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
679 |
(Binding.name "reach", reach_thm) |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
680 |
||> Sign.parent_path |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
681 |
end; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
682 |
val (reach_thms, thy) = thy |> |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
683 |
fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns); |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
684 |
|
33774 | 685 |
in |
33777 | 686 |
thy |
33774 | 687 |
end; |
688 |
||
689 |
val domain_isomorphism = gen_domain_isomorphism cert_typ; |
|
690 |
val domain_isomorphism_cmd = gen_domain_isomorphism read_typ; |
|
691 |
||
692 |
(******************************************************************************) |
|
693 |
(******************************** outer syntax ********************************) |
|
694 |
(******************************************************************************) |
|
695 |
||
696 |
local |
|
697 |
||
698 |
structure P = OuterParse and K = OuterKeyword |
|
699 |
||
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
700 |
val parse_domain_iso : |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
701 |
(string list * binding * mixfix * string * (binding * binding) option) |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
702 |
parser = |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
703 |
(P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ) -- |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
704 |
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))) |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
705 |
>> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs)); |
33774 | 706 |
|
707 |
val parse_domain_isos = P.and_list1 parse_domain_iso; |
|
708 |
||
709 |
in |
|
710 |
||
711 |
val _ = |
|
712 |
OuterSyntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" K.thy_decl |
|
713 |
(parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd)); |
|
714 |
||
715 |
end; |
|
716 |
||
717 |
end; |