--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 11 22:20:45 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 11 22:20:45 2013 +0200
@@ -12,11 +12,11 @@
fun extract_relevance_fudge args
{local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight,
- abs_rel_weight, abs_irrel_weight, skolem_irrel_weight,
- theory_const_rel_weight, theory_const_irrel_weight,
- chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus,
- local_bonus, assum_bonus, chained_bonus, max_imperfect, max_imperfect_exp,
- threshold_divisor, ridiculous_threshold} =
+ abs_rel_weight, abs_irrel_weight, theory_const_rel_weight,
+ theory_const_irrel_weight, chained_const_irrel_weight, intro_bonus,
+ elim_bonus, simp_bonus, local_bonus, assum_bonus, chained_bonus,
+ max_imperfect, max_imperfect_exp, threshold_divisor,
+ ridiculous_threshold} =
{local_const_multiplier =
get args "local_const_multiplier" local_const_multiplier,
worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
@@ -24,7 +24,6 @@
get args "higher_order_irrel_weight" higher_order_irrel_weight,
abs_rel_weight = get args "abs_rel_weight" abs_rel_weight,
abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight,
- skolem_irrel_weight = get args "skolem_irrel_weight" skolem_irrel_weight,
theory_const_rel_weight =
get args "theory_const_rel_weight" theory_const_rel_weight,
theory_const_irrel_weight =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Sep 11 22:20:45 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Sep 11 22:20:45 2013 +0200
@@ -94,13 +94,8 @@
val set_consts = [@{const_name Collect}, @{const_name Set.member}]
val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
-fun add_pconsts_in_term thy is_built_in_const pos =
+fun add_pconsts_in_term thy is_built_in_const =
let
- val flip = Option.map not
- (* We include free variables, as well as constants, to handle locales. For
- each quantifiers that must necessarily be skolemized by the automatic
- prover, we introduce a fresh constant to simulate the effect of
- Skolemization. *)
fun do_const const ext_arg (x as (s, _)) ts =
let val (built_in, ts) = is_built_in_const x ts in
if member (op =) set_consts s then
@@ -123,52 +118,41 @@
PType (order_of_type T + 1, [])))
#> fold (do_term false) (t' :: ts)
| (_, ts) => fold (do_term false) ts
- fun do_quantifier will_surely_be_skolemized abs_T body_t =
- do_formula pos body_t
and do_term_or_formula ext_arg T =
- if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
- and do_formula pos t =
+ if T = HOLogic.boolT then do_formula else do_term ext_arg
+ and do_formula t =
case t of
- Const (@{const_name all}, _) $ Abs (_, T, t') =>
- do_quantifier (pos = SOME false) T t'
- | @{const "==>"} $ t1 $ t2 =>
- do_formula (flip pos) t1 #> do_formula pos t2
+ Const (@{const_name all}, _) $ Abs (_, T, t') => do_formula t'
+ | @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2
| Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
do_term_or_formula false T t1 #> do_term_or_formula true T t2
- | @{const Trueprop} $ t1 => do_formula pos t1
+ | @{const Trueprop} $ t1 => do_formula t1
| @{const False} => I
| @{const True} => I
- | @{const Not} $ t1 => do_formula (flip pos) t1
- | Const (@{const_name All}, _) $ Abs (_, T, t') =>
- do_quantifier (pos = SOME false) T t'
- | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
- do_quantifier (pos = SOME true) T t'
- | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
- | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
- | @{const HOL.implies} $ t1 $ t2 =>
- do_formula (flip pos) t1 #> do_formula pos t2
+ | @{const Not} $ t1 => do_formula t1
+ | Const (@{const_name All}, _) $ Abs (_, T, t') => do_formula t'
+ | Const (@{const_name Ex}, _) $ Abs (_, T, t') => do_formula t'
+ | @{const HOL.conj} $ t1 $ t2 => do_formula t1 #> do_formula t2
+ | @{const HOL.disj} $ t1 $ t2 => do_formula t1 #> do_formula t2
+ | @{const HOL.implies} $ t1 $ t2 => do_formula t1 #> do_formula t2
| Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
do_term_or_formula false T t1 #> do_term_or_formula true T t2
| Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
$ t1 $ t2 $ t3 =>
- do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
- | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
- do_quantifier (is_some pos) T t'
+ do_formula t1 #> fold (do_term_or_formula false T) [t2, t3]
+ | Const (@{const_name Ex1}, _) $ Abs (_, T, t') => do_formula t'
| Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
- do_quantifier (pos = SOME false) T
- (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
+ do_formula (t1 $ Bound ~1) #> do_formula t'
| Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
- do_quantifier (pos = SOME true) T
- (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
+ do_formula (t1 $ Bound ~1) #> do_formula t'
| (t0 as Const (_, @{typ bool})) $ t1 =>
- do_term false t0 #> do_formula pos t1 (* theory constant *)
+ do_term false t0 #> do_formula t1 (* theory constant *)
| _ => do_term false t
- in do_formula pos end
+ in do_formula end
fun pconsts_in_fact thy is_built_in_const t =
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
- (Symtab.empty |> add_pconsts_in_term thy is_built_in_const
- (SOME true) t) []
+ (Symtab.empty |> add_pconsts_in_term thy is_built_in_const t) []
(* Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account. *)
@@ -254,9 +238,9 @@
if String.isSubstring "." s then 1.0 else local_const_multiplier
(* Computes a constant's weight, as determined by its frequency. *)
-fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
- theory_const_weight chained_const_weight weight_for f
- const_tab chained_const_tab (c as (s, PType (m, _))) =
+fun generic_pconst_weight local_const_multiplier abs_weight theory_const_weight
+ chained_const_weight weight_for f const_tab chained_const_tab
+ (c as (s, PType (m, _))) =
if s = pseudo_abs_name then
abs_weight
else if String.isSuffix theory_const_suffix s then
@@ -273,19 +257,18 @@
fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
theory_const_rel_weight, ...} : relevance_fudge)
const_tab =
- generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
+ generic_pconst_weight local_const_multiplier abs_rel_weight
theory_const_rel_weight 0.0 rel_weight_for I const_tab
Symtab.empty
fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
- skolem_irrel_weight,
theory_const_irrel_weight,
chained_const_irrel_weight, ...})
const_tab chained_const_tab =
generic_pconst_weight local_const_multiplier abs_irrel_weight
- skolem_irrel_weight theory_const_irrel_weight
- chained_const_irrel_weight (irrel_weight_for fudge) swap
- const_tab chained_const_tab
+ theory_const_irrel_weight chained_const_irrel_weight
+ (irrel_weight_for fudge) swap const_tab
+ chained_const_tab
fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
intro_bonus
@@ -346,7 +329,7 @@
fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
if Symtab.is_empty tab then
Symtab.empty
- |> fold (add_pconsts_in_term thy is_built_in_const (SOME false))
+ |> fold (add_pconsts_in_term thy is_built_in_const)
(map_filter (fn ((_, (sc', _)), th) =>
if sc' = sc then SOME (prop_of th) else NONE) facts)
else
@@ -385,15 +368,15 @@
let
val thy = Proof_Context.theory_of ctxt
val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
- val add_pconsts = add_pconsts_in_term thy is_built_in_const o SOME
+ val add_pconsts = add_pconsts_in_term thy is_built_in_const
val chained_ts =
facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
| _ => NONE)
- val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
+ val chained_const_tab = Symtab.empty |> fold add_pconsts chained_ts
val goal_const_tab =
Symtab.empty
- |> fold (add_pconsts true) hyp_ts
- |> add_pconsts false concl_t
+ |> fold add_pconsts hyp_ts
+ |> add_pconsts concl_t
|> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
|> fold (if_empty_replace_with_scope thy is_built_in_const facts)
[Chained, Assum, Local]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Sep 11 22:20:45 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Sep 11 22:20:45 2013 +0200
@@ -53,7 +53,6 @@
higher_order_irrel_weight : real,
abs_rel_weight : real,
abs_irrel_weight : real,
- skolem_irrel_weight : real,
theory_const_rel_weight : real,
theory_const_irrel_weight : real,
chained_const_irrel_weight : real,
@@ -276,7 +275,6 @@
higher_order_irrel_weight = 1.05,
abs_rel_weight = 0.5,
abs_irrel_weight = 2.0,
- skolem_irrel_weight = 0.05,
theory_const_rel_weight = 0.5,
theory_const_irrel_weight = 0.25,
chained_const_irrel_weight = 0.25,
@@ -298,7 +296,6 @@
higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
abs_rel_weight = #abs_rel_weight atp_relevance_fudge,
abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,
- skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,
theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,
theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,
chained_const_irrel_weight = #chained_const_irrel_weight atp_relevance_fudge,
@@ -371,7 +368,6 @@
higher_order_irrel_weight : real,
abs_rel_weight : real,
abs_irrel_weight : real,
- skolem_irrel_weight : real,
theory_const_rel_weight : real,
theory_const_irrel_weight : real,
chained_const_irrel_weight : real,