kuncar@57866
|
1 |
(* Title: HOL/Tools/Transfer/transfer_bnf.ML
|
kuncar@57866
|
2 |
Author: Ondrej Kuncar, TU Muenchen
|
kuncar@57866
|
3 |
|
kuncar@57866
|
4 |
Setup for Transfer for types that are BNF.
|
kuncar@57866
|
5 |
*)
|
kuncar@57866
|
6 |
|
kuncar@57866
|
7 |
signature TRANSFER_BNF =
|
kuncar@57866
|
8 |
sig
|
kuncar@57866
|
9 |
val base_name_of_bnf: BNF_Def.bnf -> binding
|
kuncar@57866
|
10 |
val type_name_of_bnf: BNF_Def.bnf -> string
|
kuncar@57866
|
11 |
val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
|
kuncar@57866
|
12 |
val map_local_theory: (local_theory -> local_theory) -> theory -> theory
|
kuncar@57866
|
13 |
val bnf_only_type_ctr: (BNF_Def.bnf -> 'a -> 'a) -> BNF_Def.bnf -> 'a -> 'a
|
kuncar@57866
|
14 |
end
|
kuncar@57866
|
15 |
|
kuncar@57866
|
16 |
structure Transfer_BNF : TRANSFER_BNF =
|
kuncar@57866
|
17 |
struct
|
kuncar@57866
|
18 |
|
kuncar@57866
|
19 |
open BNF_Util
|
kuncar@57866
|
20 |
open BNF_Def
|
kuncar@57866
|
21 |
open BNF_FP_Def_Sugar
|
kuncar@57866
|
22 |
|
kuncar@57866
|
23 |
(* util functions *)
|
kuncar@57866
|
24 |
|
kuncar@57866
|
25 |
fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
|
kuncar@57866
|
26 |
fun mk_Frees_free x Ts ctxt = Variable.variant_frees ctxt [] (mk_names (length Ts) x ~~ Ts) |> map Free
|
kuncar@57866
|
27 |
|
kuncar@57866
|
28 |
fun mk_Domainp P =
|
kuncar@57866
|
29 |
let
|
kuncar@57866
|
30 |
val PT = fastype_of P
|
kuncar@57866
|
31 |
val argT = hd (binder_types PT)
|
kuncar@57866
|
32 |
in
|
kuncar@57866
|
33 |
Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P
|
kuncar@57866
|
34 |
end
|
kuncar@57866
|
35 |
|
kuncar@57866
|
36 |
fun mk_pred pred_def args T =
|
kuncar@57866
|
37 |
let
|
kuncar@57866
|
38 |
val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
|
kuncar@57866
|
39 |
|> head_of |> fst o dest_Const
|
kuncar@57866
|
40 |
val argsT = map fastype_of args
|
kuncar@57866
|
41 |
in
|
kuncar@57866
|
42 |
list_comb (Const (pred_name, argsT ---> (T --> HOLogic.boolT)), args)
|
kuncar@57866
|
43 |
end
|
kuncar@57866
|
44 |
|
kuncar@57866
|
45 |
fun mk_eq_onp arg =
|
kuncar@57866
|
46 |
let
|
kuncar@57866
|
47 |
val argT = domain_type (fastype_of arg)
|
kuncar@57866
|
48 |
in
|
kuncar@57866
|
49 |
Const (@{const_name eq_onp}, (argT --> HOLogic.boolT) --> argT --> argT --> HOLogic.boolT)
|
kuncar@57866
|
50 |
$ arg
|
kuncar@57866
|
51 |
end
|
kuncar@57866
|
52 |
|
kuncar@57866
|
53 |
fun subst_conv thm =
|
kuncar@57866
|
54 |
Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) @{context}
|
kuncar@57866
|
55 |
|
kuncar@57866
|
56 |
fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
|
kuncar@57866
|
57 |
|
kuncar@57866
|
58 |
fun is_Type (Type _) = true
|
kuncar@57866
|
59 |
| is_Type _ = false
|
kuncar@57866
|
60 |
|
kuncar@57866
|
61 |
fun map_local_theory f = Named_Target.theory_init #> f #> Local_Theory.exit_global
|
kuncar@57866
|
62 |
|
kuncar@57866
|
63 |
fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I
|
kuncar@57866
|
64 |
|
kuncar@57866
|
65 |
fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
|
kuncar@57866
|
66 |
|
kuncar@57866
|
67 |
fun fp_sugar_only_type_ctr f fp_sugar =
|
kuncar@57866
|
68 |
if is_Type (T_of_bnf (bnf_of_fp_sugar fp_sugar)) then f fp_sugar else I
|
kuncar@57866
|
69 |
|
kuncar@57866
|
70 |
(* relation constraints - bi_total & co. *)
|
kuncar@57866
|
71 |
|
kuncar@57866
|
72 |
fun mk_relation_constraint name arg =
|
kuncar@57866
|
73 |
(Const (name, fastype_of arg --> HOLogic.boolT)) $ arg
|
kuncar@57866
|
74 |
|
kuncar@57866
|
75 |
fun side_constraint_tac bnf constr_defs ctxt i =
|
kuncar@57866
|
76 |
let
|
kuncar@57866
|
77 |
val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf,
|
kuncar@57866
|
78 |
rel_OO_of_bnf bnf]
|
kuncar@57866
|
79 |
in
|
kuncar@57866
|
80 |
(SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf)
|
kuncar@57866
|
81 |
THEN_ALL_NEW atac) i
|
kuncar@57866
|
82 |
end
|
kuncar@57866
|
83 |
|
kuncar@57866
|
84 |
fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
|
kuncar@57866
|
85 |
(SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
|
kuncar@57866
|
86 |
CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i
|
kuncar@57866
|
87 |
|
kuncar@57866
|
88 |
fun generate_relation_constraint_goal ctxt bnf constraint_def =
|
kuncar@57866
|
89 |
let
|
kuncar@57866
|
90 |
val constr_name = constraint_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
|
kuncar@57866
|
91 |
|> head_of |> fst o dest_Const
|
kuncar@57866
|
92 |
val live = live_of_bnf bnf
|
kuncar@57866
|
93 |
val (((As, Bs), Ds), ctxt) = ctxt
|
kuncar@57866
|
94 |
|> mk_TFrees live
|
kuncar@57866
|
95 |
||>> mk_TFrees live
|
kuncar@57866
|
96 |
||>> mk_TFrees (dead_of_bnf bnf)
|
kuncar@57866
|
97 |
|
kuncar@57866
|
98 |
val relator = mk_rel_of_bnf Ds As Bs bnf
|
kuncar@57866
|
99 |
val relsT = map2 mk_pred2T As Bs
|
kuncar@57866
|
100 |
val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
|
kuncar@57866
|
101 |
val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args)))
|
kuncar@57866
|
102 |
val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args
|
kuncar@57866
|
103 |
val goal = Logic.list_implies (assms, concl)
|
kuncar@57866
|
104 |
in
|
kuncar@57866
|
105 |
(goal, ctxt)
|
kuncar@57866
|
106 |
end
|
kuncar@57866
|
107 |
|
kuncar@57866
|
108 |
fun prove_relation_side_constraint ctxt bnf constraint_def =
|
kuncar@57866
|
109 |
let
|
kuncar@57866
|
110 |
val old_ctxt = ctxt
|
kuncar@57866
|
111 |
val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
|
kuncar@57866
|
112 |
val thm = Goal.prove ctxt [] [] goal
|
kuncar@57866
|
113 |
(fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1)
|
kuncar@57866
|
114 |
in
|
kuncar@57866
|
115 |
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
|
kuncar@57866
|
116 |
end
|
kuncar@57866
|
117 |
|
kuncar@57866
|
118 |
fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints =
|
kuncar@57866
|
119 |
let
|
kuncar@57866
|
120 |
val old_ctxt = ctxt
|
kuncar@57866
|
121 |
val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
|
kuncar@57866
|
122 |
val thm = Goal.prove ctxt [] [] goal
|
kuncar@57866
|
123 |
(fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1)
|
kuncar@57866
|
124 |
in
|
kuncar@57866
|
125 |
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
|
kuncar@57866
|
126 |
end
|
kuncar@57866
|
127 |
|
kuncar@57866
|
128 |
val defs = [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}),
|
kuncar@57866
|
129 |
("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})]
|
kuncar@57866
|
130 |
|
kuncar@57866
|
131 |
fun prove_relation_constraints bnf lthy =
|
kuncar@57866
|
132 |
let
|
kuncar@57866
|
133 |
val transfer_attr = @{attributes [transfer_rule]}
|
kuncar@57866
|
134 |
val Tname = base_name_of_bnf bnf
|
kuncar@57866
|
135 |
fun qualify suffix = Binding.qualified true suffix Tname
|
kuncar@57866
|
136 |
|
kuncar@57866
|
137 |
val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs
|
kuncar@57866
|
138 |
val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
|
kuncar@57866
|
139 |
[snd (nth defs 0), snd (nth defs 1)]
|
kuncar@57866
|
140 |
val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
|
kuncar@57866
|
141 |
[snd (nth defs 2), snd (nth defs 3)]
|
kuncar@57866
|
142 |
val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs
|
kuncar@57866
|
143 |
val notes = maps (fn (name, thm) => [((qualify name, []), [([thm], transfer_attr)])]) defs
|
kuncar@57866
|
144 |
in
|
kuncar@57866
|
145 |
notes
|
kuncar@57866
|
146 |
end
|
kuncar@57866
|
147 |
|
kuncar@57866
|
148 |
(* relator_eq *)
|
kuncar@57866
|
149 |
|
kuncar@57866
|
150 |
fun relator_eq bnf =
|
kuncar@57866
|
151 |
[((Binding.empty, []), [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
|
kuncar@57866
|
152 |
|
kuncar@57866
|
153 |
(* predicator definition and Domainp and eq_onp theorem *)
|
kuncar@57866
|
154 |
|
kuncar@57866
|
155 |
fun define_pred bnf lthy =
|
kuncar@57866
|
156 |
let
|
kuncar@57866
|
157 |
fun mk_pred_name c = Binding.prefix_name "pred_" c
|
kuncar@57866
|
158 |
val live = live_of_bnf bnf
|
kuncar@57866
|
159 |
val Tname = base_name_of_bnf bnf
|
kuncar@57866
|
160 |
val ((As, Ds), lthy) = lthy
|
kuncar@57866
|
161 |
|> mk_TFrees live
|
kuncar@57866
|
162 |
||>> mk_TFrees (dead_of_bnf bnf)
|
kuncar@57866
|
163 |
val T = mk_T_of_bnf Ds As bnf
|
kuncar@57866
|
164 |
val sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf
|
kuncar@57866
|
165 |
val argTs = map mk_pred1T As
|
kuncar@57866
|
166 |
val args = mk_Frees_free "P" argTs lthy
|
kuncar@57866
|
167 |
val conjs = map (fn (set, arg) => mk_Ball (set $ Bound 0) arg) (sets ~~ args)
|
kuncar@57866
|
168 |
val rhs = Abs ("x", T, foldr1 HOLogic.mk_conj conjs)
|
kuncar@57866
|
169 |
val pred_name = mk_pred_name Tname
|
kuncar@57866
|
170 |
val headT = argTs ---> (T --> HOLogic.boolT)
|
kuncar@57866
|
171 |
val head = Free (Binding.name_of pred_name, headT)
|
kuncar@57866
|
172 |
val lhs = list_comb (head, args)
|
kuncar@57866
|
173 |
val def = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
|
kuncar@57866
|
174 |
val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)),
|
kuncar@57866
|
175 |
((Binding.empty, []), def)) lthy
|
kuncar@57866
|
176 |
in
|
kuncar@57866
|
177 |
(pred_def, lthy)
|
kuncar@57866
|
178 |
end
|
kuncar@57866
|
179 |
|
kuncar@57866
|
180 |
fun Domainp_tac bnf pred_def ctxt i =
|
kuncar@57866
|
181 |
let
|
kuncar@57866
|
182 |
val n = live_of_bnf bnf
|
kuncar@57866
|
183 |
val set_map's = set_map_of_bnf bnf
|
kuncar@57866
|
184 |
in
|
kuncar@57866
|
185 |
EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
|
kuncar@57866
|
186 |
in_rel_of_bnf bnf, pred_def]), rtac iffI,
|
kuncar@57866
|
187 |
REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt,
|
kuncar@57866
|
188 |
CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp),
|
kuncar@57866
|
189 |
etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
|
kuncar@57866
|
190 |
hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
|
kuncar@57866
|
191 |
etac @{thm DomainPI}]) set_map's,
|
kuncar@57866
|
192 |
REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
|
kuncar@57866
|
193 |
rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym,
|
kuncar@57866
|
194 |
map_id_of_bnf bnf]),
|
kuncar@57866
|
195 |
REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]},
|
kuncar@57866
|
196 |
rtac @{thm fst_conv}]), rtac CollectI,
|
kuncar@57866
|
197 |
CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
|
kuncar@57866
|
198 |
REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
|
kuncar@57866
|
199 |
dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's
|
kuncar@57866
|
200 |
] i
|
kuncar@57866
|
201 |
end
|
kuncar@57866
|
202 |
|
kuncar@57866
|
203 |
fun prove_Domainp_rel ctxt bnf pred_def =
|
kuncar@57866
|
204 |
let
|
kuncar@57866
|
205 |
val live = live_of_bnf bnf
|
kuncar@57866
|
206 |
val old_ctxt = ctxt
|
kuncar@57866
|
207 |
val (((As, Bs), Ds), ctxt) = ctxt
|
kuncar@57866
|
208 |
|> mk_TFrees live
|
kuncar@57866
|
209 |
||>> mk_TFrees live
|
kuncar@57866
|
210 |
||>> mk_TFrees (dead_of_bnf bnf)
|
kuncar@57866
|
211 |
|
kuncar@57866
|
212 |
val relator = mk_rel_of_bnf Ds As Bs bnf
|
kuncar@57866
|
213 |
val relsT = map2 mk_pred2T As Bs
|
kuncar@57866
|
214 |
val T = mk_T_of_bnf Ds As bnf
|
kuncar@57866
|
215 |
val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
|
kuncar@57866
|
216 |
val lhs = mk_Domainp (list_comb (relator, args))
|
kuncar@57866
|
217 |
val rhs = mk_pred pred_def (map mk_Domainp args) T
|
kuncar@57866
|
218 |
val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
|
kuncar@57866
|
219 |
val thm = Goal.prove ctxt [] [] goal
|
kuncar@57866
|
220 |
(fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1)
|
kuncar@57866
|
221 |
in
|
kuncar@57866
|
222 |
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
|
kuncar@57866
|
223 |
end
|
kuncar@57866
|
224 |
|
kuncar@57866
|
225 |
fun pred_eq_onp_tac bnf pred_def ctxt i =
|
kuncar@57866
|
226 |
(SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp},
|
kuncar@57866
|
227 |
@{thm Ball_Collect}, pred_def]) THEN' CONVERSION (subst_conv (map_id0_of_bnf bnf RS sym))
|
kuncar@57866
|
228 |
THEN' rtac (rel_Grp_of_bnf bnf)) i
|
kuncar@57866
|
229 |
|
kuncar@57866
|
230 |
fun prove_rel_eq_onp ctxt bnf pred_def =
|
kuncar@57866
|
231 |
let
|
kuncar@57866
|
232 |
val live = live_of_bnf bnf
|
kuncar@57866
|
233 |
val old_ctxt = ctxt
|
kuncar@57866
|
234 |
val ((As, Ds), ctxt) = ctxt
|
kuncar@57866
|
235 |
|> mk_TFrees live
|
kuncar@57866
|
236 |
||>> mk_TFrees (dead_of_bnf bnf)
|
kuncar@57866
|
237 |
val T = mk_T_of_bnf Ds As bnf
|
kuncar@57866
|
238 |
val argTs = map mk_pred1T As
|
kuncar@57866
|
239 |
val (args, ctxt) = mk_Frees "P" argTs ctxt
|
kuncar@57866
|
240 |
val relator = mk_rel_of_bnf Ds As As bnf
|
kuncar@57866
|
241 |
val lhs = list_comb (relator, map mk_eq_onp args)
|
kuncar@57866
|
242 |
val rhs = mk_eq_onp (mk_pred pred_def args T)
|
kuncar@57866
|
243 |
val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
|
kuncar@57866
|
244 |
val thm = Goal.prove ctxt [] [] goal
|
kuncar@57866
|
245 |
(fn {context = ctxt, prems = _} => pred_eq_onp_tac bnf pred_def ctxt 1)
|
kuncar@57866
|
246 |
in
|
kuncar@57866
|
247 |
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
|
kuncar@57866
|
248 |
end
|
kuncar@57866
|
249 |
|
kuncar@57866
|
250 |
fun predicator bnf lthy =
|
kuncar@57866
|
251 |
let
|
kuncar@57866
|
252 |
val (pred_def, lthy) = define_pred bnf lthy
|
kuncar@57866
|
253 |
val pred_def = Morphism.thm (Local_Theory.target_morphism lthy) pred_def
|
kuncar@57866
|
254 |
val Domainp_rel = prove_Domainp_rel lthy bnf pred_def
|
kuncar@57866
|
255 |
val rel_eq_onp = prove_rel_eq_onp lthy bnf pred_def
|
kuncar@57866
|
256 |
fun qualify defname suffix = Binding.qualified true suffix defname
|
kuncar@57866
|
257 |
val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
|
kuncar@57866
|
258 |
val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
|
kuncar@57866
|
259 |
val pred_data = {rel_eq_onp = rel_eq_onp}
|
kuncar@57866
|
260 |
val type_name = type_name_of_bnf bnf
|
kuncar@57866
|
261 |
val relator_domain_attr = @{attributes [relator_domain]}
|
kuncar@57866
|
262 |
val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)]),
|
kuncar@57866
|
263 |
((rel_eq_onp_thm_name, []), [([rel_eq_onp], [])])]
|
kuncar@57866
|
264 |
val lthy = Local_Theory.declaration {syntax = false, pervasive = true}
|
kuncar@57866
|
265 |
(fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) lthy
|
kuncar@57866
|
266 |
in
|
kuncar@57866
|
267 |
(notes, lthy)
|
kuncar@57866
|
268 |
end
|
kuncar@57866
|
269 |
|
kuncar@57866
|
270 |
(* BNF interpretation *)
|
kuncar@57866
|
271 |
|
kuncar@57866
|
272 |
fun transfer_bnf_interpretation bnf lthy =
|
kuncar@57866
|
273 |
let
|
kuncar@57866
|
274 |
val constr_notes = if dead_of_bnf bnf > 0 then []
|
kuncar@57866
|
275 |
else prove_relation_constraints bnf lthy
|
kuncar@57866
|
276 |
val relator_eq_notes = if dead_of_bnf bnf > 0 then []
|
kuncar@57866
|
277 |
else relator_eq bnf
|
kuncar@57866
|
278 |
val (pred_notes, lthy) = predicator bnf lthy
|
kuncar@57866
|
279 |
in
|
kuncar@57866
|
280 |
snd (Local_Theory.notes (constr_notes @ relator_eq_notes @ pred_notes) lthy)
|
kuncar@57866
|
281 |
end
|
kuncar@57866
|
282 |
|
kuncar@57866
|
283 |
val _ = Context.>> (Context.map_theory (bnf_interpretation
|
kuncar@57866
|
284 |
(bnf_only_type_ctr (fn bnf => map_local_theory (transfer_bnf_interpretation bnf)))))
|
kuncar@57866
|
285 |
|
kuncar@57866
|
286 |
(* simplification rules for the predicator *)
|
kuncar@57866
|
287 |
|
kuncar@57866
|
288 |
fun lookup_defined_pred_data lthy name =
|
kuncar@57866
|
289 |
case (Transfer.lookup_pred_data lthy name) of
|
kuncar@57866
|
290 |
SOME data => data
|
kuncar@57866
|
291 |
| NONE => (error "lookup_pred_data: something went utterly wrong")
|
kuncar@57866
|
292 |
|
kuncar@57866
|
293 |
fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
|
kuncar@57866
|
294 |
let
|
kuncar@57866
|
295 |
val involved_types = distinct op= (
|
kuncar@57866
|
296 |
map type_name_of_bnf (#nested_bnfs fp_sugar)
|
kuncar@57866
|
297 |
@ map type_name_of_bnf (#nesting_bnfs fp_sugar)
|
kuncar@57866
|
298 |
@ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
|
kuncar@57866
|
299 |
val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
|
kuncar@57866
|
300 |
val live = live_of_bnf (bnf_of_fp_sugar fp_sugar)
|
kuncar@57866
|
301 |
val old_lthy = lthy
|
kuncar@57866
|
302 |
val (As, lthy) = mk_TFrees live lthy
|
kuncar@57866
|
303 |
val predTs = map mk_pred1T As
|
kuncar@57866
|
304 |
val (preds, lthy) = mk_Frees "P" predTs lthy
|
kuncar@57866
|
305 |
val args = map mk_eq_onp preds
|
kuncar@57866
|
306 |
val cTs = map (SOME o certifyT lthy) (maps (replicate 2) As)
|
kuncar@57866
|
307 |
val cts = map (SOME o certify lthy) args
|
kuncar@57866
|
308 |
fun get_rhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
|
kuncar@57866
|
309 |
fun is_eqn thm = can get_rhs thm
|
kuncar@57866
|
310 |
fun rel2pred_massage thm =
|
kuncar@57866
|
311 |
let
|
kuncar@57866
|
312 |
fun pred_eq_onp_conj 0 = error "not defined"
|
kuncar@57866
|
313 |
| pred_eq_onp_conj 1 = @{thm eq_onp_same_args}
|
kuncar@57866
|
314 |
| pred_eq_onp_conj n =
|
kuncar@57866
|
315 |
let
|
kuncar@57866
|
316 |
val conj_cong = @{thm arg_cong2[of _ _ _ _ "op \<and>"]}
|
kuncar@57866
|
317 |
val start = @{thm eq_onp_same_args} RS conj_cong
|
kuncar@57866
|
318 |
in
|
kuncar@57866
|
319 |
@{thm eq_onp_same_args} RS (funpow (n - 2) (fn thm => start RS thm) start)
|
kuncar@57866
|
320 |
end
|
kuncar@57866
|
321 |
val n = if is_eqn thm then thm |> get_rhs |> HOLogic.dest_conj |> length else 0
|
kuncar@57866
|
322 |
in
|
kuncar@57866
|
323 |
thm
|
kuncar@57866
|
324 |
|> Drule.instantiate' cTs cts
|
kuncar@57866
|
325 |
|> Local_Defs.unfold lthy eq_onps
|
kuncar@57866
|
326 |
|> (fn thm => if n > 0 then @{thm box_equals}
|
kuncar@57866
|
327 |
OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj n]
|
kuncar@57866
|
328 |
else thm RS (@{thm eq_onp_same_args} RS iffD1))
|
kuncar@57866
|
329 |
end
|
kuncar@57866
|
330 |
val rel_injects = #rel_injects fp_sugar
|
kuncar@57866
|
331 |
in
|
kuncar@57866
|
332 |
rel_injects
|
kuncar@57866
|
333 |
|> map rel2pred_massage
|
kuncar@57866
|
334 |
|> Variable.export lthy old_lthy
|
kuncar@57866
|
335 |
|> map Drule.zero_var_indexes
|
kuncar@57866
|
336 |
end
|
kuncar@57866
|
337 |
|
kuncar@57866
|
338 |
(* fp_sugar interpretation *)
|
kuncar@57866
|
339 |
|
kuncar@57866
|
340 |
fun transfer_fp_sugar_interpretation fp_sugar lthy =
|
kuncar@57866
|
341 |
let
|
kuncar@57866
|
342 |
val pred_injects = prove_pred_inject lthy fp_sugar
|
kuncar@57866
|
343 |
fun qualify defname suffix = Binding.qualified true suffix defname
|
kuncar@57866
|
344 |
val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject"
|
kuncar@57866
|
345 |
val simp_attrs = @{attributes [simp]}
|
kuncar@57866
|
346 |
in
|
kuncar@57866
|
347 |
snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
|
kuncar@57866
|
348 |
end
|
kuncar@57866
|
349 |
|
kuncar@57866
|
350 |
val _ = Context.>> (Context.map_theory (fp_sugar_interpretation
|
kuncar@57866
|
351 |
(fp_sugar_only_type_ctr (fn fp_sugar => map_local_theory (transfer_fp_sugar_interpretation fp_sugar)))))
|
kuncar@57866
|
352 |
|
kuncar@57866
|
353 |
end
|