# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282392456 -28800
# Node ID deb5be0115a7ff483d682e7dddf83fee01446800
# Parent  715ab84065a077b2a2743164b43696478e84bd5b
moved lifting code from Lift.thy to nominal_dt_quot.ML

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
 
diff -r 715ab84065a0 -r deb5be0115a7 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sat Aug 21 17:55:42 2010 +0800
+++ b/Nominal/NewParser.thy	Sat Aug 21 20:07:36 2010 +0800
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "Tacs" "Lift" "Equivp"
+        "Perm" "Tacs" "Equivp"
 begin
 
 (* TODO
diff -r 715ab84065a0 -r deb5be0115a7 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Sat Aug 21 17:55:42 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Sat Aug 21 20:07:36 2010 +0800
@@ -2,7 +2,7 @@
     Author:     Christian Urban
     Author:     Cezary Kaliszyk
 
-  Performing quotient constructions
+  Performing quotient constructions and lifting theorems
 *)
 
 signature NOMINAL_DT_QUOT =
@@ -18,6 +18,8 @@
 
   val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> 
     local_theory -> local_theory
+
+  val lift_thm: typ list -> Proof.context -> thm -> thm
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -79,5 +81,36 @@
   |> Named_Target.theory_init
 end
 
+
+(* lifts a theorem and deletes all "_raw" suffixes *)
+
+fun unraw_str s = 
+  unsuffix "_raw" s
+  handle Fail _ => s
+
+fun unraw_vars_thm thm =
+let
+  fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
+
+  val vars = Term.add_vars (prop_of thm) []
+  val vars' = map (Var o unraw_var_str) vars
+in
+  Thm.certify_instantiate ([], (vars ~~ vars')) thm
+end
+
+fun unraw_bounds_thm th =
+let
+  val trm = Thm.prop_of th
+  val trm' = Term.map_abs_vars unraw_str trm
+in
+  Thm.rename_boundvars trm trm' th
+end
+
+fun lift_thm qtys ctxt thm =
+  Quotient_Tacs.lifted qtys ctxt thm
+  |> unraw_bounds_thm
+  |> unraw_vars_thm
+
+
 end (* structure *)