diff options
Diffstat (limited to 'Nat.thy')
-rw-r--r-- | Nat.thy | 19 |
1 files changed, 9 insertions, 10 deletions
@@ -1,8 +1,7 @@ (* Title: HoTT/Nat.thy Author: Josh Chen - Date: Aug 2018 -Natural numbers. +Natural numbers *) theory Nat @@ -20,9 +19,9 @@ axiomatization where Nat_form: "\<nat>: U(O)" and - Nat_intro1: "0: \<nat>" + Nat_intro_0: "0: \<nat>" and - Nat_intro2: "n: \<nat> \<Longrightarrow> succ(n): \<nat>" + Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ(n): \<nat>" and Nat_elim: "\<lbrakk> C: \<nat> \<longrightarrow> U(i); @@ -31,13 +30,13 @@ and n: \<nat> \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(n): C(n)" and - Nat_comp1: "\<lbrakk> + 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" and - Nat_comp2: "\<lbrakk> + 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); @@ -45,11 +44,11 @@ and \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> f a n)" -text "Rule declarations:" +text "Rule attribute declarations:" -lemmas Nat_intro = Nat_intro1 Nat_intro2 -lemmas Nat_rules [intro] = Nat_form Nat_intro Nat_elim Nat_comp1 Nat_comp2 -lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2 +lemmas Nat_intro = Nat_intro_0 Nat_intro_succ +lemmas Nat_comp [comp] = Nat_comp_0 Nat_comp_succ +lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_comp Nat_elim end |