add and mul recurse on second argument instead of first

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