diff options
Diffstat (limited to 'hott')
| -rw-r--r-- | hott/Equivalence.thy | 12 | ||||
| -rw-r--r-- | hott/Identity.thy | 23 | ||||
| -rw-r--r-- | hott/Nat.thy | 12 |
3 files changed, 24 insertions, 23 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index 8007b89..c888714 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -160,7 +160,7 @@ Corollary (def) commute_homotopy': 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 + finally have "?" by infer thus "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+) qed @@ -240,7 +240,7 @@ Lemma (def) funcomp_is_qinv: 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 compute fact - finally show "?" by this + finally show "?" by infer qed show "(g \<circ> f) \<circ> finv \<circ> ginv ~ id C" @@ -248,7 +248,7 @@ Lemma (def) funcomp_is_qinv: 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 compute fact - finally show "?" by this + finally show "?" by infer qed qed done @@ -313,10 +313,10 @@ Lemma (def) is_qinv_if_is_biinv: also have ".. ~ g \<circ> f \<circ> h" by rhtpy (rule \<open>H2:_\<close>[symmetric]) 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) + finally have "g ~ h" by infer + then have "f \<circ> g ~ f \<circ> h" by (rhtpy, infer) also note \<open>H2:_\<close> - finally show "f \<circ> g ~ id B" by this + finally show "f \<circ> g ~ id B" by infer qed done done diff --git a/hott/Identity.thy b/hott/Identity.thy index ce0e0ec..6c044b4 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -203,6 +203,7 @@ Lemma (def) ap: shows "f x = f y" by (eq p) intro + definition ap_i ("_[_]" [1000, 0]) where [implicit]: "ap_i f p \<equiv> ap {} {} {} {} f p" @@ -304,7 +305,7 @@ Lemma (def) pathcomp_cancel_left: by (rewr eq: pathcomp_assoc, rewr eq: inv_pathcomp, rewr eq: refl_pathcomp) refl - finally show "?" by this + finally show "?" by infer qed Lemma (def) pathcomp_cancel_right: @@ -323,7 +324,7 @@ Lemma (def) pathcomp_cancel_right: rewr eq: pathcomp_assoc[symmetric], rewr eq: pathcomp_inv, rewr eq: pathcomp_refl) refl - finally show "?" by this + finally show "?" by infer qed method pathcomp_cancell = rule pathcomp_cancel_left[rotated 7] @@ -488,7 +489,7 @@ Lemma (def) right_whisker: have "s \<bullet> refl x = s" by (rule pathcomp_refl) also have ".. = t" by fact also have ".. = t \<bullet> refl x" by (rule pathcomp_refl[symmetric]) - finally show "?" by this + finally show "?" by infer qed done @@ -502,7 +503,7 @@ Lemma (def) left_whisker: have "refl x \<bullet> s = s" by (rule refl_pathcomp) also have ".. = t" by fact also have ".. = refl x \<bullet> t" by (rule refl_pathcomp[symmetric]) - finally show "?" by this + finally show "?" by infer qed done @@ -608,17 +609,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp: 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) - finally have eq\<alpha>: "? = \<alpha>" by this + finally have eq\<alpha>: "? = \<alpha>" by infer 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) - finally have eq\<beta>: "? = \<beta>" by this + finally have eq\<beta>: "? = \<beta>" by infer have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a)) = \<alpha> \<bullet> ?" by right_whisker (fact eq\<alpha>) also have ".. = \<alpha> \<bullet> \<beta>" by left_whisker (fact eq\<beta>) - finally show "? = \<alpha> \<bullet> \<beta>" by this + finally show "? = \<alpha> \<bullet> \<beta>" by infer qed Lemma (def) pathcomp_eq_horiz_pathcomp': @@ -630,17 +631,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp': 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) - finally have eq\<beta>: "? = \<beta>" by this + finally have eq\<beta>: "? = \<beta>" by infer 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) - finally have eq\<alpha>: "? = \<alpha>" by this + finally have eq\<alpha>: "? = \<alpha>" by infer have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a)) = \<beta> \<bullet> ?" by right_whisker (fact eq\<beta>) also have ".. = \<beta> \<bullet> \<alpha>" by left_whisker (fact eq\<alpha>) - finally show "? = \<beta> \<bullet> \<alpha>" by this + finally show "? = \<beta> \<bullet> \<alpha>" by infer qed Lemma (def) eckmann_hilton: @@ -657,7 +658,7 @@ Lemma (def) eckmann_hilton: also have ".. = \<beta> \<bullet> \<alpha>" by (rule pathcomp_eq_horiz_pathcomp') finally show "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>" - by this + by infer qed end 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 |