src/HOL/Import/HOL4Setup.thy
changeset 17322 781abf7011e6
parent 16417 9bc16273c2d4
child 17801 30cbd2685e73
equal deleted inserted replaced
17321:227f1f5c3959 17322:781abf7011e6
    22   ONE_ONE :: "('a => 'b) => bool"
    22   ONE_ONE :: "('a => 'b) => bool"
    23   ONTO    :: "('a => 'b) => bool"
    23   ONTO    :: "('a => 'b) => bool"
    24 
    24 
    25 defs
    25 defs
    26   ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
    26   ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
    27   ONTO_DEF   : "ONTO f == ALL y. EX x. y = f x"
       
    28 
    27 
    29 lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV"
    28 lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV"
    30   by (simp add: ONE_ONE_DEF inj_on_def)
    29   by (simp add: ONE_ONE_DEF inj_on_def)
    31 
    30 
    32 lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(ONTO f))"
    31 lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))"
    33 proof (rule exI,safe)
    32 proof (rule exI,safe)
    34   show "inj Suc_Rep"
    33   show "inj Suc_Rep"
    35     by (rule inj_Suc_Rep)
    34     by (rule inj_Suc_Rep)
    36 next
    35 next
    37   assume "ONTO Suc_Rep"
    36   assume "surj Suc_Rep"
    38   hence "ALL y. EX x. y = Suc_Rep x"
    37   hence "ALL y. EX x. y = Suc_Rep x"
    39     by (simp add: ONTO_DEF surj_def)
    38     by (simp add: surj_def)
    40   hence "EX x. Zero_Rep = Suc_Rep x"
    39   hence "EX x. Zero_Rep = Suc_Rep x"
    41     by (rule spec)
    40     by (rule spec)
    42   thus False
    41   thus False
    43   proof (rule exE)
    42   proof (rule exE)
    44     fix x
    43     fix x