equal
deleted
inserted
replaced
33 |
33 |
34 lemma hypnat_induct_obj: |
34 lemma hypnat_induct_obj: |
35 "(( *pNat* P) 0 & |
35 "(( *pNat* P) 0 & |
36 (\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1))) |
36 (\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1))) |
37 --> ( *pNat* P)(n)" |
37 --> ( *pNat* P)(n)" |
38 apply (rule eq_Abs_hypnat [of n]) |
38 apply (cases n) |
39 apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra) |
39 apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra) |
40 apply (erule nat_induct) |
40 apply (erule nat_induct) |
41 apply (drule_tac x = "hypnat_of_nat n" in spec) |
41 apply (drule_tac x = "hypnat_of_nat n" in spec) |
42 apply (rule ccontr) |
42 apply (rule ccontr) |
43 apply (auto simp add: starPNat hypnat_of_nat_eq hypnat_add) |
43 apply (auto simp add: starPNat hypnat_of_nat_eq hypnat_add) |