16 in |
16 in |
17 (qtys, ctxt') |
17 (qtys, ctxt') |
18 end |
18 end |
19 *} |
19 *} |
20 |
20 |
21 (* Renames schematic variables in a theorem *) |
21 (* Unrawifying schematic and bound variables *) |
|
22 |
22 ML {* |
23 ML {* |
23 fun rename_vars fnctn thm = |
24 fun unraw_str s = |
|
25 unsuffix "_raw" s |
|
26 handle Fail _ => s |
|
27 |
|
28 fun unraw_vars_thm thm = |
24 let |
29 let |
|
30 fun unraw_var ((s, i), T) = ((unraw_str s, i), T) |
|
31 |
25 val vars = Term.add_vars (prop_of thm) [] |
32 val vars = Term.add_vars (prop_of thm) [] |
26 val nvars = map (Var o ((apfst o apfst) fnctn)) vars |
33 val nvars = map (Var o unraw_var) vars |
27 in |
34 in |
28 Thm.certify_instantiate ([], (vars ~~ nvars)) thm |
35 Thm.certify_instantiate ([], (vars ~~ nvars)) thm |
29 end |
36 end |
30 *} |
37 *} |
31 |
38 |
32 ML {* |
39 ML {* |
33 fun un_raws name = |
40 fun unraw_bounds_thm th = |
34 let |
41 let |
35 fun un_raw name = unprefix "_raw" name handle Fail _ => name |
42 val trm = Thm.prop_of th |
36 fun add_under names = hd names :: (map (prefix "_") (tl names)) |
43 val trm' = Term.map_abs_vars unraw_str trm |
37 in |
44 in |
38 implode (map un_raw (add_under (space_explode "_" name))) |
45 Thm.rename_boundvars trm trm' th |
39 end |
46 end |
40 *} |
47 *} |
41 |
48 |
42 (* Similar to Tools/IsaPlanner/rw_tools.ML *) |
|
43 ML {* |
|
44 fun rename_term_bvars (Abs(s, ty, t)) = (Abs(un_raws s, ty, rename_term_bvars t)) |
|
45 | rename_term_bvars (a $ b) = (rename_term_bvars a) $ (rename_term_bvars b) |
|
46 | rename_term_bvars x = x; |
|
47 |
|
48 fun rename_thm_bvars th = |
|
49 let |
|
50 val t = Thm.prop_of th |
|
51 in |
|
52 Thm.rename_boundvars t (rename_term_bvars t) th |
|
53 end; |
|
54 *} |
|
55 |
49 |
56 ML {* |
50 ML {* |
57 fun lift_thm qtys ctxt thm = |
51 fun lift_thm qtys ctxt thm = |
58 let |
52 Quotient_Tacs.lifted qtys ctxt thm |
59 val un_raw_names = rename_vars un_raws |
53 |> unraw_bounds_thm |
60 in |
54 |> unraw_vars_thm |
61 rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm)) |
|
62 end |
|
63 *} |
55 *} |
|
56 |
64 |
57 |
65 end |
58 end |
66 |
59 |