jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 78 forks source link

Add `(un)set_then_multiple_subgoals` to control the behavior of THEN #113

Closed aqjune-aws closed 1 month ago

aqjune-aws commented 1 month ago

This patch adds unset_then_multiple_subgoals and set_then_multiple_subgoals that controls the behavior of THEN with respect to the number of subgoals that its first tactic generated.

This is useful when one wants to check whether a proof written using THEN can be syntactically converted to the e-g form. If this flag is set to true, t1 THEN t2 THEN .. can be converted to e(t1);; e(t2);; ... (modulo the validity check). To roll back the behavior of THEN to the default version, use set_then_multiple_subgoals.

  # prove(`x + 1 = 1 + x /\ x + 2 = 2 + x`, CONJ_TAC THEN ARITH_TAC);;
  val it : thm = |- x + 1 = 1 + x /\ x + 2 = 2 + x

  # unset_then_multiple_subgoals;;
  val it : bool = false
  # prove(`x + 1 = 1 + x /\ x + 2 = 2 + x`, CONJ_TAC THEN ARITH_TAC);;
  Exception: Failure "seqapply: Length mismatch".
  # prove(`x + 1 = 1 + x /\ x + 2 = 2 + x`, CONJ_TAC THENL [ARITH_TAC; ARITH_TAC]);;
  val it : thm = |- x + 1 = 1 + x /\ x + 2 = 2 + x
  # prove(`x + 1 = 1 + x /\ x + 2 = 2 + x`, CONJ_TAC THENL (replicate ARITH_TAC 2));;
  val it : thm = |- x + 1 = 1 + x /\ x + 2 = 2 + x

Also, this patch adds a Help document for unset_jrh_lexer which was missing (but not set_jrh_lexer for brevity; the command is simply mentioned in unset_jrh_lexer).

aqjune-aws commented 1 month ago

As a sanity check I turned this flag on and ran BIGNUM_COPY_CORRECT and it worked well. :)

aqjune-aws commented 1 month ago

This is my trial to change their types from bool to (preprocessor keyword). :) I omitted their actual OCaml type which is bool because it seemed less important. Also slightly edited the sentences from called to read by a preprocessor.

--

Slightly updated the sentences further to remove usage of 'flag'.