diff --git a/Help/THEN.hlp b/Help/THEN.hlp index 120b7ab8..a611b186 100644 --- a/Help/THEN.hlp +++ b/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 diff --git a/Help/unset_jrh_lexer.hlp b/Help/unset_jrh_lexer.hlp new file mode 100644 index 00000000..d91ecd0e --- /dev/null +++ b/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 diff --git a/Help/unset_then_multiple_subgoals.hlp b/Help/unset_then_multiple_subgoals.hlp new file mode 100644 index 00000000..857f39d9 --- /dev/null +++ b/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 diff --git a/pa_j/pa_j_4.xx_8.00.ml b/pa_j/pa_j_4.xx_8.00.ml index ce62d7b3..0f52add3 100755 --- a/pa_j/pa_j_4.xx_8.00.ml +++ b/pa_j/pa_j_4.xx_8.00.ml @@ -78,6 +78,7 @@ 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 @@ -85,6 +86,10 @@ value jrh_identifier find_kwd id = (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$) >> diff --git a/pa_j/pa_j_4.xx_8.02.ml b/pa_j/pa_j_4.xx_8.02.ml index 56a40108..9d2512ea 100644 --- a/pa_j/pa_j_4.xx_8.02.ml +++ b/pa_j/pa_j_4.xx_8.02.ml @@ -78,6 +78,7 @@ 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 @@ -85,6 +86,10 @@ value jrh_identifier find_kwd id = (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$) >> diff --git a/pa_j/pa_j_4.xx_8.03.ml b/pa_j/pa_j_4.xx_8.03.ml index 410ec8df..c440349a 100755 --- a/pa_j/pa_j_4.xx_8.03.ml +++ b/pa_j/pa_j_4.xx_8.03.ml @@ -88,6 +88,7 @@ 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 @@ -95,6 +96,10 @@ value jrh_identifier find_kwd id = (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$) >> diff --git a/tactics.ml b/tactics.ml index ec6a0466..6ab06d26 100644 --- a/tactics.ml +++ b/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 ->