diff options
| -rw-r--r-- | hott/Nat.thy | 69 |
1 files changed, 49 insertions, 20 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy index e36d6be..2d03293 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -46,41 +46,52 @@ text \<open>Non-dependent recursion\<close> abbreviation "NatRec C \<equiv> NatInd (\<lambda>_. C)" +text \<open>Manual notation for now:\<close> +abbreviation one ("1") where "1 \<equiv> suc 0" +abbreviation two ("2") where "2 \<equiv> suc 1" +abbreviation three ("3") where "3 \<equiv> suc 2" +abbreviation four ("4") where "4 \<equiv> suc 3" +abbreviation five ("5") where "5 \<equiv> suc 4" +abbreviation six ("6") where "6 \<equiv> suc 5" +abbreviation seven ("7") where "7 \<equiv> suc 6" +abbreviation eight ("8") where "8 \<equiv> suc 7" +abbreviation nine ("9") where "9 \<equiv> suc 8" + section \<open>Basic arithmetic\<close> subsection \<open>Addition\<close> -definition add (infixl "+" 120) where "m + n \<equiv> NatRec Nat n (K suc) m" +definition add (infixl "+" 120) where "m + n \<equiv> NatRec Nat m (K suc) n" lemma add_type [typechk]: assumes "m: Nat" "n: Nat" shows "m + n: Nat" unfolding add_def by typechk -lemma zero_add [comps]: - assumes "n: Nat" - shows "0 + n \<equiv> n" +lemma add_zero [comps]: + assumes "m: Nat" + shows "m + 0 \<equiv> m" unfolding add_def by reduce -lemma suc_add [comps]: +lemma add_suc [comps]: assumes "m: Nat" "n: Nat" - shows "suc m + n \<equiv> suc (m + n)" + shows "m + suc n \<equiv> suc (m + n)" unfolding add_def by reduce -Lemma (derive) add_zero: +Lemma (derive) zero_add: assumes "n: Nat" - shows "n + 0 = n" + shows "0 + n = n" apply (elim n) \<guillemotright> by (reduce; intro) \<guillemotright> vars _ ih by reduce (eq ih; intro) done -Lemma (derive) add_suc: +Lemma (derive) suc_add: assumes "m: Nat" "n: Nat" - shows "m + suc n = suc (m + n)" - apply (elim m) - \<guillemotright> by reduce intro + shows "suc m + n = suc (m + n)" + apply (elim n) + \<guillemotright> by reduce refl \<guillemotright> vars _ ih by reduce (eq ih; intro) done @@ -92,7 +103,7 @@ Lemma (derive) suc_eq: Lemma (derive) add_assoc: assumes "l: Nat" "m: Nat" "n: Nat" shows "l + (m + n) = (l + m) + n" - apply (elim l) + apply (elim n) \<guillemotright> by reduce intro \<guillemotright> vars _ ih by reduce (eq ih; intro) done @@ -100,20 +111,38 @@ Lemma (derive) add_assoc: Lemma (derive) add_comm: assumes "m: Nat" "n: Nat" shows "m + n = n + m" - apply (elim m) - \<guillemotright> by (reduce; rule add_zero[symmetric]) - \<guillemotright> prems vars m ih + apply (elim n) + \<guillemotright> by (reduce; rule zero_add[symmetric]) + \<guillemotright> prems vars n ih proof reduce have "suc (m + n) = suc (n + m)" by (eq ih) intro - also have ".. = n + suc m" by (rule add_suc[symmetric]) - finally show "suc (m + n) = n + suc m" by this + also have ".. = suc n + m" by (rule suc_add[symmetric]) + finally show "suc (m + n) = suc n + m" by this qed done subsection \<open>Multiplication\<close> -definition mul (infixl "*" 120) where - [comps]: "m * n \<equiv> NatRec Nat 0 (K $ add n) m" +definition mul (infixl "*" 121) where "m * n \<equiv> NatRec Nat 0 (K $ add m) n" +lemma mul_type [typechk]: + assumes "m: Nat" "n: Nat" + shows "m * n: Nat" + unfolding mul_def by typechk + +lemma mul_zero [comps]: + assumes "n: Nat" + shows "n * 0 \<equiv> 0" + unfolding mul_def by reduce + +lemma mul_one [comps]: + assumes "n: Nat" + shows "n * 1 \<equiv> n" + unfolding mul_def by reduce + +lemma mul_suc [comps]: + assumes "m: Nat" "n: Nat" + shows "m * suc n \<equiv> m + m * n" + unfolding mul_def by reduce end |