# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1277703519 -7200
# Node ID 6cf28a1dfd75eca2c74e2e011265735c4c1f1408
# Parent  21ab339715cd800b1dd969a2bb1894c90c9119a8
Add reverse lifting flag to automated theorem derivation

diff -r 21ab339715cd -r 6cf28a1dfd75 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon Jun 28 07:32:51 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon Jun 28 07:38:39 2010 +0200
@@ -91,7 +91,7 @@
 fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
 let
   val rty = fastype_of rconst
-  val qty = derive_qtyp qtys rty ctxt
+  val qty = derive_qtyp qtys rty false ctxt
   val lhs = Free (qconst_name, qty)
 in
   quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
diff -r 21ab339715cd -r 6cf28a1dfd75 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Jun 28 07:32:51 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Jun 28 07:38:39 2010 +0200
@@ -649,7 +649,7 @@
      so we do it both in the original theorem *)
   val thm' = Drule.eta_contraction_rule thm
   val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt
-  val goal = derive_qtrm qtys (prop_of thm'') ctxt' 
+  val goal = derive_qtrm qtys (prop_of thm'') false ctxt'
 in
   Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
   |> singleton (ProofContext.export ctxt' ctxt)
diff -r 21ab339715cd -r 6cf28a1dfd75 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 07:32:51 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 07:38:39 2010 +0200
@@ -26,8 +26,8 @@
   val inj_repabs_trm: Proof.context -> term * term -> term
   val inj_repabs_trm_chk: Proof.context -> term * term -> term
 
-  val derive_qtyp: typ list -> typ -> Proof.context -> typ
-  val derive_qtrm: typ list -> term -> Proof.context -> term
+  val derive_qtyp: typ list -> typ -> bool -> Proof.context -> typ
+  val derive_qtrm: typ list -> term -> bool -> Proof.context -> term
 end;
 
 structure Quotient_Term: QUOTIENT_TERM =
@@ -690,7 +690,7 @@
 
 (*** Wrapper for automatically transforming an rthm into a qthm ***)
 
-(* subst_tys takes a list of (rty, qty) substitution pairs
+(* subst_rty takes a list of (rty, qty) substitution pairs
    and replaces all occurences of rty in the given type
    by an appropriate qty
 *)
@@ -711,7 +711,7 @@
       end 
   | _ => rty
 
-(* subst_trms takes a list of (rconst, qconst) substitution pairs,
+(* subst_rtrm takes a list of (rconst, qconst) substitution pairs,
    as well as (rty, qty) substitution pairs, and replaces all
    occurences of rconst and rty by appropriate instances of
    qconst and qty
@@ -739,24 +739,27 @@
 (* generates type substitutions out of the
    types involved in a quotient
 *)
-fun get_ty_subst qtys ctxt =
+fun get_ty_subst qtys reverse ctxt =
   Quotient_Info.quotdata_dest ctxt
    |> map (fn x => (#rtyp x, #qtyp x))
    |> filter (fn (_, qty) => member (op =) qtys qty)
+   |> map (fn (x, y) => if reverse then (y, x) else (x, y))
 
 (* generates term substitutions out of the qconst 
    definitions and relations in a quotient
 *)
-fun get_trm_subst qtys ctxt =
-let  
-  val subst_rtyp' = subst_rtyp ctxt (get_ty_subst qtys ctxt)
+fun get_trm_subst qtys reverse ctxt =
+let
+  val subst_rtyp' = subst_rtyp ctxt (get_ty_subst qtys reverse ctxt)
   fun proper (rt, qt) = (subst_rtyp' (fastype_of rt) = fastype_of qt)
-  
+
   val const_substs = 
     Quotient_Info.qconsts_dest ctxt
-     |> map (fn x => (#rconst x, #qconst x)) 
+     |> map (fn x => (#rconst x, #qconst x))
+     |> map (fn (x, y) => if reverse then (y, x) else (x, y))
 
-  val rel_substs = 
+  val rel_substs =
+    if reverse then [] else
     Quotient_Info.quotdata_dest ctxt
      |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
 in
@@ -766,11 +769,11 @@
 (* derives a qtyp and qtrm out of a rtyp and rtrm,
    respectively 
 *)
-fun derive_qtyp qtys rty ctxt =
-  subst_rtyp ctxt (get_ty_subst qtys ctxt) rty
+fun derive_qtyp qtys rty unlift ctxt =
+  subst_rtyp ctxt (get_ty_subst qtys unlift ctxt) rty
 
-fun derive_qtrm qtys rtrm ctxt =
-  subst_rtrm ctxt (get_ty_subst qtys ctxt) (get_trm_subst qtys ctxt) rtrm
+fun derive_qtrm qtys rtrm unlift ctxt =
+  subst_rtrm ctxt (get_ty_subst qtys unlift ctxt) (get_trm_subst qtys unlift ctxt) rtrm
 
 
 end; (* structure *)