1 theory Lift |
|
2 imports "../Nominal-General/Nominal2_Atoms" |
|
3 "../Nominal-General/Nominal2_Eqvt" |
|
4 "../Nominal-General/Nominal2_Supp" |
|
5 "Abs" "Perm" "Rsp" |
|
6 begin |
|
7 |
|
8 ML {* |
|
9 fun define_quotient_types binds tys alphas equivps ctxt = |
|
10 let |
|
11 fun def_ty ((b, ty), (alpha, equivp)) ctxt = |
|
12 Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt; |
|
13 val alpha_equivps = List.take (equivps, length alphas) |
|
14 val (qinfo, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt; |
|
15 val qtys = map #qtyp qinfo; |
|
16 in |
|
17 (qtys, ctxt') |
|
18 end |
|
19 *} |
|
20 |
|
21 (* Unrawifying schematic and bound variables *) |
|
22 |
|
23 ML {* |
|
24 fun unraw_str s = |
|
25 unsuffix "_raw" s |
|
26 handle Fail _ => s |
|
27 |
|
28 fun unraw_vars_thm thm = |
|
29 let |
|
30 fun unraw_var ((s, i), T) = ((unraw_str s, i), T) |
|
31 |
|
32 val vars = Term.add_vars (prop_of thm) [] |
|
33 val nvars = map (Var o unraw_var) vars |
|
34 in |
|
35 Thm.certify_instantiate ([], (vars ~~ nvars)) thm |
|
36 end |
|
37 *} |
|
38 |
|
39 ML {* |
|
40 fun unraw_bounds_thm th = |
|
41 let |
|
42 val trm = Thm.prop_of th |
|
43 val trm' = Term.map_abs_vars unraw_str trm |
|
44 in |
|
45 Thm.rename_boundvars trm trm' th |
|
46 end |
|
47 *} |
|
48 |
|
49 |
|
50 ML {* |
|
51 fun lift_thm qtys ctxt thm = |
|
52 Quotient_Tacs.lifted qtys ctxt thm |
|
53 |> unraw_bounds_thm |
|
54 |> unraw_vars_thm |
|
55 *} |
|
56 |
|
57 |
|
58 end |
|
59 |
|