# HG changeset patch
# User huffman
# Date 1166553275 -3600
# Node ID b1137bd730128da7ba31bbd23ea4fd4ba9618316
# Parent  f1790ca921e14ca22fcb0f5a9daf26cf64d009a7
add lemmas Standard_starfun(2)_iff

diff -r f1790ca921e1 -r b1137bd73012 src/HOL/Hyperreal/StarDef.thy
--- a/src/HOL/Hyperreal/StarDef.thy	Tue Dec 19 17:35:33 2006 +0100
+++ b/src/HOL/Hyperreal/StarDef.thy	Tue Dec 19 19:34:35 2006 +0100
@@ -240,6 +240,53 @@
   "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> starfun2 f x y \<in> Standard"
 by (simp add: starfun2_def)
 
+lemma Standard_starfun_iff:
+  assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
+  shows "(starfun f x \<in> Standard) = (x \<in> Standard)"
+proof
+  assume "x \<in> Standard"
+  thus "starfun f x \<in> Standard" by simp
+next
+  have inj': "\<And>x y. starfun f x = starfun f y \<Longrightarrow> x = y"
+    using inj by transfer
+  assume "starfun f x \<in> Standard"
+  then obtain b where b: "starfun f x = star_of b"
+    unfolding Standard_def ..
+  hence "\<exists>x. starfun f x = star_of b" ..
+  hence "\<exists>a. f a = b" by transfer
+  then obtain a where "f a = b" ..
+  hence "starfun f (star_of a) = star_of b" by transfer
+  with b have "starfun f x = starfun f (star_of a)" by simp
+  hence "x = star_of a" by (rule inj')
+  thus "x \<in> Standard"
+    unfolding Standard_def by auto
+qed
+
+lemma Standard_starfun2_iff:
+  assumes inj: "\<And>a b a' b'. f a b = f a' b' \<Longrightarrow> a = a' \<and> b = b'"
+  shows "(starfun2 f x y \<in> Standard) = (x \<in> Standard \<and> y \<in> Standard)"
+proof
+  assume "x \<in> Standard \<and> y \<in> Standard"
+  thus "starfun2 f x y \<in> Standard" by simp
+next
+  have inj': "\<And>x y z w. starfun2 f x y = starfun2 f z w \<Longrightarrow> x = z \<and> y = w"
+    using inj by transfer
+  assume "starfun2 f x y \<in> Standard"
+  then obtain c where c: "starfun2 f x y = star_of c"
+    unfolding Standard_def ..
+  hence "\<exists>x y. starfun2 f x y = star_of c" by auto
+  hence "\<exists>a b. f a b = c" by transfer
+  then obtain a b where "f a b = c" by auto
+  hence "starfun2 f (star_of a) (star_of b) = star_of c"
+    by transfer
+  with c have "starfun2 f x y = starfun2 f (star_of a) (star_of b)"
+    by simp
+  hence "x = star_of a \<and> y = star_of b"
+    by (rule inj')
+  thus "x \<in> Standard \<and> y \<in> Standard"
+    unfolding Standard_def by auto
+qed
+
 
 subsection {* Internal predicates *}