1 theory Lift |
1 theory Lift |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" |
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 fun lift_thm ctxt thm = |
6 fun rename_vars fnctn thm = |
|
7 let |
|
8 val vars = Term.add_vars (prop_of thm) [] |
|
9 val nvars = map (Var o ((apfst o apfst) fnctn)) vars |
|
10 in |
|
11 Thm.certify_instantiate ([], (vars ~~ nvars)) thm |
|
12 end |
|
13 *} |
|
14 |
|
15 ML {* |
|
16 fun un_raws name = |
7 let |
17 let |
8 fun un_raw name = unprefix "_raw" name handle Fail _ => name |
18 fun un_raw name = unprefix "_raw" name handle Fail _ => name |
9 fun add_under names = hd names :: (map (prefix "_") (tl names)) |
19 fun add_under names = hd names :: (map (prefix "_") (tl names)) |
10 fun un_raws name = implode (map un_raw (add_under (space_explode "_" name))) |
20 in |
|
21 implode (map un_raw (add_under (space_explode "_" name))) |
|
22 end |
|
23 *} |
|
24 |
|
25 (* Similar to Tools/IsaPlanner/rw_tools.ML *) |
|
26 ML {* |
|
27 fun rename_term_bvars (Abs(s, ty, t)) = (Abs(un_raws s, ty, rename_term_bvars t)) |
|
28 | rename_term_bvars (a $ b) = (rename_term_bvars a) $ (rename_term_bvars b) |
|
29 | rename_term_bvars x = x; |
|
30 |
|
31 fun rename_thm_bvars th = |
|
32 let |
|
33 val t = Thm.prop_of th |
|
34 in |
|
35 Thm.rename_boundvars t (rename_term_bvars t) th |
|
36 end; |
|
37 *} |
|
38 |
|
39 ML {* |
|
40 fun lift_thm ctxt thm = |
|
41 let |
11 val un_raw_names = rename_vars un_raws |
42 val un_raw_names = rename_vars un_raws |
12 in |
43 in |
13 un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))) |
44 rename_thm_bvars (un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))) |
14 end |
45 end |
15 *} |
46 *} |
16 |
47 |
17 ML {* |
48 ML {* |
18 fun quotient_lift_consts_export spec ctxt = |
49 fun quotient_lift_consts_export spec ctxt = |