# HG changeset patch
# User wenzelm
# Date 1565259507 -7200
# Node ID 8cac53925407f363974180a0fa8d272bdb2a43c4
# Parent  c42a0a0a9a8d97feca4f4c4ba3b7129e27f3bda1
prefer named lemmas -- more compact proofterms;

diff -r c42a0a0a9a8d -r 8cac53925407 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Thu Aug 08 12:11:40 2019 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Thu Aug 08 12:18:27 2019 +0200
@@ -237,11 +237,6 @@
 fun mk_is_equality t =
   Const (\<^const_name>\<open>is_equality\<close>, Term.fastype_of t --> HOLogic.boolT) $ t
 
-val is_equality_lemma =
-  @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (=))"
-    by (unfold is_equality_def, rule, drule meta_spec,
-      erule meta_mp, rule refl, simp)}
-
 fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
   let
     val prop = Thm.prop_of thm
@@ -260,7 +255,7 @@
     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 ctxt prop2
-    val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
+    val equal_thm = Raw_Simplifier.rewrite ctxt false @{thms is_equality_lemma} cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
@@ -313,11 +308,6 @@
 fun mk_Domainp_assm (T, R) =
   HOLogic.mk_eq ((Const (\<^const_name>\<open>Domainp\<close>, Term.fastype_of T --> Term.fastype_of R) $ T), R)
 
-val Domainp_lemma =
-  @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
-    by (rule, drule meta_spec,
-      erule meta_mp, rule refl, simp)}
-
 fun fold_Domainp f (t as Const (\<^const_name>\<open>Domainp\<close>,_) $ (Var (_,_))) = f t
   | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
   | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
@@ -352,7 +342,7 @@
     val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
     val prop2 = Logic.list_rename_params (rev names) prop1
     val cprop = Thm.cterm_of ctxt prop2
-    val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
+    val equal_thm = Raw_Simplifier.rewrite ctxt false @{thms Domainp_lemma} cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
diff -r c42a0a0a9a8d -r 8cac53925407 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Thu Aug 08 12:11:40 2019 +0200
+++ b/src/HOL/Transfer.thy	Thu Aug 08 12:18:27 2019 +0200
@@ -229,6 +229,22 @@
 end
 
 
+lemma is_equality_lemma: "(\<And>R. is_equality R \<Longrightarrow> PROP (P R)) \<equiv> PROP (P (=))"
+  apply (unfold is_equality_def)
+  apply (rule equal_intr_rule)
+   apply (drule meta_spec)
+   apply (erule meta_mp)
+   apply (rule refl)
+  apply simp
+  done
+
+lemma Domainp_lemma: "(\<And>R. Domainp T = R \<Longrightarrow> PROP (P R)) \<equiv> PROP (P (Domainp T))"
+  apply (rule equal_intr_rule)
+   apply (drule meta_spec)
+   apply (erule meta_mp)
+   apply (rule refl)
+  apply simp
+  done
 
 ML_file \<open>Tools/Transfer/transfer.ML\<close>
 declare refl [transfer_rule]