aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--hott/Nat.thy69
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