(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)

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