equal
deleted
inserted
replaced
10 val qtype_defs: (string list * binding * mixfix) list -> typ list -> term list -> |
10 val qtype_defs: (string list * binding * mixfix) list -> typ list -> term list -> |
11 thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory |
11 thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory |
12 |
12 |
13 val qconst_defs: typ list -> (string * term * mixfix) list -> local_theory -> |
13 val qconst_defs: typ list -> (string * term * mixfix) list -> local_theory -> |
14 Quotient_Info.qconsts_info list * local_theory |
14 Quotient_Info.qconsts_info list * local_theory |
|
15 |
|
16 val qperm_defs: typ list -> string list -> (string * term * mixfix) list -> |
|
17 thm list -> theory -> theory |
15 end |
18 end |
16 |
19 |
17 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
20 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
18 struct |
21 struct |
19 |
22 |
36 in |
39 in |
37 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
40 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
38 end |
41 end |
39 |
42 |
40 |
43 |
|
44 (* defines the quotient permutations *) |
|
45 fun qperm_defs qtys full_tnames name_term_pairs thms thy = |
|
46 let |
|
47 val lthy = |
|
48 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
|
49 val (_, lthy') = qconst_defs qtys name_term_pairs lthy; |
|
50 val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; |
|
51 fun tac _ = |
|
52 Class.intro_classes_tac [] THEN |
|
53 (ALLGOALS (resolve_tac lifted_thms)) |
|
54 val lthy'' = Class.prove_instantiation_instance tac lthy' |
|
55 in |
|
56 Local_Theory.exit_global lthy'' |
|
57 end |
|
58 |
41 |
59 |
42 end (* structure *) |
60 end (* structure *) |
43 |
61 |