diff options
author | Josh Chen | 2020-07-21 02:16:14 +0200 |
---|---|---|
committer | GitHub | 2020-07-21 02:16:14 +0200 |
commit | dfd241b2d85fc5a4ad4d7ddd64adf0138b05f083 (patch) | |
tree | b4c4280b1bc4426059ddd184a2258d15d20a0bab /hott/Nat.thy | |
parent | 6aaf4d5b28a5284b3b02fa5c410d2d83a711840b (diff) | |
parent | 12eed8685674b7d5ff7bc45a44a061e01f99ce5f (diff) |
Merge pull request #8 from jaycech3n/dev
Merge big diff on dev
Diffstat (limited to 'hott/Nat.thy')
-rw-r--r-- | hott/Nat.thy | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy index 4abd315..177ec47 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -38,9 +38,10 @@ where f n (NatInd (fn n. C n) c\<^sub>0 (fn k rec. f k rec) n)" lemmas - [intros] = NatF Nat_zero Nat_suc and - [elims "?n"] = NatE and - [comps] = Nat_comp_zero Nat_comp_suc + [form] = NatF and + [intro, intros] = Nat_zero Nat_suc and + [elim "?n"] = NatE and + [comp] = Nat_comp_zero Nat_comp_suc abbreviation "NatRec C \<equiv> NatInd (fn _. C)" @@ -66,12 +67,12 @@ lemma add_type [typechk]: shows "m + n: Nat" unfolding add_def by typechk -lemma add_zero [comps]: +lemma add_zero [comp]: assumes "m: Nat" shows "m + 0 \<equiv> m" unfolding add_def by reduce -lemma add_suc [comps]: +lemma add_suc [comp]: assumes "m: Nat" "n: Nat" shows "m + suc n \<equiv> suc (m + n)" unfolding add_def by reduce @@ -127,17 +128,17 @@ lemma mul_type [typechk]: shows "m * n: Nat" unfolding mul_def by typechk -lemma mul_zero [comps]: +lemma mul_zero [comp]: assumes "n: Nat" shows "n * 0 \<equiv> 0" unfolding mul_def by reduce -lemma mul_one [comps]: +lemma mul_one [comp]: assumes "n: Nat" shows "n * 1 \<equiv> n" unfolding mul_def by reduce -lemma mul_suc [comps]: +lemma mul_suc [comp]: assumes "m: Nat" "n: Nat" shows "m * suc n \<equiv> m + m * n" unfolding mul_def by reduce |