32 let |
32 let |
33 val PT = fastype_of P |
33 val PT = fastype_of P |
34 val argT = hd (binder_types PT) |
34 val argT = hd (binder_types PT) |
35 in |
35 in |
36 Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P |
36 Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P |
37 end |
|
38 |
|
39 fun mk_eq_onp arg = |
|
40 let |
|
41 val argT = domain_type (fastype_of arg) |
|
42 in |
|
43 Const (@{const_name eq_onp}, (argT --> HOLogic.boolT) --> argT --> argT --> HOLogic.boolT) |
|
44 $ arg |
|
45 end |
37 end |
46 |
38 |
47 fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst |
39 fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst |
48 |
40 |
49 fun is_Type (Type _) = true |
41 fun is_Type (Type _) = true |
250 fun lookup_defined_pred_data lthy name = |
242 fun lookup_defined_pred_data lthy name = |
251 case Transfer.lookup_pred_data lthy name of |
243 case Transfer.lookup_pred_data lthy name of |
252 SOME data => data |
244 SOME data => data |
253 | NONE => raise NO_PRED_DATA () |
245 | NONE => raise NO_PRED_DATA () |
254 |
246 |
255 val rel_eq_onp_with_tops_of = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv |
|
256 (Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))); |
|
257 |
|
258 fun prove_pred_inject lthy ({T = fpT, fp_nesting_bnfs, live_nesting_bnfs, |
|
259 fp_res = {bnfs = fp_bnfs, ...}, fp_bnf_sugar = {rel_injects, ...}, ...} : fp_sugar) = |
|
260 let |
|
261 val As = snd (dest_Type fpT) |
|
262 val liveness = liveness_of_fp_bnf (length As) (hd fp_bnfs) |
|
263 val lives = map_filter (uncurry (fn true => SOME | false => K NONE)) (liveness ~~ As) |
|
264 |
|
265 val involved_bnfs = distinct (op = o @{apply 2} BNF_Def.T_of_bnf) |
|
266 (fp_nesting_bnfs @ live_nesting_bnfs @ fp_bnfs) |
|
267 val eq_onps = map (rel_eq_onp_with_tops_of o rel_eq_onp_of_bnf) involved_bnfs |
|
268 val old_lthy = lthy |
|
269 val (As, lthy) = mk_TFrees' (map Type.sort_of_atyp lives) lthy |
|
270 val predTs = map mk_pred1T As |
|
271 val (preds, lthy) = mk_Frees "P" predTs lthy |
|
272 val args = map mk_eq_onp preds |
|
273 val cTs = map (SOME o Thm.ctyp_of lthy) (maps (replicate 2) As) |
|
274 val cts = map (SOME o Thm.cterm_of lthy) args |
|
275 fun get_rhs thm = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd |
|
276 fun is_eqn thm = can get_rhs thm |
|
277 fun rel2pred_massage thm = |
|
278 let |
|
279 val live_step = @{lemma "x = y \<Longrightarrow> (eq_onp P a a \<and> x) = (P a \<and> y)" by (simp only: eq_onp_same_args)} |
|
280 val kill_top1 = @{lemma "(top x \<and> P) = P" by blast} |
|
281 val kill_top2 = @{lemma "(P \<and> top x) = P" by blast} |
|
282 fun pred_eq_onp_conj conjs = List.foldr (fn (_, thm) => thm RS live_step) |
|
283 @{thm refl[of True]} conjs |
|
284 val conjuncts = if is_eqn thm then thm |> get_rhs |> HOLogic.dest_conj else [] |
|
285 val kill_top = Local_Defs.unfold lthy [kill_top2] #> Local_Defs.unfold lthy [kill_top1] |
|
286 val kill_True = Local_Defs.unfold lthy [@{thm HOL.simp_thms(21)}] |
|
287 in |
|
288 thm |
|
289 |> Thm.instantiate' cTs cts |
|
290 |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv |
|
291 (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))) |
|
292 |> Local_Defs.unfold lthy eq_onps |
|
293 |> (fn thm => if conjuncts <> [] then @{thm box_equals} |
|
294 OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj conjuncts |> kill_True] |
|
295 else thm RS (@{thm eq_onp_same_args} RS iffD1)) |
|
296 |> kill_top |
|
297 end |
|
298 in |
|
299 rel_injects |
|
300 |> map (Local_Defs.unfold lthy [@{thm conj_assoc}]) |
|
301 |> map rel2pred_massage |
|
302 |> Variable.export lthy old_lthy |
|
303 |> map Drule.zero_var_indexes |
|
304 end |
|
305 |
|
306 |
247 |
307 (* fp_sugar interpretation *) |
248 (* fp_sugar interpretation *) |
308 |
249 |
309 fun fp_sugar_transfer_rules (fp_sugar:fp_sugar) = |
250 fun fp_sugar_transfer_rules (fp_sugar:fp_sugar) = |
310 let |
251 let |
315 val transfer_attr = @{attributes [transfer_rule]} |
256 val transfer_attr = @{attributes [transfer_rule]} |
316 in |
257 in |
317 map (fn thm => ((Binding.empty, []), [([thm], transfer_attr)])) transfer_rules |
258 map (fn thm => ((Binding.empty, []), [([thm], transfer_attr)])) transfer_rules |
318 end |
259 end |
319 |
260 |
320 fun pred_injects fp_sugar lthy = |
261 fun register_pred_injects fp_sugar lthy = |
321 let |
262 let |
322 val pred_injects = prove_pred_inject lthy fp_sugar |
263 val pred_injects = #pred_injects (#fp_bnf_sugar fp_sugar) |
323 fun qualify defname suffix = Binding.qualified true suffix defname |
|
324 val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject" |
|
325 val simp_attrs = @{attributes [simp]} |
|
326 val type_name = type_name_of_bnf (#fp_bnf fp_sugar) |
264 val type_name = type_name_of_bnf (#fp_bnf fp_sugar) |
327 val pred_data = lookup_defined_pred_data lthy type_name |
265 val pred_data = lookup_defined_pred_data lthy type_name |
328 |> Transfer.update_pred_simps pred_injects |
266 |> Transfer.update_pred_simps pred_injects |
329 in |
267 in |
330 lthy |
268 lthy |
331 |> Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) |
|
332 |> snd |
|
333 |> Local_Theory.declaration {syntax = false, pervasive = true} |
269 |> Local_Theory.declaration {syntax = false, pervasive = true} |
334 (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) |
270 (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) |
335 |> Local_Theory.restore |
271 |> Local_Theory.restore |
336 end |
272 end |
337 |
273 |
338 |
|
339 fun transfer_fp_sugars_interpretation fp_sugar lthy = |
274 fun transfer_fp_sugars_interpretation fp_sugar lthy = |
340 let |
275 let |
341 val lthy = pred_injects fp_sugar lthy |
276 val lthy = register_pred_injects fp_sugar lthy |
342 val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar |
277 val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar |
343 in |
278 in |
344 lthy |
279 lthy |
345 |> Local_Theory.notes transfer_rules_notes |
280 |> Local_Theory.notes transfer_rules_notes |
346 |> snd |
281 |> snd |