From e1be5f97bb2a42b3179bc24b118d69af137f8e5d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 21:28:21 +0200
Subject: Regrouping type rules

---
 Nat.thy | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

(limited to 'Nat.thy')

diff --git a/Nat.thy b/Nat.thy
index 05b0bfe..b48804a 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -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
-- 
cgit v1.2.3