ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
authorblanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 42750c8b1d9ee3758
parent 42749 47f283fcf2ae
child 42751 f42fd9754724
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
     1.5    val finish_cnf: thm list -> thm list
     1.6    val unfold_set_const_simps : Proof.context -> thm list
     1.7 -  val presimplify: thm -> thm
     1.8 +  val presimplify: Proof.context -> thm -> thm
     1.9    val make_nnf: Proof.context -> thm -> thm
    1.10    val choice_theorems : theory -> thm list
    1.11    val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
    1.12 @@ -577,11 +577,15 @@
    1.13    HOL_basic_ss addsimps nnf_extra_simps
    1.14      addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, @{simproc let_simp}];
    1.15  
    1.16 -val presimplify =
    1.17 -  rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss
    1.18 +fun presimplify ctxt =
    1.19 +  rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.20 +  #> simplify nnf_ss
    1.21 +  (* TODO: avoid introducing "Set.member" in "Ball_def" "Bex_def" above if and
    1.22 +     when "metis_unfold_set_consts" becomes the only mode of operation. *)
    1.23 +  #> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
    1.24  
    1.25  fun make_nnf ctxt th = case prems_of th of
    1.26 -    [] => th |> presimplify |> make_nnf1 ctxt
    1.27 +    [] => th |> presimplify ctxt |> make_nnf1 ctxt
    1.28    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    1.29  
    1.30  fun choice_theorems thy =
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
     2.3 @@ -345,7 +345,10 @@
     2.4        | _ => do_term bs t
     2.5    in do_formula [] end
     2.6  
     2.7 -val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
     2.8 +fun presimplify_term ctxt =
     2.9 +  Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    2.10 +  #> Meson.presimplify ctxt
    2.11 +  #> prop_of
    2.12  
    2.13  fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
    2.14  fun conceal_bounds Ts t =
    2.15 @@ -424,7 +427,7 @@
    2.16                |> Raw_Simplifier.rewrite_term thy
    2.17                       (Meson.unfold_set_const_simps ctxt) []
    2.18                |> extensionalize_term ctxt
    2.19 -              |> presimp ? presimplify_term thy
    2.20 +              |> presimp ? presimplify_term ctxt
    2.21                |> perhaps (try (HOLogic.dest_Trueprop))
    2.22                |> introduce_combinators_in_term ctxt kind
    2.23                |> kind <> Axiom ? freeze_term