src/HOL/Tools/Meson/meson.ML
author haftmann
Sat, 24 Dec 2011 16:14:58 +0100
changeset 45981 4c629115e3ab
parent 45740 132a3e1c0fe5
child 46071 1613933e412c
permissions -rw-r--r--
dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39941
02fcd9cd1eac move Meson to Plain
blanchet
parents: 39940
diff changeset
     1
(*  Title:      HOL/Tools/Meson/meson.ML
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
39941
02fcd9cd1eac move Meson to Plain
blanchet
parents: 39940
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
     4
9869
95dca9f991f2 improved meson setup;
wenzelm
parents: 9840
diff changeset
     5
The MESON resolution proof procedure for HOL.
29267
8615b4f54047 use exists_subterm directly;
wenzelm
parents: 28397
diff changeset
     6
When making clauses, avoids using the rewriter -- instead uses RS recursively.
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
     7
*)
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
     8
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
     9
signature MESON =
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
    10
sig
39979
b13515940b53 added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents: 39953
diff changeset
    11
  val trace : bool Config.T
42739
017e5dac8642 added unfold set constant functionality to Meson/Metis -- disabled by default for now
blanchet
parents: 42616
diff changeset
    12
  val unfold_set_consts : bool Config.T
39979
b13515940b53 added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents: 39953
diff changeset
    13
  val max_clauses : int Config.T
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    14
  val term_pair_of: indexname * (typ * 'a) -> term * 'a
45567
8e3891309a8e avoid that var names get changed by resolution in Metis lambda-lifting
blanchet
parents: 43964
diff changeset
    15
  val first_order_resolve : thm -> thm -> thm
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    16
  val size_of_subgoals: thm -> int
39269
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
    17
  val has_too_many_clauses: Proof.context -> term -> bool
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
    18
  val make_cnf:
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
    19
    thm list -> thm -> Proof.context
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
    20
    -> Proof.context -> thm list * Proof.context
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    21
  val finish_cnf: thm list -> thm list
42739
017e5dac8642 added unfold set constant functionality to Meson/Metis -- disabled by default for now
blanchet
parents: 42616
diff changeset
    22
  val unfold_set_const_simps : Proof.context -> thm list
43264
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 42833
diff changeset
    23
  val presimplified_consts : Proof.context -> string list
42750
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
    24
  val presimplify: Proof.context -> thm -> thm
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
    25
  val make_nnf: Proof.context -> thm -> thm
39950
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39941
diff changeset
    26
  val choice_theorems : theory -> thm list
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39941
diff changeset
    27
  val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
39904
f9e89d36a31a tune bound names
blanchet
parents: 39901
diff changeset
    28
  val skolemize : Proof.context -> thm -> thm
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
    29
  val extensionalize_conv : Proof.context -> conv
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
    30
  val extensionalize_theorem : Proof.context -> thm -> thm
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    31
  val is_fol_term: theory -> term -> bool
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
    32
  val make_clauses_unsorted: Proof.context -> thm list -> thm list
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
    33
  val make_clauses: Proof.context -> thm list -> thm list
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    34
  val make_horns: thm list -> thm list
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    35
  val best_prolog_tac: (thm -> int) -> thm list -> tactic
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    36
  val depth_prolog_tac: thm list -> tactic
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    37
  val gocls: thm list -> thm list
39900
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
    38
  val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic
39037
5146d640aa4a Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents: 38864
diff changeset
    39
  val MESON:
39269
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
    40
    tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
    41
    -> int -> tactic
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
    42
  val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
    43
  val safe_best_meson_tac: Proof.context -> int -> tactic
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
    44
  val depth_meson_tac: Proof.context -> int -> tactic
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    45
  val prolog_step_tac': thm list -> int -> tactic
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    46
  val iter_deepen_prolog_tac: thm list -> tactic
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
    47
  val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    48
  val make_meta_clause: thm -> thm
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
    49
  val make_meta_clauses: thm list -> thm list
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
    50
  val meson_tac: Proof.context -> thm list -> int -> tactic
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
    51
end
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
    52
39901
75d792edf634 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents: 39900
diff changeset
    53
structure Meson : MESON =
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
    54
struct
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
    55
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42455
diff changeset
    56
val trace = Attrib.setup_config_bool @{binding meson_trace} (K false)
39979
b13515940b53 added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents: 39953
diff changeset
    57
b13515940b53 added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents: 39953
diff changeset
    58
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
32955
4a78daeb012b local channels for tracing/debugging;
wenzelm
parents: 32740
diff changeset
    59
42739
017e5dac8642 added unfold set constant functionality to Meson/Metis -- disabled by default for now
blanchet
parents: 42616
diff changeset
    60
val unfold_set_consts =
017e5dac8642 added unfold set constant functionality to Meson/Metis -- disabled by default for now
blanchet
parents: 42616
diff changeset
    61
  Attrib.setup_config_bool @{binding meson_unfold_set_consts} (K false)
017e5dac8642 added unfold set constant functionality to Meson/Metis -- disabled by default for now
blanchet
parents: 42616
diff changeset
    62
017e5dac8642 added unfold set constant functionality to Meson/Metis -- disabled by default for now
blanchet
parents: 42616
diff changeset
    63
val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K 60)
26562
9d25ef112cf6 * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents: 26424
diff changeset
    64
38802
a925c0ee42f7 clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents: 38795
diff changeset
    65
(*No known example (on 1-5-2007) needs even thirty*)
a925c0ee42f7 clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents: 38795
diff changeset
    66
val iter_deepen_limit = 50;
a925c0ee42f7 clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents: 38795
diff changeset
    67
31454
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    68
val disj_forward = @{thm disj_forward};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    69
val disj_forward2 = @{thm disj_forward2};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    70
val make_pos_rule = @{thm make_pos_rule};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    71
val make_pos_rule' = @{thm make_pos_rule'};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    72
val make_pos_goal = @{thm make_pos_goal};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    73
val make_neg_rule = @{thm make_neg_rule};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    74
val make_neg_rule' = @{thm make_neg_rule'};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    75
val make_neg_goal = @{thm make_neg_goal};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    76
val conj_forward = @{thm conj_forward};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    77
val all_forward = @{thm all_forward};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    78
val ex_forward = @{thm ex_forward};
2c0959ab073f dropped legacy ML bindings; tuned
haftmann
parents: 30607
diff changeset
    79
39953
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    80
val not_conjD = @{thm not_conjD};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    81
val not_disjD = @{thm not_disjD};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    82
val not_notD = @{thm not_notD};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    83
val not_allD = @{thm not_allD};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    84
val not_exD = @{thm not_exD};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    85
val imp_to_disjD = @{thm imp_to_disjD};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    86
val not_impD = @{thm not_impD};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    87
val iff_to_disjD = @{thm iff_to_disjD};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    88
val not_iffD = @{thm not_iffD};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    89
val conj_exD1 = @{thm conj_exD1};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    90
val conj_exD2 = @{thm conj_exD2};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    91
val disj_exD = @{thm disj_exD};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    92
val disj_exD1 = @{thm disj_exD1};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    93
val disj_exD2 = @{thm disj_exD2};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    94
val disj_assoc = @{thm disj_assoc};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    95
val disj_comm = @{thm disj_comm};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    96
val disj_FalseD1 = @{thm disj_FalseD1};
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
    97
val disj_FalseD2 = @{thm disj_FalseD2};
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
    98
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
    99
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   100
(**** Operators for forward proof ****)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   101
20417
c611b1412056 better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents: 20361
diff changeset
   102
c611b1412056 better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents: 20361
diff changeset
   103
(** First-order Resolution **)
c611b1412056 better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents: 20361
diff changeset
   104
c611b1412056 better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents: 20361
diff changeset
   105
fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
c611b1412056 better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents: 20361
diff changeset
   106
c611b1412056 better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents: 20361
diff changeset
   107
(*FIXME: currently does not "rename variables apart"*)
c611b1412056 better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents: 20361
diff changeset
   108
fun first_order_resolve thA thB =
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   109
  (case
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   110
    try (fn () =>
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   111
      let val thy = theory_of_thm thA
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   112
          val tmA = concl_of thA
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   113
          val Const("==>",_) $ tmB $ _ = prop_of thB
37398
e194213451c9 beta-eta-contract, to respect "first_order_match"'s specification;
blanchet
parents: 37388
diff changeset
   114
          val tenv =
37410
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents: 37398
diff changeset
   115
            Pattern.first_order_match thy (tmB, tmA)
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents: 37398
diff changeset
   116
                                          (Vartab.empty, Vartab.empty) |> snd
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   117
          val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   118
      in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   119
    SOME th => th
37398
e194213451c9 beta-eta-contract, to respect "first_order_match"'s specification;
blanchet
parents: 37388
diff changeset
   120
  | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
18175
7858b777569a new version of "tryres" allowing multiple unifiers (apparently needed for
paulson
parents: 18141
diff changeset
   121
40262
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   122
(* Hack to make it less likely that we lose our precious bound variable names in
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   123
   "rename_bound_vars_RS" below, because of a clash. *)
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   124
val protect_prefix = "Meson_xyzzy"
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   125
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   126
fun protect_bound_var_names (t $ u) =
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   127
    protect_bound_var_names t $ protect_bound_var_names u
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   128
  | protect_bound_var_names (Abs (s, T, t')) =
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   129
    Abs (protect_prefix ^ s, T, protect_bound_var_names t')
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   130
  | protect_bound_var_names t = t
39930
61aa00205a88 hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
blanchet
parents: 39904
diff changeset
   131
40262
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   132
fun fix_bound_var_names old_t new_t =
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   133
  let
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   134
    fun quant_of @{const_name All} = SOME true
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   135
      | quant_of @{const_name Ball} = SOME true
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   136
      | quant_of @{const_name Ex} = SOME false
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   137
      | quant_of @{const_name Bex} = SOME false
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   138
      | quant_of _ = NONE
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   139
    val flip_quant = Option.map not
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   140
    fun some_eq (SOME x) (SOME y) = x = y
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   141
      | some_eq _ _ = false
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   142
    fun add_names quant (Const (quant_s, _) $ Abs (s, _, t')) =
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   143
        add_names quant t' #> some_eq quant (quant_of quant_s) ? cons s
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   144
      | add_names quant (@{const Not} $ t) = add_names (flip_quant quant) t
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   145
      | add_names quant (@{const implies} $ t1 $ t2) =
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   146
        add_names (flip_quant quant) t1 #> add_names quant t2
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   147
      | add_names quant (t1 $ t2) = fold (add_names quant) [t1, t2]
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   148
      | add_names _ _ = I
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   149
    fun lost_names quant =
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   150
      subtract (op =) (add_names quant new_t []) (add_names quant old_t [])
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   151
    fun aux ((t1 as Const (quant_s, _)) $ (Abs (s, T, t'))) =
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   152
      t1 $ Abs (s |> String.isPrefix protect_prefix s
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   153
                   ? perhaps (try (fn _ => hd (lost_names (quant_of quant_s)))),
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   154
                T, aux t')
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   155
      | aux (t1 $ t2) = aux t1 $ aux t2
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   156
      | aux t = t
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   157
  in aux new_t end
39930
61aa00205a88 hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
blanchet
parents: 39904
diff changeset
   158
40262
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   159
(* Forward proof while preserving bound variables names *)
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   160
fun rename_bound_vars_RS th rl =
39904
f9e89d36a31a tune bound names
blanchet
parents: 39901
diff changeset
   161
  let
f9e89d36a31a tune bound names
blanchet
parents: 39901
diff changeset
   162
    val t = concl_of th
39930
61aa00205a88 hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
blanchet
parents: 39904
diff changeset
   163
    val r = concl_of rl
40262
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   164
    val th' = th RS Thm.rename_boundvars r (protect_bound_var_names r) rl
39904
f9e89d36a31a tune bound names
blanchet
parents: 39901
diff changeset
   165
    val t' = concl_of th'
40262
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   166
  in Thm.rename_boundvars t' (fix_bound_var_names t t') th' end
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   167
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   168
(*raises exception if no rules apply*)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   169
fun tryres (th, rls) =
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18024
diff changeset
   170
  let fun tryall [] = raise THM("tryres", 0, th::rls)
40262
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   171
        | tryall (rl::rls) =
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   172
          (rename_bound_vars_RS th rl handle THM _ => tryall rls)
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18024
diff changeset
   173
  in  tryall rls  end;
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   174
21050
d0447a511edb More robust error handling in make_nnf and forward_res
paulson
parents: 21046
diff changeset
   175
(*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
d0447a511edb More robust error handling in make_nnf and forward_res
paulson
parents: 21046
diff changeset
   176
  e.g. from conj_forward, should have the form
d0447a511edb More robust error handling in make_nnf and forward_res
paulson
parents: 21046
diff changeset
   177
    "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
d0447a511edb More robust error handling in make_nnf and forward_res
paulson
parents: 21046
diff changeset
   178
  and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   179
fun forward_res ctxt nf st =
21050
d0447a511edb More robust error handling in make_nnf and forward_res
paulson
parents: 21046
diff changeset
   180
  let fun forward_tacf [prem] = rtac (nf prem) 1
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   181
        | forward_tacf prems =
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32032
diff changeset
   182
            error (cat_lines
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32032
diff changeset
   183
              ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   184
                Display.string_of_thm ctxt st ::
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   185
                "Premises:" :: map (Display.string_of_thm ctxt) prems))
21050
d0447a511edb More robust error handling in make_nnf and forward_res
paulson
parents: 21046
diff changeset
   186
  in
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents: 37539
diff changeset
   187
    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st)
21050
d0447a511edb More robust error handling in make_nnf and forward_res
paulson
parents: 21046
diff changeset
   188
    of SOME(th,_) => th
d0447a511edb More robust error handling in make_nnf and forward_res
paulson
parents: 21046
diff changeset
   189
     | NONE => raise THM("forward_res", 0, [st])
d0447a511edb More robust error handling in make_nnf and forward_res
paulson
parents: 21046
diff changeset
   190
  end;
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   191
20134
73cb53843190 has_consts renamed to has_conn, now actually parses the first-order formula
paulson
parents: 20119
diff changeset
   192
(*Are any of the logical connectives in "bs" present in the term?*)
73cb53843190 has_consts renamed to has_conn, now actually parses the first-order formula
paulson
parents: 20119
diff changeset
   193
fun has_conns bs =
39328
blanchet
parents: 39277
diff changeset
   194
  let fun has (Const _) = false
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   195
        | has (Const(@{const_name Trueprop},_) $ p) = has p
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   196
        | has (Const(@{const_name Not},_) $ p) = has p
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   197
        | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   198
        | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   199
        | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   200
        | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   201
        | has _ = false
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   202
  in  has  end;
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   203
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   204
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   205
(**** Clause handling ****)
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   206
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   207
fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   208
  | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   209
  | literals (Const(@{const_name Not},_) $ P) = [(false,P)]
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   210
  | literals P = [(true,P)];
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   211
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   212
(*number of literals in a term*)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   213
val nliterals = length o literals;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   214
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   215
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   216
(*** Tautology Checking ***)
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   217
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   218
fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) =
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   219
      signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   220
  | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   221
  | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   222
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   223
fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   224
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   225
(*Literals like X=X are tautologous*)
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38806
diff changeset
   226
fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   227
  | taut_poslit (Const(@{const_name True},_)) = true
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   228
  | taut_poslit _ = false;
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   229
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   230
fun is_taut th =
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   231
  let val (poslits,neglits) = signed_lits th
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   232
  in  exists taut_poslit poslits
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   233
      orelse
45740
132a3e1c0fe5 more antiquotations;
wenzelm
parents: 45567
diff changeset
   234
      exists (member (op aconv) neglits) (@{term False} :: poslits)
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19875
diff changeset
   235
  end
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   236
  handle TERM _ => false;       (*probably dest_Trueprop on a weird theorem*)
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   237
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   238
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   239
(*** To remove trivial negated equality literals from clauses ***)
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   240
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   241
(*They are typically functional reflexivity axioms and are the converses of
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   242
  injectivity equivalences*)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   243
39953
aa54f347e5e2 hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents: 39950
diff changeset
   244
val not_refl_disj_D = @{thm not_refl_disj_D};
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   245
20119
7923aacc10c6 fix to refl_clause_aux: added occurs check
paulson
parents: 20073
diff changeset
   246
(*Is either term a Var that does not properly occur in the other term?*)
7923aacc10c6 fix to refl_clause_aux: added occurs check
paulson
parents: 20073
diff changeset
   247
fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
7923aacc10c6 fix to refl_clause_aux: added occurs check
paulson
parents: 20073
diff changeset
   248
  | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
7923aacc10c6 fix to refl_clause_aux: added occurs check
paulson
parents: 20073
diff changeset
   249
  | eliminable _ = false;
7923aacc10c6 fix to refl_clause_aux: added occurs check
paulson
parents: 20073
diff changeset
   250
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   251
fun refl_clause_aux 0 th = th
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   252
  | refl_clause_aux n th =
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   253
       case HOLogic.dest_Trueprop (concl_of th) of
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   254
          (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   255
            refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38806
diff changeset
   256
        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) =>
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   257
            if eliminable(t,u)
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   258
            then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   259
            else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   260
        | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   261
        | _ => (*not a disjunction*) th;
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   262
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   263
fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   264
      notequal_lits_count P + notequal_lits_count Q
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38806
diff changeset
   265
  | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   266
  | notequal_lits_count _ = 0;
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   267
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   268
(*Simplify a clause by applying reflexivity to its negated equality literals*)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   269
fun refl_clause th =
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   270
  let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19875
diff changeset
   271
  in  zero_var_indexes (refl_clause_aux neqs th)  end
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   272
  handle TERM _ => th;  (*probably dest_Trueprop on a weird theorem*)
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   273
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   274
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   275
(*** Removal of duplicate literals ***)
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   276
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   277
(*Forward proof, passing extra assumptions as theorems to the tactic*)
39328
blanchet
parents: 39277
diff changeset
   278
fun forward_res2 nf hyps st =
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   279
  case Seq.pull
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   280
        (REPEAT
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents: 37539
diff changeset
   281
         (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   282
         st)
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   283
  of SOME(th,_) => th
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   284
   | NONE => raise THM("forward_res2", 0, [st]);
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   285
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   286
(*Remove duplicates in P|Q by assuming ~P in Q
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   287
  rls (initially []) accumulates assumptions of the form P==>False*)
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   288
fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   289
    handle THM _ => tryres(th,rls)
39328
blanchet
parents: 39277
diff changeset
   290
    handle THM _ => tryres(forward_res2 (nodups_aux ctxt) rls (th RS disj_forward2),
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   291
                           [disj_FalseD1, disj_FalseD2, asm_rl])
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   292
    handle THM _ => th;
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   293
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   294
(*Remove duplicate literals, if there are any*)
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   295
fun nodups ctxt th =
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   296
  if has_duplicates (op =) (literals (prop_of th))
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   297
    then nodups_aux ctxt [] th
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   298
    else th;
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   299
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   300
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   301
(*** The basic CNF transformation ***)
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   302
39328
blanchet
parents: 39277
diff changeset
   303
fun estimated_num_clauses bound t =
26562
9d25ef112cf6 * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents: 26424
diff changeset
   304
 let
39269
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
   305
  fun sum x y = if x < bound andalso y < bound then x+y else bound
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
   306
  fun prod x y = if x < bound andalso y < bound then x*y else bound
26562
9d25ef112cf6 * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents: 26424
diff changeset
   307
  
9d25ef112cf6 * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents: 26424
diff changeset
   308
  (*Estimate the number of clauses in order to detect infeasible theorems*)
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   309
  fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   310
    | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   311
    | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) =
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   312
        if b then sum (signed_nclauses b t) (signed_nclauses b u)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   313
             else prod (signed_nclauses b t) (signed_nclauses b u)
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   314
    | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) =
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   315
        if b then prod (signed_nclauses b t) (signed_nclauses b u)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   316
             else sum (signed_nclauses b t) (signed_nclauses b u)
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38709
diff changeset
   317
    | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   318
        if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   319
             else sum (signed_nclauses (not b) t) (signed_nclauses b u)
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38806
diff changeset
   320
    | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) =
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   321
        if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   322
            if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   323
                          (prod (signed_nclauses (not b) u) (signed_nclauses b t))
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   324
                 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   325
                          (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32955
diff changeset
   326
        else 1
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   327
    | signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   328
    | signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t
26562
9d25ef112cf6 * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents: 26424
diff changeset
   329
    | signed_nclauses _ _ = 1; (* literal *)
39269
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
   330
 in signed_nclauses true t end
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
   331
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
   332
fun has_too_many_clauses ctxt t =
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
   333
  let val max_cl = Config.get ctxt max_clauses in
39328
blanchet
parents: 39277
diff changeset
   334
    estimated_num_clauses (max_cl + 1) t > max_cl
39269
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
   335
  end
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19875
diff changeset
   336
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   337
(*Replaces universally quantified variables by FREE variables -- because
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   338
  assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   339
local  
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   340
  val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   341
  val spec_varT = #T (Thm.rep_cterm spec_var);
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   342
  fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   343
in  
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   344
  fun freeze_spec th ctxt =
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   345
    let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42346
diff changeset
   346
      val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   347
      val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   348
      val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   349
    in (th RS spec', ctxt') end
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   350
end;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   351
15998
bc916036cf84 new cnf function taking Skolemization theorems as an extra argument
paulson
parents: 15965
diff changeset
   352
(*Used with METAHYPS below. There is one assumption, which gets bound to prem
bc916036cf84 new cnf function taking Skolemization theorems as an extra argument
paulson
parents: 15965
diff changeset
   353
  and then normalized via function nf. The normal form is given to resolve_tac,
22515
f4061faa5fda "generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
paulson
parents: 22381
diff changeset
   354
  instantiate a Boolean variable created by resolution with disj_forward. Since
f4061faa5fda "generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
paulson
parents: 22381
diff changeset
   355
  (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   356
fun resop nf [prem] = resolve_tac (nf prem) 1;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   357
39037
5146d640aa4a Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents: 38864
diff changeset
   358
(* Any need to extend this list with "HOL.type_class", "HOL.eq_class",
5146d640aa4a Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents: 38864
diff changeset
   359
   and "Pure.term"? *)
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   360
val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
20417
c611b1412056 better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents: 20361
diff changeset
   361
37410
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents: 37398
diff changeset
   362
fun apply_skolem_theorem (th, rls) =
37398
e194213451c9 beta-eta-contract, to respect "first_order_match"'s specification;
blanchet
parents: 37388
diff changeset
   363
  let
37410
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents: 37398
diff changeset
   364
    fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
37398
e194213451c9 beta-eta-contract, to respect "first_order_match"'s specification;
blanchet
parents: 37388
diff changeset
   365
      | tryall (rl :: rls) =
e194213451c9 beta-eta-contract, to respect "first_order_match"'s specification;
blanchet
parents: 37388
diff changeset
   366
        first_order_resolve th rl handle THM _ => tryall rls
e194213451c9 beta-eta-contract, to respect "first_order_match"'s specification;
blanchet
parents: 37388
diff changeset
   367
  in tryall rls end
22515
f4061faa5fda "generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
paulson
parents: 22381
diff changeset
   368
37410
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents: 37398
diff changeset
   369
(* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents: 37398
diff changeset
   370
   Strips universal quantifiers and breaks up conjunctions.
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents: 37398
diff changeset
   371
   Eliminates existential quantifiers using Skolemization theorems. *)
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   372
fun cnf old_skolem_ths ctxt ctxt0 (th, ths) =
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   373
  let val ctxt0r = Unsynchronized.ref ctxt0   (* FIXME ??? *)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   374
      fun cnf_aux (th,ths) =
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   375
        if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   376
        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   377
        then nodups ctxt0 th :: ths (*no work to do, terminate*)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   378
        else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   379
            Const (@{const_name HOL.conj}, _) => (*conjunction*)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   380
                cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   381
          | Const (@{const_name All}, _) => (*universal quantifier*)
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   382
                let val (th',ctxt0') = freeze_spec th (!ctxt0r)
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   383
                in  ctxt0r := ctxt0'; cnf_aux (th', ths) end
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   384
          | Const (@{const_name Ex}, _) =>
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   385
              (*existential quantifier: Insert Skolem functions*)
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39328
diff changeset
   386
              cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   387
          | Const (@{const_name HOL.disj}, _) =>
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   388
              (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   389
                all combinations of converting P, Q to CNF.*)
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   390
              let val tac =
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents: 37539
diff changeset
   391
                  Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents: 37539
diff changeset
   392
                   (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   393
              in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   394
          | _ => nodups ctxt0 th :: ths  (*no work to do*)
19154
f48e36b7d8d4 fixed but in freeze_spec
paulson
parents: 19112
diff changeset
   395
      and cnf_nil th = cnf_aux (th,[])
39269
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
   396
      val cls =
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   397
        if has_too_many_clauses ctxt (concl_of th) then
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   398
          (trace_msg ctxt (fn () =>
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   399
               "cnf is ignoring: " ^ Display.string_of_thm ctxt0 th); ths)
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   400
        else
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   401
          cnf_aux (th, ths)
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   402
  in (cls, !ctxt0r) end
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   403
fun make_cnf old_skolem_ths th ctxt ctxt0 =
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   404
  cnf old_skolem_ths ctxt ctxt0 (th, [])
20417
c611b1412056 better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents: 20361
diff changeset
   405
c611b1412056 better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents: 20361
diff changeset
   406
(*Generalization, removal of redundant equalities, removal of tautologies.*)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   407
fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   408
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   409
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   410
(**** Generation of contrapositives ****)
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   411
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   412
fun is_left (Const (@{const_name Trueprop}, _) $
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   413
               (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true
21102
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   414
  | is_left _ = false;
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   415
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   416
(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   417
fun assoc_right th =
21102
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   418
  if is_left (prop_of th) then assoc_right (th RS disj_assoc)
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   419
  else th;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   420
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   421
(*Must check for negative literal first!*)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   422
val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   423
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   424
(*For ordinary resolution. *)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   425
val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   426
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   427
(*Create a goal or support clause, conclusing False*)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   428
fun make_goal th =   (*Must check for negative literal first!*)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   429
    make_goal (tryres(th, clause_rules))
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   430
  handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   431
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   432
(*Sort clauses by number of literals*)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   433
fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   434
18389
8352b1d3b639 removal of functional reflexivity axioms
paulson
parents: 18194
diff changeset
   435
fun sort_clauses ths = sort (make_ord fewerlits) ths;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   436
38099
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38089
diff changeset
   437
fun has_bool @{typ bool} = true
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38089
diff changeset
   438
  | has_bool (Type (_, Ts)) = exists has_bool Ts
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38089
diff changeset
   439
  | has_bool _ = false
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38089
diff changeset
   440
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38089
diff changeset
   441
fun has_fun (Type (@{type_name fun}, _)) = true
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38089
diff changeset
   442
  | has_fun (Type (_, Ts)) = exists has_fun Ts
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38089
diff changeset
   443
  | has_fun _ = false
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   444
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   445
(*Is the string the name of a connective? Really only | and Not can remain,
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   446
  since this code expects to be called on a clause form.*)
19875
7405ce9d4f25 avoid unqualified exception names;
wenzelm
parents: 19728
diff changeset
   447
val is_conn = member (op =)
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   448
    [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38709
diff changeset
   449
     @{const_name HOL.implies}, @{const_name Not},
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   450
     @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
15613
ab90e95ae02e meson now checks that problems are first-order
paulson
parents: 15581
diff changeset
   451
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   452
(*True if the term contains a function--not a logical connective--where the type
20524
1493053fc111 Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective
paulson
parents: 20417
diff changeset
   453
  of any argument contains bool.*)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   454
val has_bool_arg_const =
15613
ab90e95ae02e meson now checks that problems are first-order
paulson
parents: 15581
diff changeset
   455
    exists_Const
38099
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38089
diff changeset
   456
      (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
22381
cb145d434284 The first-order test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents: 22360
diff changeset
   457
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   458
(*A higher-order instance of a first-order constant? Example is the definition of
38622
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 38557
diff changeset
   459
  one, 1, at a function type in theory Function_Algebras.*)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   460
fun higher_inst_const thy (c,T) =
22381
cb145d434284 The first-order test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents: 22360
diff changeset
   461
  case binder_types T of
cb145d434284 The first-order test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents: 22360
diff changeset
   462
      [] => false (*not a function type, OK*)
cb145d434284 The first-order test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents: 22360
diff changeset
   463
    | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
cb145d434284 The first-order test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents: 22360
diff changeset
   464
42833
c0abc218b8b4 use antiquotation
blanchet
parents: 42793
diff changeset
   465
(* Returns false if any Vars in the theorem mention type bool.
c0abc218b8b4 use antiquotation
blanchet
parents: 42793
diff changeset
   466
   Also rejects functions whose arguments are Booleans or other functions. *)
22381
cb145d434284 The first-order test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents: 22360
diff changeset
   467
fun is_fol_term thy t =
42833
c0abc218b8b4 use antiquotation
blanchet
parents: 42793
diff changeset
   468
    Term.is_first_order [@{const_name all}, @{const_name All},
c0abc218b8b4 use antiquotation
blanchet
parents: 42793
diff changeset
   469
                         @{const_name Ex}] t andalso
38099
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38089
diff changeset
   470
    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
42833
c0abc218b8b4 use antiquotation
blanchet
parents: 42793
diff changeset
   471
                          | _ => false) t orelse
38099
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38089
diff changeset
   472
         has_bool_arg_const t orelse
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   473
         exists_Const (higher_inst_const thy) t orelse
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   474
         has_meta_conn t);
19204
b8f7de7ef629 Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents: 19154
diff changeset
   475
21102
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   476
fun rigid t = not (is_Var (head_of t));
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   477
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   478
fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   479
  | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
21102
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   480
  | ok4horn _ = false;
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   481
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   482
(*Create a meta-level Horn clause*)
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   483
fun make_horn crules th =
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   484
  if ok4horn (concl_of th)
21102
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   485
  then make_horn crules (tryres(th,crules)) handle THM _ => th
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   486
  else th;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   487
16563
a92f96951355 meson method taking an argument list
paulson
parents: 16173
diff changeset
   488
(*Generate Horn clauses for all contrapositives of a clause. The input, th,
a92f96951355 meson method taking an argument list
paulson
parents: 16173
diff changeset
   489
  is a HOL disjunction.*)
33339
d41f77196338 eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   490
fun add_contras crules th hcs =
39328
blanchet
parents: 39277
diff changeset
   491
  let fun rots (0,_) = hcs
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   492
        | rots (k,th) = zero_var_indexes (make_horn crules th) ::
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   493
                        rots(k-1, assoc_right (th RS disj_comm))
15862
67574c1b15a0 removed unnecessary (?) check
paulson
parents: 15779
diff changeset
   494
  in case nliterals(prop_of th) of
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   495
        1 => th::hcs
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   496
      | n => rots(n, assoc_right th)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   497
  end;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   498
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   499
(*Use "theorem naming" to label the clauses*)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   500
fun name_thms label =
33339
d41f77196338 eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   501
    let fun name1 th (k, ths) =
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 27239
diff changeset
   502
          (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
33339
d41f77196338 eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   503
    in  fn ths => #2 (fold_rev name1 ths (length ths, []))  end;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   504
16563
a92f96951355 meson method taking an argument list
paulson
parents: 16173
diff changeset
   505
(*Is the given disjunction an all-negative support clause?*)
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   506
fun is_negative th = forall (not o #1) (literals (prop_of th));
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   507
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33245
diff changeset
   508
val neg_clauses = filter is_negative;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   509
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   510
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   511
(***** MESON PROOF PROCEDURE *****)
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   512
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   513
fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   514
           As) = rhyps(phi, A::As)
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   515
  | rhyps (_, As) = As;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   516
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   517
(** Detecting repeated assumptions in a subgoal **)
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   518
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   519
(*The stringtree detects repeated assumptions.*)
33245
65232054ffd0 eliminated some old folds;
wenzelm
parents: 33222
diff changeset
   520
fun ins_term t net = Net.insert_term (op aconv) (t, t) net;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   521
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   522
(*detects repetitions in a list of terms*)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   523
fun has_reps [] = false
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   524
  | has_reps [_] = false
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   525
  | has_reps [t,u] = (t aconv u)
33245
65232054ffd0 eliminated some old folds;
wenzelm
parents: 33222
diff changeset
   526
  | has_reps ts = (fold ins_term ts Net.empty; false) handle Net.INSERT => true;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   527
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   528
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
18508
paulson
parents: 18405
diff changeset
   529
fun TRYING_eq_assume_tac 0 st = Seq.single st
paulson
parents: 18405
diff changeset
   530
  | TRYING_eq_assume_tac i st =
31945
d5f186aa0bed structure Thm: less pervasive names;
wenzelm
parents: 31454
diff changeset
   531
       TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st)
18508
paulson
parents: 18405
diff changeset
   532
       handle THM _ => TRYING_eq_assume_tac (i-1) st;
paulson
parents: 18405
diff changeset
   533
paulson
parents: 18405
diff changeset
   534
fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   535
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   536
(*Loop checking: FAIL if trying to prove the same thing twice
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   537
  -- if *ANY* subgoal has repeated literals*)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   538
fun check_tac st =
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   539
  if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   540
  then  Seq.empty  else  Seq.single st;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   541
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   542
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   543
(* net_resolve_tac actually made it slower... *)
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   544
fun prolog_step_tac horns i =
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   545
    (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
18508
paulson
parents: 18405
diff changeset
   546
    TRYALL_eq_assume_tac;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   547
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   548
(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
33339
d41f77196338 eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   549
fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz;
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   550
33339
d41f77196338 eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   551
fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0;
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15574
diff changeset
   552
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   553
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   554
(*Negation Normal Form*)
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   555
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
9869
95dca9f991f2 improved meson setup;
wenzelm
parents: 9840
diff changeset
   556
               not_impD, not_iffD, not_allD, not_exD, not_notD];
15581
f07e865d9d40 now checks for higher-order vars
paulson
parents: 15579
diff changeset
   557
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   558
fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   559
  | ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t
21102
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   560
  | ok4nnf _ = false;
7f2ebe5c5b72 Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents: 21095
diff changeset
   561
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   562
fun make_nnf1 ctxt th =
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   563
  if ok4nnf (concl_of th)
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   564
  then make_nnf1 ctxt (tryres(th, nnf_rls))
28174
626f0a79a4b9 more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
paulson
parents: 27865
diff changeset
   565
    handle THM ("tryres", _, _) =>
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   566
        forward_res ctxt (make_nnf1 ctxt)
9869
95dca9f991f2 improved meson setup;
wenzelm
parents: 9840
diff changeset
   567
           (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
28174
626f0a79a4b9 more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
paulson
parents: 27865
diff changeset
   568
    handle THM ("tryres", _, _) => th
38608
01ed56c46259 beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents: 38606
diff changeset
   569
  else th
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   570
42739
017e5dac8642 added unfold set constant functionality to Meson/Metis -- disabled by default for now
blanchet
parents: 42616
diff changeset
   571
fun unfold_set_const_simps ctxt =
45981
4c629115e3ab dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
haftmann
parents: 45740
diff changeset
   572
  if Config.get ctxt unfold_set_consts then []
42739
017e5dac8642 added unfold set constant functionality to Meson/Metis -- disabled by default for now
blanchet
parents: 42616
diff changeset
   573
  else []
017e5dac8642 added unfold set constant functionality to Meson/Metis -- disabled by default for now
blanchet
parents: 42616
diff changeset
   574
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   575
(*The simplification removes defined quantifiers and occurrences of True and False.
20018
5419a71d0baa removed the "tagging" feature
paulson
parents: 19894
diff changeset
   576
  nnf_ss also includes the one-point simprocs,
18405
afb1a52a7011 removal of some redundancies (e.g. one-point-rules) in clause production
paulson
parents: 18389
diff changeset
   577
  which are needed to avoid the various one-point theorems from generating junk clauses.*)
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19875
diff changeset
   578
val nnf_simps =
37539
c80e77e8d036 cosmetics
blanchet
parents: 37410
diff changeset
   579
  @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
c80e77e8d036 cosmetics
blanchet
parents: 37410
diff changeset
   580
         if_eq_cancel cases_simp}
c80e77e8d036 cosmetics
blanchet
parents: 37410
diff changeset
   581
val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
18405
afb1a52a7011 removal of some redundancies (e.g. one-point-rules) in clause production
paulson
parents: 18389
diff changeset
   582
43821
048619bb1dc3 always unfold "Let"s is Sledgehammer, Metis, and MESON
blanchet
parents: 43264
diff changeset
   583
(* FIXME: "let_simp" is probably redundant now that we also rewrite with
048619bb1dc3 always unfold "Let"s is Sledgehammer, Metis, and MESON
blanchet
parents: 43264
diff changeset
   584
  "Let_def_raw". *)
18405
afb1a52a7011 removal of some redundancies (e.g. one-point-rules) in clause production
paulson
parents: 18389
diff changeset
   585
val nnf_ss =
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   586
  HOL_basic_ss addsimps nnf_extra_simps
43264
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 42833
diff changeset
   587
    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 42833
diff changeset
   588
                 @{simproc let_simp}]
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 42833
diff changeset
   589
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 42833
diff changeset
   590
fun presimplified_consts ctxt =
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 42833
diff changeset
   591
  [@{const_name simp_implies}, @{const_name False}, @{const_name True},
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 42833
diff changeset
   592
   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If},
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 42833
diff changeset
   593
   @{const_name Let}]
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 42833
diff changeset
   594
  |> Config.get ctxt unfold_set_consts
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 42833
diff changeset
   595
     ? append ([@{const_name Collect}, @{const_name Set.member}])
15872
8336ff711d80 fixed treatment of higher-order simprules
paulson
parents: 15862
diff changeset
   596
42750
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   597
fun presimplify ctxt =
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   598
  rewrite_rule (map safe_mk_meta_eq nnf_simps)
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   599
  #> simplify nnf_ss
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   600
  (* TODO: avoid introducing "Set.member" in "Ball_def" "Bex_def" above if and
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   601
     when "metis_unfold_set_consts" becomes the only mode of operation. *)
43821
048619bb1dc3 always unfold "Let"s is Sledgehammer, Metis, and MESON
blanchet
parents: 43264
diff changeset
   602
  #> Raw_Simplifier.rewrite_rule
048619bb1dc3 always unfold "Let"s is Sledgehammer, Metis, and MESON
blanchet
parents: 43264
diff changeset
   603
         (@{thm Let_def_raw} :: unfold_set_const_simps ctxt)
38089
ed65a0777e10 perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents: 37926
diff changeset
   604
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   605
fun make_nnf ctxt th = case prems_of th of
42750
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   606
    [] => th |> presimplify ctxt |> make_nnf1 ctxt
21050
d0447a511edb More robust error handling in make_nnf and forward_res
paulson
parents: 21046
diff changeset
   607
  | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
15581
f07e865d9d40 now checks for higher-order vars
paulson
parents: 15579
diff changeset
   608
39950
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39941
diff changeset
   609
fun choice_theorems thy =
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39941
diff changeset
   610
  try (Global_Theory.get_thm thy) "Hilbert_Choice.choice" |> the_list
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39941
diff changeset
   611
39900
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   612
(* Pull existential quantifiers to front. This accomplishes Skolemization for
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   613
   clauses that arise from a subgoal. *)
39950
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39941
diff changeset
   614
fun skolemize_with_choice_theorems ctxt choice_ths =
39900
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   615
  let
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   616
    fun aux th =
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   617
      if not (has_conns [@{const_name Ex}] (prop_of th)) then
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   618
        th
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   619
      else
39901
75d792edf634 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents: 39900
diff changeset
   620
        tryres (th, choice_ths @
39900
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   621
                    [conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2])
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   622
        |> aux
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   623
        handle THM ("tryres", _, _) =>
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   624
               tryres (th, [conj_forward, disj_forward, all_forward])
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   625
               |> forward_res ctxt aux
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   626
               |> aux
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   627
               handle THM ("tryres", _, _) =>
40262
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 39979
diff changeset
   628
                      rename_bound_vars_RS th ex_forward
39900
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   629
                      |> forward_res ctxt aux
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   630
  in aux o make_nnf ctxt end
29684
40bf9f4e7a4e Minor reorganisation of the Skolemization code
paulson
parents: 29267
diff changeset
   631
39950
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39941
diff changeset
   632
fun skolemize ctxt =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42346
diff changeset
   633
  let val thy = Proof_Context.theory_of ctxt in
39950
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39941
diff changeset
   634
    skolemize_with_choice_theorems ctxt (choice_theorems thy)
f3c4849868b8 got rid of overkill "meson_choice" attribute;
blanchet
parents: 39941
diff changeset
   635
  end
39904
f9e89d36a31a tune bound names
blanchet
parents: 39901
diff changeset
   636
42760
d83802e7348e another concession to backward compatibility
blanchet
parents: 42750
diff changeset
   637
(* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
d83802e7348e another concession to backward compatibility
blanchet
parents: 42750
diff changeset
   638
   would be desirable to do this symmetrically but there's at least one existing
d83802e7348e another concession to backward compatibility
blanchet
parents: 42750
diff changeset
   639
   proof in "Tarski" that relies on the current behavior. *)
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   640
fun extensionalize_conv ctxt ct =
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   641
  case term_of ct of
42760
d83802e7348e another concession to backward compatibility
blanchet
parents: 42750
diff changeset
   642
    Const (@{const_name HOL.eq}, _) $ _ $ Abs _ =>
d83802e7348e another concession to backward compatibility
blanchet
parents: 42750
diff changeset
   643
    ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
d83802e7348e another concession to backward compatibility
blanchet
parents: 42750
diff changeset
   644
           then_conv extensionalize_conv ctxt)
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   645
  | _ $ _ => Conv.comb_conv (extensionalize_conv ctxt) ct
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   646
  | Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   647
  | _ => Conv.all_conv ct
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   648
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   649
val extensionalize_theorem = Conv.fconv_rule o extensionalize_conv
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   650
39900
549c00e0e89b added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents: 39893
diff changeset
   651
(* "RS" can fail if "unify_search_bound" is too small. *)
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   652
fun try_skolemize_etc ctxt =
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   653
  Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   654
  (* Extensionalize "th", because that makes sense and that's what Sledgehammer
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   655
     does, but also keep an unextensionalized version of "th" for backward
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   656
     compatibility. *)
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   657
  #> (fn th => insert Thm.eq_thm_prop (extensionalize_theorem ctxt th) [th])
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   658
  #> map_filter (fn th => try (skolemize ctxt) th
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   659
                          |> tap (fn NONE =>
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   660
                                     trace_msg ctxt (fn () =>
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   661
                                         "Failed to skolemize " ^
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   662
                                          Display.string_of_thm ctxt th)
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   663
                                   | _ => ()))
25694
cbb59ba6bf0c Skolemization now catches exception THM, which may be raised if unification fails.
paulson
parents: 24937
diff changeset
   664
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   665
fun add_clauses ctxt th cls =
36603
d5d6111761a6 renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
wenzelm
parents: 36001
diff changeset
   666
  let val ctxt0 = Variable.global_thm_context th
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   667
      val (cnfs, ctxt) = make_cnf [] th ctxt ctxt0
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24827
diff changeset
   668
  in Variable.export ctxt ctxt0 cnfs @ cls end;
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   669
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   670
(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   671
  The resulting clauses are HOL disjunctions.*)
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   672
fun make_clauses_unsorted ctxt ths = fold_rev (add_clauses ctxt) ths [];
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   673
val make_clauses = sort_clauses oo make_clauses_unsorted;
15773
f14ae2432710 Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents: 15736
diff changeset
   674
16563
a92f96951355 meson method taking an argument list
paulson
parents: 16173
diff changeset
   675
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
9869
95dca9f991f2 improved meson setup;
wenzelm
parents: 9840
diff changeset
   676
fun make_horns ths =
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   677
    name_thms "Horn#"
33339
d41f77196338 eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   678
      (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths []));
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   679
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   680
(*Could simply use nprems_of, which would count remaining subgoals -- no
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   681
  discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   682
9869
95dca9f991f2 improved meson setup;
wenzelm
parents: 9840
diff changeset
   683
fun best_prolog_tac sizef horns =
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   684
    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   685
9869
95dca9f991f2 improved meson setup;
wenzelm
parents: 9840
diff changeset
   686
fun depth_prolog_tac horns =
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   687
    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   688
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   689
(*Return all negative clauses, as possible goal clauses*)
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   690
fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   691
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   692
fun skolemize_prems_tac ctxt prems =
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42739
diff changeset
   693
  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o etac exE
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   694
22546
c40d7ab8cbc5 MESON tactical takes an additional argument: the clausification function.
paulson
parents: 22515
diff changeset
   695
(*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
c40d7ab8cbc5 MESON tactical takes an additional argument: the clausification function.
paulson
parents: 22515
diff changeset
   696
  Function mkcl converts theorems to clauses.*)
39037
5146d640aa4a Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents: 38864
diff changeset
   697
fun MESON preskolem_tac mkcl cltac ctxt i st =
16588
8de758143786 stricter first-order check for meson
paulson
parents: 16563
diff changeset
   698
  SELECT_GOAL
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35410
diff changeset
   699
    (EVERY [Object_Logic.atomize_prems_tac 1,
23552
6403d06abe25 to handle non-atomic assumptions
paulson
parents: 23440
diff changeset
   700
            rtac ccontr 1,
39269
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
   701
            preskolem_tac,
32283
3bebc195c124 qualified Subgoal.FOCUS;
wenzelm
parents: 32262
diff changeset
   702
            Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
39269
c2795d8a2461 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents: 39159
diff changeset
   703
                      EVERY1 [skolemize_prems_tac ctxt negs,
32283
3bebc195c124 qualified Subgoal.FOCUS;
wenzelm
parents: 32262
diff changeset
   704
                              Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   705
  handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   706
39037
5146d640aa4a Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents: 38864
diff changeset
   707
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   708
(** Best-first search versions **)
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   709
16563
a92f96951355 meson method taking an argument list
paulson
parents: 16173
diff changeset
   710
(*ths is a list of additional clauses (HOL disjunctions) to use.*)
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   711
fun best_meson_tac sizef ctxt =
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   712
  MESON all_tac (make_clauses ctxt)
22546
c40d7ab8cbc5 MESON tactical takes an additional argument: the clausification function.
paulson
parents: 22515
diff changeset
   713
    (fn cls =>
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   714
         THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   715
                         (has_fewer_prems 1, sizef)
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   716
                         (prolog_step_tac (make_horns cls) 1))
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   717
    ctxt
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   718
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   719
(*First, breaks the goal into independent units*)
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   720
fun safe_best_meson_tac ctxt =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42760
diff changeset
   721
  SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (best_meson_tac size_of_subgoals ctxt));
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   722
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   723
(** Depth-first search version **)
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   724
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   725
fun depth_meson_tac ctxt =
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   726
  MESON all_tac (make_clauses ctxt)
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   727
    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)])
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   728
    ctxt
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   729
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   730
(** Iterative deepening version **)
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   731
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   732
(*This version does only one inference per call;
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   733
  having only one eq_assume_tac speeds it up!*)
9869
95dca9f991f2 improved meson setup;
wenzelm
parents: 9840
diff changeset
   734
fun prolog_step_tac' horns =
39328
blanchet
parents: 39277
diff changeset
   735
    let val (horn0s, _) = (*0 subgoals vs 1 or more*)
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   736
            take_prefix Thm.no_prems horns
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   737
        val nrtac = net_resolve_tac horns
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   738
    in  fn i => eq_assume_tac i ORELSE
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   739
                match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   740
                ((assume_tac i APPEND nrtac i) THEN check_tac)
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   741
    end;
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   742
9869
95dca9f991f2 improved meson setup;
wenzelm
parents: 9840
diff changeset
   743
fun iter_deepen_prolog_tac horns =
38802
a925c0ee42f7 clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents: 38795
diff changeset
   744
    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   745
43964
9338aa218f09 thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents: 43821
diff changeset
   746
fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt)
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32032
diff changeset
   747
  (fn cls =>
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32032
diff changeset
   748
    (case (gocls (cls @ ths)) of
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32032
diff changeset
   749
      [] => no_tac  (*no goal clauses*)
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32032
diff changeset
   750
    | goes =>
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32032
diff changeset
   751
        let
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32032
diff changeset
   752
          val horns = make_horns (cls @ ths)
39979
b13515940b53 added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents: 39953
diff changeset
   753
          val _ = trace_msg ctxt (fn () =>
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 32032
diff changeset
   754
            cat_lines ("meson method called:" ::
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   755
              map (Display.string_of_thm ctxt) (cls @ ths) @
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   756
              ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
38802
a925c0ee42f7 clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents: 38795
diff changeset
   757
        in
a925c0ee42f7 clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents: 38795
diff changeset
   758
          THEN_ITER_DEEPEN iter_deepen_limit
a925c0ee42f7 clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents: 38795
diff changeset
   759
            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
a925c0ee42f7 clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents: 38795
diff changeset
   760
        end));
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   761
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32231
diff changeset
   762
fun meson_tac ctxt ths =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42760
diff changeset
   763
  SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
9869
95dca9f991f2 improved meson setup;
wenzelm
parents: 9840
diff changeset
   764
95dca9f991f2 improved meson setup;
wenzelm
parents: 9840
diff changeset
   765
14813
826edbc317e6 new skolemize_tac and skolemize method
paulson
parents: 14763
diff changeset
   766
(**** Code to support ordinary resolution, rather than Model Elimination ****)
14744
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   767
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   768
(*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
15008
5abd18710a1f new method for explicit classical resolution
paulson
parents: 14890
diff changeset
   769
  with no contrapositives, for ordinary resolution.*)
14744
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   770
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   771
(*Rules to convert the head literal into a negated assumption. If the head
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   772
  literal is already negated, then using notEfalse instead of notEfalse'
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   773
  prevents a double negation.*)
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27230
diff changeset
   774
val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
14744
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   775
val notEfalse' = rotate_prems 1 notEfalse;
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   776
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   777
fun negated_asm_of_head th =
14744
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   778
    th RS notEfalse handle THM _ => th RS notEfalse';
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   779
26066
19df083a2bbf make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
paulson
parents: 25710
diff changeset
   780
(*Converting one theorem from a disjunction to a meta-level clause*)
19df083a2bbf make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
paulson
parents: 25710
diff changeset
   781
fun make_meta_clause th =
33832
cff42395c246 explicitly mark some legacy freeze operations;
wenzelm
parents: 33339
diff changeset
   782
  let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
26066
19df083a2bbf make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
paulson
parents: 25710
diff changeset
   783
  in  
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35625
diff changeset
   784
      (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
26066
19df083a2bbf make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
paulson
parents: 25710
diff changeset
   785
       negated_asm_of_head o make_horn resolution_clause_rules) fth
19df083a2bbf make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
paulson
parents: 25710
diff changeset
   786
  end;
24300
e170cee91c66 proper signature for Meson;
wenzelm
parents: 24040
diff changeset
   787
14744
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   788
fun make_meta_clauses ths =
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   789
    name_thms "MClause#"
22360
26ead7ed4f4b moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents: 22130
diff changeset
   790
      (distinct Thm.eq_thm_prop (map make_meta_clause ths));
14744
7ccfc167e451 clauses for ordinary resolution
paulson
parents: 14733
diff changeset
   791
9840
9dfcb0224f8c meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff changeset
   792
end;