aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-05-30 14:38:12 +0200
committerJosh Chen2020-05-30 14:38:12 +0200
commit2e807b74bd0f4e9a2ccfcb861bef876dba5aa066 (patch)
treec27a067e063508a609547a2459d147235b295fb6
parent9ed05b8027122d9b5e450b811deb8897ffe78417 (diff)
fix name
-rw-r--r--hott/Nat.thy6
1 files changed, 5 insertions, 1 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy
index e8657a4..e36d6be 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -49,6 +49,8 @@ abbreviation "NatRec C \<equiv> NatInd (\<lambda>_. C)"
section \<open>Basic arithmetic\<close>
+subsection \<open>Addition\<close>
+
definition add (infixl "+" 120) where "m + n \<equiv> NatRec Nat n (K suc) m"
lemma add_type [typechk]:
@@ -82,7 +84,7 @@ Lemma (derive) add_suc:
\<guillemotright> vars _ ih by reduce (eq ih; intro)
done
-Lemma (derive) suc_monotone:
+Lemma (derive) suc_eq:
assumes "m: Nat" "n: Nat"
shows "p: m = n \<Longrightarrow> suc m = suc n"
by (eq p) intro
@@ -108,6 +110,8 @@ Lemma (derive) add_comm:
qed
done
+subsection \<open>Multiplication\<close>
+
definition mul (infixl "*" 120) where
[comps]: "m * n \<equiv> NatRec Nat 0 (K $ add n) m"