# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265357209 -3600
# Node ID 8d4d52f51e0d52c5ad0d132f8a1aff7410d32d39
# Parent  96651cddeba9a67f3c59543a121b6963e0d0e26b# Parent  3664eafcad0940fee8e5d38bb6813ba571d418a4
merged

diff -r 96651cddeba9 -r 8d4d52f51e0d Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Fri Feb 05 09:06:27 2010 +0100
+++ b/Quot/quotient_info.ML	Fri Feb 05 09:06:49 2010 +0100
@@ -23,6 +23,7 @@
   val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
   val quotdata_update_thy: string -> quotdata_info -> theory -> theory
   val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
+  val quotdata_dest: Proof.context -> quotdata_info list
   val print_quotinfo: Proof.context -> unit
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
@@ -166,6 +167,9 @@
 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
 
+fun quotdata_dest lthy =
+  map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))
+
 fun print_quotinfo ctxt =
 let
   fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = 
diff -r 96651cddeba9 -r 8d4d52f51e0d Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Feb 05 09:06:27 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Feb 05 09:06:49 2010 +0100
@@ -25,6 +25,8 @@
 
   val inj_repabs_trm: Proof.context -> term * term -> term
   val inj_repabs_trm_chk: Proof.context -> term * term -> term
+
+  val quotient_lift_all: Proof.context -> term -> term
 end;
 
 structure Quotient_Term: QUOTIENT_TERM =
@@ -681,6 +683,48 @@
   inj_repabs_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
 
+(* Finds subterms of a term that are lifted to constants and replaces
+   those as well as occurrences of the equivalence relation and replaces
+   those by equality.
+   Currently types are not checked so because of the dummyTs it may
+   not be complete *)
+fun quotient_lift_all ctxt t =
+let
+  val thy = ProofContext.theory_of ctxt
+  val const_infos = Quotient_Info.qconsts_dest ctxt
+  val rel_infos = Quotient_Info.quotdata_dest ctxt
+  fun treat_const_info t qc_info s =
+    if s <> NONE then s else
+      case try (Pattern.match thy (t, #rconst qc_info)) (Vartab.empty, Vartab.empty) of
+        SOME inst => SOME (Envir.subst_term inst (#qconst qc_info))
+      | NONE => NONE;
+  fun treat_const t = fold (treat_const_info t) const_infos NONE
+  fun treat_rel_info t rel_info s =
+    if s <> NONE then s else
+    if Pattern.matches thy (t, #equiv_rel rel_info) then SOME (Const ("op =", dummyT))
+    else NONE
+  fun treat_rel t = fold (treat_rel_info t) rel_infos NONE
+  fun lift_aux t =
+    case treat_const t of
+      SOME x => x
+    | NONE =>
+      (case treat_rel t of
+        SOME x => x
+      | NONE =>
+        (case t of
+          a $ b => lift_aux a $ lift_aux b
+        | Abs(a, T, s) =>
+            let val (y, s') = Term.dest_abs (a, T, s) in
+            Abs(y, dummyT, abstract_over (Free (y, dummyT), (lift_aux s')))
+            end
+        | Free(n, _) => Free(n, dummyT)
+        | Var(n, _) => Var(n, dummyT)
+        | Bound i => Bound i
+        | Const(s, _) => Const(s, dummyT)))
+in
+  lift_aux t
+end
+
 end; (* structure *)