# HG changeset patch
# User krauss
# Date 1262131713 -3600
# Node ID a7acd6c68d9b8b107206130fef545b0fe2f8a946
# Parent  88300168baf80efe5c6181ca3971b2db4ef70984
more regular axiom of infinity, with no (indirect) reference to overloaded constants

diff -r 88300168baf8 -r a7acd6c68d9b src/HOL/Import/HOL4Setup.thy
--- a/src/HOL/Import/HOL4Setup.thy	Tue Dec 29 20:59:47 2009 +0100
+++ b/src/HOL/Import/HOL4Setup.thy	Wed Dec 30 01:08:33 2009 +0100
@@ -29,7 +29,7 @@
 lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))"
 proof (rule exI,safe)
   show "inj Suc_Rep"
-    by (rule inj_Suc_Rep)
+    by (rule injI) (rule Suc_Rep_inject)
 next
   assume "surj Suc_Rep"
   hence "ALL y. EX x. y = Suc_Rep x"
diff -r 88300168baf8 -r a7acd6c68d9b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Dec 29 20:59:47 2009 +0100
+++ b/src/HOL/Nat.thy	Wed Dec 30 01:08:33 2009 +0100
@@ -27,10 +27,9 @@
   Suc_Rep :: "ind => ind"
 where
   -- {* the axiom of infinity in 2 parts *}
-  inj_Suc_Rep:          "inj Suc_Rep" and
+  Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
   Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
 
-
 subsection {* Type nat *}
 
 text {* Type definition *}
@@ -69,6 +68,9 @@
 lemma Zero_not_Suc: "0 \<noteq> Suc m"
   by (rule not_sym, rule Suc_not_Zero not_sym)
 
+lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y"
+  by (rule iffI, rule Suc_Rep_inject) simp_all
+
 rep_datatype "0 \<Colon> nat" Suc
   apply (unfold Zero_nat_def Suc_def)
      apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
@@ -77,7 +79,7 @@
     apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
       Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
       Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
-      inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
+      Suc_Rep_inject' Rep_Nat_inject)
   done
 
 lemma nat_induct [case_names 0 Suc, induct type: nat]: