diff options
author | Josh Chen | 2020-07-31 14:56:24 +0200 |
---|---|---|
committer | Josh Chen | 2020-07-31 14:56:24 +0200 |
commit | ff5454812f9e2720bd90c3a5437505644f63b487 (patch) | |
tree | 2df5f45de006c56391118db75e2f185036b02cd7 /hott/Nat.thy | |
parent | 2b0e14b16dcef0e829da95800b3c0af1975bb1ce (diff) |
(FEAT) Term elaboration of assumption and goal statements.
. spartan/core/goals.ML
. spartan/core/elaboration.ML
. spartan/core/elaborated_statement.ML
(FEAT) More context tacticals and search tacticals.
. spartan/core/context_tactical.ML
(FEAT) Improved subgoal focus.
Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
. spartan/core/focus.ML
(FIX) Normalize facts in order to be able to resolve properly.
. spartan/core/typechecking.ML
(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.
Diffstat (limited to '')
-rw-r--r-- | hott/Nat.thy | 58 |
1 files changed, 29 insertions, 29 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy index 177ec47..fd567f3 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -77,43 +77,43 @@ lemma add_suc [comp]: shows "m + suc n \<equiv> suc (m + n)" unfolding add_def by reduce -Lemma (derive) zero_add: +Lemma (def) zero_add: assumes "n: Nat" shows "0 + n = n" apply (elim n) - \<guillemotright> by (reduce; intro) - \<guillemotright> vars _ ih by reduce (eq ih; intro) + \<^item> by (reduce; intro) + \<^item> vars _ ih by reduce (eq ih; refl) done -Lemma (derive) suc_add: +Lemma (def) suc_add: assumes "m: Nat" "n: Nat" shows "suc m + n = suc (m + n)" apply (elim n) - \<guillemotright> by reduce refl - \<guillemotright> vars _ ih by reduce (eq ih; intro) + \<^item> by reduce refl + \<^item> vars _ ih by reduce (eq ih; refl) done -Lemma (derive) suc_eq: +Lemma (def) suc_eq: assumes "m: Nat" "n: Nat" shows "p: m = n \<Longrightarrow> suc m = suc n" by (eq p) intro -Lemma (derive) add_assoc: +Lemma (def) add_assoc: assumes "l: Nat" "m: Nat" "n: Nat" shows "l + (m + n) = l + m+ n" apply (elim n) - \<guillemotright> by reduce intro - \<guillemotright> vars _ ih by reduce (eq ih; intro) + \<^item> by reduce intro + \<^item> vars _ ih by reduce (eq ih; refl) done -Lemma (derive) add_comm: +Lemma (def) add_comm: assumes "m: Nat" "n: Nat" shows "m + n = n + m" apply (elim n) - \<guillemotright> by (reduce; rule zero_add[symmetric]) - \<guillemotright> prems vars n ih + \<^item> by (reduce; rule zero_add[symmetric]) + \<^item> vars n ih proof reduce - have "suc (m + n) = suc (n + m)" by (eq ih) intro + have "suc (m + n) = suc (n + m)" by (eq ih) refl also have ".. = suc n + m" by (transport eq: suc_add) refl finally show "{}" by this qed @@ -143,12 +143,12 @@ lemma mul_suc [comp]: shows "m * suc n \<equiv> m + m * n" unfolding mul_def by reduce -Lemma (derive) zero_mul: +Lemma (def) zero_mul: assumes "n: Nat" shows "0 * n = 0" apply (elim n) - \<guillemotright> by reduce refl - \<guillemotright> prems vars n ih + \<^item> by reduce refl + \<^item> vars n ih proof reduce have "0 + 0 * n = 0 + 0 " by (eq ih) refl also have ".. = 0" by reduce refl @@ -156,12 +156,12 @@ Lemma (derive) zero_mul: qed done -Lemma (derive) suc_mul: +Lemma (def) suc_mul: assumes "m: Nat" "n: Nat" shows "suc m * n = m * n + n" apply (elim n) - \<guillemotright> by reduce refl - \<guillemotright> prems vars n ih + \<^item> by reduce refl + \<^item> vars n ih proof (reduce, transport eq: \<open>ih:_\<close>) have "suc m + (m * n + n) = suc (m + {})" by (rule suc_add) also have ".. = suc (m + m * n + n)" by (transport eq: add_assoc) refl @@ -169,12 +169,12 @@ Lemma (derive) suc_mul: qed done -Lemma (derive) mul_dist_add: +Lemma (def) mul_dist_add: assumes "l: Nat" "m: Nat" "n: Nat" shows "l * (m + n) = l * m + l * n" apply (elim n) - \<guillemotright> by reduce refl - \<guillemotright> prems prms vars n ih + \<^item> by reduce refl + \<^item> vars n ih proof reduce have "l + l * (m + n) = l + (l * m + l * n)" by (eq ih) refl also have ".. = l + l * m + l * n" by (rule add_assoc) @@ -184,12 +184,12 @@ Lemma (derive) mul_dist_add: qed done -Lemma (derive) mul_assoc: +Lemma (def) mul_assoc: assumes "l: Nat" "m: Nat" "n: Nat" shows "l * (m * n) = l * m * n" apply (elim n) - \<guillemotright> by reduce refl - \<guillemotright> prems vars n ih + \<^item> by reduce refl + \<^item> vars n ih proof reduce have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add) also have ".. = l * m + l * m * n" by (transport eq: \<open>ih:_\<close>) refl @@ -197,12 +197,12 @@ Lemma (derive) mul_assoc: qed done -Lemma (derive) mul_comm: +Lemma (def) mul_comm: assumes "m: Nat" "n: Nat" shows "m * n = n * m" apply (elim n) - \<guillemotright> by reduce (transport eq: zero_mul, refl) - \<guillemotright> prems vars n ih + \<^item> by reduce (transport eq: zero_mul, refl) + \<^item> vars n ih proof (reduce, rule pathinv) have "suc n * m = n * m + m" by (rule suc_mul) also have ".. = m + m * n" |