diff options
| author | Josh Chen | 2020-05-30 14:38:12 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-30 14:38:12 +0200 |
| commit | 2e807b74bd0f4e9a2ccfcb861bef876dba5aa066 (patch) | |
| tree | c27a067e063508a609547a2459d147235b295fb6 | |
| parent | 9ed05b8027122d9b5e450b811deb8897ffe78417 (diff) | |
fix name
| -rw-r--r-- | hott/Nat.thy | 6 |
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" |