added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
authorblanchet
Fri Oct 01 14:01:29 2010 +0200 (2010-10-01)
changeset 39900549c00e0e89b
parent 39899 608b108ec979
child 39901 75d792edf634
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
src/HOL/Hilbert_Choice.thy
src/HOL/Tools/Sledgehammer/meson_clausify.ML
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Oct 01 12:01:07 2010 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Oct 01 14:01:29 2010 +0200
     1.3 @@ -81,8 +81,17 @@
     1.4  
     1.5  subsection{*Axiom of Choice, Proved Using the Description Operator*}
     1.6  
     1.7 -text{*Used in @{text "Tools/meson.ML"}*}
     1.8 -lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
     1.9 +ML {*
    1.10 +structure Meson_Choices = Named_Thms
    1.11 +(
    1.12 +  val name = "meson_choice"
    1.13 +  val description = "choice axioms for MESON's (and Metis's) skolemizer"
    1.14 +)
    1.15 +*}
    1.16 +
    1.17 +setup Meson_Choices.setup
    1.18 +
    1.19 +lemma choice [meson_choice]: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
    1.20  by (fast elim: someI)
    1.21  
    1.22  lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
     2.1 --- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 12:01:07 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 14:01:29 2010 +0200
     2.3 @@ -281,6 +281,7 @@
     2.4      #> cprop_of #> Thm.dest_equals #> snd
     2.5    end
     2.6  
     2.7 +(* FIXME: needed? and should we add ex_simps[symmetric]? *)
     2.8  val pull_out_quant_ss =
     2.9    MetaSimplifier.clear_ss HOL_basic_ss
    2.10        addsimps @{thms all_simps[symmetric]}
     3.1 --- a/src/HOL/Tools/meson.ML	Fri Oct 01 12:01:07 2010 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Fri Oct 01 14:01:29 2010 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4    val best_prolog_tac: (thm -> int) -> thm list -> tactic
     3.5    val depth_prolog_tac: thm list -> tactic
     3.6    val gocls: thm list -> thm list
     3.7 -  val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic
     3.8 +  val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic
     3.9    val MESON:
    3.10      tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context
    3.11      -> int -> tactic
    3.12 @@ -62,7 +62,6 @@
    3.13  val conj_forward = @{thm conj_forward};
    3.14  val all_forward = @{thm all_forward};
    3.15  val ex_forward = @{thm ex_forward};
    3.16 -val choice = @{thm choice};
    3.17  
    3.18  val not_conjD = @{thm meson_not_conjD};
    3.19  val not_disjD = @{thm meson_not_disjD};
    3.20 @@ -523,33 +522,38 @@
    3.21      addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
    3.22  
    3.23  val presimplify =
    3.24 -  rewrite_rule (map safe_mk_meta_eq nnf_simps)
    3.25 -  #> simplify nnf_ss
    3.26 +  rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss
    3.27  
    3.28  fun make_nnf ctxt th = case prems_of th of
    3.29      [] => th |> presimplify |> make_nnf1 ctxt
    3.30    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    3.31  
    3.32 -(*Pull existential quantifiers to front. This accomplishes Skolemization for
    3.33 -  clauses that arise from a subgoal.*)
    3.34 -fun skolemize1 ctxt th =
    3.35 -  if not (has_conns [@{const_name Ex}] (prop_of th)) then th
    3.36 -  else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2,
    3.37 -                              disj_exD, disj_exD1, disj_exD2])))
    3.38 -    handle THM ("tryres", _, _) =>
    3.39 -        skolemize1 ctxt (forward_res ctxt (skolemize1 ctxt)
    3.40 -                   (tryres (th, [conj_forward, disj_forward, all_forward])))
    3.41 -    handle THM ("tryres", _, _) => 
    3.42 -        forward_res ctxt (skolemize1 ctxt) (rename_bvs_RS th ex_forward);
    3.43 +(* Pull existential quantifiers to front. This accomplishes Skolemization for
    3.44 +   clauses that arise from a subgoal. *)
    3.45 +fun skolemize ctxt =
    3.46 +  let
    3.47 +    fun aux th =
    3.48 +      if not (has_conns [@{const_name Ex}] (prop_of th)) then
    3.49 +        th
    3.50 +      else
    3.51 +        tryres (th, Meson_Choices.get ctxt @
    3.52 +                    [conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2])
    3.53 +        |> aux
    3.54 +        handle THM ("tryres", _, _) =>
    3.55 +               tryres (th, [conj_forward, disj_forward, all_forward])
    3.56 +               |> forward_res ctxt aux
    3.57 +               |> aux
    3.58 +               handle THM ("tryres", _, _) =>
    3.59 +                      rename_bvs_RS th ex_forward
    3.60 +                      |> forward_res ctxt aux
    3.61 +  in aux o make_nnf ctxt end
    3.62  
    3.63 -fun skolemize ctxt th = skolemize1 ctxt (make_nnf ctxt th);
    3.64 -
    3.65 -fun skolemize_nnf_list _ [] = []
    3.66 -  | skolemize_nnf_list ctxt (th::ths) =
    3.67 -      skolemize ctxt th :: skolemize_nnf_list ctxt ths
    3.68 -      handle THM _ => (*RS can fail if Unify.search_bound is too small*)
    3.69 -       (trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th);
    3.70 -        skolemize_nnf_list ctxt ths);
    3.71 +(* "RS" can fail if "unify_search_bound" is too small. *)
    3.72 +fun try_skolemize ctxt th =
    3.73 +  try (skolemize ctxt) th
    3.74 +  |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^
    3.75 +                                         Display.string_of_thm ctxt th)
    3.76 +           | _ => ())
    3.77  
    3.78  fun add_clauses th cls =
    3.79    let val ctxt0 = Variable.global_thm_context th
    3.80 @@ -579,7 +583,7 @@
    3.81  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
    3.82  
    3.83  fun skolemize_prems_tac ctxt prems =
    3.84 -  cut_facts_tac (skolemize_nnf_list ctxt prems) THEN' REPEAT o etac exE
    3.85 +  cut_facts_tac (map_filter (try_skolemize ctxt) prems) THEN' REPEAT o etac exE
    3.86  
    3.87  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
    3.88    Function mkcl converts theorems to clauses.*)