transfer package: more flexible handling of equality relations using is_equality predicate

--- a/src/HOL/Library/Mapping.thy	Wed Oct 24 17:40:56 2012 +0200
+++ b/src/HOL/Library/Mapping.thy	Wed Oct 24 18:43:25 2012 +0200
@@ -5,7 +5,7 @@
 header {* An abstract view on maps for code generation. *}
 
 theory Mapping
-imports Main
+imports Main Quotient_Option
 begin
 
 subsection {* Type definition and primitive operations *}
@@ -61,10 +61,8 @@
     | Some v \<Rightarrow> m (k \<mapsto> (f v)))" .
 
 lemma map_entry_code [code]: "map_entry k f m = (case lookup m k of None \<Rightarrow> m
-    | Some v \<Rightarrow> update k (f v) m)" 
-    apply (cases "lookup m k") 
-    apply simp_all 
-    by (transfer, simp)+
+    | Some v \<Rightarrow> update k (f v) m)"
+  by transfer rule
 
 definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
   "map_default k v f m = map_entry k f (default k v m)" 
@@ -274,4 +272,4 @@
 hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size
   replace default map_entry map_default tabulate bulkload map
 
-end
\ No newline at end of file
+end

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Oct 24 17:40:56 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Oct 24 18:43:25 2012 +0200
@@ -316,10 +316,8 @@
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
     fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) lthy'
-    val expand_rel_conv = Trueprop_conv (Conv.fun2_conv(top_rewr_conv (Transfer.get_sym_relator_eq lthy')))
     val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
-        |> Conv.fconv_rule expand_rel_conv
-     
+
     val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
     val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
 

--- a/src/HOL/Tools/transfer.ML	Wed Oct 24 17:40:56 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Wed Oct 24 18:43:25 2012 +0200
@@ -85,20 +85,6 @@
 
 fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm))
 
-val relator_eq_setup =
-  let
-    val name = @{binding relator_eq}
-    fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
-    fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
-    val add = Thm.declaration_attribute add_thm
-    val del = Thm.declaration_attribute del_thm
-    val text = "declaration of relator equality rule (used by transfer method)"
-    val content = Item_Net.content o #relator_eq o Data.get
-  in
-    Attrib.setup name (Attrib.add_del add del) text
-    #> Global_Theory.add_thms_dynamic (name, content)
-  end
-
 (** Conversions **)
 
 val Rel_rule = Thm.symmetric @{thm Rel_def}
@@ -125,22 +111,60 @@
       else_conv
       Conv.all_conv) ct
 
-(** Transfer proof method **)
+(** Replacing explicit equalities with is_equality premises **)
+
+fun mk_is_equality t =
+  Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
 
-fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y
-  | RelT t = raise TERM ("RelT", [t])
+val is_equality_lemma =
+  @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
+    by (unfold is_equality_def, rule, drule meta_spec,
+      erule meta_mp, rule refl, simp)}
 
-(* Tactic to correspond a value to itself *)
-fun eq_tac ctxt = SUBGOAL (fn (t, i) =>
+fun gen_abstract_equalities (dest : term -> term * (term -> term)) thm =
   let
-    val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t))
-    val cT = ctyp_of (Proof_Context.theory_of ctxt) T
-    val rews = get_sym_relator_eq ctxt
-    val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl}
-    val thm2 = Raw_Simplifier.rewrite_rule rews thm1
+    val thy = Thm.theory_of_thm thm
+    val prop = Thm.prop_of thm
+    val (t, mk_prop') = dest prop
+    val add_eqs = Term.fold_aterms
+      (fn t as Const (@{const_name HOL.eq}, _) => insert (op =) t | _ => I)
+    val eq_consts = rev (add_eqs t [])
+    val eqTs = map (snd o dest_Const) eq_consts
+    val used = Term.add_free_names prop []
+    val names = map (K "") eqTs |> Name.variant_list used
+    val frees = map Free (names ~~ eqTs)
+    val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
+    val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
+    val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
+    val cprop = Thm.cterm_of thy prop2
+    val equal_thm = Raw_Simplifier.rewrite false [is_equality_lemma] cprop
+    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   in
-    rtac thm2 i
-  end handle Match => no_tac | TERM _ => no_tac)
+    forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
+  end
+    handle TERM _ => thm
+
+fun abstract_equalities_transfer thm =
+  let
+    fun dest prop =
+      let
+        val prems = Logic.strip_imp_prems prop
+        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+        val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+      in
+        (rel, fn rel' =>
+          Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
+      end
+  in
+    gen_abstract_equalities dest thm
+  end
+
+fun abstract_equalities_relator_eq rel_eq_thm =
+  gen_abstract_equalities (fn x => (x, I))
+    (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
+
+
+(** Transfer proof method **)
 
 val post_simps =
   @{thms transfer_forall_eq [symmetric]
@@ -273,7 +297,7 @@
          (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
            THEN_ALL_NEW
              (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
-               ORELSE' eq_tac ctxt ORELSE' end_tac)) (i + 1)) i,
+               ORELSE' end_tac)) (i + 1)) i,
        (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
        rewrite_goal_tac post_simps i,
        rtac @{thm _} i]
@@ -289,8 +313,7 @@
       [CONVERSION prep_conv i,
        rtac @{thm transfer_prover_start} i,
        (rtac rule1 THEN_ALL_NEW
-         REPEAT_ALL_NEW
-           (resolve_tac rules ORELSE' eq_tac ctxt)) (i+1),
+         REPEAT_ALL_NEW (resolve_tac rules)) (i+1),
        rtac @{thm refl} i]
   end)
 
@@ -311,7 +334,7 @@
 
 (* Attribute for transfer rules *)
 
-val prep_rule = Conv.fconv_rule prep_conv
+val prep_rule = abstract_equalities_transfer o Conv.fconv_rule prep_conv
 
 val transfer_add =
   Thm.declaration_attribute (add_transfer_thm o prep_rule)
@@ -324,6 +347,22 @@
 
 (* Theory setup *)
 
+val relator_eq_setup =
+  let
+    val name = @{binding relator_eq}
+    fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
+      #> add_transfer_thm (abstract_equalities_relator_eq thm)
+    fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
+      #> del_transfer_thm (abstract_equalities_relator_eq thm)
+    val add = Thm.declaration_attribute add_thm
+    val del = Thm.declaration_attribute del_thm
+    val text = "declaration of relator equality rule (used by transfer method)"
+    val content = Item_Net.content o #relator_eq o Data.get
+  in
+    Attrib.setup name (Attrib.add_del add del) text
+    #> Global_Theory.add_thms_dynamic (name, content)
+  end
+
 val setup =
   relator_eq_setup
   #> Attrib.setup @{binding transfer_rule} transfer_attribute

--- a/src/HOL/Transfer.thy	Wed Oct 24 17:40:56 2012 +0200
+++ b/src/HOL/Transfer.thy	Wed Oct 24 18:43:25 2012 +0200
@@ -52,6 +52,11 @@
 definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   where "Rel r \<equiv> r"
 
+text {* Handling of equality relations *}
+
+definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+  where "is_equality R \<longleftrightarrow> R = (op =)"
+
 text {* Handling of meta-logic connectives *}
 
 definition transfer_forall where
@@ -98,6 +103,8 @@
 ML_file "Tools/transfer.ML"
 setup Transfer.setup
 
+declare refl [transfer_rule]
+
 declare fun_rel_eq [relator_eq]
 
 hide_const (open) Rel
@@ -172,6 +179,9 @@
 
 subsection {* Properties of relators *}
 
+lemma is_equality_eq [transfer_rule]: "is_equality (op =)"
+  unfolding is_equality_def by simp
+
 lemma right_total_eq [transfer_rule]: "right_total (op =)"
   unfolding right_total_def by simp