encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML Thu Sep 30 19:15:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML Thu Sep 30 20:44:53 2010 +0200
@@ -20,7 +20,8 @@
structure Meson_Clausify : MESON_CLAUSIFY =
struct
-val new_skolem_var_prefix = "SK?" (* purposedly won't parse *)
+val new_skolem_var_prefix = "SK?"
+val new_nonskolem_var_prefix = "V?"
(**** Transformation of Elimination Rules into First-Order Formulas****)
@@ -226,39 +227,50 @@
val eqth = eqth RS @{thm TruepropI}
in Thm.equal_elim eqth th end
-val kill_quantifiers =
+fun zapped_var_name ax_no (skolem, cluster_no) s =
+ (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
+ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ s
+
+fun zap_quantifiers ax_no =
let
- fun conv pos ct =
+ fun conv (cluster as (cluster_skolem, cluster_no)) pos ct =
ct |> (case term_of ct of
Const (s, _) $ Abs (s', _, _) =>
if s = @{const_name all} orelse s = @{const_name All} orelse
s = @{const_name Ex} then
- Thm.dest_comb #> snd
- #> Thm.dest_abs (SOME (s' |> pos = (s = @{const_name Ex})
- ? prefix new_skolem_var_prefix))
- #> snd #> conv pos
+ let
+ val skolem = (pos = (s = @{const_name Ex}))
+ val cluster =
+ if skolem = cluster_skolem then cluster
+ else (skolem, cluster_no |> cluster_skolem ? Integer.add 1)
+ in
+ Thm.dest_comb #> snd
+ #> Thm.dest_abs (SOME (zapped_var_name ax_no cluster s'))
+ #> snd #> conv cluster pos
+ end
else
Conv.all_conv
| Const (s, _) $ _ $ _ =>
if s = @{const_name "==>"} orelse
s = @{const_name HOL.implies} then
- Conv.combination_conv (Conv.arg_conv (conv (not pos)))
- (conv pos)
+ Conv.combination_conv (Conv.arg_conv (conv cluster (not pos)))
+ (conv cluster pos)
else if s = @{const_name HOL.conj} orelse
s = @{const_name HOL.disj} then
- Conv.combination_conv (Conv.arg_conv (conv pos)) (conv pos)
+ Conv.combination_conv (Conv.arg_conv (conv cluster pos))
+ (conv cluster pos)
else
Conv.all_conv
| Const (s, _) $ _ =>
if s = @{const_name Trueprop} then
- Conv.arg_conv (conv pos)
+ Conv.arg_conv (conv cluster pos)
else if s = @{const_name Not} then
- Conv.arg_conv (conv (not pos))
+ Conv.arg_conv (conv cluster (not pos))
else
Conv.all_conv
| _ => Conv.all_conv)
in
- conv true #> Drule.export_without_context
+ conv (true, 0) true #> Drule.export_without_context
#> cprop_of #> Thm.dest_equals #> snd
end
@@ -267,7 +279,7 @@
addsimps @{thms all_simps[symmetric]}
(* Converts an Isabelle theorem into NNF. *)
-fun nnf_axiom new_skolemizer th ctxt =
+fun nnf_axiom new_skolemizer ax_no th ctxt =
let
val thy = ProofContext.theory_of ctxt
val th =
@@ -284,7 +296,7 @@
val th' = th |> Meson.skolemize ctxt
|> simplify pull_out_quant_ss
|> Drule.eta_contraction_rule
- val t = th' |> cprop_of |> kill_quantifiers |> term_of
+ val t = th' |> cprop_of |> zap_quantifiers ax_no |> term_of
in
if exists_subterm (fn Var ((s, _), _) =>
String.isPrefix new_skolem_var_prefix s
@@ -305,7 +317,7 @@
fun cnf_axiom thy new_skolemizer ax_no th =
let
val ctxt0 = Variable.global_thm_context th
- val (opt, nnf_th, ctxt) = nnf_axiom new_skolemizer th ctxt0
+ val (opt, nnf_th, ctxt) = nnf_axiom new_skolemizer ax_no th ctxt0
fun clausify th =
Meson.make_cnf (if new_skolemizer then
[]
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Thu Sep 30 19:15:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Thu Sep 30 20:44:53 2010 +0200
@@ -121,7 +121,7 @@
val nterms = length ts - ntypes
val tts = map tm_to_tt ts
val tys = types_of (List.take(tts,ntypes))
- val t = if String.isPrefix new_skolem_prefix c then
+ val t = if String.isPrefix new_skolem_const_prefix c then
Var (new_skolem_var_from_const c, tl tys ---> hd tys)
else
Const (c, dummyT)
--- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Thu Sep 30 19:15:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML Thu Sep 30 20:44:53 2010 +0200
@@ -45,7 +45,7 @@
val const_prefix: string
val type_const_prefix: string
val class_prefix: string
- val new_skolem_prefix : string
+ val new_skolem_const_prefix : string
val invert_const: string -> string
val ascii_of: string -> string
val unascii_of: string -> string
@@ -95,9 +95,9 @@
val type_const_prefix = "tc_";
val class_prefix = "class_";
-val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
-val old_skolem_prefix = skolem_prefix ^ "o"
-val new_skolem_prefix = skolem_prefix ^ "n"
+val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
+val old_skolem_const_prefix = skolem_const_prefix ^ "o"
+val new_skolem_const_prefix = skolem_const_prefix ^ "n"
fun union_all xss = fold (union (op =)) xss []
@@ -209,7 +209,7 @@
(instances of) Skolem pseudoconstants, this information is encoded in the
constant name. *)
fun num_type_args thy s =
- if String.isPrefix skolem_prefix s then
+ if String.isPrefix skolem_const_prefix s then
s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
else
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
@@ -396,8 +396,8 @@
| simple_combtype_of (TVar (x, _)) =
CombTVar (make_schematic_type_var x, string_of_indexname x)
-fun new_skolem_name th_no s num_T_args =
- [new_skolem_prefix, string_of_int th_no, s, string_of_int num_T_args]
+fun new_skolem_const_name th_no s num_T_args =
+ [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args]
|> space_implode Long_Name.separator
(* Converts a term (with combinators) into a combterm. Also accummulates sort
@@ -410,7 +410,7 @@
let
val (tp, ts) = combtype_of T
val tvar_list =
- (if String.isPrefix old_skolem_prefix c then
+ (if String.isPrefix old_skolem_const_prefix c then
[] |> Term.add_tvarsT T |> map TVar
else
(c, T) |> Sign.const_typargs thy)
@@ -428,7 +428,7 @@
if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
val tys = T |> strip_type |> swap |> op ::
- val s' = new_skolem_name th_no s (length tys)
+ val s' = new_skolem_const_name th_no s (length tys)
in
CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
end
@@ -458,8 +458,8 @@
end
val literals_of_term = literals_of_term1 ([], [])
-fun old_skolem_name i j num_T_args =
- old_skolem_prefix ^ Long_Name.separator ^
+fun old_skolem_const_name i j num_T_args =
+ old_skolem_const_prefix ^ Long_Name.separator ^
(space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
fun conceal_old_skolem_terms i old_skolems t =
@@ -475,8 +475,8 @@
s :: _ => (old_skolems, s)
| [] =>
let
- val s = old_skolem_name i (length old_skolems)
- (length (Term.add_tvarsT T []))
+ val s = old_skolem_const_name i (length old_skolems)
+ (length (Term.add_tvarsT T []))
in ((s, t) :: old_skolems, s) end
in (old_skolems, Const (s, T)) end
| aux old_skolems (t1 $ t2) =
@@ -495,7 +495,7 @@
fun reveal_old_skolem_terms old_skolems =
map_aterms (fn t as Const (s, _) =>
- if String.isPrefix old_skolem_prefix s then
+ if String.isPrefix old_skolem_const_prefix s then
AList.lookup (op =) old_skolems s |> the
|> map_types Type_Infer.paramify_vars
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Sep 30 19:15:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Sep 30 20:44:53 2010 +0200
@@ -77,8 +77,8 @@
only: bool}
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-val abs_name = "Sledgehammer.abs"
-val skolem_prefix = "Sledgehammer.sko"
+val abs_name = sledgehammer_prefix ^ "abs"
+val skolem_prefix = sledgehammer_prefix ^ "sko"
val theory_const_suffix = Long_Name.separator ^ " 1"
fun repair_name reserved multi j name =