23 |
23 |
24 val setify: Proof.context -> term -> term |
24 val setify: Proof.context -> term -> term |
25 val listify: Proof.context -> term -> term |
25 val listify: Proof.context -> term -> term |
26 |
26 |
27 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
27 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
28 bclause list list list -> thm list -> Proof.context -> term list * term list * thm list * local_theory |
28 bclause list list list -> thm list -> Proof.context -> |
|
29 term list * term list * thm list * thm list * local_theory |
|
30 |
|
31 val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list |
29 end |
32 end |
30 |
33 |
31 |
34 |
32 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
35 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
33 struct |
36 struct |
226 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
229 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
227 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
230 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
228 |
231 |
229 val (info, lthy'') = prove_termination (Local_Theory.restore lthy') |
232 val (info, lthy'') = prove_termination (Local_Theory.restore lthy') |
230 |
233 |
231 val {fs, simps, ...} = info; |
234 val {fs, simps, inducts, ...} = info; |
232 |
235 |
233 val morphism = ProofContext.export_morphism lthy'' lthy |
236 val morphism = ProofContext.export_morphism lthy'' lthy |
234 val fs_exp = map (Morphism.term morphism) fs |
237 val fs_exp = map (Morphism.term morphism) fs |
235 |
238 |
236 val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp |
239 val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp |
237 val simps_exp = Morphism.fact morphism (the simps) |
240 val simps_exp = map (Morphism.thm morphism) (the simps) |
238 in |
241 val fv_bns_inducts_exp = map (Morphism.thm morphism) (the inducts) |
239 (fv_frees_exp, fv_bns_exp, simps_exp, lthy'') |
242 in |
|
243 (fv_frees_exp, fv_bns_exp, simps_exp, fv_bns_inducts_exp, lthy'') |
|
244 end |
|
245 |
|
246 |
|
247 (** equivarance proofs **) |
|
248 |
|
249 fun mk_eqvt_goal pi const arg = |
|
250 let |
|
251 val lhs = mk_perm pi (const $ arg) |
|
252 val rhs = const $ (mk_perm pi arg) |
|
253 in |
|
254 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
255 end |
|
256 |
|
257 fun raw_prove_eqvt consts ind_thms simps ctxt = |
|
258 let |
|
259 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
|
260 val p = Free (p, @{typ perm}) |
|
261 val arg_tys = |
|
262 consts |
|
263 |> map fastype_of |
|
264 |> map domain_type |
|
265 val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt' |
|
266 val args = map Free (arg_names ~~ arg_tys) |
|
267 val goals = map2 (mk_eqvt_goal p) consts args |
|
268 val insts = map (single o SOME) arg_names |
|
269 val const_names = map (fst o dest_Const) consts |
|
270 fun tac ctxt = |
|
271 Object_Logic.full_atomize_tac |
|
272 THEN' InductTacs.induct_rules_tac ctxt insts ind_thms |
|
273 THEN_ALL_NEW |
|
274 (asm_full_simp_tac (HOL_basic_ss addsimps simps) |
|
275 THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names |
|
276 THEN' asm_simp_tac HOL_basic_ss) |
|
277 in |
|
278 Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) |
|
279 |> ProofContext.export ctxt'' ctxt |
240 end |
280 end |
241 |
281 |
242 end (* structure *) |
282 end (* structure *) |
243 |
283 |