aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
Diffstat (limited to 'hott')
-rw-r--r--hott/Nat.thy47
1 files changed, 30 insertions, 17 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy
index bd58fbc..4825404 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -18,8 +18,8 @@ where
NatE: "\<lbrakk>
n: Nat;
c\<^sub>0: C 0;
- \<And>n. n: Nat \<Longrightarrow> C n: U i;
- \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k)
+ \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k);
+ \<And>n. n: Nat \<Longrightarrow> C n: U i
\<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) n: C n" and
Nat_comp_zero: "\<lbrakk>
@@ -56,44 +56,57 @@ lemma add_type [typechk]:
shows "m + n: Nat"
unfolding add_def by typechk
-lemma add_rec [comps]:
- assumes "m: Nat" "n: Nat"
- shows "suc m + n \<equiv> suc (m + n)"
- unfolding add_def by reduce
-
lemma zero_add [comps]:
assumes "n: Nat"
shows "0 + n \<equiv> n"
unfolding add_def by reduce
+lemma suc_add [comps]:
+ assumes "m: Nat" "n: Nat"
+ shows "suc m + n \<equiv> suc (m + n)"
+ unfolding add_def by reduce
+
Lemma (derive) add_zero:
assumes "n: Nat"
shows "n + 0 = n"
apply (elim n)
\<guillemotright> by (reduce; intro)
- \<guillemotright> vars _ IH by reduce (elim IH; intro)
+ \<guillemotright> vars _ ih by reduce (eq ih; intro)
done
+Lemma (derive) add_suc:
+ assumes "m: Nat" "n: Nat"
+ shows "m + suc n = suc (m + n)"
+ apply (elim m)
+ \<guillemotright> by reduce intro
+ \<guillemotright> vars _ ih by reduce (eq ih; intro)
+ done
+
+Lemma (derive) suc_monotone:
+ assumes "m: Nat" "n: Nat"
+ shows "p: m = n \<Longrightarrow> suc m = suc n"
+ by (eq p) intro
+
Lemma (derive) add_assoc:
assumes "l: Nat" "m: Nat" "n: Nat"
shows "l + (m + n) = (l + m) + n"
apply (elim l)
\<guillemotright> by reduce intro
- \<guillemotright> vars _ IH by reduce (elim IH; intro)
+ \<guillemotright> vars _ ih by reduce (eq ih; intro)
done
Lemma (derive) add_comm:
assumes "m: Nat" "n: Nat"
shows "m + n = n + m"
apply (elim m)
- \<guillemotright> by (reduce; rule add_zero[sym])
- \<guillemotright> vars m p
- apply (elim n)
- (*Should also change the `n`s in the premises!*)
- (*FIXME: Elimination tactic needs to do the same kind of thing as the
- equality tactic with pushing context premises into the statement, applying
- the appropriate elimination rule and then pulling back out.*)
-oops
+ \<guillemotright> by (reduce; rule add_zero[symmetric])
+ \<guillemotright> prems prms vars m 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 reduce
+ qed
+ done
definition mul (infixl "*" 120) where
[comps]: "m * n \<equiv> NatRec Nat 0 (K $ add n) m"