# HG changeset patch
# User blanchet
# Date 1677654051 -3600
# Node ID 7c76221baecbd2906f80d3e3a0a8c1b0118a46a0
# Parent  4cdefee3f97f59b4c3b5b9935d28fa0ffbdddbaa
adopt terminology suggested by Larry Paulson

diff -r 4cdefee3f97f -r 7c76221baecb NEWS
--- a/NEWS	Wed Mar 01 08:00:51 2023 +0100
+++ b/NEWS	Wed Mar 01 08:00:51 2023 +0100
@@ -241,8 +241,7 @@
 * Sledgehammer:
   - Added an inconsistency check mode to find likely unprovable
     conjectures. It is enabled by default in addition to the usual
-    proving mode and can be controlled using the 'check_inconsistent'
-    option.
+    proving mode and can be controlled using the 'falsify' option.
   - Added an abduction mode to find likely missing hypotheses to
     conjectures. It currently works only with the E prover. It is
     enabled by default and can be controlled using the 'abduce'
diff -r 4cdefee3f97f -r 7c76221baecb src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Mar 01 08:00:51 2023 +0100
@@ -100,7 +100,7 @@
 
 Sledgehammer is a tool that applies automatic theorem provers (ATPs)
 and satisfiability-modulo-theories (SMT) solvers on the current goal, mostly
-to find proofs but also to find inconsistencies.%
+to find proofs but also to refute the goal.%
 \footnote{The distinction between ATPs and SMT solvers is mostly
 historical but convenient.}
 %
@@ -276,8 +276,8 @@
 
 \prew
 \slshape
-vampire found an inconsistency\ldots \\
-vampire: The goal is inconsistent with these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
+vampire found a falsification\ldots \\
+vampire: The goal is falsified by these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
 \postw
 
 Sometimes Sledgehammer will helpfully suggest a missing assumption:
@@ -818,11 +818,11 @@
 \opnodefault{prover}{string}
 Alias for \textit{provers}.
 
-\opsmartx{check\_inconsistent}{dont\_check\_inconsistent}
-Specifies whether Sledgehammer should look for inconsistencies or for proofs. By
-default, it looks for both proofs and inconsistencies.
+\opsmartx{falsify}{dont\_falsify}
+Specifies whether Sledgehammer should look for falsifications or for proofs. By
+default, it looks for both.
 
-An inconsistency indicates that the goal, taken as an axiom, would be
+A falsification indicates that the goal, taken as an axiom, would be
 inconsistent with some specific background facts if it were added as a lemma,
 indicating a likely issue with the goal. Sometimes the inconsistency involves
 only the background theory; this might happen, for example, if a flawed axiom is
diff -r 4cdefee3f97f -r 7c76221baecb src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -159,20 +159,18 @@
 
 fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
     (problem as {state, subgoal, factss, ...} : prover_problem)
-    (slice as ((slice_size, abduce, check_inconsistent, num_facts, fact_filter), _)) name =
+    (slice as ((slice_size, abduce, falsify, num_facts, fact_filter), _)) name =
   let
     val ctxt = Proof.context_of state
 
     val _ = spying spy (fn () => (state, subgoal, name,
-      "Launched" ^ (if abduce then " (abduce)" else "") ^
-      (if check_inconsistent then " (check_inconsistent)" else "")))
+      "Launched" ^ (if abduce then " (abduce)" else "") ^ (if falsify then " (falsify)" else "")))
 
     val _ =
       if verbose then
         writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^
           plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slice_size slices timeout) ^
-          (if abduce then " (abduce)" else "") ^
-          (if check_inconsistent then " (check_inconsistent)" else "") ^ "...")
+          (if abduce then " (abduce)" else "") ^ (if falsify then " (falsify)" else "") ^ "...")
       else
         ()
 
@@ -182,8 +180,7 @@
       |> filter_used_facts false used_facts
       |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
       |> commas
-      |> prefix ("Facts in " ^ name ^ " " ^
-        (if check_inconsistent then "inconsistency" else "proof") ^ ": ")
+      |> prefix ("Facts in " ^ name ^ " " ^ (if falsify then "falsification" else "proof") ^ ": ")
       |> writeln
 
     fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
@@ -211,7 +208,7 @@
             |> AList.group (op =)
             |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
         in
-          "Success: Found " ^ (if check_inconsistent then "inconsistency" else "proof") ^ " with " ^
+          "Success: Found " ^ (if falsify then "falsification" else "proof") ^ " with " ^
           string_of_int num_used_facts ^ " fact" ^ plural_s num_used_facts ^
           (if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
         end
@@ -262,7 +259,7 @@
        (if member (op = o apsnd fst) used_facts sledgehammer_goal_as_fact then
           (case map fst (filter_out (equal sledgehammer_goal_as_fact o fst) used_facts) of
             [] => "The goal is inconsistent"
-          | facts => "The goal is inconsistent with these facts: " ^ commas facts)
+          | facts => "The goal is falsified by these facts: " ^ commas facts)
         else
           "The following facts are inconsistent: " ^
           commas (map fst used_facts)))
@@ -292,8 +289,7 @@
 
 fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode
     has_already_found_something found_something writeln_result learn
-    (problem as {state, subgoal, ...}) (slice as ((_, _, check_inconsistent, _, _), _))
-    prover_name =
+    (problem as {state, subgoal, ...}) (slice as ((_, _, falsify, _, _), _)) prover_name =
   let
     val ctxt = Proof.context_of state
     val hard_timeout = Time.scale 5.0 timeout
@@ -321,11 +317,11 @@
          found_something = found_something "an inconsistency"}
       end
 
-    val problem as {goal, ...} = problem |> check_inconsistent ? flip_problem
+    val problem as {goal, ...} = problem |> falsify ? flip_problem
 
     fun really_go () =
       launch_prover params mode learn problem slice prover_name
-      |> (if check_inconsistent then analyze_prover_result_for_inconsistency else
+      |> (if falsify then analyze_prover_result_for_inconsistency else
         preplay_prover_result params state goal subgoal)
 
     fun go () =
@@ -392,15 +388,15 @@
   end
 
 fun prover_slices_of_schedule ctxt goal subgoal factss
-    ({abduce, check_inconsistent, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
+    ({abduce, falsify, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
       ...} : params)
     schedule =
   let
     fun triplicate_slices original =
       let
         val shift =
-          map (apfst (fn (slice_size, abduce, check_inconsistent, num_facts, fact_filter) =>
-            (slice_size, abduce, check_inconsistent, num_facts,
+          map (apfst (fn (slice_size, abduce, falsify, num_facts, fact_filter) =>
+            (slice_size, abduce, falsify, num_facts,
              if fact_filter = mashN then mepoN
              else if fact_filter = mepoN then meshN
              else mashN)))
@@ -418,7 +414,7 @@
       | adjust_extra (extra as SMT_Slice _) = extra
 
     fun adjust_slice max_slice_size
-        ((slice_size0, abduce0, check_inconsistent0, num_facts0, fact_filter0), extra) =
+        ((slice_size0, abduce0, falsify0, num_facts0, fact_filter0), extra) =
       let
         val slice_size = Int.min (max_slice_size, slice_size0)
         val goal_not_False = not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False})
@@ -426,15 +422,15 @@
           (case abduce of
             NONE => abduce0 andalso goal_not_False
           | SOME max_candidates => max_candidates > 0)
-        val check_inconsistent =
-          (case check_inconsistent of
-            NONE => check_inconsistent0 andalso goal_not_False
-          | SOME check_inconsistent => check_inconsistent)
+        val falsify =
+          (case falsify of
+            NONE => falsify0 andalso goal_not_False
+          | SOME falsify => falsify)
         val fact_filter = fact_filter |> the_default fact_filter0
         val max_facts = max_facts |> the_default num_facts0
         val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss))
       in
-        ((slice_size, abduce, check_inconsistent, num_facts, fact_filter), adjust_extra extra)
+        ((slice_size, abduce, falsify, num_facts, fact_filter), adjust_extra extra)
       end
 
     val provers = distinct (op =) schedule
@@ -463,9 +459,8 @@
     |> distinct (op =)
   end
 
-fun run_sledgehammer (params as {verbose, spy, provers, check_inconsistent, induction_rules,
-      max_facts, max_proofs, slices, ...})
-    mode writeln_result i (fact_override as {only, ...}) state =
+fun run_sledgehammer (params as {verbose, spy, provers, falsify, induction_rules, max_facts,
+    max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state =
   if null provers then
     error "No prover is set"
   else
@@ -476,17 +471,17 @@
         val _ = Proof.assert_backward state
         val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
 
-        val found_proofs_and_inconsistencies = Synchronized.var "found_proofs_and_inconsistencies" 0
+        val found_proofs_and_falsifications = Synchronized.var "found_proofs_and_falsifications" 0
 
         fun has_already_found_something () =
           if mode = Normal then
-            Synchronized.value found_proofs_and_inconsistencies > 0
+            Synchronized.value found_proofs_and_falsifications > 0
           else
             false
 
         fun found_something a_proof_or_inconsistency prover_name =
           if mode = Normal then
-            (Synchronized.change found_proofs_and_inconsistencies (fn n => n + 1);
+            (Synchronized.change found_proofs_and_falsifications (fn n => n + 1);
              (the_default writeln writeln_result) (prover_name ^ " found " ^
              a_proof_or_inconsistency ^ "..."))
           else
@@ -571,7 +566,7 @@
             else
               (learn chained_thms;
                Par_List.map (fn (prover, slice) =>
-                   if Synchronized.value found_proofs_and_inconsistencies < max_proofs then
+                   if Synchronized.value found_proofs_and_falsifications < max_proofs then
                      launch problem slice prover
                    else
                      (SH_None, ""))
@@ -581,7 +576,7 @@
 
         fun normal_failure () =
           (the_default writeln writeln_result
-             ("No " ^ (if check_inconsistent = SOME true then "inconsistency" else "proof") ^
+             ("No " ^ (if falsify = SOME true then "falsification" else "proof") ^
               " found");
            false)
       in
diff -r 4cdefee3f97f -r 7c76221baecb src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -67,7 +67,7 @@
 val default_max_mono_iters = 3 (* FUDGE *)
 val default_max_new_mono_instances = 100 (* FUDGE *)
 
-(* desired slice size, abduce, check_inconsistent, desired number of facts, fact filter *)
+(* desired slice size, abduce, falsify, desired number of facts, fact filter *)
 type base_slice = int * bool * bool * int * string
 
 (* problem file format, type encoding, lambda translation scheme, uncurried aliases?,
diff -r 4cdefee3f97f -r 7c76221baecb src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -54,7 +54,7 @@
    ("overlord", "false"),
    ("spy", "false"),
    ("abduce", "smart"),
-   ("check_inconsistent", "smart"),
+   ("falsify", "smart"),
    ("type_enc", "smart"),
    ("strict", "false"),
    ("lam_trans", "smart"),
@@ -87,7 +87,7 @@
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
    ("dont_spy", "spy"),
-   ("dont_check_inconsistent", "check_inconsistent"),
+   ("dont_falsify", "falsify"),
    ("non_strict", "strict"),
    ("no_uncurried_aliases", "uncurried_aliases"),
    ("dont_learn", "learn"),
@@ -235,9 +235,9 @@
     val abduce =
       if mode = Auto_Try then SOME 0
       else lookup_option lookup_int "abduce"
-    val check_inconsistent =
+    val falsify =
       if mode = Auto_Try then SOME false
-      else lookup_option lookup_bool "check_inconsistent"
+      else lookup_option lookup_bool "falsify"
     val type_enc =
       if mode = Auto_Try then
         NONE
@@ -271,7 +271,7 @@
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
-     abduce = abduce, check_inconsistent = check_inconsistent, type_enc = type_enc, strict = strict,
+     abduce = abduce, falsify = falsify, type_enc = type_enc, strict = strict,
      lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn,
      fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts,
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
diff -r 4cdefee3f97f -r 7c76221baecb src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -30,7 +30,7 @@
      spy : bool,
      provers : string list,
      abduce : int option,
-     check_inconsistent : bool option,
+     falsify : bool option,
      type_enc : string option,
      strict : bool,
      lam_trans : string option,
@@ -141,7 +141,7 @@
    spy : bool,
    provers : string list,
    abduce : int option,
-   check_inconsistent : bool option,
+   falsify : bool option,
    type_enc : string option,
    strict : bool,
    lam_trans : string option,
diff -r 4cdefee3f97f -r 7c76221baecb src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -83,8 +83,8 @@
 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
       type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
       minimize, preplay_timeout, induction_rules, ...} : params)
-    (slice as ((_, _, check_inconsistent, _, fact_filter), slice_extra)) silent
-    (prover : prover) timeout i n state goal facts =
+    (slice as ((_, _, falsify, _, fact_filter), slice_extra)) silent (prover : prover) timeout i n
+    state goal facts =
   let
     val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
       (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
@@ -92,7 +92,7 @@
     val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
     val params =
       {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
-       type_enc = type_enc, abduce = SOME 0, check_inconsistent = SOME false, strict = strict,
+       type_enc = type_enc, abduce = SOME 0, falsify = SOME false, strict = strict,
        lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false,
        fact_filter = NONE, induction_rules = induction_rules, max_facts = SOME (length facts),
        fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
@@ -118,7 +118,7 @@
       (case outcome of
         SOME failure => string_of_atp_failure failure
       | NONE =>
-        "Found " ^ (if check_inconsistent then "inconsistency" else "proof") ^
+        "Found " ^ (if falsify then "falsification" else "proof") ^
          (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
          " (" ^ string_of_time run_time ^ ")"));
     result