--- a/Nominal/Lift.thy Sat Aug 21 20:07:36 2010 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-theory Lift
-imports "../Nominal-General/Nominal2_Atoms"
- "../Nominal-General/Nominal2_Eqvt"
- "../Nominal-General/Nominal2_Supp"
- "Abs" "Perm" "Rsp"
-begin
-
-ML {*
-fun define_quotient_types binds tys alphas equivps ctxt =
-let
- fun def_ty ((b, ty), (alpha, equivp)) ctxt =
- Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt;
- val alpha_equivps = List.take (equivps, length alphas)
- val (qinfo, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt;
- val qtys = map #qtyp qinfo;
-in
- (qtys, ctxt')
-end
-*}
-
-(* Unrawifying schematic and bound variables *)
-
-ML {*
-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 unraw_var) vars
-in
- Thm.certify_instantiate ([], (vars ~~ nvars)) thm
-end
-*}
-
-ML {*
-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
-*}
-
-
-ML {*
-fun lift_thm qtys ctxt thm =
- Quotient_Tacs.lifted qtys ctxt thm
- |> unraw_bounds_thm
- |> unraw_vars_thm
-*}
-
-
-end
-