aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
authorstuebinm2022-06-29 01:28:53 +0200
committerstuebinm2022-06-29 01:28:53 +0200
commit4fd7d22b0efb69bc13c43dae4e4c1bd6d392f37d (patch)
tree2819976f3fe60d2e9796ec37d2b0736df55daa59 /hott
parentcb4139dc35527bd8c8f9b70753c3d1f552c5f19d (diff)
(broken) update hott for Isabelle 2021-1HEADmaster
this just replaces all instance of `this` with instances of `infer`. Unfortunately, it looks likes something else also broke, and I have no idea what it is (but the proof for equiv_if_equal fails). Sadly this means we can't get to univalence for now … (but rn I'm too tired to try anything else with it)
Diffstat (limited to 'hott')
-rw-r--r--hott/Equivalence.thy12
-rw-r--r--hott/Identity.thy23
-rw-r--r--hott/Nat.thy12
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