aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--hott/Equivalence.thy58
-rw-r--r--hott/Identity.thy100
-rw-r--r--hott/Nat.thy60
3 files changed, 105 insertions, 113 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 379dc81..9fe11a7 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -88,12 +88,12 @@ lemmas
Lemma id_funcomp_htpy:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
shows "homotopy_refl A f: (id B) \<circ> f ~ f"
- by reduce
+ by compute
Lemma funcomp_id_htpy:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
shows "homotopy_refl A f: f \<circ> (id A) ~ f"
- by reduce
+ by compute
Lemma funcomp_left_htpy:
assumes
@@ -105,7 +105,7 @@ Lemma funcomp_left_htpy:
"H: g ~ g'"
shows "(g \<circ> f) ~ (g' \<circ> f)"
unfolding homotopy_def
- apply (intro, reduce)
+ apply (intro, compute)
apply (htpy H)
done
@@ -118,12 +118,12 @@ Lemma funcomp_right_htpy:
"H: f ~ f'"
shows "(g \<circ> f) ~ (g \<circ> f')"
unfolding homotopy_def
- proof (intro, reduce)
+ proof (intro, compute)
fix x assuming "x: A"
have *: "f x = f' x"
by (htpy H)
show "g (f x) = g (f' x)"
- by (transport eq: *) refl
+ by (rewr eq: *) refl
qed
method lhtpy = rule funcomp_left_htpy[rotated 6]
@@ -139,8 +139,8 @@ Lemma (def) commute_homotopy:
shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)"
using \<open>H:_\<close>
unfolding homotopy_def
- apply (eq p, reduce)
- apply (transport eq: pathcomp_refl, transport eq: refl_pathcomp)
+ apply (eq p, compute)
+ apply (rewr eq: pathcomp_refl, rewr eq: refl_pathcomp)
by refl
Corollary (def) commute_homotopy':
@@ -151,21 +151,13 @@ Corollary (def) commute_homotopy':
"H: f ~ (id A)"
shows "H (f x) = f [H x]"
proof -
- (* Rewrite the below proof
- have *: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x"
- using \<open>H:_\<close> unfolding homotopy_def by (rule commute_homotopy)
-
- thus "H (f x) = f[H x]"
- apply (pathcomp_cancelr)
- ...
- *)
- (*FUTURE: Because we don't have very good normalization integrated into
+ (*FUTURE: Because we don't have very good normalization integrated into
things yet, we need to manually unfold the type of H.*)
from \<open>H: f ~ id A\<close> have [type]: "H: \<Prod>x: A. f x = x"
- by (reduce add: homotopy_def)
+ by (compute add: homotopy_def)
have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]"
- by (rule left_whisker, transport eq: ap_id, refl)
+ by (rule left_whisker, rewr eq: ap_id, refl)
also have [simplified id_comp]: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x"
by (rule commute_homotopy)
finally have "?" by this
@@ -198,7 +190,7 @@ Lemma (def) id_is_qinv:
unfolding is_qinv_def
proof intro
show "id A: A \<rightarrow> A" by typechk
- qed (reduce, intro; refl)
+ qed (compute, intro; refl)
Lemma is_qinvI:
assumes
@@ -245,17 +237,17 @@ Lemma (def) funcomp_is_qinv:
\<^item> proof intro
show "(finv \<circ> ginv) \<circ> g \<circ> f ~ id A"
proof -
- have "(finv \<circ> ginv) \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by reduce refl
+ have "(finv \<circ> ginv) \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by compute refl
also have ".. ~ finv \<circ> id B \<circ> f" by (rhtpy, lhtpy) fact
- also have ".. ~ id A" by reduce fact
+ also have ".. ~ id A" by compute fact
finally show "?" by this
qed
show "(g \<circ> f) \<circ> finv \<circ> ginv ~ id C"
proof -
- have "(g \<circ> f) \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by reduce refl
+ have "(g \<circ> f) \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by compute refl
also have ".. ~ g \<circ> id B \<circ> ginv" by (rhtpy, lhtpy) fact
- also have ".. ~ id C" by reduce fact
+ also have ".. ~ id C" by compute fact
finally show "?" by this
qed
qed
@@ -317,10 +309,10 @@ Lemma (def) is_qinv_if_is_biinv:
\<^item> by (fact \<open>g: _\<close>)
\<^item> by (fact \<open>H1: _\<close>)
\<^item> proof -
- have "g ~ g \<circ> (id B)" by reduce refl
+ have "g ~ g \<circ> (id B)" by compute refl
also have ".. ~ g \<circ> f \<circ> h" by rhtpy (rule \<open>H2:_\<close>[symmetric])
- also have ".. ~ (id A) \<circ> h" by (rewrite funcomp_assoc[symmetric]) (lhtpy, fact)
- also have ".. ~ h" by reduce refl
+ also have ".. ~ (id A) \<circ> h" by (comp funcomp_assoc[symmetric]) (lhtpy, fact)
+ also have ".. ~ h" by compute refl
finally have "g ~ h" by this
then have "f \<circ> g ~ f \<circ> h" by (rhtpy, this)
also note \<open>H2:_\<close>
@@ -420,24 +412,24 @@ Lemma (def) equiv_if_equal:
apply intro defer
\<^item> apply (eq p)
\<^enum> vars A B
- apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
+ apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
using [[solve_side_conds=1]]
- apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
+ apply (comp at B in "_ \<rightarrow> B" id_comp[symmetric])
apply (rule transport, rule Ui_in_USi)
by (rule lift_universe_codomain, rule Ui_in_USi)
\<^enum> vars A
using [[solve_side_conds=1]]
- apply (rewrite transport_comp)
+ apply (comp transport_comp)
\<circ> by (rule Ui_in_USi)
- \<circ> by reduce (rule U_lift)
- \<circ> by reduce (rule id_is_biinv)
+ \<circ> by compute (rule U_lift)
+ \<circ> by compute (rule id_is_biinv)
done
done
\<^item> \<comment> \<open>Similar proof as in the first subgoal above\<close>
- apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
+ apply (comp at A in "A \<rightarrow> B" id_comp[symmetric])
using [[solve_side_conds=1]]
- apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
+ apply (comp at B in "_ \<rightarrow> B" id_comp[symmetric])
apply (rule transport, rule Ui_in_USi)
by (rule lift_universe_codomain, rule Ui_in_USi)
done
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 0a31dc7..caab2e3 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -85,7 +85,7 @@ Lemma (def) pathinv:
Lemma pathinv_comp [comp]:
assumes "A: U i" "x: A"
shows "pathinv A x x (refl x) \<equiv> refl x"
- unfolding pathinv_def by reduce
+ unfolding pathinv_def by compute
Lemma (def) pathcomp:
assumes
@@ -101,7 +101,7 @@ Lemma (def) pathcomp:
Lemma pathcomp_comp [comp]:
assumes "A: U i" "a: A"
shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a"
- unfolding pathcomp_def by reduce
+ unfolding pathcomp_def by compute
method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q]
@@ -137,12 +137,12 @@ section \<open>Basic propositional equalities\<close>
Lemma (def) refl_pathcomp:
assumes "A: U i" "x: A" "y: A" "p: x = y"
shows "(refl x) \<bullet> p = p"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
Lemma (def) pathcomp_refl:
assumes "A: U i" "x: A" "y: A" "p: x = y"
shows "p \<bullet> (refl y) = p"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
definition [implicit]: "lu p \<equiv> refl_pathcomp {} {} {} p"
definition [implicit]: "ru p \<equiv> pathcomp_refl {} {} {} p"
@@ -154,27 +154,27 @@ translations
Lemma lu_refl [comp]:
assumes "A: U i" "x: A"
shows "lu (refl x) \<equiv> refl (refl x)"
- unfolding refl_pathcomp_def by reduce
+ unfolding refl_pathcomp_def by compute
Lemma ru_refl [comp]:
assumes "A: U i" "x: A"
shows "ru (refl x) \<equiv> refl (refl x)"
- unfolding pathcomp_refl_def by reduce
+ unfolding pathcomp_refl_def by compute
Lemma (def) inv_pathcomp:
assumes "A: U i" "x: A" "y: A" "p: x = y"
shows "p\<inverse> \<bullet> p = refl y"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
Lemma (def) pathcomp_inv:
assumes "A: U i" "x: A" "y: A" "p: x = y"
shows "p \<bullet> p\<inverse> = refl x"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
Lemma (def) pathinv_pathinv:
assumes "A: U i" "x: A" "y: A" "p: x = y"
shows "p\<inverse>\<inverse> = p"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
Lemma (def) pathcomp_assoc:
assumes
@@ -187,7 +187,7 @@ Lemma (def) pathcomp_assoc:
proof (eq q)
fix x r assuming "x: A" "r: x = w"
show "refl x \<bullet> (refl x \<bullet> r) = refl x \<bullet> refl x \<bullet> r"
- by (eq r) (reduce, refl)
+ by (eq r) (compute, refl)
qed
qed
@@ -211,7 +211,7 @@ translations "f[p]" \<leftharpoondown> "CONST ap A B x y f p"
Lemma ap_refl [comp]:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "x: A"
shows "f[refl x] \<equiv> refl (f x)"
- unfolding ap_def by reduce
+ unfolding ap_def by compute
Lemma (def) ap_pathcomp:
assumes
@@ -224,7 +224,7 @@ Lemma (def) ap_pathcomp:
proof (eq p)
fix x q assuming "x: A" "q: x = z"
show "f[refl x \<bullet> q] = f[refl x] \<bullet> f[q]"
- by (eq q) (reduce, refl)
+ by (eq q) (compute, refl)
qed
Lemma (def) ap_pathinv:
@@ -234,7 +234,7 @@ Lemma (def) ap_pathinv:
"f: A \<rightarrow> B"
"p: x = y"
shows "f[p\<inverse>] = f[p]\<inverse>"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
Lemma (def) ap_funcomp:
assumes
@@ -244,14 +244,14 @@ Lemma (def) ap_funcomp:
"p: x = y"
shows "(g \<circ> f)[p] = g[f[p]]"
apply (eq p)
- \<^item> by reduce
- \<^item> by reduce refl
+ \<^item> by compute
+ \<^item> by compute refl
done
Lemma (def) ap_id:
assumes "A: U i" "x: A" "y: A" "p: x = y"
shows "(id A)[p] = p"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
section \<open>Transport\<close>
@@ -276,7 +276,7 @@ Lemma transport_comp [comp]:
"A: U i"
"\<And>x. x: A \<Longrightarrow> P x: U i"
shows "transp P (refl a) \<equiv> id (P a)"
- unfolding transport_def by reduce
+ unfolding transport_def by compute
Lemma apply_transport:
assumes
@@ -287,7 +287,7 @@ Lemma apply_transport:
shows "transp P p\<inverse> u: P y"
by typechk
-method transport uses eq = (rule apply_transport[OF _ _ _ _ eq])
+method rewr uses eq = (rule apply_transport[OF _ _ _ _ eq])
Lemma (def) pathcomp_cancel_left:
assumes
@@ -297,13 +297,13 @@ Lemma (def) pathcomp_cancel_left:
shows "q = r"
proof -
have "q = (p\<inverse> \<bullet> p) \<bullet> q"
- by (transport eq: inv_pathcomp, transport eq: refl_pathcomp) refl
+ by (rewr eq: inv_pathcomp, rewr eq: refl_pathcomp) refl
also have ".. = p\<inverse> \<bullet> (p \<bullet> r)"
- by (transport eq: pathcomp_assoc[symmetric], transport eq: \<open>\<alpha>:_\<close>) refl
+ by (rewr eq: pathcomp_assoc[symmetric], rewr eq: \<open>\<alpha>:_\<close>) refl
also have ".. = r"
- by (transport eq: pathcomp_assoc,
- transport eq: inv_pathcomp,
- transport eq: refl_pathcomp) refl
+ by (rewr eq: pathcomp_assoc,
+ rewr eq: inv_pathcomp,
+ rewr eq: refl_pathcomp) refl
finally show "?" by this
qed
@@ -315,14 +315,14 @@ Lemma (def) pathcomp_cancel_right:
shows "p = q"
proof -
have "p = p \<bullet> r \<bullet> r\<inverse>"
- by (transport eq: pathcomp_assoc[symmetric],
- transport eq: pathcomp_inv,
- transport eq: pathcomp_refl) refl
+ by (rewr eq: pathcomp_assoc[symmetric],
+ rewr eq: pathcomp_inv,
+ rewr eq: pathcomp_refl) refl
also have ".. = q"
- by (transport eq: \<open>\<alpha>:_\<close>,
- transport eq: pathcomp_assoc[symmetric],
- transport eq: pathcomp_inv,
- transport eq: pathcomp_refl) refl
+ by (rewr eq: \<open>\<alpha>:_\<close>,
+ rewr eq: pathcomp_assoc[symmetric],
+ rewr eq: pathcomp_inv,
+ rewr eq: pathcomp_refl) refl
finally show "?" by this
qed
@@ -336,7 +336,7 @@ Lemma (def) transport_left_inv:
"x: A" "y: A"
"p: x = y"
shows "(transp P p\<inverse>) \<circ> (transp P p) = id (P x)"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
Lemma (def) transport_right_inv:
assumes
@@ -345,7 +345,7 @@ Lemma (def) transport_right_inv:
"x: A" "y: A"
"p: x = y"
shows "(transp P p) \<circ> (transp P p\<inverse>) = id (P y)"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
Lemma (def) transport_pathcomp:
assumes
@@ -359,7 +359,7 @@ proof (eq p)
fix x q u
assuming "x: A" "q: x = z" "u: P x"
show "transp P q (transp P (refl x) u) = transp P ((refl x) \<bullet> q) u"
- by (eq q) (reduce, refl)
+ by (eq q) (compute, refl)
qed
Lemma (def) transport_compose_typefam:
@@ -371,7 +371,7 @@ Lemma (def) transport_compose_typefam:
"p: x = y"
"u: P (f x)"
shows "transp (fn x. P (f x)) p u = transp P f[p] u"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
Lemma (def) transport_function_family:
assumes
@@ -383,7 +383,7 @@ Lemma (def) transport_function_family:
"u: P x"
"p: x = y"
shows "transp Q p ((f x) u) = (f y) (transp P p u)"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
Lemma (def) transport_const:
assumes
@@ -391,7 +391,7 @@ Lemma (def) transport_const:
"x: A" "y: A"
"p: x = y"
shows "\<Prod>b: B. transp (fn _. B) p b = b"
- by intro (eq p, reduce, refl)
+ by intro (eq p, compute, refl)
definition transport_const_i ("transp'_c")
where [implicit]: "transp_c B p \<equiv> transport_const {} B {} {} p"
@@ -403,7 +403,7 @@ Lemma transport_const_comp [comp]:
"x: A" "b: B"
"A: U i" "B: U i"
shows "transp_c B (refl x) b \<equiv> refl b"
- unfolding transport_const_def by reduce
+ unfolding transport_const_def by compute
Lemma (def) pathlift:
assumes
@@ -413,7 +413,7 @@ Lemma (def) pathlift:
"p: x = y"
"u: P x"
shows "<x, u> = <y, transp P p u>"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
definition pathlift_i ("lift")
where [implicit]: "lift P p u \<equiv> pathlift {} P {} {} p u"
@@ -427,7 +427,7 @@ Lemma pathlift_comp [comp]:
"\<And>x. x: A \<Longrightarrow> P x: U i"
"A: U i"
shows "lift P (refl x) u \<equiv> refl <x, u>"
- unfolding pathlift_def by reduce
+ unfolding pathlift_def by compute
Lemma (def) pathlift_fst:
assumes
@@ -437,7 +437,7 @@ Lemma (def) pathlift_fst:
"u: P x"
"p: x = y"
shows "fst[lift P p u] = p"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
section \<open>Dependent paths\<close>
@@ -450,7 +450,7 @@ Lemma (def) apd:
"x: A" "y: A"
"p: x = y"
shows "transp P p (f x) = f y"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
definition apd_i ("apd")
where [implicit]: "apd f p \<equiv> Identity.apd {} {} f {} {} p"
@@ -464,7 +464,7 @@ Lemma dependent_map_comp [comp]:
"A: U i"
"\<And>x. x: A \<Longrightarrow> P x: U i"
shows "apd f (refl x) \<equiv> refl (f x)"
- unfolding apd_def by reduce
+ unfolding apd_def by compute
Lemma (def) apd_ap:
assumes
@@ -473,7 +473,7 @@ Lemma (def) apd_ap:
"x: A" "y: A"
"p: x = y"
shows "apd f p = transp_c B p (f x) \<bullet> f[p]"
- by (eq p) (reduce, refl)
+ by (eq p) (compute, refl)
section \<open>Whiskering\<close>
@@ -519,12 +519,12 @@ translations
Lemma whisker_refl [comp]:
assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\<alpha>: p = q"
shows "\<alpha> \<bullet>\<^sub>r (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>"
- unfolding right_whisker_def by reduce
+ unfolding right_whisker_def by compute
Lemma refl_whisker [comp]:
assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\<alpha>: p = q"
shows "(refl a) \<bullet>\<^sub>l \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>"
- unfolding left_whisker_def by reduce
+ unfolding left_whisker_def by compute
method left_whisker = (rule left_whisker)
method right_whisker = (rule right_whisker)
@@ -569,7 +569,7 @@ Lemma (def) horiz_pathcomp_eq_horiz_pathcomp':
unfolding horiz_pathcomp_def horiz_pathcomp'_def
apply (eq \<alpha>, eq \<beta>)
focus vars p apply (eq p)
- focus vars a _ _ _ r by (eq r) (reduce, refl)
+ focus vars a _ _ _ r by (eq r) (compute, refl)
done
done
@@ -604,14 +604,14 @@ Lemma
and horiz_pathcomp'_type [type]: "\<alpha> \<star>' \<beta>: \<Omega>2 A a"
using assms
unfolding \<Omega>2.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def \<Omega>2_def
- by reduce+
+ by compute+
Lemma (def) pathcomp_eq_horiz_pathcomp:
assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
shows "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>"
unfolding \<Omega>2.horiz_pathcomp_def
using assms[unfolded \<Omega>2_def, type] (*TODO: A `noting` keyword that puts the noted theorem into [type]*)
- proof (reduce, rule pathinv)
+ proof (compute, rule pathinv)
have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>"
by (rule pathcomp_refl)
also have ".. = \<alpha>" by (rule refl_pathcomp)
@@ -633,7 +633,7 @@ Lemma (def) pathcomp_eq_horiz_pathcomp':
shows "\<alpha> \<star>' \<beta> = \<beta> \<bullet> \<alpha>"
unfolding \<Omega>2.horiz_pathcomp'_def
using assms[unfolded \<Omega>2_def, type]
- proof reduce
+ proof compute
have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>"
by (rule pathcomp_refl)
also have ".. = \<beta>" by (rule refl_pathcomp)
@@ -660,7 +660,7 @@ Lemma (def) eckmann_hilton:
also have [simplified comp]: ".. = \<alpha> \<star>' \<beta>"
\<comment> \<open>Danger! Inferred implicit has an equivalent form but needs to be
manually simplified.\<close>
- by (transport eq: \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp') refl
+ by (rewr eq: \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp') refl
also have ".. = \<beta> \<bullet> \<alpha>"
by (rule pathcomp_eq_horiz_pathcomp')
finally show "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>"
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 1aa7932..33a5d0a 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -70,27 +70,27 @@ Lemma add_type [type]:
Lemma add_zero [comp]:
assumes "m: Nat"
shows "m + 0 \<equiv> m"
- unfolding add_def by reduce
+ unfolding add_def by compute
Lemma add_suc [comp]:
assumes "m: Nat" "n: Nat"
shows "m + suc n \<equiv> suc (m + n)"
- unfolding add_def by reduce
+ unfolding add_def by compute
Lemma (def) zero_add:
assumes "n: Nat"
shows "0 + n = n"
apply (elim n)
- \<^item> by (reduce; intro)
- \<^item> vars _ ih by reduce (eq ih; refl)
+ \<^item> by (compute; intro)
+ \<^item> vars _ ih by compute (eq ih; refl)
done
Lemma (def) suc_add:
assumes "m: Nat" "n: Nat"
shows "suc m + n = suc (m + n)"
apply (elim n)
- \<^item> by reduce refl
- \<^item> vars _ ih by reduce (eq ih; refl)
+ \<^item> by compute refl
+ \<^item> vars _ ih by compute (eq ih; refl)
done
Lemma (def) suc_eq:
@@ -102,19 +102,19 @@ Lemma (def) add_assoc:
assumes "l: Nat" "m: Nat" "n: Nat"
shows "l + (m + n) = l + m+ n"
apply (elim n)
- \<^item> by reduce intro
- \<^item> vars _ ih by reduce (eq ih; refl)
+ \<^item> by compute intro
+ \<^item> vars _ ih by compute (eq ih; refl)
done
Lemma (def) add_comm:
assumes "m: Nat" "n: Nat"
shows "m + n = n + m"
apply (elim n)
- \<^item> by (reduce; rule zero_add[symmetric])
+ \<^item> by (compute; rule zero_add[symmetric])
\<^item> vars n ih
- proof reduce
+ proof compute
have "suc (m + n) = suc (n + m)" by (eq ih) refl
- also have ".. = suc n + m" by (transport eq: suc_add) refl
+ also have ".. = suc n + m" by (rewr eq: suc_add) refl
finally show "?" by this
qed
done
@@ -131,27 +131,27 @@ Lemma mul_type [type]:
Lemma mul_zero [comp]:
assumes "n: Nat"
shows "n * 0 \<equiv> 0"
- unfolding mul_def by reduce
+ unfolding mul_def by compute
Lemma mul_one [comp]:
assumes "n: Nat"
shows "n * 1 \<equiv> n"
- unfolding mul_def by reduce
+ unfolding mul_def by compute
Lemma mul_suc [comp]:
assumes "m: Nat" "n: Nat"
shows "m * suc n \<equiv> m + m * n"
- unfolding mul_def by reduce
+ unfolding mul_def by compute
Lemma (def) zero_mul:
assumes "n: Nat"
shows "0 * n = 0"
apply (elim n)
- \<^item> by reduce refl
+ \<^item> by compute refl
\<^item> vars n ih
- proof reduce
+ proof compute
have "0 + 0 * n = 0 + 0 " by (eq ih) refl
- also have ".. = 0" by reduce refl
+ also have ".. = 0" by compute refl
finally show "?" by this
qed
done
@@ -160,11 +160,11 @@ Lemma (def) suc_mul:
assumes "m: Nat" "n: Nat"
shows "suc m * n = m * n + n"
apply (elim n)
- \<^item> by reduce refl
+ \<^item> by compute refl
\<^item> vars n ih
- proof (reduce, transport eq: \<open>ih:_\<close>)
+ 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 (transport eq: add_assoc) refl
+ also have ".. = suc (m + m * n + n)" by (rewr eq: add_assoc) refl
finally show "?" by this
qed
done
@@ -173,13 +173,13 @@ Lemma (def) mul_dist_add:
assumes "l: Nat" "m: Nat" "n: Nat"
shows "l * (m + n) = l * m + l * n"
apply (elim n)
- \<^item> by reduce refl
+ \<^item> by compute refl
\<^item> vars n ih
- proof reduce
+ proof compute
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)
- also have ".. = l * m + l + l * n" by (transport eq: add_comm) refl
- also have ".. = l * m + (l + l * n)" by (transport eq: add_assoc) refl
+ 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
qed
done
@@ -188,11 +188,11 @@ Lemma (def) mul_assoc:
assumes "l: Nat" "m: Nat" "n: Nat"
shows "l * (m * n) = l * m * n"
apply (elim n)
- \<^item> by reduce refl
+ \<^item> by compute refl
\<^item> vars n ih
- proof reduce
+ 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 (transport eq: \<open>ih:_\<close>) refl
+ also have ".. = l * m + l * m * n" by (rewr eq: \<open>ih:_\<close>) refl
finally show "?" by this
qed
done
@@ -201,12 +201,12 @@ Lemma (def) mul_comm:
assumes "m: Nat" "n: Nat"
shows "m * n = n * m"
apply (elim n)
- \<^item> by reduce (transport eq: zero_mul, refl)
+ \<^item> by compute (rewr eq: zero_mul, refl)
\<^item> vars n ih
- proof (reduce, rule pathinv)
+ proof (compute, rule pathinv)
have "suc n * m = n * m + m" by (rule suc_mul)
also have ".. = m + m * n"
- by (transport eq: \<open>ih:_\<close>, transport eq: add_comm) refl
+ by (rewr eq: \<open>ih:_\<close>, rewr eq: add_comm) refl
finally show "?" by this
qed
done