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