Merge pull request #113 from aqjune-aws/then1

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

Help/THEN.hlp

@@ -18,6 +18,11 @@ The application of {THEN} to a pair of tactics never fails.
 The resulting tactic fails if {t1} fails when applied to the goal, or if
 {t2} does when applied to any of the resulting subgoals.
 
+If {unset_then_multiple_subgoals} is used, {THEN} is configured to fail
+when {t1} generates more than one subgoal.
+This is useful when one wants to check whether a proof written using {THEN} can
+be syntactically converted to the `e` form.
+
 \EXAMPLE
 Suppose we want to prove the inbuilt theorem {DELETE_INSERT} ourselves:
 {
@@ -61,6 +66,6 @@ If using this several times in succession, remember that {THEN} is
 left-associative.
 
 \SEEALSO
-EVERY, ORELSE, THENL.
+EVERY, ORELSE, THENL, unset_then_multiple_subgoals
 
 \ENDDOC

Help/unset_jrh_lexer.hlp

@@ -0,0 +1,34 @@
+\DOC unset_jrh_lexer
+
+\TYPE {unset_jrh_lexer : (preprocessor keyword)}
+
+\SYNOPSIS
+Updates the HOL Light preprocessor to respect OCaml's identifier convention.
+
+\DESCRIBE
+If a preprocessor reads {unset_jrh_lexer}, it switches its lexer to
+use OCaml's identifier convention. This makes an identifier starting with a
+capiter letter unusable as the name of a let binding, but enables using it as a
+module constructor.
+Modulo this side effect, {unset_jrh_lexer} is simply identical to {false}.
+The lexer can be enabled again using {set_jrh_lexer}, which is identical to
+{true} after preprocessing.
+
+\EXAMPLE
+{
+  # module OrdInt = struct type t = int let compare = (-) end;;
+  Toplevel input:
+  # module OrdInt = struct type t = int let compare = (-) end;;
+          ^^^^^^
+  Parse error: 'type' or [ext_attributes] expected after 'module' (in
+    [str_item])
+  # unset_jrh_lexer;;
+  val it : bool = false
+  # module OrdInt = struct type t = int let compare = (-) end;;
+  module OrdInt : sig type t = int val compare : int -> int -> int end
+}
+
+\FAILURE
+Never fails.
+
+\ENDDOC

Help/unset_then_multiple_subgoals.hlp

@@ -0,0 +1,48 @@
+\DOC unset_then_multiple_subgoals
+
+\TYPE {unset_then_multiple_subgoals : (preprocessor keyword)}
+
+\SYNOPSIS
+Updates the HOL Light preprocessor to read {THEN} as an alternative operator
+which fails if the first tactic creates more than one subgoal.
+
+\KEYWORDS
+tactical.
+
+\DESCRIBE
+If a preprocessor reads {unset_then_multiple_subgoals}, it starts to translate
+{t1 THEN t2} into {then1_ t1 t2} which fails when {t1} generates more than one
+subgoal.
+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 setting is on, {t1 THEN t2 THEN ..} and {e(t1);; e(t2);; ...}
+have the same meaning (modulo the validity check).
+After preprocessing, {unset_then_multiple_subgoals} is identical to the {false}
+constant in OCaml.
+To roll back the behavior of {THEN}, use {set_then_multiple_subgoals},
+which is identical to {true} modulo its side effect.
+
+This command is only available for OCaml 4.xx and above.
+
+\EXAMPLE
+{
+  # 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
+}
+
+\FAILURE
+Never fails.
+
+\SEEALSO
+e, THEN, VALID.
+
+\ENDDOC

pa_j/pa_j_4.xx_8.00.ml

@@ -78,13 +78,18 @@ value is_uppercase s = String.uppercase_ascii s = s;
 value is_only_lowercase s = String.lowercase_ascii s = s && not(is_uppercase s);
 
 value jrh_lexer = ref True;
+value then_multiple_subgoals = ref True;
 
 value jrh_identifier find_kwd id =
   let jflag = jrh_lexer.val in
   if id = "set_jrh_lexer" then
     (let _ = jrh_lexer.val := True in ("",find_kwd "true"))
   else if id = "unset_jrh_lexer" then
     (let _ = jrh_lexer.val := False in ("",find_kwd "false"))
+  else if id = "set_then_multiple_subgoals" then
+    (let _ = then_multiple_subgoals.val := True in ("",find_kwd "true"))
+  else if id = "unset_then_multiple_subgoals" then
+    (let _ = then_multiple_subgoals.val := False in ("",find_kwd "false"))
   else
   try ("", find_kwd id) with
    [ Not_found ->
@@ -1229,7 +1234,7 @@ value is_operator = do {
 value translate_operator =
   fun s ->
    match s with
-    [ "THEN" -> "then_"
+    [ "THEN" -> if then_multiple_subgoals.val then "then_" else "then1_"
     | "THENC" -> "thenc_"
     | "THENL" -> "thenl_"
     | "ORELSE" -> "orelse_"
@@ -3559,7 +3564,10 @@ EXTEND
     | f = expr; "upto"; g = expr -> <:expr< ((upto $f$) $g$) >>
     | f = expr; "F_F"; g = expr -> <:expr< ((f_f_ $f$) $g$) >>
     | f = expr; "THENC"; g = expr -> <:expr< ((thenc_ $f$) $g$) >>
-    | f = expr; "THEN"; g = expr -> <:expr< ((then_ $f$) $g$) >>
+    | f = expr; "THEN"; g = expr ->
+      if then_multiple_subgoals.val
+      then <:expr< ((then_ $f$) $g$) >>
+      else <:expr< ((then1_ $f$) $g$) >>
     | f = expr; "THENL"; g = expr -> <:expr< ((thenl_ $f$) $g$) >>
     | f = expr; "ORELSE"; g = expr -> <:expr< ((orelse_ $f$) $g$) >>
     | f = expr; "ORELSEC"; g = expr -> <:expr< ((orelsec_ $f$) $g$) >>

pa_j/pa_j_4.xx_8.02.ml

@@ -78,13 +78,18 @@ value is_uppercase s = String.uppercase_ascii s = s;
 value is_only_lowercase s = String.lowercase_ascii s = s && not(is_uppercase s);
 
 value jrh_lexer = ref True;
+value then_multiple_subgoals = ref True;
 
 value jrh_identifier find_kwd id =
   let jflag = jrh_lexer.val in
   if id = "set_jrh_lexer" then
     (let _ = jrh_lexer.val := True in ("",find_kwd "true"))
   else if id = "unset_jrh_lexer" then
     (let _ = jrh_lexer.val := False in ("",find_kwd "false"))
+  else if id = "set_then_multiple_subgoals" then
+    (let _ = then_multiple_subgoals.val := True in ("",find_kwd "true"))
+  else if id = "unset_then_multiple_subgoals" then
+    (let _ = then_multiple_subgoals.val := False in ("",find_kwd "false"))
   else
   try ("", find_kwd id) with
    [ Not_found ->
@@ -1229,7 +1234,7 @@ value is_operator = do {
 value translate_operator =
   fun s ->
    match s with
-    [ "THEN" -> "then_"
+    [ "THEN" -> if then_multiple_subgoals.val then "then_" else "then1_"
     | "THENC" -> "thenc_"
     | "THENL" -> "thenl_"
     | "ORELSE" -> "orelse_"
@@ -3559,7 +3564,10 @@ EXTEND
     | f = expr; "upto"; g = expr -> <:expr< ((upto $f$) $g$) >>
     | f = expr; "F_F"; g = expr -> <:expr< ((f_f_ $f$) $g$) >>
     | f = expr; "THENC"; g = expr -> <:expr< ((thenc_ $f$) $g$) >>
-    | f = expr; "THEN"; g = expr -> <:expr< ((then_ $f$) $g$) >>
+    | f = expr; "THEN"; g = expr ->
+      if then_multiple_subgoals.val
+      then <:expr< ((then_ $f$) $g$) >>
+      else <:expr< ((then1_ $f$) $g$) >>
     | f = expr; "THENL"; g = expr -> <:expr< ((thenl_ $f$) $g$) >>
     | f = expr; "ORELSE"; g = expr -> <:expr< ((orelse_ $f$) $g$) >>
     | f = expr; "ORELSEC"; g = expr -> <:expr< ((orelsec_ $f$) $g$) >>

pa_j/pa_j_4.xx_8.03.ml

@@ -88,13 +88,18 @@ value is_uppercase s = String.uppercase_ascii s = s;
 value is_only_lowercase s = String.lowercase_ascii s = s && not(is_uppercase s);
 
 value jrh_lexer = ref True;
+value then_multiple_subgoals = ref True;
 
 value jrh_identifier find_kwd id =
   let jflag = jrh_lexer.val in
   if id = "set_jrh_lexer" then
     (let _ = jrh_lexer.val := True in ("",find_kwd "true"))
   else if id = "unset_jrh_lexer" then
     (let _ = jrh_lexer.val := False in ("",find_kwd "false"))
+  else if id = "set_then_multiple_subgoals" then
+    (let _ = then_multiple_subgoals.val := True in ("",find_kwd "true"))
+  else if id = "unset_then_multiple_subgoals" then
+    (let _ = then_multiple_subgoals.val := False in ("",find_kwd "false"))
   else
   try ("", find_kwd id) with
    [ Not_found ->
@@ -1298,7 +1303,7 @@ value is_operator = do {
 value translate_operator =
   fun s ->
    match s with
-    [ "THEN" -> "then_"
+    [ "THEN" -> if then_multiple_subgoals.val then "then_" else "then1_"
     | "THENC" -> "thenc_"
     | "THENL" -> "thenl_"
     | "ORELSE" -> "orelse_"
@@ -3734,7 +3739,10 @@ EXTEND
     | f = expr; "upto"; g = expr -> <:expr< ((upto $f$) $g$) >>
     | f = expr; "F_F"; g = expr -> <:expr< ((f_f_ $f$) $g$) >>
     | f = expr; "THENC"; g = expr -> <:expr< ((thenc_ $f$) $g$) >>
-    | f = expr; "THEN"; g = expr -> <:expr< ((then_ $f$) $g$) >>
+    | f = expr; "THEN"; g = expr ->
+      if then_multiple_subgoals.val
+      then <:expr< ((then_ $f$) $g$) >>
+      else <:expr< ((then1_ $f$) $g$) >>
     | f = expr; "THENL"; g = expr -> <:expr< ((thenl_ $f$) $g$) >>
     | f = expr; "ORELSE"; g = expr -> <:expr< ((orelse_ $f$) $g$) >>
     | f = expr; "ORELSEC"; g = expr -> <:expr< ((orelsec_ $f$) $g$) >>

tactics.ml

@@ -130,7 +130,7 @@ let (VALID:tactic->tactic) =
 (* Various simple combinators for tactics, identity tactic etc.              *)
 (* ------------------------------------------------------------------------- *)
 
-let (THEN),(THENL) =
+let (THEN),(THENL),then1_ =
   let propagate_empty i [] = []
   and propagate_thm th i [] = INSTANTIATE_ALL i th in
   let compose_justs n just1 just2 insts2 i ths =
@@ -161,7 +161,7 @@ let (THEN),(THENL) =
       let _,gls,_ as gstate = tac1 g in
       if gls = [] then tacsequence gstate []
       else tacsequence gstate tac2l in
-  then_,thenl_;;
+  then_,thenl_,(fun tac1 tac2 -> thenl_ tac1 [tac2]);;
 
 let ((ORELSE): tactic -> tactic -> tactic) =
   fun tac1 tac2 g ->