equal
deleted
inserted
replaced
37 end |
37 end |
38 |
38 |
39 |
39 |
40 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
40 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
41 struct |
41 struct |
|
42 |
|
43 open Nominal_Permeq |
42 |
44 |
43 (* string list - type variables of a datatype |
45 (* string list - type variables of a datatype |
44 binding - name of the datatype |
46 binding - name of the datatype |
45 mixfix - its mixfix |
47 mixfix - its mixfix |
46 (binding * typ list * mixfix) list - datatype constructors of the type |
48 (binding * typ list * mixfix) list - datatype constructors of the type |
359 |
361 |
360 fun subproof_tac const_names simps = |
362 fun subproof_tac const_names simps = |
361 SUBPROOF (fn {prems, context, ...} => |
363 SUBPROOF (fn {prems, context, ...} => |
362 HEADGOAL |
364 HEADGOAL |
363 (simp_tac (HOL_basic_ss addsimps simps) |
365 (simp_tac (HOL_basic_ss addsimps simps) |
364 THEN' Nominal_Permeq.eqvt_tac context [] const_names |
366 THEN' eqvt_tac context (eqvt_relaxed_config addexcls const_names) |
365 THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym])))) |
367 THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym])))) |
366 |
368 |
367 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
369 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
368 HEADGOAL |
370 HEADGOAL |
369 (Object_Logic.full_atomize_tac |
371 (Object_Logic.full_atomize_tac |