diff options
Diffstat (limited to 'hott/Nat.thy')
| -rw-r--r-- | hott/Nat.thy | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy index 33a5d0a..0a38f99 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -115,7 +115,7 @@ Lemma (def) add_comm: proof compute have "suc (m + n) = suc (n + m)" by (eq ih) refl also have ".. = suc n + m" by (rewr eq: suc_add) refl - finally show "?" by this + finally show "?" by infer qed done @@ -152,7 +152,7 @@ Lemma (def) zero_mul: proof compute have "0 + 0 * n = 0 + 0 " by (eq ih) refl also have ".. = 0" by compute refl - finally show "?" by this + finally show "?" by infer qed done @@ -165,7 +165,7 @@ Lemma (def) suc_mul: proof (compute, rewr eq: \<open>ih:_\<close>) have "suc m + (m * n + n) = suc (m + ?)" by (rule suc_add) also have ".. = suc (m + m * n + n)" by (rewr eq: add_assoc) refl - finally show "?" by this + finally show "?" by infer qed done @@ -180,7 +180,7 @@ Lemma (def) mul_dist_add: also have ".. = l + l * m + l * n" by (rule add_assoc) also have ".. = l * m + l + l * n" by (rewr eq: add_comm) refl also have ".. = l * m + (l + l * n)" by (rewr eq: add_assoc) refl - finally show "?" by this + finally show "?" by infer qed done @@ -193,7 +193,7 @@ Lemma (def) mul_assoc: proof compute have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add) also have ".. = l * m + l * m * n" by (rewr eq: \<open>ih:_\<close>) refl - finally show "?" by this + finally show "?" by infer qed done @@ -207,7 +207,7 @@ Lemma (def) mul_comm: have "suc n * m = n * m + m" by (rule suc_mul) also have ".. = m + m * n" by (rewr eq: \<open>ih:_\<close>, rewr eq: add_comm) refl - finally show "?" by this + finally show "?" by infer qed done |