equal
deleted
inserted
replaced
4 |
4 |
5 ML {* |
5 ML {* |
6 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) |
6 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) |
7 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
7 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
8 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
8 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
|
9 *} |
|
10 |
|
11 ML {* |
|
12 fun quotient_lift_consts_export qtys spec ctxt = |
|
13 let |
|
14 val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |
|
15 val (ts_loc, defs_loc) = split_list result; |
|
16 val morphism = ProofContext.export_morphism ctxt' ctxt; |
|
17 val ts = map (Morphism.term morphism) ts_loc |
|
18 val defs = Morphism.fact morphism defs_loc |
|
19 in |
|
20 (ts, defs, ctxt') |
|
21 end |
9 *} |
22 *} |
10 |
23 |
11 ML {* |
24 ML {* |
12 fun prove_perm_empty lthy induct perm_def perm_frees = |
25 fun prove_perm_empty lthy induct perm_def perm_frees = |
13 let |
26 let |
116 end |
129 end |
117 |
130 |
118 *} |
131 *} |
119 |
132 |
120 ML {* |
133 ML {* |
121 fun define_lifted_perms full_tnames name_term_pairs thms thy = |
134 fun define_lifted_perms qtys full_tnames name_term_pairs thms thy = |
122 let |
135 let |
123 val lthy = |
136 val lthy = |
124 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
137 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
125 val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy |
138 val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy; |
126 val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) thms |
139 val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; |
127 fun tac _ = |
140 fun tac _ = |
128 Class.intro_classes_tac [] THEN |
141 Class.intro_classes_tac [] THEN |
129 (ALLGOALS (resolve_tac lifted_thms)) |
142 (ALLGOALS (resolve_tac lifted_thms)) |
130 val lthy'' = Class.prove_instantiation_instance tac lthy' |
143 val lthy'' = Class.prove_instantiation_instance tac lthy' |
131 in |
144 in |