# HG changeset patch
# User huffman
# Date 1333715967 -7200
# Node ID 09c5160ba550a15d07ff80f86ccdc388ceacbbc5
# Parent  ee89d066579d12abfe2a6a09443c60f41c4e0c9b
more robust generation of quotient rules using tactics

diff -r ee89d066579d -r 09c5160ba550 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Apr 06 13:50:07 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Apr 06 14:39:27 2012 +0200
@@ -246,7 +246,8 @@
 fun lift_def_cmd (raw_var, rhs_raw) lthy =
   let
     val ((binding, SOME qty, mx), ctxt) = yield_singleton Proof_Context.read_vars raw_var lthy 
-    val rhs = (Syntax.check_term ctxt o Syntax.parse_term ctxt) rhs_raw
+    val rhs' = (Syntax.check_term ctxt o Syntax.parse_term ctxt) rhs_raw
+    val rhs = singleton (Variable.polymorphic ctxt) rhs'
  
     fun try_to_prove_refl thm = 
       let
@@ -263,7 +264,8 @@
           | _ => NONE
       end
 
-    val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty)
+    val quot_thm = Lifting_Term.prove_quot_theorem lthy (fastype_of rhs, qty)
+    val rsp_rel = Lifting_Term.quot_thm_rel quot_thm
     val rty_forced = (domain_type o fastype_of) rsp_rel;
     val forced_rhs = force_rty_type ctxt rty_forced rhs;
     val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
diff -r ee89d066579d -r 09c5160ba550 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Fri Apr 06 13:50:07 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Fri Apr 06 14:39:27 2012 +0200
@@ -31,28 +31,6 @@
 exception QUOT_THM_INTERNAL of Pretty.T
 exception QUOT_THM of typ * typ * Pretty.T
 
-(* matches a type pattern with a type *)
-fun match ctxt err ty_pat ty =
-  let
-    val thy = Proof_Context.theory_of ctxt
-  in
-    Sign.typ_match thy (ty_pat, ty) Vartab.empty
-      handle Type.TYPE_MATCH => err ctxt ty_pat ty
-  end
-
-fun equiv_match_err ctxt ty_pat ty =
-  let
-    val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
-    val ty_str = Syntax.string_of_typ ctxt ty
-  in
-    raise QUOT_THM_INTERNAL (Pretty.block
-      [Pretty.str ("The quotient type " ^ quote ty_str),
-       Pretty.brk 1,
-       Pretty.str ("and the quotient type pattern " ^ quote ty_pat_str),
-       Pretty.brk 1,
-       Pretty.str "don't match."])
-  end
-
 fun get_quot_thm ctxt s =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -77,12 +55,6 @@
        Pretty.str "found."]))
   end
 
-fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
-
-infix 0 MRSL
-
-fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
-
 exception NOT_IMPL of string
 
 fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
@@ -120,60 +92,58 @@
   else
     ()
 
-fun prove_quot_theorem' ctxt (rty, qty) =
-  (case (rty, qty) of
-    (Type (s, tys), Type (s', tys')) =>
+fun quotient_tac ctxt = SUBGOAL (fn (t, i) =>
+  let
+    val (_, abs, _, _) = dest_Quotient (HOLogic.dest_Trueprop t)
+    val (rty, qty) = Term.dest_funT (fastype_of abs)
+  in
+    case (rty, qty) of
+      (Type (s, _), Type (s', _)) =>
       if s = s'
       then
         let
-          val args = map (prove_quot_theorem' ctxt) (tys ~~ tys')
+          val thm1 = SOME @{thm identity_quotient}
+          val thm2 = try (get_rel_quot_thm ctxt) s
         in
-          if forall is_id_quot args
-          then
-            @{thm identity_quotient}
-          else
-            args MRSL (get_rel_quot_thm ctxt s)
+          resolve_tac (map_filter I [thm1, thm2]) i
         end
       else
         let
           val quot_thm = get_quot_thm ctxt s'
-          val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm
+          val (Type (rs, _), _) = quot_thm_rty_qty quot_thm
           val _ = check_raw_types (s, rs) s'
-          val qtyenv = match ctxt equiv_match_err qty_pat qty
-          val rtys' = map (Envir.subst_type qtyenv) rtys
-          val args = map (prove_quot_theorem' ctxt) (tys ~~ rtys')
         in
-          if forall is_id_quot args
-          then
-            quot_thm
-          else
-            let
-              val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
-            in
-              [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
-           end
+          resolve_tac [quot_thm, quot_thm RSN (2, @{thm Quotient_compose})] i
         end
-  | _ => @{thm identity_quotient})
+    | (_, Type (s, _)) =>
+      let
+        val thm1 = try (get_quot_thm ctxt) s
+        val thm2 = SOME @{thm identity_quotient}
+        val thm3 = try (get_rel_quot_thm ctxt) s
+      in
+        resolve_tac (map_filter I [thm1, thm2, thm3]) i
+      end
+  | _ => rtac @{thm identity_quotient} i
     handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg)
-
-fun force_qty_type thy qty quot_thm =
-  let
-    val abs_schematic = quot_thm_abs quot_thm 
-    val qty_schematic = (range_type o fastype_of) abs_schematic  
-    val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty
-    fun prep_ty thy (x, (S, ty)) =
-      (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
-    val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env []
-  in
-    Thm.instantiate (ty_inst, []) quot_thm
-  end
+  end)
 
 fun prove_quot_theorem ctxt (rty, qty) =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val quot_thm = prove_quot_theorem' ctxt (rty, qty)
+    val relT = [rty, rty] ---> HOLogic.boolT
+    val absT = rty --> qty
+    val repT = qty --> rty
+    val crT = [rty, qty] ---> HOLogic.boolT
+    val quotT = [relT, absT, repT, crT] ---> HOLogic.boolT
+    val rel = Var (("R", 0), relT)
+    val abs = Var (("Abs", 0), absT)
+    val rep = Var (("Rep", 0), repT)
+    val cr = Var (("T", 0), crT)
+    val quot = Const (@{const_name Quotient}, quotT)
+    val goal = HOLogic.Trueprop $ (quot $ rel $ abs $ rep $ cr)
+    val cgoal = Thm.cterm_of (Proof_Context.theory_of ctxt) goal
+    val tac = REPEAT (quotient_tac ctxt 1)
   in
-    force_qty_type thy qty quot_thm
+    Goal.prove_internal [] cgoal (K tac)
   end
 
 fun absrep_fun ctxt (rty, qty) =