# HG changeset patch
# User kuncar
# Date 1416323997 -3600
# Node ID 40c63ffce97f7bbb1d1597605d41dfc3d6e87e9b
# Parent  ef4f0b5b925e1d4e52c11a47fb9603300c0d6020
generalize prove_schematic_quot_thm

diff -r ef4f0b5b925e -r 40c63ffce97f src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Nov 18 16:19:51 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Nov 18 16:19:57 2014 +0100
@@ -289,7 +289,6 @@
       SOME (simplify_code_eq ctxt (unabs_def RS @{thm meta_eq_to_obj_eq}))
     else 
       let
-        val thy = Proof_Context.theory_of ctxt
         val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
         val rel_fun = prove_rel ctxt rsp_thm (rty, qty)
         val rep_abs_thm = [quot_thm, rel_fun] MRSL @{thm Quotient_rep_abs_eq}
diff -r ef4f0b5b925e -r 40c63ffce97f src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Tue Nov 18 16:19:51 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Tue Nov 18 16:19:57 2014 +0100
@@ -11,6 +11,13 @@
   exception MERGE_TRANSFER_REL of Pretty.T
   exception CHECK_RTY of typ * typ
 
+  type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
+  comp_lift: typ -> thm * 'a -> thm * 'a }
+
+  val force_qty_type: Proof.context -> typ -> thm -> thm
+
+  val prove_schematic_quot_thm: 'a fold_quot_thm -> Proof.context -> typ * typ -> 'a -> thm * 'a
+
   val instantiate_rtys: Proof.context -> typ * typ -> typ * typ
 
   val prove_quot_thm: Proof.context -> typ * typ -> thm
@@ -218,25 +225,34 @@
   end
   | instantiate_rtys _ _ = error "instantiate_rtys: not Type"
 
-fun prove_schematic_quot_thm ctxt (rty, qty) =
+type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
+  comp_lift: typ -> thm * 'a -> thm * 'a }
+
+fun prove_schematic_quot_thm actions ctxt (rty, qty) fold_val =
   let
     fun lifting_step (rty, qty) =
       let
         val (rty', rtyq) = instantiate_rtys ctxt (rty, qty)
         val (rty's, rtyqs) = if rty_is_TVar ctxt qty then ([rty'],[rtyq]) 
           else (Targs rty', Targs rtyq) 
-        val args = map (prove_schematic_quot_thm ctxt) (rty's ~~ rtyqs)
+        val (args, fold_val) = 
+          fold_map (prove_schematic_quot_thm actions ctxt) (rty's ~~ rtyqs) fold_val
       in
         if forall is_id_quot args
         then
-          get_quot_thm ctxt (Tname qty)
+          let
+            val quot_thm = get_quot_thm ctxt (Tname qty)
+          in
+            #lift actions qty (quot_thm, fold_val)
+          end
         else
           let
             val quot_thm = get_quot_thm ctxt (Tname qty)
             val rel_quot_thm = if rty_is_TVar ctxt qty then the_single args else
               args MRSL (get_rel_quot_thm ctxt (Tname rty))
+            val comp_quot_thm = [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
           in
-            [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
+            #comp_lift actions qty (comp_quot_thm, fold_val)
          end
       end
   in
@@ -245,13 +261,18 @@
         if s = s'
         then
           let
-            val args = map (prove_schematic_quot_thm ctxt) (zip_Tvars ctxt s tys tys')
+            val (args, fold_val) = 
+              fold_map (prove_schematic_quot_thm actions ctxt) (zip_Tvars ctxt s tys tys') fold_val
           in
             if forall is_id_quot args
             then
-              @{thm identity_quotient}
+              (@{thm identity_quotient}, fold_val)
             else
-              args MRSL (get_rel_quot_thm ctxt s)
+              let
+                val quot_thm = args MRSL (get_rel_quot_thm ctxt s)
+              in
+                #constr actions qty (quot_thm, fold_val)
+              end
           end
         else
           lifting_step (rty, qty)
@@ -267,9 +288,10 @@
             let                                               
               val rty_pat = Type (s', map (fn _ => TFree ("a",[])) tys')
             in
-              prove_schematic_quot_thm ctxt (rty_pat, qty)
+              prove_schematic_quot_thm actions ctxt (rty_pat, qty) fold_val
             end)
-      | _ => @{thm identity_quotient})
+      | _ => (@{thm identity_quotient}, fold_val)
+      )
   end
   handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg)
 
@@ -302,14 +324,19 @@
     qty, a representation type of the theorem is an instance of rty in general.
 *)
 
-fun prove_quot_thm ctxt (rty, qty) =
-  let
-    val schematic_quot_thm = prove_schematic_quot_thm ctxt (rty, qty)
+
+local
+  val id_actions = { constr = K I, lift = K I, comp_lift = K I }
+in
+  fun prove_quot_thm ctxt (rty, qty) =
+    let
+      val (schematic_quot_thm, _) = prove_schematic_quot_thm id_actions ctxt (rty, qty) ()
     val quot_thm = force_qty_type ctxt qty schematic_quot_thm
-    val _ = check_rty_type ctxt rty quot_thm
-  in
-    quot_thm
-  end
+      val _ = check_rty_type ctxt rty quot_thm
+    in
+      quot_thm
+    end
+end
 
 (*
   Computes the composed abstraction function for rty and qty.