diff -r 715ab84065a0 -r deb5be0115a7 Nominal/Lift.thy --- a/Nominal/Lift.thy Sat Aug 21 17:55:42 2010 +0800 +++ b/Nominal/Lift.thy Sat Aug 21 20:07:36 2010 +0800 @@ -18,49 +18,42 @@ end *} -(* Renames schematic variables in a theorem *) +(* Unrawifying schematic and bound variables *) + ML {* -fun rename_vars fnctn thm = +fun unraw_str s = + unsuffix "_raw" s + handle Fail _ => s + +fun unraw_vars_thm thm = let + fun unraw_var ((s, i), T) = ((unraw_str s, i), T) + val vars = Term.add_vars (prop_of thm) [] - val nvars = map (Var o ((apfst o apfst) fnctn)) vars + val nvars = map (Var o unraw_var) vars in Thm.certify_instantiate ([], (vars ~~ nvars)) thm end *} ML {* -fun un_raws name = +fun unraw_bounds_thm th = let - fun un_raw name = unprefix "_raw" name handle Fail _ => name - fun add_under names = hd names :: (map (prefix "_") (tl names)) + val trm = Thm.prop_of th + val trm' = Term.map_abs_vars unraw_str trm in - implode (map un_raw (add_under (space_explode "_" name))) + Thm.rename_boundvars trm trm' th end *} -(* Similar to Tools/IsaPlanner/rw_tools.ML *) -ML {* -fun rename_term_bvars (Abs(s, ty, t)) = (Abs(un_raws s, ty, rename_term_bvars t)) - | rename_term_bvars (a $ b) = (rename_term_bvars a) $ (rename_term_bvars b) - | rename_term_bvars x = x; - -fun rename_thm_bvars th = -let - val t = Thm.prop_of th -in - Thm.rename_boundvars t (rename_term_bvars t) th -end; -*} ML {* fun lift_thm qtys ctxt thm = -let - val un_raw_names = rename_vars un_raws -in - rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm)) -end + Quotient_Tacs.lifted qtys ctxt thm + |> unraw_bounds_thm + |> unraw_vars_thm *} + end