5 Definitions of the raw fv, fv_bn and permute functions. |
5 Definitions of the raw fv, fv_bn and permute functions. |
6 *) |
6 *) |
7 |
7 |
8 signature NOMINAL_DT_RAWFUNS = |
8 signature NOMINAL_DT_RAWFUNS = |
9 sig |
9 sig |
10 (* info of raw datatypes *) |
|
11 type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list |
|
12 |
|
13 (* info of raw binding functions *) |
|
14 type bn_info = term * int * (int * term option) list list |
|
15 |
|
16 (* binding modes and binding clauses *) |
|
17 datatype bmode = Lst | Res | Set |
|
18 datatype bclause = BC of bmode * (term option * int) list * int list |
|
19 |
|
20 val get_all_binders: bclause list -> (term option * int) list |
10 val get_all_binders: bclause list -> (term option * int) list |
21 val is_recursive_binder: bclause -> bool |
11 val is_recursive_binder: bclause -> bool |
22 |
12 |
23 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
13 val define_raw_bns: raw_dt_info -> (binding * typ option * mixfix) list -> |
24 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
14 (Attrib.binding * term) list -> local_theory -> |
25 (term list * thm list * bn_info list * thm list * local_theory) |
15 (term list * thm list * bn_info list * thm list * local_theory) |
26 |
16 |
27 val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> |
17 val define_raw_fvs: raw_dt_info -> bn_info list -> bclause list list list -> |
28 thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
18 Proof.context -> term list * term list * thm list * thm list * local_theory |
29 |
19 |
30 val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> |
20 val define_raw_bn_perms: raw_dt_info -> bn_info list -> local_theory -> |
31 local_theory -> (term list * thm list * local_theory) |
21 (term list * thm list * local_theory) |
|
22 |
|
23 val define_raw_perms: raw_dt_info -> local_theory -> (term list * thm list * thm list) * local_theory |
32 |
24 |
33 val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list |
25 val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list |
34 |
26 |
35 val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm -> |
|
36 local_theory -> (term list * thm list * thm list) * local_theory |
|
37 end |
27 end |
38 |
28 |
39 |
29 |
40 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
30 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
41 struct |
31 struct |
42 |
32 |
43 open Nominal_Permeq |
33 open Nominal_Permeq |
44 |
|
45 (* string list - type variables of a datatype |
|
46 binding - name of the datatype |
|
47 mixfix - its mixfix |
|
48 (binding * typ list * mixfix) list - datatype constructors of the type |
|
49 *) |
|
50 type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list |
|
51 |
|
52 |
|
53 (* term - is constant of the bn-function |
|
54 int - is datatype number over which the bn-function is defined |
|
55 int * term option - is number of the corresponding argument with possibly |
|
56 recursive call with bn-function term |
|
57 *) |
|
58 type bn_info = term * int * (int * term option) list list |
|
59 |
|
60 |
|
61 datatype bmode = Lst | Res | Set |
|
62 datatype bclause = BC of bmode * (term option * int) list * int list |
|
63 |
34 |
64 fun get_all_binders bclauses = |
35 fun get_all_binders bclauses = |
65 bclauses |
36 bclauses |
66 |> map (fn (BC (_, binders, _)) => binders) |
37 |> map (fn (BC (_, binders, _)) => binders) |
67 |> flat |
38 |> flat |
134 |> AList.group (op=) (* eqs grouped according to bn_functions *) |
105 |> AList.group (op=) (* eqs grouped according to bn_functions *) |
135 |> map cntrs_order (* inner data ordered according to constructors *) |
106 |> map cntrs_order (* inner data ordered according to constructors *) |
136 |> order (op=) bn_funs (* ordered according to bn_functions *) |
107 |> order (op=) bn_funs (* ordered according to bn_functions *) |
137 end |
108 end |
138 |
109 |
139 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = |
110 fun define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs lthy = |
140 if null raw_bn_funs |
111 if null raw_bn_funs |
141 then ([], [], [], [], lthy) |
112 then ([], [], [], [], lthy) |
142 else |
113 else |
143 let |
114 let |
|
115 val RawDtInfo |
|
116 {raw_dt_names, raw_dts, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info |
|
117 |
144 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
118 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
145 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
119 Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy |
146 |
120 |
147 val (info, lthy2) = prove_termination_fun size_thms (Local_Theory.restore lthy1) |
121 val (info, lthy2) = prove_termination_fun raw_size_thms (Local_Theory.restore lthy1) |
148 val {fs, simps, inducts, ...} = info |
122 val {fs, simps, inducts, ...} = info |
149 |
123 |
150 val raw_bn_induct = (the inducts) |
124 val raw_bn_induct = (the inducts) |
151 val raw_bn_eqs = the simps |
125 val raw_bn_eqs = the simps |
152 |
126 |
153 val raw_bn_info = |
127 val raw_bn_info = |
154 prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs) |
128 prep_bn_info lthy raw_dt_names raw_dts fs (map prop_of raw_bn_eqs) |
155 in |
129 in |
156 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) |
130 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) |
157 end |
131 end |
158 |
132 |
159 |
133 |
268 val fv_bn_arg_tys = map (nth raw_tys) bn_tys |
246 val fv_bn_arg_tys = map (nth raw_tys) bn_tys |
269 val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys |
247 val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys |
270 val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) |
248 val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) |
271 val fv_bn_map = bns ~~ fv_bn_frees |
249 val fv_bn_map = bns ~~ fv_bn_frees |
272 |
250 |
273 val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss |
251 val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) raw_cns_info bclausesss |
274 val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info |
252 val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map raw_cns_info bclausesss) bn_info |
275 |
253 |
276 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
254 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
277 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
255 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
278 |
256 |
279 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
257 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
280 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
258 Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy |
281 |
259 |
282 val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy') |
260 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
283 |
261 |
284 val {fs, simps, inducts, ...} = info; |
262 val {fs, simps, inducts, ...} = info; |
285 |
263 |
286 val morphism = ProofContext.export_morphism lthy'' lthy |
264 val morphism = ProofContext.export_morphism lthy'' lthy |
287 val simps_exp = map (Morphism.thm morphism) (the simps) |
265 val simps_exp = map (Morphism.thm morphism) (the simps) |
323 val nth_cns_info = nth cns_info bn_n |
301 val nth_cns_info = nth cns_info bn_n |
324 in |
302 in |
325 map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info |
303 map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info |
326 end |
304 end |
327 |
305 |
328 fun define_raw_bn_perms raw_tys bn_info cns_info cns_thms size_thms lthy = |
306 fun define_raw_bn_perms raw_dt_info bn_info lthy = |
329 if null bn_info |
307 if null bn_info |
330 then ([], [], lthy) |
308 then ([], [], lthy) |
331 else |
309 else |
332 let |
310 let |
|
311 val RawDtInfo |
|
312 {raw_tys, raw_cns_info, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info |
|
313 |
333 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |
314 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |
334 val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns |
315 val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns |
335 val perm_bn_names = map (prefix "permute_") bn_names |
316 val perm_bn_names = map (prefix "permute_") bn_names |
336 val perm_bn_arg_tys = map (nth raw_tys) bn_tys |
317 val perm_bn_arg_tys = map (nth raw_tys) bn_tys |
337 val perm_bn_tys = map (fn ty => @{typ "perm"} --> ty --> ty) perm_bn_arg_tys |
318 val perm_bn_tys = map (fn ty => @{typ "perm"} --> ty --> ty) perm_bn_arg_tys |
338 val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys) |
319 val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys) |
339 val perm_bn_map = bns ~~ perm_bn_frees |
320 val perm_bn_map = bns ~~ perm_bn_frees |
340 |
321 |
341 val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map cns_info) bn_info |
322 val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map raw_cns_info) bn_info |
342 |
323 |
343 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names |
324 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names |
344 val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs) |
325 val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs) |
345 |
326 |
346 val prod_simps = @{thms prod.inject HOL.simp_thms} |
327 val prod_simps = @{thms prod.inject HOL.simp_thms} |
347 |
328 |
348 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
329 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
349 Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy |
330 Function_Common.default_config |
|
331 (pat_completeness_simp (prod_simps @ raw_inject_thms @ raw_distinct_thms)) lthy |
350 |
332 |
351 val (info, lthy'') = prove_termination_fun size_thms (Local_Theory.restore lthy') |
333 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
352 |
334 |
353 val {fs, simps, ...} = info; |
335 val {fs, simps, ...} = info; |
354 |
336 |
355 val morphism = ProofContext.export_morphism lthy'' lthy |
337 val morphism = ProofContext.export_morphism lthy'' lthy |
356 val simps_exp = map (Morphism.thm morphism) (the simps) |
338 val simps_exp = map (Morphism.thm morphism) (the simps) |
357 in |
339 in |
358 (fs, simps_exp, lthy'') |
340 (fs, simps_exp, lthy'') |
359 end |
341 end |
|
342 |
|
343 (*** raw permutation functions ***) |
|
344 |
|
345 (** proves the two pt-type class properties **) |
|
346 |
|
347 fun prove_permute_zero induct perm_defs perm_fns lthy = |
|
348 let |
|
349 val perm_types = map (body_type o fastype_of) perm_fns |
|
350 val perm_indnames = Datatype_Prop.make_tnames perm_types |
|
351 |
|
352 fun single_goal ((perm_fn, T), x) = |
|
353 HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
|
354 |
|
355 val goals = |
|
356 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
357 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
|
358 |
|
359 val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) |
|
360 |
|
361 val tac = (Datatype_Aux.indtac induct perm_indnames |
|
362 THEN_ALL_NEW asm_simp_tac simps) 1 |
|
363 in |
|
364 Goal.prove lthy perm_indnames [] goals (K tac) |
|
365 |> Datatype_Aux.split_conj_thm |
|
366 end |
|
367 |
|
368 |
|
369 fun prove_permute_plus induct perm_defs perm_fns lthy = |
|
370 let |
|
371 val p = Free ("p", @{typ perm}) |
|
372 val q = Free ("q", @{typ perm}) |
|
373 val perm_types = map (body_type o fastype_of) perm_fns |
|
374 val perm_indnames = Datatype_Prop.make_tnames perm_types |
|
375 |
|
376 fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq |
|
377 (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) |
|
378 |
|
379 val goals = |
|
380 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
381 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
|
382 |
|
383 val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) |
|
384 |
|
385 val tac = (Datatype_Aux.indtac induct perm_indnames |
|
386 THEN_ALL_NEW asm_simp_tac simps) 1 |
|
387 in |
|
388 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
|
389 |> Datatype_Aux.split_conj_thm |
|
390 end |
|
391 |
|
392 |
|
393 fun mk_perm_eq ty_perm_assoc cnstr = |
|
394 let |
|
395 fun lookup_perm p (ty, arg) = |
|
396 case (AList.lookup (op=) ty_perm_assoc ty) of |
|
397 SOME perm => perm $ p $ arg |
|
398 | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg |
|
399 |
|
400 val p = Free ("p", @{typ perm}) |
|
401 val (arg_tys, ty) = |
|
402 fastype_of cnstr |
|
403 |> strip_type |
|
404 |
|
405 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
|
406 val args = map Free (arg_names ~~ arg_tys) |
|
407 |
|
408 val lhs = lookup_perm p (ty, list_comb (cnstr, args)) |
|
409 val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) |
|
410 |
|
411 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
412 in |
|
413 (Attrib.empty_binding, eq) |
|
414 end |
|
415 |
|
416 |
|
417 fun define_raw_perms raw_dt_info lthy = |
|
418 let |
|
419 val RawDtInfo |
|
420 {raw_dt_names, raw_tys, raw_ty_args, raw_all_cns, raw_induct_thm, ...} = raw_dt_info |
|
421 |
|
422 val perm_fn_names = raw_dt_names |
|
423 |> map Long_Name.base_name |
|
424 |> map (prefix "permute_") |
|
425 |
|
426 val perm_fn_types = map perm_ty raw_tys |
|
427 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
|
428 val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names |
|
429 |
|
430 val perm_eqs = map (mk_perm_eq (raw_tys ~~ perm_fn_frees)) (flat raw_all_cns) |
|
431 |
|
432 fun tac _ (_, _, simps) = |
|
433 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
|
434 |
|
435 fun morphism phi (fvs, dfs, simps) = |
|
436 (map (Morphism.term phi) fvs, |
|
437 map (Morphism.thm phi) dfs, |
|
438 map (Morphism.thm phi) simps); |
|
439 |
|
440 val ((perm_funs, perm_eq_thms), lthy') = |
|
441 lthy |
|
442 |> Local_Theory.exit_global |
|
443 |> Class.instantiation (raw_dt_names, raw_ty_args, @{sort pt}) |
|
444 |> Primrec.add_primrec perm_fn_binds perm_eqs |
|
445 |
|
446 val perm_zero_thms = prove_permute_zero raw_induct_thm perm_eq_thms perm_funs lthy' |
|
447 val perm_plus_thms = prove_permute_plus raw_induct_thm perm_eq_thms perm_funs lthy' |
|
448 in |
|
449 lthy' |
|
450 |> Class.prove_instantiation_exit_result morphism tac |
|
451 (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) |
|
452 ||> Named_Target.theory_init |
|
453 end |
360 |
454 |
361 |
455 |
362 (** equivarance proofs **) |
456 (** equivarance proofs **) |
363 |
457 |
364 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} |
458 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} |
406 prove_eqvt_tac insts ind_thms const_names simps context) |
500 prove_eqvt_tac insts ind_thms const_names simps context) |
407 |> ProofContext.export ctxt'' ctxt |
501 |> ProofContext.export ctxt'' ctxt |
408 end |
502 end |
409 |
503 |
410 |
504 |
411 |
|
412 (*** raw permutation functions ***) |
|
413 |
|
414 (** proves the two pt-type class properties **) |
|
415 |
|
416 fun prove_permute_zero induct perm_defs perm_fns lthy = |
|
417 let |
|
418 val perm_types = map (body_type o fastype_of) perm_fns |
|
419 val perm_indnames = Datatype_Prop.make_tnames perm_types |
|
420 |
|
421 fun single_goal ((perm_fn, T), x) = |
|
422 HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
|
423 |
|
424 val goals = |
|
425 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
426 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
|
427 |
|
428 val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) |
|
429 |
|
430 val tac = (Datatype_Aux.indtac induct perm_indnames |
|
431 THEN_ALL_NEW asm_simp_tac simps) 1 |
|
432 in |
|
433 Goal.prove lthy perm_indnames [] goals (K tac) |
|
434 |> Datatype_Aux.split_conj_thm |
|
435 end |
|
436 |
|
437 |
|
438 fun prove_permute_plus induct perm_defs perm_fns lthy = |
|
439 let |
|
440 val p = Free ("p", @{typ perm}) |
|
441 val q = Free ("q", @{typ perm}) |
|
442 val perm_types = map (body_type o fastype_of) perm_fns |
|
443 val perm_indnames = Datatype_Prop.make_tnames perm_types |
|
444 |
|
445 fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq |
|
446 (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) |
|
447 |
|
448 val goals = |
|
449 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
450 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
|
451 |
|
452 val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) |
|
453 |
|
454 val tac = (Datatype_Aux.indtac induct perm_indnames |
|
455 THEN_ALL_NEW asm_simp_tac simps) 1 |
|
456 in |
|
457 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
|
458 |> Datatype_Aux.split_conj_thm |
|
459 end |
|
460 |
|
461 |
|
462 fun mk_perm_eq ty_perm_assoc cnstr = |
|
463 let |
|
464 fun lookup_perm p (ty, arg) = |
|
465 case (AList.lookup (op=) ty_perm_assoc ty) of |
|
466 SOME perm => perm $ p $ arg |
|
467 | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg |
|
468 |
|
469 val p = Free ("p", @{typ perm}) |
|
470 val (arg_tys, ty) = |
|
471 fastype_of cnstr |
|
472 |> strip_type |
|
473 |
|
474 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
|
475 val args = map Free (arg_names ~~ arg_tys) |
|
476 |
|
477 val lhs = lookup_perm p (ty, list_comb (cnstr, args)) |
|
478 val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) |
|
479 |
|
480 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
481 in |
|
482 (Attrib.empty_binding, eq) |
|
483 end |
|
484 |
|
485 |
|
486 fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy = |
|
487 let |
|
488 val perm_fn_names = full_ty_names |
|
489 |> map Long_Name.base_name |
|
490 |> map (prefix "permute_") |
|
491 |
|
492 val perm_fn_types = map perm_ty tys |
|
493 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
|
494 val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names |
|
495 |
|
496 val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs |
|
497 |
|
498 fun tac _ (_, _, simps) = |
|
499 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
|
500 |
|
501 fun morphism phi (fvs, dfs, simps) = |
|
502 (map (Morphism.term phi) fvs, |
|
503 map (Morphism.thm phi) dfs, |
|
504 map (Morphism.thm phi) simps); |
|
505 |
|
506 val ((perm_funs, perm_eq_thms), lthy') = |
|
507 lthy |
|
508 |> Local_Theory.exit_global |
|
509 |> Class.instantiation (full_ty_names, tvs, @{sort pt}) |
|
510 |> Primrec.add_primrec perm_fn_binds perm_eqs |
|
511 |
|
512 val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' |
|
513 val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' |
|
514 in |
|
515 lthy' |
|
516 |> Class.prove_instantiation_exit_result morphism tac |
|
517 (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) |
|
518 ||> Named_Target.theory_init |
|
519 end |
|
520 |
|
521 |
|
522 end (* structure *) |
505 end (* structure *) |
523 |
506 |