rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user

--- a/src/HOL/Lifting.thy	Mon Feb 24 23:17:55 2014 +0000
+++ b/src/HOL/Lifting.thy	Tue Feb 25 15:02:19 2014 +0100
@@ -591,6 +591,21 @@
 
 subsection {* Domains *}
 
+lemma composed_equiv_rel_invariant:
+  assumes "left_unique R"
+  assumes "(R ===> op=) P P'"
+  assumes "Domainp R = P''"
+  shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
+using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def
+fun_eq_iff by blast
+
+lemma composed_equiv_rel_eq_invariant:
+  assumes "left_unique R"
+  assumes "Domainp R = P"
+  shows "(R OO op= OO R\<inverse>\<inverse>) = Lifting.invariant P"
+using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def invariant_def
+fun_eq_iff is_equality_def by metis
+
 lemma pcr_Domainp_par_left_total:
   assumes "Domainp B = P"
   assumes "left_total A"

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Feb 24 23:17:55 2014 +0000
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Feb 25 15:02:19 2014 +0100
@@ -443,10 +443,65 @@
       |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
   end
 
+local
+  val invariant_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
+    [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, 
+      @{thm pcr_Domainp}]
+in
 fun mk_readable_rsp_thm_eq tm lthy =
   let
     val ctm = cterm_of (Proof_Context.theory_of lthy) tm
     
+    (* This is not very cheap way of getting the rules but we have only few active
+      liftings in the current setting *)
+    fun get_cr_pcr_eqs ctxt =
+      let
+        fun collect (data : Lifting_Info.quotient) l =
+          if is_some (#pcr_info data) 
+          then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l) 
+          else l
+        val table = Lifting_Info.get_quotients ctxt
+      in
+        Symtab.fold (fn (_, data) => fn l => collect data l) table []
+      end
+
+    fun assms_rewr_conv tactic rule ct =
+      let
+        fun prove_extra_assms thm =
+          let
+            val assms = cprems_of thm
+            fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE
+            fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm))
+          in
+            map_interrupt prove assms
+          end
+    
+        fun cconl_of thm = Drule.strip_imp_concl (cprop_of thm)
+        fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
+        fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
+        val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
+        val lhs = lhs_of rule1;
+        val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
+        val rule3 =
+          Thm.instantiate (Thm.match (lhs, ct)) rule2
+            handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]);
+        val proved_assms = prove_extra_assms rule3
+      in
+        case proved_assms of
+          SOME proved_assms =>
+            let
+              val rule3 = proved_assms MRSL rule3
+              val rule4 =
+                if lhs_of rule3 aconvc ct then rule3
+                else
+                  let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
+                  in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end
+            in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end
+          | NONE => Conv.no_conv ct
+      end
+
+    fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules)
+
     fun simp_arrows_conv ctm =
       let
         val unfold_conv = Conv.rewrs_conv 
@@ -455,8 +510,13 @@
             @{thm fun_rel_eq_rel[THEN eq_reflection]}, 
             @{thm fun_rel_def[THEN eq_reflection]}]
         fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
+        val invariant_assms_tac_rules = @{thm left_unique_composition} :: 
+            invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
+        val invariant_assms_tac = (TRY o REPEAT_ALL_NEW (resolve_tac invariant_assms_tac_rules) 
+          THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
         val invariant_commute_conv = Conv.bottom_conv
-          (K (Conv.try_conv (Conv.rewrs_conv (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
+          (K (Conv.try_conv (assms_rewrs_conv invariant_assms_tac
+            (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
         val relator_eq_conv = Conv.bottom_conv
           (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
       in
@@ -467,8 +527,9 @@
       end
     
     val unfold_ret_val_invs = Conv.bottom_conv 
-      (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy 
-    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
+      (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
+    val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
+    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (cr_to_pcr_conv then_conv simp_arrows_conv))
     val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
     val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
     val beta_conv = Thm.beta_conversion true
@@ -477,6 +538,7 @@
   in
     Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   end
+end
 
 fun rename_to_tnames ctxt term =
   let

--- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Feb 24 23:17:55 2014 +0000
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Feb 25 15:02:19 2014 +0100
@@ -516,6 +516,11 @@
   #> relfexivity_rule_setup
   #> relator_distr_attribute_setup
 
+(* setup fixed invariant rules *)
+
+val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context}) 
+  [@{thm composed_equiv_rel_invariant}, @{thm composed_equiv_rel_eq_invariant}])
+
 (* outer syntax commands *)
 
 val _ =

--- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon Feb 24 23:17:55 2014 +0000
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Tue Feb 25 15:02:19 2014 +0100
@@ -447,16 +447,6 @@
    end
   
   fun rewrs_imp rules = first_imp (map rewr_imp rules)
-
-  fun map_interrupt f l =
-    let
-      fun map_interrupt' _ [] l = SOME (rev l)
-       | map_interrupt' f (x::xs) l = (case f x of
-        NONE => NONE
-        | SOME v => map_interrupt' f xs (v::l))
-    in
-      map_interrupt' f l []
-    end
 in
 
   (*

--- a/src/HOL/Tools/Lifting/lifting_util.ML	Mon Feb 24 23:17:55 2014 +0000
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Tue Feb 25 15:02:19 2014 +0100
@@ -31,6 +31,7 @@
   val relation_types: typ -> typ * typ
   val mk_HOL_eq: thm -> thm
   val safe_HOL_meta_eq: thm -> thm
+  val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option
 end
 
 
@@ -121,4 +122,14 @@
 
 fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
 
+fun map_interrupt f l =
+  let
+    fun map_interrupt' _ [] l = SOME (rev l)
+     | map_interrupt' f (x::xs) l = (case f x of
+      NONE => NONE
+      | SOME v => map_interrupt' f xs (v::l))
+  in
+    map_interrupt' f l []
+  end
+
 end

--- a/src/HOL/Tools/transfer.ML	Mon Feb 24 23:17:55 2014 +0000
+++ b/src/HOL/Tools/transfer.ML	Tue Feb 25 15:02:19 2014 +0100
@@ -25,10 +25,13 @@
   val transfer_raw_del: thm -> Context.generic -> Context.generic
   val transferred_attribute: thm list -> attribute
   val untransferred_attribute: thm list -> attribute
+  val prep_transfer_domain_thm: Proof.context -> thm -> thm
   val transfer_domain_add: attribute
   val transfer_domain_del: attribute
   val transfer_rule_of_term: Proof.context -> bool -> term -> thm
   val transfer_rule_of_lhs: Proof.context -> term -> thm
+  val eq_tac: Proof.context -> int -> tactic
+  val transfer_step_tac: Proof.context -> int -> tactic
   val transfer_tac: bool -> Proof.context -> int -> tactic
   val transfer_prover_tac: Proof.context -> int -> tactic
   val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
@@ -346,11 +349,14 @@
 
 (** Adding transfer domain rules **)
 
-fun add_transfer_domain_thm thm ctxt = 
-  (add_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
+fun prep_transfer_domain_thm ctxt thm = 
+  (abstract_equalities_domain ctxt o detect_transfer_rules) thm 
 
-fun del_transfer_domain_thm thm ctxt = 
-  (del_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
+fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o 
+  prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
+
+fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o 
+  prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
 
 (** Transfer proof method **)
 
@@ -571,7 +577,13 @@
       |> Thm.instantiate (map tinst binsts, map inst binsts)
   end
 
-fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq}
+fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) 
+  THEN_ALL_NEW rtac @{thm is_equality_eq}
+
+fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
+
+fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt)) 
+  THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
 
 fun transfer_tac equiv ctxt i =
   let
@@ -587,7 +599,7 @@
       rtac start_rule i THEN
       (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
         THEN_ALL_NEW
-          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))
+          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))
             ORELSE' end_tac)) (i + 1)
         handle TERM (_, ts) => raise TERM (err_msg, ts)
   in
@@ -612,7 +624,7 @@
        rtac @{thm transfer_prover_start} i,
        ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
         THEN_ALL_NEW
-         (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))) (i+1),
+         (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),
        rtac @{thm refl} i]
   end)
 
@@ -640,7 +652,7 @@
       (rtac rule
         THEN_ALL_NEW
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
-            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
+            THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
         handle TERM (_, ts) => raise TERM (err_msg, ts)
     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
     val tnames = map (fst o dest_TFree o snd) instT
@@ -676,7 +688,7 @@
       (rtac rule
         THEN_ALL_NEW
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
-            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
+            THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
         handle TERM (_, ts) => raise TERM (err_msg, ts)
     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
     val tnames = map (fst o dest_TFree o snd) instT