use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
authorblanchet
Thu Jan 03 17:28:55 2013 +0100 (2013-01-03)
changeset 507050e943b33d907
parent 50704 cd1fcda1ea88
child 50706 573d84e08f3f
use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
src/HOL/Metis_Examples/Binary_Tree.thy
src/HOL/Metis_Examples/Clausification.thy
src/HOL/Metis_Examples/Message.thy
src/HOL/Metis_Examples/Sets.thy
src/HOL/Metis_Examples/Tarski.thy
src/HOL/Metis_Examples/Trans_Closure.thy
src/HOL/Metis_Examples/Type_Encodings.thy
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.1 --- a/src/HOL/Metis_Examples/Binary_Tree.thy	Thu Jan 03 17:10:12 2013 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Thu Jan 03 17:28:55 2013 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -declare [[metis_new_skolemizer]]
     1.8 +declare [[metis_new_skolem]]
     1.9  
    1.10  datatype 'a bt =
    1.11      Lf
     2.1 --- a/src/HOL/Metis_Examples/Clausification.thy	Thu Jan 03 17:10:12 2013 +0100
     2.2 +++ b/src/HOL/Metis_Examples/Clausification.thy	Thu Jan 03 17:28:55 2013 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4  axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     2.5  qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
     2.6  
     2.7 -declare [[metis_new_skolemizer = false]]
     2.8 +declare [[metis_new_skolem = false]]
     2.9  
    2.10  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    2.11  by (metis qax)
    2.12 @@ -32,7 +32,7 @@
    2.13  lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    2.14  by (metis (full_types) qax)
    2.15  
    2.16 -declare [[metis_new_skolemizer]]
    2.17 +declare [[metis_new_skolem]]
    2.18  
    2.19  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    2.20  by (metis qax)
    2.21 @@ -54,7 +54,7 @@
    2.22        (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
    2.23        (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
    2.24  
    2.25 -declare [[metis_new_skolemizer = false]]
    2.26 +declare [[metis_new_skolem = false]]
    2.27  
    2.28  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    2.29  by (metis rax)
    2.30 @@ -62,7 +62,7 @@
    2.31  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    2.32  by (metis (full_types) rax)
    2.33  
    2.34 -declare [[metis_new_skolemizer]]
    2.35 +declare [[metis_new_skolem]]
    2.36  
    2.37  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    2.38  by (metis rax)
    2.39 @@ -88,7 +88,7 @@
    2.40  axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    2.41  pax: "\<exists>b. \<forall>a. (p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b)"
    2.42  
    2.43 -declare [[metis_new_skolemizer = false]]
    2.44 +declare [[metis_new_skolem = false]]
    2.45  
    2.46  lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
    2.47                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    2.48 @@ -98,7 +98,7 @@
    2.49                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    2.50  by (metis (full_types) pax)
    2.51  
    2.52 -declare [[metis_new_skolemizer]]
    2.53 +declare [[metis_new_skolem]]
    2.54  
    2.55  lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
    2.56                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    2.57 @@ -111,7 +111,7 @@
    2.58  
    2.59  text {* New Skolemizer *}
    2.60  
    2.61 -declare [[metis_new_skolemizer]]
    2.62 +declare [[metis_new_skolem]]
    2.63  
    2.64  lemma
    2.65    fixes x :: real
     3.1 --- a/src/HOL/Metis_Examples/Message.thy	Thu Jan 03 17:10:12 2013 +0100
     3.2 +++ b/src/HOL/Metis_Examples/Message.thy	Thu Jan 03 17:28:55 2013 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -declare [[metis_new_skolemizer]]
     3.8 +declare [[metis_new_skolem]]
     3.9  
    3.10  lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
    3.11  by (metis Un_commute Un_left_absorb)
     4.1 --- a/src/HOL/Metis_Examples/Sets.thy	Thu Jan 03 17:10:12 2013 +0100
     4.2 +++ b/src/HOL/Metis_Examples/Sets.thy	Thu Jan 03 17:28:55 2013 +0100
     4.3 @@ -11,7 +11,7 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 -declare [[metis_new_skolemizer]]
     4.8 +declare [[metis_new_skolem]]
     4.9  
    4.10  lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
    4.11                 (S(x,y) | ~S(y,z) | Q(Z,Z))  &
     5.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Thu Jan 03 17:10:12 2013 +0100
     5.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Thu Jan 03 17:28:55 2013 +0100
     5.3 @@ -11,7 +11,7 @@
     5.4  imports Main "~~/src/HOL/Library/FuncSet"
     5.5  begin
     5.6  
     5.7 -declare [[metis_new_skolemizer]]
     5.8 +declare [[metis_new_skolem]]
     5.9  
    5.10  (*Many of these higher-order problems appear to be impossible using the
    5.11  current linkup. They often seem to need either higher-order unification
     6.1 --- a/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Jan 03 17:10:12 2013 +0100
     6.2 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Jan 03 17:28:55 2013 +0100
     6.3 @@ -11,7 +11,7 @@
     6.4  imports Main
     6.5  begin
     6.6  
     6.7 -declare [[metis_new_skolemizer]]
     6.8 +declare [[metis_new_skolem]]
     6.9  
    6.10  type_synonym addr = nat
    6.11  
     7.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy	Thu Jan 03 17:10:12 2013 +0100
     7.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Thu Jan 03 17:28:55 2013 +0100
     7.3 @@ -12,7 +12,7 @@
     7.4  imports Main
     7.5  begin
     7.6  
     7.7 -declare [[metis_new_skolemizer]]
     7.8 +declare [[metis_new_skolem]]
     7.9  
    7.10  sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30,
    7.11                       preplay_timeout = 0, dont_minimize]
     8.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Jan 03 17:10:12 2013 +0100
     8.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Jan 03 17:28:55 2013 +0100
     8.3 @@ -300,20 +300,20 @@
     8.4    |> Skip_Proof.make_thm @{theory}
     8.5  
     8.6  (* Converts an Isabelle theorem into NNF. *)
     8.7 -fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt =
     8.8 +fun nnf_axiom choice_ths new_skolem ax_no th ctxt =
     8.9    let
    8.10      val thy = Proof_Context.theory_of ctxt
    8.11      val th =
    8.12        th |> transform_elim_theorem
    8.13           |> zero_var_indexes
    8.14 -         |> new_skolemizer ? forall_intr_vars
    8.15 +         |> new_skolem ? forall_intr_vars
    8.16      val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
    8.17      val th = th |> Conv.fconv_rule Object_Logic.atomize
    8.18                  |> cong_extensionalize_thm thy
    8.19                  |> abs_extensionalize_thm ctxt
    8.20                  |> make_nnf ctxt
    8.21    in
    8.22 -    if new_skolemizer then
    8.23 +    if new_skolem then
    8.24        let
    8.25          fun skolemize choice_ths =
    8.26            skolemize_with_choice_theorems ctxt choice_ths
    8.27 @@ -364,14 +364,14 @@
    8.28    end
    8.29  
    8.30  (* Convert a theorem to CNF, with additional premises due to skolemization. *)
    8.31 -fun cnf_axiom ctxt0 new_skolemizer combinators ax_no th =
    8.32 +fun cnf_axiom ctxt0 new_skolem combinators ax_no th =
    8.33    let
    8.34      val thy = Proof_Context.theory_of ctxt0
    8.35      val choice_ths = choice_theorems thy
    8.36      val (opt, (nnf_th, ctxt)) =
    8.37 -      nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
    8.38 +      nnf_axiom choice_ths new_skolem ax_no th ctxt0
    8.39      fun clausify th =
    8.40 -      make_cnf (if new_skolemizer orelse null choice_ths then []
    8.41 +      make_cnf (if new_skolem orelse null choice_ths then []
    8.42                  else map (old_skolem_theorem_from_def thy) (old_skolem_defs th))
    8.43                 th ctxt ctxt
    8.44      val (cnf_ths, ctxt) = clausify nnf_th
     9.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 03 17:10:12 2013 +0100
     9.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 03 17:28:55 2013 +0100
     9.3 @@ -11,7 +11,7 @@
     9.4  sig
     9.5    val trace : bool Config.T
     9.6    val verbose : bool Config.T
     9.7 -  val new_skolemizer : bool Config.T
     9.8 +  val new_skolem : bool Config.T
     9.9    val advisory_simp : bool Config.T
    9.10    val type_has_top_sort : typ -> bool
    9.11    val metis_tac :
    9.12 @@ -29,8 +29,8 @@
    9.13  open Metis_Generate
    9.14  open Metis_Reconstruct
    9.15  
    9.16 -val new_skolemizer =
    9.17 -  Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    9.18 +val new_skolem =
    9.19 +  Attrib.setup_config_bool @{binding metis_new_skolem} (K false)
    9.20  val advisory_simp =
    9.21    Attrib.setup_config_bool @{binding metis_advisory_simp} (K true)
    9.22  
    9.23 @@ -137,8 +137,8 @@
    9.24  (* Main function to start Metis proof and reconstruction *)
    9.25  fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
    9.26    let val thy = Proof_Context.theory_of ctxt
    9.27 -      val new_skolemizer =
    9.28 -        Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    9.29 +      val new_skolem =
    9.30 +        Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
    9.31        val do_lams =
    9.32          (lam_trans = liftingN orelse lam_trans = lam_liftingN)
    9.33          ? introduce_lam_wrappers ctxt
    9.34 @@ -146,7 +146,7 @@
    9.35          map2 (fn j => fn th =>
    9.36                  (Thm.get_name_hint th,
    9.37                   th |> Drule.eta_contraction_rule
    9.38 -                    |> Meson_Clausify.cnf_axiom ctxt new_skolemizer
    9.39 +                    |> Meson_Clausify.cnf_axiom ctxt new_skolem
    9.40                                                  (lam_trans = combsN) j
    9.41                      ||> map do_lams))
    9.42               (0 upto length ths0 - 1) ths0
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 03 17:10:12 2013 +0100
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 03 17:28:55 2013 +0100
    10.3 @@ -482,8 +482,8 @@
    10.4        #> simplify_spaces
    10.5        #> maybe_quote
    10.6      val reconstr = Metis (type_enc, lam_trans)
    10.7 -    fun do_metis ind (ls, ss) =
    10.8 -      "\n" ^ do_indent (ind + 1) ^
    10.9 +    fun do_metis ind options (ls, ss) =
   10.10 +      "\n" ^ do_indent (ind + 1) ^ options ^
   10.11        reconstructor_command reconstr 1 1 [] 0
   10.12            (ls |> sort_distinct (prod_ord string_ord int_ord),
   10.13             ss |> sort_distinct string_ord)
   10.14 @@ -495,15 +495,19 @@
   10.15          do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   10.16        | do_step ind (Obtain (qs, xs, l, t, By_Metis facts)) =
   10.17          do_indent ind ^ do_obtain qs xs ^ " " ^
   10.18 -        do_label l ^ do_term t ^ do_metis ind facts ^ "\n"
   10.19 +        do_label l ^ do_term t ^
   10.20 +        (* The new skolemizer puts the arguments in the same order as the ATPs
   10.21 +           (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
   10.22 +           Vampire). *)
   10.23 +        do_metis ind "using [[metis_new_skolem]] " facts ^ "\n"
   10.24        | do_step ind (Prove (qs, l, t, By_Metis facts)) =
   10.25          do_indent ind ^ do_have qs ^ " " ^
   10.26 -        do_label l ^ do_term t ^ do_metis ind facts ^ "\n"
   10.27 +        do_label l ^ do_term t ^ do_metis ind "" facts ^ "\n"
   10.28        | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
   10.29          implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
   10.30                       proofs) ^
   10.31          do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^
   10.32 -        do_metis ind facts ^ "\n"
   10.33 +        do_metis ind "" facts ^ "\n"
   10.34      and do_steps prefix suffix ind steps =
   10.35        let val s = implode (map (do_step ind) steps) in
   10.36          replicate_string (ind * indent_size - size prefix) " " ^ prefix ^