Modified transfer principle in HOL/NSA to cause less ho-unficiation

--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Oct 17 11:07:01 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Oct 17 15:23:06 2016 +0200
@@ -78,6 +78,28 @@
   "P \<equiv> eventually (\<lambda>n. Q) \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
   by (simp add: FreeUltrafilterNat.proper)
 
+text \<open>Standard principles that play a central role in the transfer tactic.\<close>
+definition
+  Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300) where
+  "Ifun f \<equiv> \<lambda>x. Abs_star
+       (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
+
+lemma Ifun_congruent2:
+  "congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})"
+by (auto simp add: congruent2_def equiv_starrel_iff elim!: eventually_rev_mp)
+
+lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
+by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
+    UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
+
+lemma transfer_Ifun:
+  "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
+by (simp only: Ifun_star_n)
+
+definition
+  star_of :: "'a \<Rightarrow> 'a star" where
+  "star_of x == star_n (\<lambda>n. x)"
+
 text \<open>Initialize transfer tactic.\<close>
 ML_file "transfer.ML"
 
@@ -155,47 +177,23 @@
 subsection \<open>Standard elements\<close>
 
 definition
-  star_of :: "'a \<Rightarrow> 'a star" where
-  "star_of x == star_n (\<lambda>n. x)"
-
-definition
   Standard :: "'a star set" where
   "Standard = range star_of"
 
 text \<open>Transfer tactic should remove occurrences of @{term star_of}\<close>
 setup \<open>Transfer_Principle.add_const @{const_name star_of}\<close>
 
-declare star_of_def [transfer_intro]
-
 lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
 by (transfer, rule refl)
 
 lemma Standard_star_of [simp]: "star_of x \<in> Standard"
 by (simp add: Standard_def)
 
-
 subsection \<open>Internal functions\<close>
 
-definition
-  Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300) where
-  "Ifun f \<equiv> \<lambda>x. Abs_star
-       (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
-
-lemma Ifun_congruent2:
-  "congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})"
-by (auto simp add: congruent2_def equiv_starrel_iff elim!: eventually_rev_mp)
-
-lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
-by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
-    UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
-
 text \<open>Transfer tactic should remove occurrences of @{term Ifun}\<close>
 setup \<open>Transfer_Principle.add_const @{const_name Ifun}\<close>
 
-lemma transfer_Ifun [transfer_intro]:
-  "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
-by (simp only: Ifun_star_n)
-
 lemma Ifun_star_of [simp]: "star_of f \<star> star_of x = star_of (f x)"
 by (transfer, rule refl)
 

--- a/src/HOL/Nonstandard_Analysis/transfer.ML	Mon Oct 17 11:07:01 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/transfer.ML	Mon Oct 17 15:23:06 2016 +0200
@@ -50,6 +50,25 @@
     unstar term
   end
 
+local exception MATCH
+in
+fun transfer_star_tac ctxt =
+  let
+    fun thm_of (Const (@{const_name Ifun}, _) $ t $ u) = @{thm transfer_Ifun} OF [thm_of t, thm_of u]
+    | thm_of (Const (@{const_name star_of}, _) $ _) = @{thm star_of_def}
+    | thm_of (Const (@{const_name star_n}, _) $ _) = @{thm Pure.reflexive}
+    | thm_of _ = raise MATCH;
+
+    fun thm_of_goal (Const (@{const_name Pure.eq}, _) $ t $ (Const (@{const_name star_n}, _) $ _)) =
+      thm_of t
+    | thm_of_goal _ = raise MATCH;
+  in
+    SUBGOAL (fn (t, i) =>
+      resolve_tac ctxt [thm_of_goal (strip_all_body t |> Logic.strip_imp_concl)] i
+      handle MATCH => no_tac)
+  end;
+end;
+
 fun transfer_thm_of ctxt ths t =
   let
     val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
@@ -58,12 +77,12 @@
     val unfolds' = map meta unfolds and refolds' = map meta refolds;
     val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t))
     val u = unstar_term consts t'
-    val tac =
+   val tac =
       rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
       ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
       match_tac ctxt [transitive_thm] 1 THEN
       resolve_tac ctxt [@{thm transfer_start}] 1 THEN
-      REPEAT_ALL_NEW (resolve_tac ctxt intros) 1 THEN
+      REPEAT_ALL_NEW (resolve_tac ctxt intros ORELSE' transfer_star_tac ctxt) 1 THEN
       match_tac ctxt [reflexive_thm] 1
   in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end