author | wenzelm |
Fri, 09 Aug 2019 17:14:49 +0200 | |
changeset 70494 | 41108e3e9ca5 |
parent 69597 | ff784d5a5bfb |
child 74381 | 79f484b0e35b |
permissions | -rw-r--r-- |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
2 |
Author: Martin Desharnais, TU Muenchen |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
3 |
Copyright 2014 |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
4 |
|
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
5 |
Parametricity of primitively (co)recursive functions. |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
6 |
*) |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
7 |
|
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
8 |
signature BNF_FP_REC_SUGAR_TRANSFER = |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
9 |
sig |
63801 | 10 |
val set_transfer_rule_attrs: thm list -> local_theory -> local_theory |
11 |
||
59281 | 12 |
val lfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context -> |
59276 | 13 |
Proof.context |
59281 | 14 |
val gfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context -> |
59276 | 15 |
Proof.context |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
16 |
end; |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
17 |
|
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
18 |
structure BNF_FP_Rec_Sugar_Transfer : BNF_FP_REC_SUGAR_TRANSFER = |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
19 |
struct |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
20 |
|
59276 | 21 |
open Ctr_Sugar_Util |
22 |
open Ctr_Sugar_Tactics |
|
59297 | 23 |
open BNF_Util |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
24 |
open BNF_Def |
59276 | 25 |
open BNF_FP_Util |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
26 |
open BNF_FP_Def_Sugar |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
27 |
open BNF_FP_Rec_Sugar_Util |
59281 | 28 |
open BNF_LFP_Rec_Sugar |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
29 |
|
59276 | 30 |
val transferN = "transfer"; |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
31 |
|
63801 | 32 |
val transfer_rule_attrs = @{attributes [transfer_rule]}; |
33 |
||
34 |
fun set_transfer_rule_attrs thms = |
|
35 |
snd o Local_Theory.notes [(Binding.empty_atts, [(thms, transfer_rule_attrs)])]; |
|
36 |
||
59281 | 37 |
fun mk_lfp_rec_sugar_transfer_tac ctxt def = |
59297 | 38 |
unfold_thms_tac ctxt [def] THEN HEADGOAL (Transfer.transfer_prover_tac ctxt); |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
39 |
|
59297 | 40 |
fun mk_gfp_rec_sugar_transfer_tac ctxt f_def corec_def type_definitions dtor_corec_transfers |
41 |
rel_pre_defs disc_eq_cases cases case_distribs case_congs = |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
42 |
let |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
43 |
fun instantiate_with_lambda thm = |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
44 |
let |
69597 | 45 |
val prop as \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, fT) $ _) $ _) = |
59297 | 46 |
Thm.prop_of thm; |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
47 |
val T = range_type fT; |
59276 | 48 |
val j = Term.maxidx_of_term prop + 1; |
49 |
val cond = Var (("x", j), HOLogic.boolT); |
|
50 |
val then_branch = Var (("t", j), T); |
|
51 |
val else_branch = Var (("e", j), T); |
|
59297 | 52 |
val lam = Term.lambda cond (mk_If cond then_branch else_branch); |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
53 |
in |
60784 | 54 |
infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt lam)] thm |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
55 |
end; |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
56 |
|
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
57 |
val transfer_rules = |
59297 | 58 |
@{thm Abs_transfer[OF type_definition_id_bnf_UNIV type_definition_id_bnf_UNIV]} :: |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
59 |
map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions @ |
63170 | 60 |
map (Local_Defs.unfold0 ctxt rel_pre_defs) dtor_corec_transfers; |
59276 | 61 |
val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add; |
62 |
val ctxt' = Context.proof_map (fold add_transfer_rule transfer_rules) ctxt; |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
63 |
|
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
64 |
val case_distribs = map instantiate_with_lambda case_distribs; |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
65 |
val simps = case_distribs @ disc_eq_cases @ cases @ @{thms if_True if_False}; |
59297 | 66 |
val ctxt'' = put_simpset (simpset_of (ss_only simps ctxt)) ctxt'; |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
67 |
in |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
68 |
unfold_thms_tac ctxt ([f_def, corec_def] @ @{thms split_beta if_conn}) THEN |
59297 | 69 |
HEADGOAL (simp_tac (fold Simplifier.add_cong case_congs ctxt'')) THEN |
70 |
HEADGOAL (Transfer.transfer_prover_tac ctxt') |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
71 |
end; |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
72 |
|
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
73 |
fun massage_simple_notes base = |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
74 |
filter_out (null o #2) |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
75 |
#> map (fn (thmN, thms, f_attrs) => |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
76 |
((Binding.qualify true base (Binding.name thmN), []), |
59297 | 77 |
map_index (fn (kk, thm) => ([thm], f_attrs kk)) thms)); |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
78 |
|
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
79 |
fun fp_sugar_of_bnf ctxt = fp_sugar_of ctxt o (fn Type (s, _) => s) o T_of_bnf; |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
80 |
|
59297 | 81 |
fun bnf_depth_first_traverse ctxt f T = |
59276 | 82 |
(case T of |
59297 | 83 |
Type (s, Ts) => |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
84 |
(case bnf_of ctxt s of |
59297 | 85 |
NONE => I |
86 |
| SOME bnf => fold (bnf_depth_first_traverse ctxt f) Ts o f bnf) |
|
87 |
| _ => I); |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
88 |
|
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
89 |
fun mk_goal lthy f = |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
90 |
let |
59276 | 91 |
val skematic_Ts = Term.add_tvarsT (fastype_of f) []; |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
92 |
|
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
93 |
val ((As, Bs), names_lthy) = lthy |
59297 | 94 |
|> mk_TFrees' (map snd skematic_Ts) |
95 |
||>> mk_TFrees' (map snd skematic_Ts); |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
96 |
|
63565
91f03f3b6470
made generation of transfer goals more robust w.r.t. dead variables
traytel
parents:
63170
diff
changeset
|
97 |
val ((Rs, Rs'), names_lthy) = mk_Frees' "R" (map2 mk_pred2T As Bs) names_lthy; |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
98 |
|
59276 | 99 |
val fA = Term.subst_TVars (map fst skematic_Ts ~~ As) f; |
100 |
val fB = Term.subst_TVars (map fst skematic_Ts ~~ Bs) f; |
|
63565
91f03f3b6470
made generation of transfer goals more robust w.r.t. dead variables
traytel
parents:
63170
diff
changeset
|
101 |
|
91f03f3b6470
made generation of transfer goals more robust w.r.t. dead variables
traytel
parents:
63170
diff
changeset
|
102 |
val goal = mk_parametricity_goal lthy Rs fA fB; |
91f03f3b6470
made generation of transfer goals more robust w.r.t. dead variables
traytel
parents:
63170
diff
changeset
|
103 |
val used_Rs = Term.add_frees goal []; |
91f03f3b6470
made generation of transfer goals more robust w.r.t. dead variables
traytel
parents:
63170
diff
changeset
|
104 |
val subst = map (dest_pred2T o snd) (filter_out (member (op =) used_Rs) Rs'); |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
105 |
in |
63565
91f03f3b6470
made generation of transfer goals more robust w.r.t. dead variables
traytel
parents:
63170
diff
changeset
|
106 |
(goal |> Term.subst_atomic_types subst, names_lthy) |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
107 |
end; |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
108 |
|
59297 | 109 |
fun fp_rec_sugar_transfer_interpretation prove {transfers, fun_names, funs, fun_defs, fpTs} = |
110 |
fold_index (fn (kk, (((transfer, fun_name), funx), fun_def)) => fn lthy => |
|
111 |
if transfer then |
|
112 |
(case try (map the) (map (fn Type (s, _) => bnf_of lthy s | _ => NONE) fpTs) of |
|
113 |
NONE => error "No transfer rule possible" |
|
114 |
| SOME bnfs => |
|
115 |
(case try (prove kk bnfs funx fun_def) lthy of |
|
116 |
NONE => error "Failed to prove transfer rule" |
|
117 |
| SOME thm => |
|
118 |
let |
|
119 |
val notes = [(transferN, [thm], K @{attributes [transfer_rule]})] |
|
120 |
|> massage_simple_notes fun_name; |
|
121 |
in |
|
122 |
snd (Local_Theory.notes notes lthy) |
|
123 |
end)) |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
124 |
else |
59297 | 125 |
lthy) |
126 |
(transfers ~~ fun_names ~~ funs ~~ fun_defs); |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
127 |
|
59281 | 128 |
val lfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation |
59276 | 129 |
(fn _ => fn _ => fn f => fn def => fn lthy => |
61334
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60784
diff
changeset
|
130 |
let |
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60784
diff
changeset
|
131 |
val (goal, _) = mk_goal lthy f; |
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60784
diff
changeset
|
132 |
val vars = Variable.add_free_names lthy goal []; |
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60784
diff
changeset
|
133 |
in |
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60784
diff
changeset
|
134 |
Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} => |
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60784
diff
changeset
|
135 |
mk_lfp_rec_sugar_transfer_tac ctxt def) |
70494 | 136 |
|> Thm.close_derivation \<^here> |
61334
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60784
diff
changeset
|
137 |
end); |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
138 |
|
59281 | 139 |
val gfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation |
59297 | 140 |
(fn kk => fn bnfs => fn f => fn def => fn lthy => |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
141 |
let |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
142 |
val fp_sugars = map (the o fp_sugar_of_bnf lthy) bnfs; |
61334
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60784
diff
changeset
|
143 |
val (goal, _) = mk_goal lthy f; |
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60784
diff
changeset
|
144 |
val vars = Variable.add_free_names lthy goal []; |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
145 |
val (disc_eq_cases, case_thms, case_distribs, case_congs) = |
59297 | 146 |
bnf_depth_first_traverse lthy (fn bnf => |
147 |
(case fp_sugar_of_bnf lthy bnf of |
|
148 |
NONE => I |
|
149 |
| SOME {fp_ctr_sugar = {ctr_sugar = {disc_eq_cases, case_thms, case_distribs, |
|
150 |
case_cong, ...}, ...}, ...} => |
|
151 |
(fn (disc_eq_cases0, case_thms0, case_distribs0, case_congs0) => |
|
152 |
(union Thm.eq_thm disc_eq_cases disc_eq_cases0, |
|
153 |
union Thm.eq_thm case_thms case_thms0, |
|
154 |
union Thm.eq_thm case_distribs case_distribs0, |
|
155 |
insert Thm.eq_thm case_cong case_congs0)))) |
|
156 |
(fastype_of f) ([], [], [], []); |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
157 |
in |
61334
8d40ddaa427f
collect the names from goals in favor of fragile exports
traytel
parents:
60784
diff
changeset
|
158 |
Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} => |
59297 | 159 |
mk_gfp_rec_sugar_transfer_tac ctxt def |
63859
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
63801
diff
changeset
|
160 |
(#co_rec_def (the (#fp_co_induct_sugar (nth fp_sugars kk)))) |
63801 | 161 |
(map (#type_definition o #absT_info) fp_sugars) |
162 |
(maps (#xtor_co_rec_transfers o #fp_res) fp_sugars) |
|
163 |
(map (rel_def_of_bnf o #pre_bnf) fp_sugars) |
|
164 |
disc_eq_cases case_thms case_distribs case_congs) |
|
70494 | 165 |
|> Thm.close_derivation \<^here> |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
166 |
end); |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
diff
changeset
|
167 |
|
61348
d7215449be83
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
blanchet
parents:
61334
diff
changeset
|
168 |
val _ = Theory.setup (lfp_rec_sugar_interpretation transfer_plugin |
59281 | 169 |
lfp_rec_sugar_transfer_interpretation); |
59276 | 170 |
|
171 |
end; |