Merge branch 'develop', ready for release 0.1.0

1 files changed, 29 insertions, 34 deletions

diff --git a/Nat.thy b/Nat.thy
index e879c92..8a55852 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -1,54 +1,49 @@
-(*  Title:  HoTT/Nat.thy
-    Author: Josh Chen
+(*
+Title:  Nat.thy
+Author: Joshua Chen
+Date:   2018
 
 Natural numbers
 *)
 
 theory Nat
-  imports HoTT_Base
-begin
+imports HoTT_Base
 
+begin
 
-section \<open>Constants and type rules\<close>
 
 axiomatization
-  Nat :: Term   ("\<nat>") and
-  zero :: Term  ("0") and
-  succ :: "Term \<Rightarrow> Term" and
-  indNat :: "[[Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<nat>)")
+  Nat    :: t  ("\<nat>") and
+  zero   :: t  ("0") and
+  succ   :: "t \<Rightarrow> t" and
+  indNat :: "[[t, t] \<Rightarrow> t, t, t] \<Rightarrow> t"  ("(1ind\<^sub>\<nat>)")
 where
-  Nat_form: "\<nat>: U O"
-and
-  Nat_intro_0: "0: \<nat>"
-and
-  Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>"
-and
+  Nat_form: "\<nat>: U O" and
+
+  Nat_intro_0: "0: \<nat>" and
+
+  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;
-    n: \<nat>
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n"
-and
+    n: \<nat>;
+    C: \<nat> \<longrightarrow> U i;
+    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a n: C n" and
+
   Nat_comp_0: "\<lbrakk>
+    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
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a"
-and
+    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) 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;
-    n: \<nat>
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
-
-
-text "Rule attribute declarations:"
+    n: \<nat>;
+    C: \<nat> \<longrightarrow> U i;
+    \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
 
-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_elim
+lemmas Nat_form [form]
+lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
+lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ
 
 
 end