diff options
Diffstat (limited to 'Nat.thy')
| -rw-r--r-- | Nat.thy | 28 |
1 files changed, 14 insertions, 14 deletions
@@ -17,31 +17,31 @@ axiomatization succ :: "Term \<Rightarrow> Term" and indNat :: "[[Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<nat>)") where - Nat_form: "\<nat>: U(O)" + Nat_form: "\<nat>: U O" and Nat_intro_0: "0: \<nat>" and - Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ(n): \<nat>" + Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>" and Nat_elim: "\<lbrakk> - C: \<nat> \<longrightarrow> U(i); - \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n); - a: C(0); + C: \<nat> \<longrightarrow> U i; + \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n); + a: C 0; n: \<nat> - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(n): C(n)" + \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n" and Nat_comp_0: "\<lbrakk> - C: \<nat> \<longrightarrow> U(i); - \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n); - a: C(0) - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(0) \<equiv> a" + C: \<nat> \<longrightarrow> U i; + \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n); + a: C 0 + \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a" and Nat_comp_succ: "\<lbrakk> - C: \<nat> \<longrightarrow> U(i); - \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n); - a: C(0); + C: \<nat> \<longrightarrow> U i; + \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n); + a: C 0; n: \<nat> - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> f a n)" + \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)" text "Rule attribute declarations:" |