aboutsummaryrefslogtreecommitdiff
path: root/Nat.thy
diff options
context:
space:
mode:
Diffstat (limited to 'Nat.thy')
-rw-r--r--Nat.thy46
1 files changed, 0 insertions, 46 deletions
diff --git a/Nat.thy b/Nat.thy
deleted file mode 100644
index cbfbe2d..0000000
--- a/Nat.thy
+++ /dev/null
@@ -1,46 +0,0 @@
-(********
-Isabelle/HoTT: Natural numbers
-Feb 2019
-
-********)
-
-theory Nat
-imports HoTT_Base
-
-begin
-
-axiomatization
- Nat :: t and
- zero :: t ("0") and
- succ :: "t \<Rightarrow> t" and
- indNat :: "[t \<Rightarrow> t, [t, t] \<Rightarrow> t, t, t] \<Rightarrow> t"
-where
- 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>
- a: C 0;
- n: Nat;
- C: Nat \<leadsto> U i;
- \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> indNat C f a n: C n" and
-
- Nat_cmp_0: "\<lbrakk>
- a: C 0;
- C: Nat \<leadsto> U i;
- \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> indNat C f a 0 \<equiv> a" and
-
- Nat_cmp_succ: "\<lbrakk>
- a: C 0;
- n: Nat;
- C: Nat \<leadsto> U i;
- \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n)
- \<rbrakk> \<Longrightarrow> indNat C f a (succ n) \<equiv> f n (indNat C f a n)"
-
-lemmas Nat_form [form]
-lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
-lemmas Nat_comp [comp] = Nat_cmp_0 Nat_cmp_succ
-
-end