more regular axiom of infinity, with no (indirect) reference to overloaded constants
authorkrauss
Wed Dec 30 01:08:33 2009 +0100 (2009-12-30)
changeset 34208a7acd6c68d9b
parent 34207 88300168baf8
child 34209 c7f621786035
more regular axiom of infinity, with no (indirect) reference to overloaded constants
src/HOL/Import/HOL4Setup.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Import/HOL4Setup.thy	Tue Dec 29 20:59:47 2009 +0100
     1.2 +++ b/src/HOL/Import/HOL4Setup.thy	Wed Dec 30 01:08:33 2009 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))"
     1.5  proof (rule exI,safe)
     1.6    show "inj Suc_Rep"
     1.7 -    by (rule inj_Suc_Rep)
     1.8 +    by (rule injI) (rule Suc_Rep_inject)
     1.9  next
    1.10    assume "surj Suc_Rep"
    1.11    hence "ALL y. EX x. y = Suc_Rep x"
     2.1 --- a/src/HOL/Nat.thy	Tue Dec 29 20:59:47 2009 +0100
     2.2 +++ b/src/HOL/Nat.thy	Wed Dec 30 01:08:33 2009 +0100
     2.3 @@ -27,10 +27,9 @@
     2.4    Suc_Rep :: "ind => ind"
     2.5  where
     2.6    -- {* the axiom of infinity in 2 parts *}
     2.7 -  inj_Suc_Rep:          "inj Suc_Rep" and
     2.8 +  Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
     2.9    Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    2.10  
    2.11 -
    2.12  subsection {* Type nat *}
    2.13  
    2.14  text {* Type definition *}
    2.15 @@ -69,6 +68,9 @@
    2.16  lemma Zero_not_Suc: "0 \<noteq> Suc m"
    2.17    by (rule not_sym, rule Suc_not_Zero not_sym)
    2.18  
    2.19 +lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y"
    2.20 +  by (rule iffI, rule Suc_Rep_inject) simp_all
    2.21 +
    2.22  rep_datatype "0 \<Colon> nat" Suc
    2.23    apply (unfold Zero_nat_def Suc_def)
    2.24       apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    2.25 @@ -77,7 +79,7 @@
    2.26      apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
    2.27        Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
    2.28        Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
    2.29 -      inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
    2.30 +      Suc_Rep_inject' Rep_Nat_inject)
    2.31    done
    2.32  
    2.33  lemma nat_induct [case_names 0 Suc, induct type: nat]: