author Simon Wimmer Mon, 17 Oct 2016 15:23:06 +0200 changeset 64270 bf474d719011 parent 64266 4699d3b3173e child 64271 912573107a2e
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"

+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>

-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"

-
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>

-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
```