(FEAT) Context data slots for known types and conditional type rules, as well as a separate one for judgmental equality rules.

(REF) Goal statement assumptions are now put into the new context data slots.

(FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data.

(REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context.
  MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`.

(REF) Fixed incompatibilities in theories.

3 files changed, 47 insertions, 48 deletions

diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 7d1f2b1..a57ed44 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -52,7 +52,7 @@ Lemma (def) hsym:
   shows "g ~ f"
   unfolding homotopy_def
   proof intro
-    fix x assume "x: A" then have "f x = g x"
+    fix x assuming "x: A" then have "f x = g x"
       by (htpy H)
     thus "g x = f x"
       by (rule pathinv) fact
@@ -70,7 +70,7 @@ Lemma (def) htrans:
   shows "f ~ h"
   unfolding homotopy_def
   proof intro
-    fix x assume "x: A"
+    fix x assuming "x: A"
     have *: "f x = g x" "g x = h x"
       by (htpy H1, htpy H2)
     show "f x = h x"
@@ -119,7 +119,7 @@ Lemma funcomp_right_htpy:
   shows "(g \<circ> f) ~ (g \<circ> f')"
   unfolding homotopy_def
   proof (intro, reduce)
-    fix x assume "x: A"
+    fix x assuming "x: A"
     have *: "f x = f' x"
       by (htpy H)
     show "g (f x) = g (f' x)"
@@ -154,18 +154,18 @@ Corollary (def) commute_homotopy':
     "H: f ~ (id A)"
   shows "H (f x) = f [H x]"
   proof -
-    from \<open>H: f ~ id A\<close> have "H: \<Prod>x: A. f x = x"
+    from \<open>H: f ~ id A\<close> have [type]: "H: \<Prod>x: A. f x = x"
       by (reduce add: homotopy_def)
 
-    have "(id A)[H x]: f x = x"
+    have *: "(id A)[H x]: f x = x"
       by (rewrite at "\<hole> = _" id_comp[symmetric],
           rewrite at "_ = \<hole>" id_comp[symmetric])
 
     have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]"
-      by (rule left_whisker, transport eq: ap_id) (reduce+, refl)
+      by (rule left_whisker, fact *, transport eq: ap_id) (reduce+, 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 *: "{}" using * by this
 
     show "H (f x) = f [H x]"
       by pathcomp_cancelr (fact, typechk+)
@@ -179,7 +179,7 @@ subsection \<open>Quasi-inverses\<close>
 definition "is_qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A.
   homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A) \<times> homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B)"
 
-lemma is_qinv_type [type]:
+Lemma is_qinv_type [type]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "is_qinv A B f: U i"
   unfolding is_qinv_def
@@ -266,7 +266,7 @@ definition "is_biinv A B f \<equiv>
   (\<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A))
     \<times> (\<Sum>g: B \<rightarrow> A. homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))"
 
-lemma is_biinv_type [type]:
+Lemma is_biinv_type [type]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "is_biinv A B f: U i"
   unfolding is_biinv_def by typechk
@@ -365,7 +365,7 @@ text \<open>
 definition equivalence (infix "\<simeq>" 110)
   where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.is_biinv A B f"
 
-lemma equivalence_type [type]:
+Lemma equivalence_type [type]:
   assumes "A: U i" "B: U i"
   shows "A \<simeq> B: U i"
   unfolding equivalence_def by typechk
@@ -432,28 +432,24 @@ Lemma (def) equiv_if_equal:
       \<^enum> vars A B
         apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
         using [[solve_side_conds=1]]
-        apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric], fact)
+        apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
         apply (rule transport, rule Ui_in_USi)
-        apply (rule lift_universe_codomain, rule Ui_in_USi)
-        apply (typechk, rule Ui_in_USi)
-        by facts
+        by (rule lift_universe_codomain, rule Ui_in_USi)
       \<^enum> vars A
         using [[solve_side_conds=1]]
         apply (subst transport_comp)
           \<circ> by (rule Ui_in_USi)
           \<circ> by reduce (rule in_USi_if_in_Ui)
-          \<circ> by reduce (rule id_is_biinv, fact)
+          \<circ> by reduce (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])
       using [[solve_side_conds=1]]
-      apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric], fact)
+      apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
       apply (rule transport, rule Ui_in_USi)
-      apply (rule lift_universe_codomain, rule Ui_in_USi)
-      apply (typechk, rule Ui_in_USi)
-      by facts
+      by (rule lift_universe_codomain, rule Ui_in_USi)
   done
 
 (*Uncomment this to see all implicits from here on.
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 4829b6f..247d6a4 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -82,7 +82,7 @@ Lemma (def) pathinv:
   shows "y =\<^bsub>A\<^esub> x"
   by (eq p) intro
 
-lemma pathinv_comp [comp]:
+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
@@ -94,11 +94,11 @@ Lemma (def) pathcomp:
   shows
     "x =\<^bsub>A\<^esub> z"
   proof (eq p)
-    fix x q assume "x: A" and "q: x =\<^bsub>A\<^esub> z"
+    fix x q assuming "x: A" and "q: x =\<^bsub>A\<^esub> z"
     show "x =\<^bsub>A\<^esub> z" by (eq q) refl
   qed
 
-lemma pathcomp_comp [comp]:
+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
@@ -491,9 +491,9 @@ Lemma (def) right_whisker:
   shows "p \<bullet> r = q \<bullet> r"
   apply (eq r)
     focus vars x s t proof -
-      have "t \<bullet> refl x = t" by (rule pathcomp_refl)
-      also have ".. = s" by fact
-      also have ".. = s \<bullet> refl x" by (rule pathcomp_refl[symmetric])
+      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
     qed
   done
@@ -505,9 +505,9 @@ Lemma (def) left_whisker:
   shows "r \<bullet> p = r \<bullet> q"
   apply (eq r)
     focus vars x s t proof -
-      have "refl x \<bullet> t = t" by (rule refl_pathcomp)
-      also have ".. = s" by fact
-      also have ".. = refl x \<bullet> s" by (rule refl_pathcomp[symmetric])
+      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
     qed
   done
@@ -542,14 +542,13 @@ text \<open>Conditions under which horizontal path-composition is defined.\<clos
 locale horiz_pathcomposable =
 fixes
   i A a b c p q r s
-assumes assums:
+assumes [type]:
   "A: U i" "a: A" "b: A" "c: A"
   "p: a =\<^bsub>A\<^esub> b" "q: a =\<^bsub>A\<^esub> b"
   "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c"
 begin
 
 Lemma (def) horiz_pathcomp:
-  notes assums
   assumes "\<alpha>: p = q" "\<beta>: r = s"
   shows "p \<bullet> r = q \<bullet> s"
 proof (rule pathcomp)
@@ -560,7 +559,6 @@ qed typechk
 text \<open>A second horizontal composition:\<close>
 
 Lemma (def) horiz_pathcomp':
-  notes assums
   assumes "\<alpha>: p = q" "\<beta>: r = s"
   shows "p \<bullet> r = q \<bullet> s"
 proof (rule pathcomp)
@@ -572,13 +570,12 @@ notation horiz_pathcomp (infix "\<star>" 121)
 notation horiz_pathcomp' (infix "\<star>''" 121)
 
 Lemma (def) horiz_pathcomp_eq_horiz_pathcomp':
-  notes assums
   assumes "\<alpha>: p = q" "\<beta>: r = s"
   shows "\<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>"
   unfolding horiz_pathcomp_def horiz_pathcomp'_def
   apply (eq \<alpha>, eq \<beta>)
     focus vars p apply (eq p)
-      focus vars a q by (eq q) (reduce, refl)
+      focus vars a _ _ _ r by (eq r) (reduce, refl)
     done
   done
 
@@ -597,7 +594,7 @@ Lemma \<Omega>2_alt_def:
 
 section \<open>Eckmann-Hilton\<close>
 
-context fixes i A a assumes "A: U i" "a: A"
+context fixes i A a assumes [type]: "A: U i" "a: A"
 begin
 
 interpretation \<Omega>2:
@@ -619,14 +616,18 @@ 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_alt_def]
+  (*FIXME: Definitional unfolding + normalization; shouldn't need explicit
+    unfolding*)
+  using assms[unfolded \<Omega>2_alt_def, type]
   proof (reduce, rule pathinv)
     \<comment> \<open>Propositional equality rewriting needs to be improved\<close>
-    have "{} = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl)
+    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
 
-    have "{} = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl)
+    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
 
@@ -640,13 +641,15 @@ Lemma (def) pathcomp_eq_horiz_pathcomp':
   assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
   shows "\<alpha> \<star>' \<beta> = \<beta> \<bullet> \<alpha>"
   unfolding \<Omega>2.horiz_pathcomp'_def
-  using assms[unfolded \<Omega>2_alt_def]
+  using assms[unfolded \<Omega>2_alt_def, type]
   proof reduce
-    have "{} = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl)
+    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
 
-    have "{} = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl)
+    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
 
@@ -659,7 +662,7 @@ Lemma (def) pathcomp_eq_horiz_pathcomp':
 Lemma (def) eckmann_hilton:
   assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a"
   shows "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>"
-  using assms[unfolded \<Omega>2_alt_def]
+  using assms[unfolded \<Omega>2_alt_def, type]
   proof -
     have "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>"
       by (rule pathcomp_eq_horiz_pathcomp)
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 716703a..f45387c 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -62,17 +62,17 @@ subsection \<open>Addition\<close>
 
 definition add (infixl "+" 120) where "m + n \<equiv> NatRec Nat m (K suc) n"
 
-lemma add_type [type]:
+Lemma add_type [type]:
   assumes "m: Nat" "n: Nat"
   shows "m + n: Nat"
   unfolding add_def by typechk
 
-lemma add_zero [comp]:
+Lemma add_zero [comp]:
   assumes "m: Nat"
   shows "m + 0 \<equiv> m"
   unfolding add_def by reduce
 
-lemma add_suc [comp]:
+Lemma add_suc [comp]:
   assumes "m: Nat" "n: Nat"
   shows "m + suc n \<equiv> suc (m + n)"
   unfolding add_def by reduce
@@ -123,22 +123,22 @@ subsection \<open>Multiplication\<close>
 
 definition mul (infixl "*" 121) where "m * n \<equiv> NatRec Nat 0 (K $ add m) n"
 
-lemma mul_type [type]:
+Lemma mul_type [type]:
   assumes "m: Nat" "n: Nat"
   shows "m * n: Nat"
   unfolding mul_def by typechk
 
-lemma mul_zero [comp]:
+Lemma mul_zero [comp]:
   assumes "n: Nat"
   shows "n * 0 \<equiv> 0"
   unfolding mul_def by reduce
 
-lemma mul_one [comp]:
+Lemma mul_one [comp]:
   assumes "n: Nat"
   shows "n * 1 \<equiv> n"
   unfolding mul_def by reduce
 
-lemma mul_suc [comp]:
+Lemma mul_suc [comp]:
   assumes "m: Nat" "n: Nat"
   shows "m * suc n \<equiv> m + m * n"
   unfolding mul_def by reduce