{Co,}Inductive rule labels now replace conj'ns entirely

Build at -t (with new test cases in tools/Holmake/tests/quote-filter/)
passes.

Closes #1154

doc/next-release.md

@@ -6,7 +6,7 @@
 (Released: xxxxxx)
 
 We are pleased to announce the Trindemossen 1 release of HOL4.
-We have changed the name (from Kananaskis) because of the kernel change reflected by the new efficient compute tool (see below).
+We have changed the name (from Kananaskis) because of the kernel change reflected by the new efficient compute tool (see [below](#verified-comp)).
 
 Contents
 --------
@@ -96,7 +96,7 @@ New tools:
     To use the library, it has to be loaded before the functions that should be
     evaluated are **defined**.
 
-- **Fast in-logic computation primitive**:
+- <a name="verified-comp">**Fast in-logic computation primitive**:</a>
   A port of the Candle theorem prover's primitive rule for computation, described in the paper *"Fast, Verified Computation for Candle"* (ITP 2023), has been added to the kernel.
   The new compute primitive works on certain operations on a lisp-like datatype of pairs of numbers:
 
@@ -244,6 +244,54 @@ Incompatibilities:
     The failure to flag the second as an error meant that the theorem called `xor_F` completely masked the rewrite in the opposite direction.
     The fix was to rename the second `xor_F` to now be `F_xor`, which is an incompatibility if your theory depends on `extra_boolTheory`.
 
+*   The labels for clauses/rules in the “modern” `Inductive` syntax are now syntactically equivalent to conjunctions, so what used to be written as something like
+
+           Inductive reln:
+           [~name1:] (!x y. x < y ==> reln (x + 1) y) /\
+           [~sym:]
+              (!x y. reln x y ==> reln y x) /\
+           [~zero:]
+              (!x. reln x 0)
+           End
+
+    should now be written
+
+           Inductive reln:
+           [~name1:] (!x y. x < y ==> reln (x + 1) y)
+           [~sym:]
+              (!x y. reln x y ==> reln y x)
+           [~zero:]
+              (!x. reln x 0)
+           End
+
+     where all of the trailing/separating conjunctions have been removed.
+     The parentheses around each clause above can also be removed, if desired.
+
+     Attempting to mix labels and top-level conjunctions will lead to very confusing results: it’s best to only use one or the other.
+     If you do not wish to name rules, you can use any of the following as “nullary” labels: `[]`, `[/\]`, or `[∧]`.
+     As with normal labels, these need to occur in column zero.
+
+     The first rule need not have a label at all, so that
+
+           Inductive reln:
+              !x y. x < y ==> reln (x + 1) y
+           [/\]
+              !x y. reln x y ==> reln y x
+           [~zero:]
+              !x. reln x 0
+           End
+
+     will work.
+     It will also work to switch to conjunctions for trailing rules:
+
+           Inductive reln:
+           [~name1:] !x y. x < y ==> reln (x + 1) y
+           [~sym:]
+              (!x y. reln x y ==> reln y x) /\
+              (!x. reln x 0) /\
+              (!y. reln 100 y)
+           End
+
 * * * * *
 
 <div class="footer">

examples/formal-languages/context-free/pegScript.sml

@@ -100,71 +100,71 @@ QED
 (* Option type should be replaced with sum type (loc. for NONE *)
 Inductive peg_eval:
 [~empty:]
-  (∀s c. peg_eval G (s, empty c) (Success s c NONE)) ∧
+  (∀s c. peg_eval G (s, empty c) (Success s c NONE))
 [~nt:]
   (∀n s f res.
        n ∈ FDOM G.rules ∧ peg_eval G (s, G.rules ' n) res ⇒
-       peg_eval G (s, nt n f) (resultmap f res)) ∧
+       peg_eval G (s, nt n f) (resultmap f res))
 [~any_success:]
-  (∀h t f. peg_eval G (h::t, any f) (Success t (f h) NONE)) ∧
+  (∀h t f. peg_eval G (h::t, any f) (Success t (f h) NONE))
 [~any_failure:]
-  (∀f. peg_eval G ([], any f) (Failure EOF G.anyEOF)) ∧
+  (∀f. peg_eval G ([], any f) (Failure EOF G.anyEOF))
 [~tok_success:]
   (∀e t P f.
-     P (FST e) ⇒ peg_eval G (e::t, tok P f) (Success t (f e) NONE)) ∧
+     P (FST e) ⇒ peg_eval G (e::t, tok P f) (Success t (f e) NONE))
 [~tok_failureF:]
   (∀h t P f.
      ¬P (FST h) ⇒
-     peg_eval G (h::t, tok P f) (Failure (SND h) G.tokFALSE)) ∧
+     peg_eval G (h::t, tok P f) (Failure (SND h) G.tokFALSE))
 [~tok_failureEOF:]
-  (∀P f. peg_eval G ([], tok P f) (Failure EOF G.tokEOF)) ∧
+  (∀P f. peg_eval G ([], tok P f) (Failure EOF G.tokEOF))
 [~not_success:]
   (∀e s c fr.
      peg_eval G (s, e) fr ∧ isFailure fr ⇒
-     peg_eval G (s, not e c) (Success s c NONE)) ∧
+     peg_eval G (s, not e c) (Success s c NONE))
 [~not_failure:]
   (∀e s r c.
      peg_eval G (s, e) r ∧ isSuccess r ⇒
-     peg_eval G (s, not e c) (Failure (sloc s) G.notFAIL))  ∧
+     peg_eval G (s, not e c) (Failure (sloc s) G.notFAIL))
 [~seq_fail1:]
   (∀e1 e2 s f fl fe.
      peg_eval G (s, e1) (Failure fl fe) ⇒
-     peg_eval G (s, seq e1 e2 f) (Failure fl fe))  ∧
+     peg_eval G (s, seq e1 e2 f) (Failure fl fe))
 [~seq_fail2:]
   (∀e1 e2 f s0 eo s1 c1 fl fe.
      peg_eval G (s0, e1) (Success s1 c1 eo) ∧
      peg_eval G (s1, e2) (Failure fl fe) ⇒
-     peg_eval G (s0, seq e1 e2 f) (Failure fl fe)) ∧
+     peg_eval G (s0, seq e1 e2 f) (Failure fl fe))
 [~seq_success:]
   (∀e1 e2 s0 s1 s2 c1 c2 f eo1 eo2.
      peg_eval G (s0, e1) (Success s1 c1 eo1) ∧
      peg_eval G (s1, e2) (Success s2 c2 eo2) ⇒
-     peg_eval G (s0, seq e1 e2 f) (Success s2 (f c1 c2) eo2)) ∧
+     peg_eval G (s0, seq e1 e2 f) (Success s2 (f c1 c2) eo2))
 [~choice_fail:]
   (∀e1 e2 s f fl1 fe1 fl2 fe2.
      peg_eval G (s, e1) (Failure fl1 fe1) ∧
      peg_eval G (s, e2) (Failure fl2 fe2) ⇒
      peg_eval G (s, choice e1 e2 f)
-              (UNCURRY Failure (MAXerr (fl1,fe1) (fl2,fe2)))) ∧
+              (UNCURRY Failure (MAXerr (fl1,fe1) (fl2,fe2))))
 [~choice_success1:]
   (∀e1 e2 s0 f s r eo.
      peg_eval G (s0, e1) (Success s r eo) ⇒
-     peg_eval G (s0, choice e1 e2 f) (Success s (f (INL r)) eo)) ∧
+     peg_eval G (s0, choice e1 e2 f) (Success s (f (INL r)) eo))
 [~choice_success2:]
   (∀e1 e2 s0 s r eo f fl fe.
      peg_eval G (s0, e1) (Failure fl fe) ∧
      peg_eval G (s0, e2) (Success s r eo) ⇒
      peg_eval G (s0, choice e1 e2 f)
-              (Success s (f (INR r)) (optmax MAXerr (SOME (fl,fe)) eo))) ∧
+              (Success s (f (INR r)) (optmax MAXerr (SOME (fl,fe)) eo)))
 [~error:]
-  (∀e s. peg_eval G (s, error e) (Failure (sloc s) e)) ∧
+  (∀e s. peg_eval G (s, error e) (Failure (sloc s) e))
 [~rpt:]
   (∀e f s s1 list err.
      peg_eval_list G (s, e) (s1,list,err) ⇒
-     peg_eval G (s, rpt e f) (Success s1 (f list) (SOME err))) ∧
+     peg_eval G (s, rpt e f) (Success s1 (f list) (SOME err)))
 [~list_nil:]
   (∀e s fl fe. peg_eval G (s, e) (Failure fl fe) ⇒
-               peg_eval_list G (s, e) (s,[],(fl,fe))) ∧
+               peg_eval_list G (s, e) (s,[],(fl,fe)))
 [~list_cons:]
   (∀e eo0 eo s0 s1 s2 c cs.
      peg_eval G (s0, e) (Success s1 c eo0) ∧
@@ -379,13 +379,13 @@ QED
 Theorem lemma4_1a = lemma4_1a0 |> SIMP_RULE (srw_ss() ++ DNF_ss) [AND_IMP_INTRO]
 
 Inductive wfpeg:
-  (∀n f. n ∈ FDOM G.rules ∧ wfpeg G (G.rules ' n) ⇒ wfpeg G (nt n f)) ∧
+  (∀n f. n ∈ FDOM G.rules ∧ wfpeg G (G.rules ' n) ⇒ wfpeg G (nt n f))
 [~_empty[simp]:]
-  (∀c. wfpeg G (empty c)) ∧
+  (∀c. wfpeg G (empty c))
 [~_any[simp]:]
-  (∀f. wfpeg G (any f)) ∧
+  (∀f. wfpeg G (any f))
 [~tok[simp]:]
-  (∀t f. wfpeg G (tok t f)) ∧
+  (∀t f. wfpeg G (tok t f))
 [~_error[simp]:]
   (∀e. wfpeg G (error e)) ∧
   (∀e c. wfpeg G e ⇒ wfpeg G (not e c)) ∧

examples/lambda/barendregt/chap2Script.sml

@@ -79,19 +79,19 @@ val one_hole_is_normal = store_thm(
 
 Inductive lameq :
 [~BETA:]
-     (!x M N. (LAM x M) @@ N == [N/x]M) /\
+  !x M N. (LAM x M) @@ N == [N/x]M
 [~REFL:]
-     (!M. M == M) /\
+  !M. M == M
 [~SYM:]
-     (!M N. M == N ==> N == M) /\
+  !M N. M == N ==> N == M
 [~TRANS:]
-     (!M N L. M == N /\ N == L ==> M == L) /\
+  !M N L. M == N /\ N == L ==> M == L
 [~APPL:]
-     (!M N Z. M == N ==> M @@ Z == N @@ Z) /\
+  !M N Z. M == N ==> M @@ Z == N @@ Z
 [~APPR:]
-     (!M N Z. M == N ==> Z @@ M == Z @@ N) /\
+  !M N Z. M == N ==> Z @@ M == Z @@ N
 [~ABS:]
-     (!M N x. M == N ==> LAM x M == LAM x N)
+  !M N x. M == N ==> LAM x M == LAM x N
 End
 
 Theorem lameq_refl[simp] = lameq_REFL
@@ -278,21 +278,21 @@ End
  *)
 Inductive asmlam :
 [~eqn:]
-  (!M N. (M,N) IN eqns ==> asmlam eqns M N) /\
+  !M N. (M,N) IN eqns ==> asmlam eqns M N
 [~beta:]
-  (!x M N. asmlam eqns (LAM x M @@ N) ([N/x]M)) /\
+  !x M N. asmlam eqns (LAM x M @@ N) ([N/x]M)
 [~refl:]
-  (!M. asmlam eqns M M) /\
+  !M. asmlam eqns M M
 [~sym:]
-  (!M N. asmlam eqns M N ==> asmlam eqns N M) /\
+  !M N. asmlam eqns M N ==> asmlam eqns N M
 [~trans:]
-  (!M N P. asmlam eqns M N /\ asmlam eqns N P ==> asmlam eqns M P) /\
+  !M N P. asmlam eqns M N /\ asmlam eqns N P ==> asmlam eqns M P
 [~lcong:]
-  (!M M' N. asmlam eqns M M' ==> asmlam eqns (M @@ N) (M' @@ N)) /\
+  !M M' N. asmlam eqns M M' ==> asmlam eqns (M @@ N) (M' @@ N)
 [~rcong:]
-  (!M N N'. asmlam eqns N N' ==> asmlam eqns (M @@ N) (M @@ N')) /\
+  !M N N'. asmlam eqns N N' ==> asmlam eqns (M @@ N) (M @@ N')
 [~abscong:]
-  (!x M M'. asmlam eqns M M' ==> asmlam eqns (LAM x M) (LAM x M'))
+  !x M M'. asmlam eqns M M' ==> asmlam eqns (LAM x M) (LAM x M')
 End
 
 (* Definition 2.1.32 [1, p.33]

examples/lambda/barendregt/head_reductionScript.sml

@@ -13,9 +13,9 @@ val _ = ParseExtras.temp_loose_equality()
 fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n]
 
 Inductive hreduce1 :
-  (∀v M N. hreduce1 (LAM v M @@ N) ([N/v]M)) ∧
+  (∀v M N. hreduce1 (LAM v M @@ N) ([N/v]M))
 [~LAM:]
-  (∀v M1 M2. hreduce1 M1 M2 ⇒ hreduce1 (LAM v M1) (LAM v M2)) ∧
+  (∀v M1 M2. hreduce1 M1 M2 ⇒ hreduce1 (LAM v M1) (LAM v M2))
 [~APP:]
   (∀M1 M2 N. hreduce1 M1 M2 ∧ ¬is_abs M1 ⇒ hreduce1 (M1 @@ N) (M2 @@ N))
 End

examples/lambda/examples/holScript.sml

@@ -113,12 +113,12 @@ QED
 
 Inductive aeq:
 [~var:]
-  (!v. aeq (rhvar v) (rhvar v)) /\
+  (!v. aeq (rhvar v) (rhvar v))
 [~const:]
-  (!v. aeq (rhconst v) (rhconst v)) /\
+  (!v. aeq (rhconst v) (rhconst v))
 [~app:]
   (!t1 t2 u1 u2. aeq t1 u1 /\ aeq t2 u2 ==>
-                 aeq (rhapp t1 t2) (rhapp u1 u2)) /\
+                 aeq (rhapp t1 t2) (rhapp u1 u2))
 [~lam:]
   (!v1 v2 u t z ty.
       ~(z IN allvars ty t) /\ ~(z IN allvars ty u) /\ ~(z = v1) /\

examples/lambda/typing/sttScript.sml

@@ -356,11 +356,11 @@ QED
 Inductive gentype:
 [~VAR:]
   (∀Γ s τ.
-     valid_ctxt Γ ∧ MEM (s,τ) Γ ⇒ gentype Γ (VAR s : term) τ {(Γ,VAR s,τ)}) ∧
+     valid_ctxt Γ ∧ MEM (s,τ) Γ ⇒ gentype Γ (VAR s : term) τ {(Γ,VAR s,τ)})
 [~APP:]
   (∀Γ M N A B fs xs.
      gentype Γ M (A → B) fs ∧ gentype Γ N A xs ⇒
-     gentype Γ (M @@ N) B ({(Γ,M @@ N,B)} ∪ fs ∪ xs)) ∧
+     gentype Γ (M @@ N) B ({(Γ,M @@ N,B)} ∪ fs ∪ xs))
 [~LAM:]
   (∀Γ v M A B bs.
      gentype ((v,A) :: Γ) M B bs ⇒
@@ -394,13 +394,13 @@ QED
 
 Inductive subterm:
 [~refl:]
-  (∀M:term Γ. FINITE Γ ∧ FV M ⊆ Γ ⇒ (subterm (Γ, M) (Γ, M))) ∧
+  (∀M:term Γ. FINITE Γ ∧ FV M ⊆ Γ ⇒ (subterm (Γ, M) (Γ, M)))
 [~appL:]
   (∀Γ Γ₀ M0 M N.
-     FV N ⊆ Γ ∧ subterm (Γ₀, M0) (Γ, M) ⇒ subterm (Γ₀, M0) (Γ, M @@ N)) ∧
+     FV N ⊆ Γ ∧ subterm (Γ₀, M0) (Γ, M) ⇒ subterm (Γ₀, M0) (Γ, M @@ N))
 [~appR:]
   (∀Γ₀ Γ N0 M N.
-     FV M ⊆ Γ ∧ subterm (Γ₀, N0) (Γ, N) ⇒ subterm (Γ₀, N0) (Γ, M @@ N)) ∧
+     FV M ⊆ Γ ∧ subterm (Γ₀, N0) (Γ, N) ⇒ subterm (Γ₀, N0) (Γ, M @@ N))
 [~lam:]
   (∀Γ₀ Γ v M N.
      v ∉ Γ ∧

examples/lambda/wcbv-reasonable/AbstractHeapMachineScript.sml

@@ -104,15 +104,15 @@ Inductive step:
 [~pushVal:]
   (∀P P' Q a T V H.
     jumpTarget 0 [] P = SOME (Q, P')
-    ⇒ step (closC (lamT::P) a::T, V, H) (closC P' a::T, closC Q a::V, H)) ∧
+    ⇒ step (closC (lamT::P) a::T, V, H) (closC P' a::T, closC Q a::V, H))
 [~beta:]
   (∀a b g P Q H H' c T V.
     put H (heapEntryC g b) = (H', c)
-    ⇒ step (closC (appT::P) a::T, g::closC Q b::V, H) (closC Q c::closC P a::T, V, H')) ∧
+    ⇒ step (closC (appT::P) a::T, g::closC Q b::V, H) (closC Q c::closC P a::T, V, H'))
 [~load:]
   (∀P a x g T V H.
     lookup H a x = SOME g
-    ⇒ step (closC (varT x::P) a::T, V, H) (closC P a::T, g::V, H)) ∧
+    ⇒ step (closC (varT x::P) a::T, V, H) (closC P a::T, g::V, H))
 [~nil:]
   (∀a T V H.
     step (closC [] a::T, V, H) (T, V, H))
@@ -125,18 +125,18 @@ End
 Inductive unfolds:
 [~Unbound:]
   (∀H k n.
-    n < k ⇒ unfolds H a k (dV n) (dV n)) ∧
+    n < k ⇒ unfolds H a k (dV n) (dV n))
 [~Bound:]
   (∀H k b P s s' n.
     k ≤ n ∧
     lookup H a (n-k) = SOME (closC P b) ∧
     reprP P s ∧
     unfolds H b 0 s s' ⇒
-    unfolds H a k (dV n) s') ∧
+    unfolds H a k (dV n) s')
 [~Lam:]
   (∀H k s s'.
     unfolds H a (SUC k) s s' ⇒
-    unfolds H a k (dABS s) (dABS s')) ∧
+    unfolds H a k (dABS s) (dABS s'))
 [~App:]
   (∀H k s t s' t'.
     unfolds H a k s s' ∧

examples/lambda/wcbv-reasonable/AbstractSubstMachineScript.sml

@@ -42,11 +42,11 @@ End
 
 Inductive step:
 [~pushVal:]
-  (∀P P' Q T V.
-    jumpTarget 0 [] P = SOME (Q,P') ⇒ step ((lamT::P)::T,V) (tc P' T,Q::V)) ∧
+  ∀P P' Q T V.
+    jumpTarget 0 [] P = SOME (Q,P') ⇒ step ((lamT::P)::T,V) (tc P' T,Q::V)
 [~beta:]
-  (∀P Q R T V.
-    step ((appT::P)::T,Q::R::V) (substP R 0 (lamT::Q++[retT])::tc P T,V))
+  ∀P Q R T V.
+    step ((appT::P)::T,Q::R::V) (substP R 0 (lamT::Q++[retT])::tc P T,V)
 End
 
 Definition init:

examples/lambda/wcbv-reasonable/PrelimsScript.sml

@@ -278,13 +278,13 @@ QED
 (* reduce while keeping track of the maximum size of terms *)
 Inductive redWithMaxSize:
 [~R:]
-        (∀size step (m: num) s. m = size s ⇒ redWithMaxSize size step m s s) ∧
+  ∀size step (m: num) s. m = size s ⇒ redWithMaxSize size step m s s
 [~C:]
-        (∀size step (s: 'a) (s': 'a) (t: 'a) (m: num) (m':num).
-                step s s' ∧
-                redWithMaxSize size step m' s' t ∧
-                m = MAX (size s) m' ⇒
-                redWithMaxSize size step m s t)
+  ∀size step (s: 'a) (s': 'a) (t: 'a) (m: num) (m':num).
+    step s s' ∧
+    redWithMaxSize size step m' s' t ∧
+    m = MAX (size s) m' ⇒
+    redWithMaxSize size step m s t
 End
 
 Theorem redWithMaxSize_ge: