parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Nov 29 14:29:29 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Nov 29 17:54:20 2012 +0100
@@ -48,28 +48,28 @@
 
 fun define_pcrel crel lthy =
   let
-    val pcrel = Morphism.term (Local_Theory.target_morphism lthy) crel
-    val [crel_poly] = Variable.polymorphic lthy [pcrel]
-    val rty_raw = (domain_type o fastype_of) crel_poly
-    val (quot_thm, assms) = Lifting_Term.prove_param_quot_thm lthy rty_raw
-    val args = map (fn (_, q_thm) => quot_thm_crel q_thm) assms
-    val parametrized_relator = quot_thm_crel quot_thm
-    val [rty, rty'] = (binder_types o fastype_of) parametrized_relator
+    val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy
+    val [rty', qty] = (binder_types o fastype_of) fixed_crel
+    val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy rty'
+    val rty_raw = (domain_type o range_type o fastype_of) param_rel
     val thy = Proof_Context.theory_of lthy
     val tyenv_match = Sign.typ_match thy (rty_raw, rty') Vartab.empty
-    val crel_subst = Envir.subst_term (tyenv_match,Vartab.empty) crel_poly
-    val lthy = Variable.declare_names parametrized_relator lthy
-    val (crel_typed, lthy) = yield_singleton Variable.importT_terms crel_subst lthy
-    val qty = (domain_type o range_type o fastype_of) crel_typed
+    val param_rel_subst = Envir.subst_term (tyenv_match,Vartab.empty) param_rel
+    val args_subst = map (Envir.subst_term (tyenv_match,Vartab.empty)) args
+    val lthy = Variable.declare_names fixed_crel lthy
+    val (instT, lthy) = Variable.importT_inst (param_rel_subst :: args_subst) lthy
+    val args_fixed = (map (Term_Subst.instantiate (instT, []))) args_subst
+    val param_rel_fixed = Term_Subst.instantiate (instT, []) param_rel_subst
+    val rty = (domain_type o fastype_of) param_rel_fixed
     val relcomp_op = Const (@{const_name "relcompp"}, 
           (rty --> rty' --> HOLogic.boolT) --> 
           (rty' --> qty --> HOLogic.boolT) --> 
           rty --> qty --> HOLogic.boolT)
-    val relator_type = foldr1 (op -->) ((map type_of args) @ [rty, qty, HOLogic.boolT])
+    val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT])
     val qty_name = (fst o dest_Type) qty
     val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
-    val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args)
-    val rhs = relcomp_op $ parametrized_relator $ crel_typed
+    val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
+    val rhs = relcomp_op $ param_rel_fixed $ fixed_crel;
     val definition_term = Logic.mk_equals (lhs, rhs)
     val ((_, (_, def_thm)), lthy) = Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), 
       ((Binding.empty, []), definition_term)) lthy

--- a/src/HOL/Tools/Lifting/lifting_term.ML	Thu Nov 29 14:29:29 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Thu Nov 29 17:54:20 2012 +0100
@@ -16,7 +16,9 @@
 
   val equiv_relation: Proof.context -> typ * typ -> term
 
-  val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list
+  val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list * Proof.context
+
+  val generate_parametrized_relator: Proof.context -> typ -> term * term list
 end
 
 structure Lifting_Term: LIFTING_TERM =
@@ -238,14 +240,33 @@
 fun equiv_relation ctxt (rty, qty) =
   quot_thm_rel (prove_quot_thm ctxt (rty, qty))
 
-fun get_fresh_Q_t ctxt =
+val get_fresh_Q_t =
   let
-    val Q_t = Syntax.read_term ctxt "Trueprop (Quotient R Abs Rep T)"
-    val ctxt = Variable.declare_names Q_t ctxt
+    val Q_t = @{term "Trueprop (Quotient R Abs Rep T)"}
     val frees_Q_t = Term.add_free_names Q_t []
-    val (_, ctxt) = Variable.variant_fixes frees_Q_t ctxt
+    val tfrees_Q_t = rev (Term.add_tfree_names Q_t [])
   in
-    (Q_t, ctxt)
+    fn ctxt =>
+    let
+      fun rename_free_var tab (Free (name, typ)) = Free (the_default name (AList.lookup op= tab name),typ)
+        | rename_free_var _ t = t
+      
+      fun rename_free_vars tab = map_aterms (rename_free_var tab)
+      
+      fun rename_free_tvars tab =
+        map_types (map_type_tfree (fn (name, sort) => TFree (the_default name (AList.lookup op= tab name), sort)))
+      
+      val (new_frees_Q_t, ctxt) = Variable.variant_fixes frees_Q_t ctxt
+      val tab_frees = frees_Q_t ~~ new_frees_Q_t
+      
+      val (new_tfrees_Q_t, ctxt) = Variable.invent_types (replicate (length tfrees_Q_t) []) ctxt
+      val tab_tfrees = tfrees_Q_t ~~ (fst o split_list) new_tfrees_Q_t
+
+      val renamed_Q_t = rename_free_vars tab_frees Q_t
+      val renamed_Q_t = rename_free_tvars tab_tfrees renamed_Q_t
+    in
+      (renamed_Q_t, ctxt)
+    end
   end
 
 fun prove_param_quot_thm ctxt ty = 
@@ -265,7 +286,7 @@
         in
           (args MRSL (get_rel_quot_thm ctxt s), table_ctxt)
         end 
-      | generate (ty as (TVar _)) (table, ctxt) =
+      | generate (ty as (TFree _)) (table, ctxt) =
         if AList.defined (op=) table ty 
         then (the (AList.lookup (op=) table ty), (table, ctxt))
         else 
@@ -277,12 +298,23 @@
           in
             (Q_thm, (table', ctxt'))
           end
-      | generate _ _ = error "generate_param_quot_thm: TFree"
+      | generate _ _ = error "generate_param_quot_thm: TVar"
 
-    val (param_quot_thm, (table, _)) = generate ty ([], ctxt)
+    val (param_quot_thm, (table, ctxt)) = generate ty ([], ctxt)
   in
-    (param_quot_thm, rev table)
+    (param_quot_thm, rev table, ctxt)
   end
   handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg)
 
+fun generate_parametrized_relator ctxt ty =
+  let
+    val orig_ctxt = ctxt
+    val (quot_thm, table, ctxt) = prove_param_quot_thm ctxt ty
+    val parametrized_relator = quot_thm_crel quot_thm
+    val args = map (fn (_, q_thm) => quot_thm_crel q_thm) table
+    val exported_terms = Variable.exportT_terms ctxt orig_ctxt (parametrized_relator :: args)
+  in
+    (hd exported_terms, tl exported_terms)
+  end
+
 end;