37 inductive Nat :: "ind \<Rightarrow> bool" |
37 inductive Nat :: "ind \<Rightarrow> bool" |
38 where |
38 where |
39 Zero_RepI: "Nat Zero_Rep" |
39 Zero_RepI: "Nat Zero_Rep" |
40 | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)" |
40 | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)" |
41 |
41 |
42 typedef (open Nat) nat = Nat |
42 typedef (open Nat) nat = "{n. Nat n}" |
43 by (rule exI, unfold mem_def, rule Nat.Zero_RepI) |
43 using Nat.Zero_RepI by auto |
44 |
44 |
45 definition Suc :: "nat => nat" where |
45 lemma Nat_Rep_Nat: |
46 "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" |
46 "Nat (Rep_Nat n)" |
|
47 using Rep_Nat by simp |
|
48 |
|
49 lemma Nat_Abs_Nat_inverse: |
|
50 "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n" |
|
51 using Abs_Nat_inverse by simp |
|
52 |
|
53 lemma Nat_Abs_Nat_inject: |
|
54 "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m" |
|
55 using Abs_Nat_inject by simp |
47 |
56 |
48 instantiation nat :: zero |
57 instantiation nat :: zero |
49 begin |
58 begin |
50 |
59 |
51 definition Zero_nat_def: |
60 definition Zero_nat_def: |
53 |
62 |
54 instance .. |
63 instance .. |
55 |
64 |
56 end |
65 end |
57 |
66 |
|
67 definition Suc :: "nat \<Rightarrow> nat" where |
|
68 "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" |
|
69 |
58 lemma Suc_not_Zero: "Suc m \<noteq> 0" |
70 lemma Suc_not_Zero: "Suc m \<noteq> 0" |
59 by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def] |
71 by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat) |
60 Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]) |
|
61 |
72 |
62 lemma Zero_not_Suc: "0 \<noteq> Suc m" |
73 lemma Zero_not_Suc: "0 \<noteq> Suc m" |
63 by (rule not_sym, rule Suc_not_Zero not_sym) |
74 by (rule not_sym, rule Suc_not_Zero not_sym) |
64 |
75 |
65 lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y" |
76 lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y" |
66 by (rule iffI, rule Suc_Rep_inject) simp_all |
77 by (rule iffI, rule Suc_Rep_inject) simp_all |
67 |
78 |
68 rep_datatype "0 \<Colon> nat" Suc |
79 rep_datatype "0 \<Colon> nat" Suc |
69 apply (unfold Zero_nat_def Suc_def) |
80 apply (unfold Zero_nat_def Suc_def) |
70 apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} |
81 apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} |
71 apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct]) |
82 apply (erule Nat_Rep_Nat [THEN Nat.induct]) |
72 apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst]) |
83 apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst]) |
73 apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def] |
84 apply (simp_all add: Nat_Abs_Nat_inject Nat_Rep_Nat |
74 Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def] |
85 Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep |
75 Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric] |
86 Suc_Rep_not_Zero_Rep [symmetric] |
76 Suc_Rep_inject' Rep_Nat_inject) |
87 Suc_Rep_inject' Rep_Nat_inject) |
77 done |
88 done |
78 |
89 |
79 lemma nat_induct [case_names 0 Suc, induct type: nat]: |
90 lemma nat_induct [case_names 0 Suc, induct type: nat]: |
80 -- {* for backward compatibility -- names of variables differ *} |
91 -- {* for backward compatibility -- names of variables differ *} |