# HG changeset patch # User blanchet # Date 1285872293 -7200 # Node ID 13b3a2ba9ea774bae8baf2604167729d9b295a14 # Parent a91a84b1dfdd49e622247a6484da66e50a9ada0e encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions diff -r a91a84b1dfdd -r 13b3a2ba9ea7 src/HOL/Tools/Sledgehammer/meson_clausify.ML --- 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 [] diff -r a91a84b1dfdd -r 13b3a2ba9ea7 src/HOL/Tools/Sledgehammer/metis_reconstruct.ML --- 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) diff -r a91a84b1dfdd -r 13b3a2ba9ea7 src/HOL/Tools/Sledgehammer/metis_translate.ML --- 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 diff -r a91a84b1dfdd -r 13b3a2ba9ea7 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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 =