--- a/NEWS Sun Feb 05 16:53:11 2012 +0100
+++ b/NEWS Sun Feb 05 16:53:20 2012 +0100
@@ -305,7 +305,7 @@
affecting 'rat' and 'real'.
* Sledgehammer:
- - Added "lam_trans" and "minimize" options.
+ - Added "lam_trans", "uncurry_aliases", and "minimize" options.
- Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
- Renamed "sound" option to "strict".
--- a/doc-src/Sledgehammer/sledgehammer.tex Sun Feb 05 16:53:11 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sun Feb 05 16:53:20 2012 +0100
@@ -722,6 +722,7 @@
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
\def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
@@ -1005,6 +1006,10 @@
For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting},
irrespective of the value of this option.
+\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases}
+Specifies whether fresh function symbols should be generated as aliases for
+applications of curried functions in ATP problems.
+
\opdefault{type\_enc}{string}{smart}
Specifies the type encoding to use in ATP problems. Some of the type encodings
are unsound, meaning that they can give rise to spurious proofs
--- a/src/HOL/Fun.thy Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Fun.thy Sun Feb 05 16:53:20 2012 +0100
@@ -427,27 +427,6 @@
using * by blast
qed
-lemma bij_betw_Disj_Un:
- assumes DISJ: "A \<inter> B = {}" and DISJ': "A' \<inter> B' = {}" and
- B1: "bij_betw f A A'" and B2: "bij_betw f B B'"
- shows "bij_betw f (A \<union> B) (A' \<union> B')"
-proof-
- have 1: "inj_on f A \<and> inj_on f B"
- using B1 B2 by (auto simp add: bij_betw_def)
- have 2: "f`A = A' \<and> f`B = B'"
- using B1 B2 by (auto simp add: bij_betw_def)
- hence "f`(A - B) \<inter> f`(B - A) = {}"
- using DISJ DISJ' by blast
- hence "inj_on f (A \<union> B)"
- using 1 by (auto simp add: inj_on_Un)
- (* *)
- moreover
- have "f`(A \<union> B) = A' \<union> B'"
- using 2 by auto
- ultimately show ?thesis
- unfolding bij_betw_def by auto
-qed
-
lemma bij_betw_subset:
assumes BIJ: "bij_betw f A A'" and
SUB: "B \<le> A" and IM: "f ` B = B'"
--- a/src/HOL/IsaMakefile Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/IsaMakefile Sun Feb 05 16:53:20 2012 +0100
@@ -1051,10 +1051,10 @@
ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy \
ex/Coercion_Examples.thy ex/Coherent.thy \
ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \
- ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \
- ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
- ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
- ex/Iff_Oracle.thy ex/Induction_Schema.thy \
+ ex/Eval_Examples.thy ex/Executable_Relation.thy ex/Fundefs.thy \
+ ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
+ ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
+ ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \
ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy \
ex/Lagrange.thy ex/List_to_Set_Comprehension_Examples.thy \
ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy \
--- a/src/HOL/Library/Multiset.thy Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Library/Multiset.thy Sun Feb 05 16:53:20 2012 +0100
@@ -1175,12 +1175,12 @@
by (simp add: Bag_def count_of_multiset Abs_multiset_inverse)
lemma Mempty_Bag [code]:
- "{#} = Bag (Alist [])"
- by (simp add: multiset_eq_iff alist.Alist_inverse)
+ "{#} = Bag (DAList.empty)"
+ by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def)
lemma single_Bag [code]:
- "{#x#} = Bag (Alist [(x, 1)])"
- by (simp add: multiset_eq_iff alist.Alist_inverse)
+ "{#x#} = Bag (DAList.update x 1 DAList.empty)"
+ by (simp add: multiset_eq_iff alist.Alist_inverse impl_of_update impl_of_empty)
lemma union_Bag [code]:
"Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"
--- a/src/HOL/List.thy Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/List.thy Sun Feb 05 16:53:20 2012 +0100
@@ -5676,10 +5676,28 @@
text {* Further operations on sets *}
+(* Minimal refinement of equality on sets *)
+declare subset_eq[code del]
+lemma subset_code [code]:
+ "set xs <= B \<longleftrightarrow> (ALL x : set xs. x : B)"
+ "List.coset xs <= List.coset ys \<longleftrightarrow> set ys <= set xs"
+ "List.coset [] <= set [] \<longleftrightarrow> False"
+by auto
+
lemma setsum_code [code]:
"setsum f (set xs) = listsum (map f (remdups xs))"
by (simp add: listsum_distinct_conv_setsum_set)
+definition map_project :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a set \<Rightarrow> 'b set" where
+ "map_project f A = {b. \<exists> a \<in> A. f a = Some b}"
+
+lemma [code]:
+ "map_project f (set xs) = set (List.map_filter f xs)"
+unfolding map_project_def map_filter_def
+by auto (metis (lifting, mono_tags) CollectI image_eqI o_apply the.simps)
+
+hide_const (open) map_project
+
text {* Operations on relations *}
lemma product_code [code]:
@@ -5690,6 +5708,10 @@
"Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
by (auto simp add: Id_on_def)
+lemma [code]:
+ "R `` S = List.map_project (%(x, y). if x : S then Some y else None) R"
+unfolding map_project_def by (auto split: prod.split split_if_asm)
+
lemma trancl_set_ntrancl [code]:
"trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
by (simp add: finite_trancl_ntranl)
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Feb 05 16:53:20 2012 +0100
@@ -12,6 +12,7 @@
val strictK = "strict"
val sliceK = "slice"
val lam_transK = "lam_trans"
+val uncurried_aliasesK = "uncurried_aliases"
val e_weight_methodK = "e_weight_method"
val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
@@ -362,7 +363,8 @@
SH_ERROR
fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans
- e_weight_method force_sos hard_timeout timeout dir pos st =
+ uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos
+ st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
@@ -387,7 +389,7 @@
("type_enc", type_enc),
("strict", strict),
("lam_trans", lam_trans |> the_default "smart"),
- ("preplay_timeout", preplay_timeout),
+ ("uncurried_aliases", uncurried_aliases |> the_default "smart"),
("max_relevant", max_relevant),
("slice", slice),
("timeout", string_of_int timeout),
@@ -471,6 +473,7 @@
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val slice = AList.lookup (op =) args sliceK |> the_default "true"
val lam_trans = AList.lookup (op =) args lam_transK
+ val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK
val e_weight_method = AList.lookup (op =) args e_weight_methodK
val force_sos = AList.lookup (op =) args force_sosK
|> Option.map (curry (op <>) "false")
@@ -481,7 +484,8 @@
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
run_sh prover_name prover type_enc strict max_relevant slice lam_trans
- e_weight_method force_sos hard_timeout timeout dir pos st
+ uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos
+ st
in
case result of
SH_OK (time_isa, time_prover, names) =>
--- a/src/HOL/Quickcheck_Exhaustive.thy Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Feb 05 16:53:20 2012 +0100
@@ -425,7 +425,8 @@
begin
definition
- "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
+ "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1)
+ orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
where
@@ -439,7 +440,9 @@
begin
definition
- "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))"
+ "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1)
+ orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2)
+ orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3))"
definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
where
@@ -449,6 +452,23 @@
end
+instantiation Enum.finite_4 :: check_all
+begin
+
+definition
+ "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>1)
+ orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>2)
+ orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>3)
+ orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>4))"
+
+definition enum_term_of_finite_4 :: "Enum.finite_4 itself => unit => term list"
+where
+ "enum_term_of_finite_4 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
+
+instance ..
+
+end
+
subsection {* Bounded universal quantifiers *}
class bounded_forall =
--- a/src/HOL/Quotient_Examples/FSet.thy Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy Sun Feb 05 16:53:20 2012 +0100
@@ -546,7 +546,34 @@
by (rule pred_compI) (rule a', rule d')
qed
+lemma map_rsp2 [quot_respect]:
+ "((op \<approx> ===> op \<approx>) ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) map map"
+proof (auto intro!: fun_relI)
+ fix f f' :: "'a list \<Rightarrow> 'b list"
+ fix xa ya x y :: "'a list list"
+ assume fs: "(op \<approx> ===> op \<approx>) f f'" and x: "list_all2 op \<approx> xa x" and xy: "set x = set y" and y: "list_all2 op \<approx> y ya"
+ have a: "(list_all2 op \<approx>) (map f xa) (map f x)"
+ using x
+ by (induct xa x rule: list_induct2')
+ (simp_all, metis fs fun_relE list_eq_def)
+ have b: "set (map f x) = set (map f y)"
+ using xy fs
+ by (induct x y rule: list_induct2')
+ (simp_all, metis image_insert)
+ have c: "(list_all2 op \<approx>) (map f y) (map f' ya)"
+ using y fs
+ by (induct y ya rule: list_induct2')
+ (simp_all, metis apply_rsp' list_eq_def)
+ show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)"
+ by (metis a b c list_eq_def pred_comp.intros)
+qed
+lemma map_prs2 [quot_preserve]:
+ "((abs_fset ---> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) map = map_fset"
+ apply (auto simp add: fun_eq_iff)
+ apply (induct_tac xa rule: list.induct[quot_lifted])
+ apply (simp_all add: map.simps[quot_lifted] Quotient_abs_rep[OF Quotient_fset] bot_fset_def map_fset_def insert_fset_def)
+ done
section {* Lifted theorems *}
@@ -907,16 +934,19 @@
lemma concat_empty_fset [simp]:
shows "concat_fset {||} = {||}"
- by (lifting concat.simps(1))
+ by descending simp
lemma concat_insert_fset [simp]:
shows "concat_fset (insert_fset x S) = x |\<union>| concat_fset S"
- by (lifting concat.simps(2))
+ by descending simp
lemma concat_inter_fset [simp]:
shows "concat_fset (xs |\<union>| ys) = concat_fset xs |\<union>| concat_fset ys"
- by (lifting concat_append)
+ by descending simp
+lemma map_concat_fset:
+ shows "map_fset f (concat_fset xs) = concat_fset (map_fset (map_fset f) xs)"
+ by (lifting map_concat)
subsection {* filter_fset *}
--- a/src/HOL/TPTP/atp_theory_export.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Sun Feb 05 16:53:20 2012 +0100
@@ -102,8 +102,8 @@
fun inference infers ident =
these (AList.lookup (op =) infers ident) |> inference_term
fun add_inferences_to_problem_line infers
- (Formula (ident, Axiom, phi, NONE, NONE)) =
- Formula (ident, Lemma, phi, inference infers ident, NONE)
+ (Formula (ident, Axiom, phi, NONE, tms)) =
+ Formula (ident, Lemma, phi, inference infers ident, tms)
| add_inferences_to_problem_line _ line = line
fun add_inferences_to_problem infers =
map (apsnd (map (add_inferences_to_problem_line infers)))
@@ -139,7 +139,7 @@
exists (fn prefix => String.isPrefix prefix ident)
likely_tautology_prefixes andalso
is_none (run_some_atp ctxt format
- [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])])
+ [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])])
| is_problem_line_tautology _ _ _ = false
structure String_Graph = Graph(type key = string val ord = string_ord);
@@ -181,7 +181,7 @@
((Thm.get_name_hint th, loc),
th |> prop_of |> mono ? monomorphize_term ctxt))
|> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false
- true [] @{prop False}
+ false true [] @{prop False}
|> #1
val atp_problem =
atp_problem
--- a/src/HOL/Tools/ATP/atp_problem.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sun Feb 05 16:53:20 2012 +0100
@@ -41,15 +41,9 @@
Formula of string * formula_kind
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
* (string, string ho_type) ho_term option
- * (string, string ho_type) ho_term option
+ * (string, string ho_type) ho_term list
type 'a problem = (string * 'a problem_line list) list
- val isabelle_info_prefix : string
- val isabelle_info : atp_format -> string -> (string, 'a) ho_term option
- val introN : string
- val elimN : string
- val simpN : string
- val eqN : string
val tptp_cnf : string
val tptp_fof : string
val tptp_tff : string
@@ -80,6 +74,15 @@
val tptp_false : string
val tptp_true : string
val tptp_empty_list : string
+ val isabelle_info_prefix : string
+ val isabelle_info : atp_format -> string -> int -> (string, 'a) ho_term list
+ val introN : string
+ val elimN : string
+ val simpN : string
+ val spec_eqN : string
+ val rankN : string
+ val minimum_rank : int
+ val default_rank : int
val is_tptp_equal : string -> bool
val is_built_in_tptp_symbol : string -> bool
val is_tptp_variable : string -> bool
@@ -154,27 +157,12 @@
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
- Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
- * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
+ Formula of string * formula_kind
+ * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
+ * (string, string ho_type) ho_term option
+ * (string, string ho_type) ho_term list
type 'a problem = (string * 'a problem_line list) list
-val isabelle_info_prefix = "isabelle_"
-
-(* Currently, only newer versions of SPASS, with sorted DFG format support, can
- process Isabelle metainformation. *)
-fun isabelle_info (DFG DFG_Sorted) s =
- SOME (ATerm ("[]", [ATerm (isabelle_info_prefix ^ s, [])]))
- | isabelle_info _ _ = NONE
-
-val introN = "intro"
-val elimN = "elim"
-val simpN = "simp"
-val eqN = "eq"
-
-fun extract_isabelle_info (SOME (ATerm ("[]", [ATerm (s, [])]))) =
- try (unprefix isabelle_info_prefix) s
- | extract_isabelle_info _ = NONE
-
(* official TPTP syntax *)
val tptp_cnf = "cnf"
val tptp_fof = "fof"
@@ -207,6 +195,36 @@
val tptp_true = "$true"
val tptp_empty_list = "[]"
+val isabelle_info_prefix = "isabelle_"
+
+val introN = "intro"
+val elimN = "elim"
+val simpN = "simp"
+val spec_eqN = "spec_eq"
+val rankN = "rank"
+
+val minimum_rank = 0
+val default_rank = 1000
+
+(* Currently, only newer versions of SPASS, with sorted DFG format support, can
+ process Isabelle metainformation. *)
+fun isabelle_info (DFG DFG_Sorted) status rank =
+ [] |> rank <> default_rank
+ ? cons (ATerm (isabelle_info_prefix ^ rankN,
+ [ATerm (string_of_int rank, [])]))
+ |> status <> "" ? cons (ATerm (isabelle_info_prefix ^ status, []))
+ | isabelle_info _ _ _ = []
+
+fun extract_isabelle_status (ATerm (s, []) :: _) =
+ try (unprefix isabelle_info_prefix) s
+ | extract_isabelle_status _ = NONE
+
+fun extract_isabelle_rank (tms as _ :: _) =
+ (case List.last tms of
+ ATerm (_, [ATerm (rank, [])]) => the (Int.fromString rank)
+ | _ => default_rank)
+ | extract_isabelle_rank _ = default_rank
+
fun is_tptp_equal s = (s = tptp_equal orelse s = tptp_old_equal)
fun is_built_in_tptp_symbol s =
s = tptp_old_equal orelse not (Char.isAlpha (String.sub (s, 0)))
@@ -406,11 +424,12 @@
tptp_string_for_kind kind ^ ",\n (" ^
tptp_string_for_formula format phi ^ ")" ^
(case (source, info) of
- (NONE, NONE) => ""
- | (SOME tm, NONE) => ", " ^ tptp_string_for_term format tm
- | (_, SOME tm) =>
+ (NONE, []) => ""
+ | (SOME tm, []) => ", " ^ tptp_string_for_term format tm
+ | (_, tms) =>
", " ^ tptp_string_for_term format (the_source source) ^
- ", " ^ tptp_string_for_term format tm) ^ ").\n"
+ ", " ^ tptp_string_for_term format (ATerm (tptp_empty_list, tms))) ^
+ ").\n"
fun tptp_lines format =
maps (fn (_, []) => []
@@ -439,9 +458,9 @@
let
fun suffix_tag top_level s =
if top_level then
- case extract_isabelle_info info of
+ case extract_isabelle_status info of
SOME s' => if s' = simpN then s ^ ":lr"
- else if s' = eqN then s ^ ":lt"
+ else if s' = spec_eqN then s ^ ":lt"
else s
| NONE => s
else
@@ -484,40 +503,47 @@
commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")."
fun formula pred (Formula (ident, kind, phi, _, info)) =
if pred kind then
- SOME ("formula(" ^ dfg_string_for_formula flavor info phi ^ ", " ^
- ident ^ ").")
+ let val rank = extract_isabelle_rank info in
+ "formula(" ^ dfg_string_for_formula flavor info phi ^ ", " ^ ident ^
+ (if rank = default_rank then "" else ", " ^ string_of_int rank) ^
+ ")." |> SOME
+ end
else
NONE
| formula _ _ = NONE
- fun filt f = problem |> map (map_filter f o snd) |> flat
+ fun filt f = problem |> map (map_filter f o snd) |> filter_out null
val func_aries =
filt (fn Decl (_, sym, ty) =>
if is_function_type ty then SOME (ary sym ty) else NONE
| _ => NONE)
- |> commas |> enclose "functions [" "]."
+ |> flat |> commas |> enclose "functions [" "]."
val pred_aries =
filt (fn Decl (_, sym, ty) =>
- if is_nontrivial_predicate_type ty then SOME (ary sym ty)
- else NONE
+ if is_predicate_type ty then SOME (ary sym ty) else NONE
| _ => NONE)
- |> commas |> enclose "predicates [" "]."
+ |> flat |> commas |> enclose "predicates [" "]."
fun sorts () =
filt (fn Decl (_, sym, AType (s, [])) =>
if s = tptp_type_of_types then SOME sym else NONE
- | _ => NONE) @ [dfg_individual_type]
- |> commas |> enclose "sorts [" "]."
+ | _ => NONE) @ [[dfg_individual_type]]
+ |> flat |> commas |> enclose "sorts [" "]."
val syms = [func_aries, pred_aries] @ (if sorted then [sorts ()] else [])
fun func_sigs () =
filt (fn Decl (_, sym, ty) =>
if is_function_type ty then SOME (fun_typ sym ty) else NONE
| _ => NONE)
+ |> flat
fun pred_sigs () =
filt (fn Decl (_, sym, ty) =>
- if is_predicate_type ty then SOME (pred_typ sym ty) else NONE
+ if is_nontrivial_predicate_type ty then SOME (pred_typ sym ty)
+ else NONE
| _ => NONE)
+ |> flat
val decls = if sorted then func_sigs () @ pred_sigs () else []
- val axioms = filt (formula (curry (op <>) Conjecture))
- val conjs = filt (formula (curry (op =) Conjecture))
+ val axioms =
+ filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat
+ val conjs =
+ filt (formula (curry (op =) Conjecture)) |> separate [""] |> flat
fun list_of _ [] = []
| list_of heading ss =
"list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @
@@ -658,6 +684,20 @@
is still necessary). *)
val reserved_nice_names = [tptp_old_equal, "op", "eq"]
+(* hack to get the same hashing across Mirabelle runs (see "mirabelle.pl") *)
+fun cleanup_mirabelle_name s =
+ let
+ val mirabelle_infix = "_Mirabelle_"
+ val random_suffix_len = 10
+ val (s1, s2) = Substring.position mirabelle_infix (Substring.full s)
+ in
+ if Substring.isEmpty s2 then
+ s
+ else
+ Substring.string s1 ^
+ Substring.string (Substring.triml (size mirabelle_infix + random_suffix_len) s2)
+ end
+
fun readable_name protect full_name s =
(if s = full_name then
s
@@ -668,7 +708,7 @@
|> (fn s =>
if size s > max_readable_name_size then
String.substring (s, 0, max_readable_name_size div 2 - 4) ^
- string_of_int (hash_string full_name) ^
+ string_of_int (hash_string (cleanup_mirabelle_name full_name)) ^
String.extract (s, size s - max_readable_name_size div 2 + 4,
NONE)
else
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Feb 05 16:53:20 2012 +0100
@@ -16,7 +16,7 @@
type 'a problem = 'a ATP_Problem.problem
datatype scope = Global | Local | Assum | Chained
- datatype status = General | Induct | Intro | Elim | Simp | Eq
+ datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
type stature = scope * status
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
@@ -96,14 +96,14 @@
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
val unmangled_const : string -> string * (string, 'b) ho_term list
- val unmangled_const_name : string -> string
+ val unmangled_const_name : string -> string list
val helper_table : ((string * bool) * thm list) list
val trans_lams_from_string :
Proof.context -> type_enc -> string -> term list -> term list * term list
val factsN : string
val prepare_atp_problem :
Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
- -> bool -> string -> bool -> bool -> term list -> term
+ -> bool -> string -> bool -> bool -> bool -> term list -> term
-> ((string * stature) * term) list
-> string problem * string Symtab.table * (string * stature) list vector
* (string * term) list * int Symtab.table
@@ -149,13 +149,14 @@
val class_prefix = "cl_"
(* Freshness almost guaranteed! *)
+val atp_prefix = "ATP" ^ Long_Name.separator
val atp_weak_prefix = "ATP:"
val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
-val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
+val skolem_const_prefix = atp_prefix ^ "Sko"
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
val new_skolem_const_prefix = skolem_const_prefix ^ "n"
@@ -165,6 +166,7 @@
val sym_decl_prefix = "sy_"
val guards_sym_formula_prefix = "gsy_"
val tags_sym_formula_prefix = "tsy_"
+val uncurried_alias_eq_prefix = "unc_"
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
@@ -547,7 +549,7 @@
in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
datatype scope = Global | Local | Assum | Chained
-datatype status = General | Induct | Intro | Elim | Simp | Eq
+datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
type stature = scope * status
datatype order = First_Order | Higher_Order
@@ -873,7 +875,10 @@
if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
(* This shouldn't clash with anything else. *)
-val mangled_type_sep = "\000"
+val uncurried_alias_sep = "\000"
+val mangled_type_sep = "\001"
+
+val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
fun generic_mangled_type_name f (ATerm (name, [])) = f name
| generic_mangled_type_name f (ATerm (name, tys)) =
@@ -914,13 +919,23 @@
ho_type_from_ho_term type_enc pred_sym ary
o ho_term_from_typ format type_enc
-fun mangled_const_name format type_enc T_args (s, s') =
+fun aliased_uncurried ary (s, s') =
+ (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
+fun unaliased_uncurried (s, s') =
+ case space_explode uncurried_alias_sep s of
+ [_] => (s, s')
+ | [s1, s2] => (s1, unsuffix s2 s')
+ | _ => raise Fail "ill-formed explicit application alias"
+
+fun raw_mangled_const_name type_name ty_args (s, s') =
let
- val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
fun type_suffix f g =
- fold_rev (curry (op ^) o g o prefix mangled_type_sep
- o generic_mangled_type_name f) ty_args ""
+ fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f)
+ ty_args ""
in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
+fun mangled_const_name format type_enc =
+ map_filter (ho_term_for_type_arg format type_enc)
+ #> raw_mangled_const_name generic_mangled_type_name
val parse_mangled_ident =
Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
@@ -939,9 +954,10 @@
quote s)) parse_mangled_type))
|> fst
-val unmangled_const_name = space_explode mangled_type_sep #> hd
+fun unmangled_const_name s =
+ (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
fun unmangled_const s =
- let val ss = space_explode mangled_type_sep s in
+ let val ss = unmangled_const_name s in
(hd ss, map unmangled_type (tl ss))
end
@@ -992,19 +1008,21 @@
| intro _ _ tm = tm
in intro true [] end
+fun mangle_type_args_in_const format type_enc (name as (s, _)) T_args =
+ case unprefix_and_unascii const_prefix s of
+ NONE => (name, T_args)
+ | SOME s'' =>
+ case type_arg_policy [] type_enc (invert_const s'') of
+ Mangled_Type_Args => (mangled_const_name format type_enc T_args name, [])
+ | _ => (name, T_args)
fun mangle_type_args_in_iterm format type_enc =
if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
let
fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
| mangle (tm as IConst (_, _, [])) = tm
- | mangle (tm as IConst (name as (s, _), T, T_args)) =
- (case unprefix_and_unascii const_prefix s of
- NONE => tm
- | SOME s'' =>
- case type_arg_policy [] type_enc (invert_const s'') of
- Mangled_Type_Args =>
- IConst (mangled_const_name format type_enc T_args name, T, [])
- | _ => tm)
+ | mangle (IConst (name, T, T_args)) =
+ mangle_type_args_in_const format type_enc name T_args
+ |> (fn (name, T_args) => IConst (name, T, T_args))
| mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
| mangle tm = tm
in mangle end
@@ -1029,31 +1047,30 @@
end
handle TYPE _ => T_args
+fun filter_type_args_in_const _ _ _ _ _ [] = []
+ | filter_type_args_in_const thy monom_constrs type_enc ary s T_args =
+ case unprefix_and_unascii const_prefix s of
+ NONE =>
+ if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
+ else T_args
+ | SOME s'' =>
+ let
+ val s'' = invert_const s''
+ fun filter_T_args false = T_args
+ | filter_T_args true = filter_const_type_args thy s'' ary T_args
+ in
+ case type_arg_policy monom_constrs type_enc s'' of
+ Explicit_Type_Args infer_from_term_args =>
+ filter_T_args infer_from_term_args
+ | No_Type_Args => []
+ | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
+ end
fun filter_type_args_in_iterm thy monom_constrs type_enc =
let
fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
- | filt _ (tm as IConst (_, _, [])) = tm
| filt ary (IConst (name as (s, _), T, T_args)) =
- (case unprefix_and_unascii const_prefix s of
- NONE =>
- (name,
- if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
- []
- else
- T_args)
- | SOME s'' =>
- let
- val s'' = invert_const s''
- fun filter_T_args false = T_args
- | filter_T_args true = filter_const_type_args thy s'' ary T_args
- in
- case type_arg_policy monom_constrs type_enc s'' of
- Explicit_Type_Args infer_from_term_args =>
- (name, filter_T_args infer_from_term_args)
- | No_Type_Args => (name, [])
- | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
- end)
- |> (fn (name, T_args) => IConst (name, T, T_args))
+ filter_type_args_in_const thy monom_constrs type_enc ary s T_args
+ |> (fn T_args => IConst (name, T, T_args))
| filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
| filt _ tm = tm
in filt 0 end
@@ -1064,8 +1081,7 @@
fun do_term bs t atomic_Ts =
iterm_from_term thy format bs (Envir.eta_contract t)
|>> (introduce_proxies_in_iterm type_enc
- #> mangle_type_args_in_iterm format type_enc
- #> AAtom)
+ #> mangle_type_args_in_iterm format type_enc #> AAtom)
||> union (op =) atomic_Ts
fun do_quant bs q pos s T t' =
let
@@ -1191,7 +1207,8 @@
|>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
val lam_facts =
map2 (fn t => fn j =>
- ((lam_fact_prefix ^ Int.toString j, (Global, Eq)), (Axiom, t)))
+ ((lam_fact_prefix ^ Int.toString j, (Global, Spec_Eq)),
+ (Axiom, t)))
lambda_ts (1 upto length lambda_ts)
in (facts, lam_facts) end
@@ -1377,7 +1394,9 @@
{pred_sym = true, min_ary = 1, max_ary = 1, types = [],
in_conj = false})
-fun sym_table_for_facts ctxt type_enc explicit_apply conjs facts =
+datatype app_op_level = Incomplete_Apply | Sufficient_Apply | Full_Apply
+
+fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
let
fun consider_var_ary const_T var_T max_ary =
let
@@ -1389,7 +1408,7 @@
iter (ary + 1) (range_type T)
in iter 0 const_T end
fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
- if explicit_apply = NONE andalso
+ if app_op_level = Sufficient_Apply andalso
(can dest_funT T orelse T = @{typ bool}) then
let
val bool_vars' = bool_vars orelse body_type T = @{typ bool}
@@ -1408,63 +1427,63 @@
end
else
accum
+ fun add_iterm_syms conj_fact top_level tm
+ (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
+ let val (head, args) = strip_iterm_comb tm in
+ (case head of
+ IConst ((s, _), T, _) =>
+ if String.isPrefix bound_var_prefix s orelse
+ String.isPrefix all_bound_var_prefix s then
+ add_universal_var T accum
+ else if String.isPrefix exist_bound_var_prefix s then
+ accum
+ else
+ let val ary = length args in
+ ((bool_vars, fun_var_Ts),
+ case Symtab.lookup sym_tab s of
+ SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
+ let
+ val pred_sym =
+ pred_sym andalso top_level andalso not bool_vars
+ val types' = types |> insert_type ctxt I T
+ val in_conj = in_conj orelse conj_fact
+ val min_ary =
+ if app_op_level = Sufficient_Apply andalso
+ not (pointer_eq (types', types)) then
+ fold (consider_var_ary T) fun_var_Ts min_ary
+ else
+ min_ary
+ in
+ Symtab.update (s, {pred_sym = pred_sym,
+ min_ary = Int.min (ary, min_ary),
+ max_ary = Int.max (ary, max_ary),
+ types = types', in_conj = in_conj})
+ sym_tab
+ end
+ | NONE =>
+ let
+ val pred_sym = top_level andalso not bool_vars
+ val min_ary =
+ case app_op_level of
+ Incomplete_Apply => ary
+ | Sufficient_Apply =>
+ fold (consider_var_ary T) fun_var_Ts ary
+ | Full_Apply => 0
+ in
+ Symtab.update_new (s,
+ {pred_sym = pred_sym, min_ary = min_ary,
+ max_ary = ary, types = [T], in_conj = conj_fact})
+ sym_tab
+ end)
+ end
+ | IVar (_, T) => add_universal_var T accum
+ | IAbs ((_, T), tm) =>
+ accum |> add_universal_var T |> add_iterm_syms conj_fact false tm
+ | _ => accum)
+ |> fold (add_iterm_syms conj_fact false) args
+ end
fun add_fact_syms conj_fact =
- let
- fun add_iterm_syms top_level tm
- (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
- let val (head, args) = strip_iterm_comb tm in
- (case head of
- IConst ((s, _), T, _) =>
- if String.isPrefix bound_var_prefix s orelse
- String.isPrefix all_bound_var_prefix s then
- add_universal_var T accum
- else if String.isPrefix exist_bound_var_prefix s then
- accum
- else
- let val ary = length args in
- ((bool_vars, fun_var_Ts),
- case Symtab.lookup sym_tab s of
- SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
- let
- val pred_sym =
- pred_sym andalso top_level andalso not bool_vars
- val types' = types |> insert_type ctxt I T
- val in_conj = in_conj orelse conj_fact
- val min_ary =
- if is_some explicit_apply orelse
- pointer_eq (types', types) then
- min_ary
- else
- fold (consider_var_ary T) fun_var_Ts min_ary
- in
- Symtab.update (s, {pred_sym = pred_sym,
- min_ary = Int.min (ary, min_ary),
- max_ary = Int.max (ary, max_ary),
- types = types', in_conj = in_conj})
- sym_tab
- end
- | NONE =>
- let
- val pred_sym = top_level andalso not bool_vars
- val min_ary =
- case explicit_apply of
- SOME true => 0
- | SOME false => ary
- | NONE => fold (consider_var_ary T) fun_var_Ts ary
- in
- Symtab.update_new (s,
- {pred_sym = pred_sym, min_ary = min_ary,
- max_ary = ary, types = [T], in_conj = conj_fact})
- sym_tab
- end)
- end
- | IVar (_, T) => add_universal_var T accum
- | IAbs ((_, T), tm) =>
- accum |> add_universal_var T |> add_iterm_syms false tm
- | _ => accum)
- |> fold (add_iterm_syms false) args
- end
- in K (add_iterm_syms true) |> formula_fold NONE |> fact_lift end
+ K (add_iterm_syms conj_fact true) |> formula_fold NONE |> fact_lift
in
((false, []), Symtab.empty)
|> fold (add_fact_syms true) conjs
@@ -1479,7 +1498,7 @@
| NONE =>
case unprefix_and_unascii const_prefix s of
SOME s =>
- let val s = s |> unmangled_const_name |> invert_const in
+ let val s = s |> unmangled_const_name |> hd |> invert_const in
if s = predicator_name then 1
else if s = app_op_name then 2
else if s = type_guard_name then 1
@@ -1504,25 +1523,35 @@
fun list_app head args = fold (curry (IApp o swap)) args head
fun predicator tm = IApp (predicator_combconst, tm)
-fun firstorderize_fact thy monom_constrs format type_enc sym_tab =
+fun mk_app_op format type_enc head arg =
let
- fun do_app arg head =
- let
- val head_T = ityp_of head
- val (arg_T, res_T) = dest_funT head_T
- val app =
- IConst (app_op, head_T --> head_T, [arg_T, res_T])
- |> mangle_type_args_in_iterm format type_enc
- in list_app app [head, arg] end
+ val head_T = ityp_of head
+ val (arg_T, res_T) = dest_funT head_T
+ val app =
+ IConst (app_op, head_T --> head_T, [arg_T, res_T])
+ |> mangle_type_args_in_iterm format type_enc
+ in list_app app [head, arg] end
+
+fun firstorderize_fact thy monom_constrs format type_enc sym_tab
+ uncurried_aliases =
+ let
+ fun do_app arg head = mk_app_op format type_enc head arg
fun list_app_ops head args = fold do_app args head
fun introduce_app_ops tm =
- case strip_iterm_comb tm of
- (head as IConst ((s, _), _, _), args) =>
- args |> map introduce_app_ops
- |> chop (min_ary_of sym_tab s)
- |>> list_app head
- |-> list_app_ops
- | (head, args) => list_app_ops head (map introduce_app_ops args)
+ let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
+ case head of
+ IConst (name as (s, _), T, T_args) =>
+ if uncurried_aliases andalso String.isPrefix const_prefix s then
+ let
+ val ary = length args
+ val name = name |> ary > min_ary_of sym_tab s
+ ? aliased_uncurried ary
+ in list_app (IConst (name, T, T_args)) args end
+ else
+ args |> chop (min_ary_of sym_tab s)
+ |>> list_app head |-> list_app_ops
+ | _ => list_app_ops head args
+ end
fun introduce_predicators tm =
case strip_iterm_comb tm of
(IConst ((s, _), _, _), _) =>
@@ -1587,12 +1616,19 @@
atype_of_type_vars type_enc)
| _ => NONE) Ts)
-fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
+fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
(if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
+ |> mk_aquant AForall bounds
|> close_formula_universally
|> bound_tvars type_enc true atomic_Ts
+val helper_rank = default_rank
+val min_rank = 9 * helper_rank div 10
+val max_rank = 4 * min_rank
+
+fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n
+
val type_tag = `(make_fixed_const NONE) type_tag_name
fun type_tag_idempotence_fact format type_enc =
@@ -1602,8 +1638,8 @@
val tagged_var = tag (var "X")
in
Formula (type_tag_idempotence_helper_name, Axiom,
- eq_formula type_enc [] false (tag tagged_var) tagged_var,
- NONE, isabelle_info format eqN)
+ eq_formula type_enc [] [] false (tag tagged_var) tagged_var,
+ NONE, isabelle_info format spec_eqN helper_rank)
end
fun should_specialize_helper type_enc t =
@@ -1616,7 +1652,7 @@
SOME mangled_s =>
let
val thy = Proof_Context.theory_of ctxt
- val unmangled_s = mangled_s |> unmangled_const_name
+ val unmangled_s = mangled_s |> unmangled_const_name |> hd
fun dub needs_fairly_sound j k =
unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
(if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
@@ -1631,7 +1667,8 @@
[t]
end
|> tag_list 1
- |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Eq)), t))
+ |> map (fn (k, t) =>
+ ((dub needs_fairly_sound j k, (Global, Spec_Eq)), t))
val make_facts = map_filter (make_fact ctxt format type_enc false)
val fairly_sound = is_type_enc_fairly_sound type_enc
in
@@ -1826,6 +1863,13 @@
fun mk_aterm format type_enc name T_args args =
ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
+fun do_bound_type ctxt format mono type_enc =
+ case type_enc of
+ Simple_Types (_, _, level) =>
+ fused_type ctxt mono level 0
+ #> ho_type_from_typ format type_enc false 0 #> SOME
+ | _ => K NONE
+
fun tag_with_type ctxt format mono type_enc pos T tm =
IConst (type_tag, T --> T, [T])
|> mangle_type_args_in_iterm format type_enc
@@ -1870,11 +1914,6 @@
val thy = Proof_Context.theory_of ctxt
val level = level_of_type_enc type_enc
val do_term = ho_term_from_iterm ctxt format mono type_enc
- val do_bound_type =
- case type_enc of
- Simple_Types _ => fused_type ctxt mono level 0
- #> ho_type_from_typ format type_enc false 0 #> SOME
- | _ => K NONE
fun do_out_of_bound_type pos phi universal (name, T) =
if should_guard_type ctxt mono type_enc
(fn () => should_guard_var thy polym_constrs level pos phi
@@ -1893,6 +1932,7 @@
let
val phi = phi |> do_formula pos
val universal = Option.map (q = AExists ? not) pos
+ val do_bound_type = do_bound_type ctxt format mono type_enc
in
AQuant (q, xs |> map (apsnd (fn NONE => NONE
| SOME T => do_bound_type T)),
@@ -1912,7 +1952,7 @@
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos
- mono type_enc (j, {name, stature, kind, iformula, atomic_types}) =
+ mono type_enc rank (j, {name, stature, kind, iformula, atomic_types}) =
(prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
iformula
|> formula_from_iformula ctxt polym_constrs format mono type_enc
@@ -1920,12 +1960,14 @@
|> close_formula_universally
|> bound_tvars type_enc true atomic_types,
NONE,
- case snd stature of
- Intro => isabelle_info format introN
- | Elim => isabelle_info format elimN
- | Simp => isabelle_info format simpN
- | Eq => isabelle_info format eqN
- | _ => NONE)
+ let val rank = rank j in
+ case snd stature of
+ Intro => isabelle_info format introN rank
+ | Elim => isabelle_info format elimN rank
+ | Simp => isabelle_info format simpN rank
+ | Spec_Eq => isabelle_info format spec_eqN rank
+ | _ => isabelle_info format "" rank
+ end)
|> Formula
fun formula_line_for_class_rel_clause format type_enc
@@ -1937,7 +1979,7 @@
type_class_formula type_enc superclass ty_arg])
|> mk_aquant AForall
[(tvar_a_name, atype_of_type_vars type_enc)],
- NONE, isabelle_info format introN)
+ NONE, isabelle_info format introN helper_rank)
end
fun formula_from_arity_atom type_enc (class, t, args) =
@@ -1951,7 +1993,7 @@
(formula_from_arity_atom type_enc concl_atom)
|> mk_aquant AForall
(map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
- NONE, isabelle_info format introN)
+ NONE, isabelle_info format introN helper_rank)
fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
({name, kind, iformula, atomic_types, ...} : translated_formula) =
@@ -1960,10 +2002,10 @@
|> formula_from_iformula ctxt polym_constrs format mono type_enc
should_guard_var_in_formula (SOME false)
|> close_formula_universally
- |> bound_tvars type_enc true atomic_types, NONE, NONE)
+ |> bound_tvars type_enc true atomic_types, NONE, [])
fun formula_line_for_free_type j phi =
- Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
+ Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
let
val phis =
@@ -1992,7 +2034,8 @@
map (decl_line_for_class order) classes
| _ => []
-fun sym_decl_table_for_facts ctxt format type_enc sym_tab (conjs, facts) =
+fun sym_decl_table_for_facts ctxt format type_enc sym_tab
+ (conjs, facts, extra_tms) =
let
fun add_iterm_syms tm =
let val (head, args) = strip_iterm_comb tm in
@@ -2052,6 +2095,7 @@
Symtab.empty
|> is_type_enc_fairly_sound type_enc
? (fold (fold add_fact_syms) [conjs, facts]
+ #> fold add_iterm_syms extra_tms
#> (case type_enc of
Simple_Types (First_Order, Polymorphic, _) =>
if avoid_first_order_ghost_type_vars then add_TYPE_const ()
@@ -2158,16 +2202,16 @@
always_guard_var_in_formula (SOME true)
|> close_formula_universally
|> bound_tvars type_enc true (atomic_types_of T),
- NONE, isabelle_info format introN)
+ NONE, isabelle_info format introN helper_rank)
fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
let val x_var = ATerm (`make_bound_var "X", []) in
Formula (tags_sym_formula_prefix ^
ascii_of (mangled_type format type_enc T),
Axiom,
- eq_formula type_enc (atomic_types_of T) false
+ eq_formula type_enc (atomic_types_of T) [] false
(tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
- NONE, isabelle_info format eqN)
+ NONE, isabelle_info format spec_eqN helper_rank)
end
fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
@@ -2199,13 +2243,15 @@
? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
end
+fun honor_conj_sym_kind in_conj conj_sym_kind =
+ if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
+ else (Axiom, I)
+
fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
j (s', T_args, T, _, ary, in_conj) =
let
val thy = Proof_Context.theory_of ctxt
- val (kind, maybe_negate) =
- if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
- else (Axiom, I)
+ val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
val (arg_Ts, res_T) = chop_fun ary T
val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
val bounds =
@@ -2236,7 +2282,7 @@
|> close_formula_universally
|> bound_tvars type_enc (n > 1) (atomic_types_of T)
|> maybe_negate,
- NONE, isabelle_info format introN)
+ NONE, isabelle_info format introN helper_rank)
end
fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
@@ -2248,14 +2294,12 @@
val ident_base =
tags_sym_formula_prefix ^ s ^
(if n > 1 then "_" ^ string_of_int j else "")
- val (kind, maybe_negate) =
- if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
- else (Axiom, I)
+ val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
val (arg_Ts, res_T) = chop_fun ary T
val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
val bounds = bound_names |> map (fn name => ATerm (name, []))
val cst = mk_aterm format type_enc (s, s') T_args
- val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) pred_sym
+ val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
val should_encode = should_encode_type ctxt mono level
val tag_with = tag_with_type ctxt format mono type_enc NONE
val add_formula_for_res =
@@ -2272,7 +2316,7 @@
in
cons (Formula (ident_base ^ "_res", kind,
eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
- NONE, isabelle_info format eqN))
+ NONE, isabelle_info format spec_eqN helper_rank))
end
else
I
@@ -2284,7 +2328,7 @@
cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
(cst bounds),
- NONE, isabelle_info format eqN))
+ NONE, isabelle_info format spec_eqN helper_rank))
| _ => raise Fail "expected nonempty tail"
else
I
@@ -2348,6 +2392,75 @@
syms []
in mono_lines @ decl_lines end
+fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
+
+fun do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
+ mono type_enc sym_tab0 sym_tab base_s0 types in_conj =
+ let
+ fun do_alias ary =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
+ val base_name = base_s0 |> `(make_fixed_const (SOME format))
+ val T = case types of [T] => T | _ => robust_const_type thy base_s0
+ val T_args = robust_const_typargs thy (base_s0, T)
+ val (base_name as (base_s, _), T_args) =
+ mangle_type_args_in_const format type_enc base_name T_args
+ val base_ary = min_ary_of sym_tab0 base_s
+ fun do_const name = IConst (name, T, T_args)
+ val do_term =
+ filter_type_args_in_iterm thy monom_constrs type_enc
+ #> ho_term_from_iterm ctxt format mono type_enc (SOME true)
+ val name1 as (s1, _) =
+ base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
+ val name2 as (s2, _) = base_name |> aliased_uncurried ary
+ val (arg_Ts, _) = chop_fun ary T
+ val bound_names =
+ 1 upto ary |> map (`I o make_bound_var o string_of_int)
+ val bounds = bound_names ~~ arg_Ts
+ val (first_bounds, last_bound) =
+ bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last
+ val tm1 =
+ mk_app_op format type_enc (list_app (do_const name1) first_bounds)
+ last_bound
+ val tm2 = list_app (do_const name2) (first_bounds @ [last_bound])
+ val do_bound_type = do_bound_type ctxt format mono type_enc
+ val eq =
+ eq_formula type_enc (atomic_types_of T)
+ (map (apsnd do_bound_type) bounds) false
+ (do_term tm1) (do_term tm2)
+ in
+ ([tm1, tm2],
+ [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,
+ NONE, isabelle_info format spec_eqN helper_rank)])
+ |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
+ else pair_append (do_alias (ary - 1)))
+ end
+ in do_alias end
+fun uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
+ type_enc sym_tab0 sym_tab
+ (s, {min_ary, types, in_conj, ...} : sym_info) =
+ case unprefix_and_unascii const_prefix s of
+ SOME mangled_s =>
+ if String.isSubstring uncurried_alias_sep mangled_s then
+ let
+ val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
+ in
+ do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
+ mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary
+ end
+ else
+ ([], [])
+ | NONE => ([], [])
+fun uncurried_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
+ mono type_enc uncurried_aliases sym_tab0 sym_tab =
+ ([], [])
+ |> uncurried_aliases
+ ? Symtab.fold_rev
+ (pair_append
+ o uncurried_alias_lines_for_sym ctxt monom_constrs format
+ conj_sym_kind mono type_enc sym_tab0 sym_tab) sym_tab
+
fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
Config.get ctxt type_tag_idempotence andalso
is_type_level_monotonicity_based level andalso
@@ -2356,6 +2469,7 @@
val implicit_declsN = "Should-be-implicit typings"
val explicit_declsN = "Explicit typings"
+val uncurried_alias_eqsN = "Uncurried aliases"
val factsN = "Relevant facts"
val class_relsN = "Class relationships"
val aritiesN = "Arities"
@@ -2385,17 +2499,18 @@
fun undeclared_syms_in_problem type_enc problem =
let
val declared = declared_syms_in_problem problem
- fun do_sym name ty =
- if member (op =) declared name then I else AList.default (op =) (name, ty)
- fun do_type (AType (name as (s, _), tys)) =
- is_tptp_user_symbol s
- ? do_sym name (fn () => nary_type_constr_type (length tys))
+ fun do_sym (name as (s, _)) ty =
+ if is_tptp_user_symbol s andalso not (member (op =) declared name) then
+ AList.default (op =) (name, ty)
+ else
+ I
+ fun do_type (AType (name, tys)) =
+ do_sym name (fn () => nary_type_constr_type (length tys))
#> fold do_type tys
| do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
| do_type (ATyAbs (_, ty)) = do_type ty
fun do_term pred_sym (ATerm (name as (s, _), tms)) =
- is_tptp_user_symbol s
- ? do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
+ do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
#> fold (do_term false) tms
| do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
fun do_formula (AQuant (_, xs, phi)) =
@@ -2436,23 +2551,24 @@
|> List.partition is_poly_constr
|> pairself (map fst)
-(* Forcing explicit applications is expensive for polymorphic encodings, because
- it takes only one existential variable ranging over "'a => 'b" to ruin
- everything. Hence we do it only if there are few facts (which is normally the
- case for "metis" and the minimizer). *)
-val explicit_apply_threshold = 50
+val app_op_threshold = 50
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
- lam_trans readable_names preproc hyp_ts concl_t facts =
+ lam_trans uncurried_aliases readable_names preproc
+ hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
val type_enc = type_enc |> adjust_type_enc format
- val explicit_apply =
+ (* Forcing explicit applications is expensive for polymorphic encodings,
+ because it takes only one existential variable ranging over "'a => 'b" to
+ ruin everything. Hence we do it only if there are few facts (which is
+ normally the case for "metis" and the minimizer). *)
+ val app_op_level =
if polymorphism_of_type_enc type_enc = Polymorphic andalso
- length facts >= explicit_apply_threshold then
- SOME false
+ length facts >= app_op_threshold then
+ Incomplete_Apply
else
- NONE
+ Sufficient_Apply
val lam_trans =
if lam_trans = keep_lamsN andalso
not (is_type_enc_higher_order type_enc) then
@@ -2464,30 +2580,40 @@
lifted) =
translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
concl_t facts
- val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts
+ val sym_tab0 = sym_table_for_facts ctxt type_enc app_op_level conjs facts
val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
val (polym_constrs, monom_constrs) =
all_constrs_of_polymorphic_datatypes thy
|>> map (make_fixed_const (SOME format))
- val firstorderize =
- firstorderize_fact thy monom_constrs format type_enc sym_tab
- val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
- val sym_tab = sym_table_for_facts ctxt type_enc (SOME false) conjs facts
+ fun firstorderize in_helper =
+ firstorderize_fact thy monom_constrs format type_enc sym_tab0
+ (uncurried_aliases andalso not in_helper)
+ val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
+ val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
val helpers =
sym_tab |> helper_facts_for_sym_table ctxt format type_enc
- |> map firstorderize
+ |> map (firstorderize true)
val mono_Ts =
helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
val class_decl_lines = decl_lines_for_classes type_enc classes
+ val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
+ uncurried_alias_lines_for_sym_table ctxt monom_constrs format
+ conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
val sym_decl_lines =
- (conjs, helpers @ facts)
+ (conjs, helpers @ facts, uncurried_alias_eq_tms)
|> sym_decl_table_for_facts ctxt format type_enc sym_tab
|> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
type_enc mono_Ts
+ val num_facts = length facts
+ val fact_lines =
+ map (formula_line_for_fact ctxt polym_constrs format fact_prefix
+ ascii_of (not exporter) (not exporter) mono type_enc
+ (rank_of_fact_num num_facts))
+ (0 upto num_facts - 1 ~~ facts)
val helper_lines =
0 upto length helpers - 1 ~~ helpers
|> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I
- false true mono type_enc)
+ false true mono type_enc (K default_rank))
|> (if needs_type_tag_idempotence ctxt type_enc then
cons (type_tag_idempotence_fact format type_enc)
else
@@ -2496,10 +2622,8 @@
FLOTTER hack. *)
val problem =
[(explicit_declsN, class_decl_lines @ sym_decl_lines),
- (factsN,
- map (formula_line_for_fact ctxt polym_constrs format fact_prefix
- ascii_of (not exporter) (not exporter) mono type_enc)
- (0 upto length facts - 1 ~~ facts)),
+ (uncurried_alias_eqsN, uncurried_alias_eq_lines),
+ (factsN, fact_lines),
(class_relsN,
map (formula_line_for_class_rel_clause format type_enc)
class_rel_clauses),
--- a/src/HOL/Tools/ATP/atp_proof.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sun Feb 05 16:53:20 2012 +0100
@@ -115,7 +115,7 @@
"The prover claims the conjecture is a theorem but did not provide a proof."
| string_for_failure ProofIncomplete =
"The prover claims the conjecture is a theorem but provided an incomplete \
- \proof."
+ \(or unparsable) proof."
| string_for_failure (UnsoundProof (false, ss)) =
"The prover found a type-unsound proof " ^ involving ss ^
"(or, less likely, your axioms are inconsistent). Specify a sound type \
@@ -431,21 +431,30 @@
-- Scan.repeat parse_decorated_atom
>> (mk_horn o apfst (op @))) x
-fun resolve_spass_num spass_names num =
- case Int.fromString num of
- SOME j => if j > 0 andalso j <= Vector.length spass_names then
- Vector.sub (spass_names, j - 1)
- else
- []
- | NONE => []
+fun resolve_spass_num (SOME names) _ _ = names
+ | resolve_spass_num NONE spass_names num =
+ case Int.fromString num of
+ SOME j => if j > 0 andalso j <= Vector.length spass_names then
+ Vector.sub (spass_names, j - 1)
+ else
+ []
+ | NONE => []
-(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. *)
+val parse_spass_debug =
+ Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ","))
+ --| $$ ")")
+
+(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
+ derived from formulae <ident>* *)
fun parse_spass_line spass_names =
- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" -- Symbol.scan_id
- -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
- >> (fn (((num, rule), deps), u) =>
- Inference ((num, resolve_spass_num spass_names num), u, rule,
- map (swap o `(resolve_spass_num spass_names)) deps))
+ parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
+ -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
+ -- parse_horn_clause --| $$ "."
+ -- Scan.option (Scan.this_string "derived from formulae "
+ |-- Scan.repeat scan_general_id)
+ >> (fn ((((num, rule), deps), u), names) =>
+ Inference ((num, resolve_spass_num names spass_names num), u, rule,
+ map (swap o `(resolve_spass_num NONE spass_names)) deps))
(* Syntax: <name> *)
fun parse_satallax_line x =
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Feb 05 16:53:20 2012 +0100
@@ -211,9 +211,7 @@
fun used_facts_in_unsound_atp_proof _ _ [] = NONE
| used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
- let
- val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
- in
+ let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
SOME (map fst used_facts)
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun Feb 05 16:53:20 2012 +0100
@@ -11,6 +11,7 @@
type formula_kind = ATP_Problem.formula_kind
type failure = ATP_Proof.failure
+ type slice_spec = int * atp_format * string * string * bool
type atp_config =
{exec : string * string,
required_execs : (string * string) list,
@@ -22,8 +23,7 @@
conj_sym_kind : formula_kind,
prem_kind : formula_kind,
best_slices :
- Proof.context
- -> (real * (bool * (int * atp_format * string * string * string))) list}
+ Proof.context -> (real * (bool * (slice_spec * string))) list}
val force_sos : bool Config.T
val e_smartN : string
@@ -57,8 +57,7 @@
val remote_atp :
string -> string -> string list -> (string * string) list
-> (failure * string) list -> formula_kind -> formula_kind
- -> (Proof.context -> int * atp_format * string * string)
- -> string * atp_config
+ -> (Proof.context -> slice_spec) -> string * atp_config
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
@@ -76,6 +75,8 @@
(* ATP configuration *)
+type slice_spec = int * atp_format * string * string * bool
+
type atp_config =
{exec : string * string,
required_execs : (string * string) list,
@@ -86,17 +87,16 @@
known_failures : (failure * string) list,
conj_sym_kind : formula_kind,
prem_kind : formula_kind,
- best_slices :
- Proof.context
- -> (real * (bool * (int * atp_format * string * string * string))) list}
+ best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
(* "best_slices" must be found empirically, taking a wholistic approach since
- the ATPs are run in parallel. The "real" components give the faction of the
- time available given to the slice and should add up to 1.0. The "bool"
+ the ATPs are run in parallel. The "real" component gives the faction of the
+ time available given to the slice and should add up to 1.0. The first "bool"
component indicates whether the slice's strategy is complete; the "int", the
preferred number of facts to pass; the first "string", the preferred type
system (which should be sound or quasi-sound); the second "string", the
- preferred lambda translation scheme; the third "string", extra information to
+ preferred lambda translation scheme; the second "bool", whether uncurried
+ aliased should be generated; the third "string", extra information to
the prover (e.g., SOS or no SOS).
The last slice should be the most "normal" one, because it will get all the
@@ -150,7 +150,8 @@
type T = (atp_config * stamp) Symtab.table
val empty = Symtab.empty
val extend = I
- fun merge data : T = Symtab.merge (eq_snd op =) data
+ fun merge data : T =
+ Symtab.merge (eq_snd (op =)) data
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
)
@@ -246,14 +247,14 @@
let val method = effective_e_weight_method ctxt in
(* FUDGE *)
if method = e_smartN then
- [(0.333, (true, (500, FOF, "mono_tags??", combsN,
+ [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false),
e_fun_weightN))),
- (0.334, (true, (50, FOF, "mono_guards??", combsN,
+ (0.334, (true, ((50, FOF, "mono_guards??", combsN, false),
e_fun_weightN))),
- (0.333, (true, (1000, FOF, "mono_tags??", combsN,
+ (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false),
e_sym_offset_weightN)))]
else
- [(1.0, (true, (500, FOF, "mono_tags??", combsN, method)))]
+ [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))]
end}
val e = (eN, e_config)
@@ -278,9 +279,9 @@
prem_kind = Hypothesis,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", liftingN,
+ [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN, false),
sosN))),
- (0.333, (true, (50, leo2_thf0, "mono_simple_higher", liftingN,
+ (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN, false),
no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -305,8 +306,8 @@
prem_kind = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", keep_lamsN,
- "")))]}
+ K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN,
+ false), "")))]}
val satallax = (satallaxN, satallax_config)
@@ -338,23 +339,29 @@
prem_kind = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", liftingN,
+ [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
sosN))),
- (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", liftingN,
+ (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false),
sosN))),
- (0.334, (false, (50, DFG DFG_Unsorted, "mono_tags??", liftingN,
+ (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
val spass = (spassN, spass_config)
+val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN, true)
+val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN, true)
+val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN, true)
+
(* Experimental *)
val spass_new_config : atp_config =
- {exec = ("ISABELLE_ATP", "scripts/spass_new"),
+ {exec = ("SPASS_NEW_HOME", "SPASS"),
required_execs = [],
arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ =>
- ("-Auto -LR=1 -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
+ (* TODO: add: -FPDFGProof -FPFCR *)
+ ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
+ (* TODO: not used yet *)
|> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ",
proof_delims = #proof_delims spass_config,
known_failures = #known_failures spass_config,
@@ -362,11 +369,9 @@
prem_kind = #prem_kind spass_config,
best_slices = fn _ =>
(* FUDGE *)
- [(0.334, (false, (50, DFG DFG_Sorted, "mono_simple", combs_and_liftingN,
- spass_incompleteN))),
- (0.333, (false, (150, DFG DFG_Sorted, "poly_tags??", combs_and_liftingN,
- ""))),
- (0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN, "")))]}
+ [(0.300, (true, (spass_new_slice_1, ""))),
+ (0.333, (true, (spass_new_slice_2, ""))),
+ (0.333, (true, (spass_new_slice_3, "")))]}
val spass_new = (spass_newN, spass_new_config)
@@ -406,16 +411,19 @@
best_slices = fn ctxt =>
(* FUDGE *)
(if is_old_vampire_version () then
- [(0.333, (false, (150, FOF, "poly_guards??", combs_or_liftingN, sosN))),
- (0.333, (false, (500, FOF, "mono_tags??", combs_or_liftingN, sosN))),
- (0.334, (true, (50, FOF, "mono_guards??", combs_or_liftingN, no_sosN)))]
+ [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false),
+ sosN))),
+ (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false),
+ sosN))),
+ (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false),
+ no_sosN)))]
else
- [(0.333, (false, (150, vampire_tff0, "poly_guards??", combs_or_liftingN,
- sosN))),
- (0.333, (false, (500, vampire_tff0, "mono_simple", combs_or_liftingN,
- sosN))),
- (0.334, (true, (50, vampire_tff0, "mono_simple", combs_or_liftingN,
- no_sosN)))])
+ [(0.333, (false, ((150, vampire_tff0, "poly_guards??",
+ combs_or_liftingN, false), sosN))),
+ (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN,
+ false), sosN))),
+ (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN,
+ false), no_sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -437,10 +445,10 @@
prem_kind = Hypothesis,
best_slices =
(* FUDGE *)
- K [(0.5, (false, (250, z3_tff0, "mono_simple", combsN, ""))),
- (0.25, (false, (125, z3_tff0, "mono_simple", combsN, ""))),
- (0.125, (false, (62, z3_tff0, "mono_simple", combsN, ""))),
- (0.125, (false, (31, z3_tff0, "mono_simple", combsN, "")))]}
+ K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN, false), ""))),
+ (0.25, (false, ((125, z3_tff0, "mono_simple", combsN, false), ""))),
+ (0.125, (false, ((62, z3_tff0, "mono_simple", combsN, false), ""))),
+ (0.125, (false, ((31, z3_tff0, "mono_simple", combsN, false), "")))]}
val z3_tptp = (z3_tptpN, z3_tptp_config)
@@ -456,9 +464,9 @@
conj_sym_kind = Hypothesis,
prem_kind = Hypothesis,
best_slices =
- K [(1.0, (false, (200, format, type_enc,
- if is_format_higher_order format then keep_lamsN
- else combsN, "")))]}
+ K [(1.0, (false, ((200, format, type_enc,
+ if is_format_higher_order format then keep_lamsN
+ else combsN, false), "")))]}
val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
@@ -509,16 +517,13 @@
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
- "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
- ^ " -s " ^ the_system system_name system_versions,
+ "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
+ " -s " ^ the_system system_name system_versions,
proof_delims = union (op =) tstp_proof_delims proof_delims,
known_failures = known_failures @ known_perl_failures @ known_says_failures,
conj_sym_kind = conj_sym_kind,
prem_kind = prem_kind,
- best_slices = fn ctxt =>
- let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in
- [(1.0, (false, (max_relevant, format, type_enc, lam_trans, "")))]
- end}
+ best_slices = fn ctxt => [(1.0, (false, (best_slice ctxt, "")))]}
fun remotify_config system_name system_versions best_slice
({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
@@ -539,43 +544,44 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
- (K (750, FOF, "mono_tags??", combsN) (* FUDGE *))
+ (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
- (K (100, leo2_thf0, "mono_simple_higher", liftingN) (* FUDGE *))
+ (K (100, leo2_thf0, "mono_simple_higher", liftingN, false) (* FUDGE *))
val remote_satallax =
remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
- (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *))
+ (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN, false)
+ (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["1.8"]
- (K (250, FOF, "mono_guards??", combs_or_liftingN) (* FUDGE *))
+ (K (250, FOF, "mono_guards??", combs_or_liftingN, false) (* FUDGE *))
val remote_z3_tptp =
remotify_atp z3_tptp "Z3" ["3.0"]
- (K (250, z3_tff0, "mono_simple", combsN) (* FUDGE *))
+ (K (250, z3_tff0, "mono_simple", combsN, false) (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
- Conjecture (K (500, FOF, "mono_guards??", combsN) (* FUDGE *))
+ Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *))
val remote_iprover =
remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
- (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
+ (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
val remote_iprover_eq =
remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
- (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
+ (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
- (K (100, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
+ (K (100, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
val remote_e_tofof =
remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
Hypothesis
- (K (150, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
+ (K (150, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
[("#START OF PROOF", "Proved Goals:")]
[(OutOfResources, "Too many function symbols"),
(Crashed, "Unrecoverable Segmentation Fault")]
Hypothesis Hypothesis
- (K (50, CNF_UEQ, "mono_tags??", combsN) (* FUDGE *))
+ (K (50, CNF_UEQ, "mono_tags??", combsN, false) (* FUDGE *))
(* Setup *)
--- a/src/HOL/Tools/ATP/scripts/spass Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/ATP/scripts/spass Sun Feb 05 16:53:20 2012 +0100
@@ -8,11 +8,11 @@
options=${@:1:$(($#-1))}
name=${@:$(($#)):1}
-"$SPASS_HOME/SPASS" -Flotter $name \
+"$SPASS_HOME/SPASS" -Flotter "$name" \
| sed 's/description({$/description({*/' \
| sed 's/set_ClauseFormulaRelation()\.//' \
> $name.cnf
cat $name.cnf
-"$SPASS_HOME/SPASS" $options $name.cnf \
+"$SPASS_HOME/SPASS" $options "$name.cnf" \
| sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
-rm -f $name.cnf
+rm -f "$name.cnf"
--- a/src/HOL/Tools/ATP/scripts/spass_new Sun Feb 05 16:53:11 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-#!/usr/bin/env bash
-#
-# Wrapper for SPASS 3.8 that also outputs the clause-to-formula relation
-#
-# Author: Jasmin Blanchette, TU Muenchen
-
-options=${@:1:$(($#-1))}
-name=${@:$(($#)):1}
-
-rm -f $name.prf
-"$SPASS_NEW_HOME/SPASS" -FPDFGProof -FPFCR $options $name \
- | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
-cat $name.prf
-#rm -f $name.cnf
--- a/src/HOL/Tools/Metis/metis_generate.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML Sun Feb 05 16:53:20 2012 +0100
@@ -242,7 +242,7 @@
val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
val (atp_problem, _, _, lifted, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
- false false [] @{prop False} props
+ false false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Feb 05 16:53:20 2012 +0100
@@ -337,7 +337,7 @@
let
val s = s |> Metis_Name.toString
|> perhaps (try (unprefix_and_unascii const_prefix
- #> the #> unmangled_const_name))
+ #> the #> unmangled_const_name #> hd))
in
if s = metis_predicator orelse s = predicator_name orelse
s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Sun Feb 05 16:53:20 2012 +0100
@@ -3,11 +3,12 @@
-}
module Narrowing_Engine where
-import Monad
+import Control.Monad
import Control.Exception
+import System.IO
import System.Exit
-import Maybe
-import List (partition, findIndex)
+import Data.Maybe
+import Data.List (partition, findIndex)
import qualified Generated_Code
@@ -35,7 +36,7 @@
termListOf' i [] = []
termListOf' i (e : es) =
let
- (ts, rs) = List.partition (\e -> head (posOf e) == i) (e : es)
+ (ts, rs) = Data.List.partition (\e -> head (posOf e) == i) (e : es)
t = termOf (pos ++ [i]) (map tailPosEdge ts)
in
(t : termListOf' (i + 1) rs)
--- a/src/HOL/Tools/Quotient/quotient_term.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Sun Feb 05 16:53:20 2012 +0100
@@ -728,7 +728,7 @@
| matches ((rty, qty)::tail) =
(case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
NONE => matches tail
- | SOME inst => Envir.subst_type inst qty)
+ | SOME inst => subst_typ ctxt ty_subst (Envir.subst_type inst qty))
in
matches ty_subst
end
@@ -749,7 +749,7 @@
| matches ((rconst, qconst)::tail) =
(case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
NONE => matches tail
- | SOME inst => Envir.subst_term inst qconst)
+ | SOME inst => subst_trm ctxt ty_subst trm_subst (Envir.subst_term inst qconst))
in
matches trm_subst
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun Feb 05 16:53:20 2012 +0100
@@ -7,6 +7,7 @@
signature SLEDGEHAMMER_FILTER =
sig
+ type status = ATP_Problem_Generate.status
type stature = ATP_Problem_Generate.stature
type relevance_fudge =
@@ -42,8 +43,9 @@
val const_names_in_fact :
theory -> (string * typ -> term list -> bool * term list) -> term
-> string list
+ val clasimpset_rule_table_of : Proof.context -> status Termtab.table
val fact_from_ref :
- Proof.context -> unit Symtab.table -> thm list
+ Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
-> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
val all_facts :
Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list
@@ -109,6 +111,35 @@
val skolem_prefix = sledgehammer_prefix ^ "sko"
val theory_const_suffix = Long_Name.separator ^ " 1"
+val crude_zero_vars =
+ map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
+ #> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S)))
+
+fun clasimpset_rule_table_of ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
+ fun add stature g f =
+ fold (Termtab.update o rpair stature o g o crude_zero_vars o prop_of o f)
+ val {safeIs, safeEs, hazIs, hazEs, ...} =
+ ctxt |> claset_of |> Classical.rep_cs
+ val intros = Item_Net.content safeIs @ Item_Net.content hazIs
+ val elims =
+ Item_Net.content safeEs @ Item_Net.content hazEs
+ |> map Classical.classical_rule
+ val simps = ctxt |> simpset_of |> dest_ss |> #simps
+ val spec_eqs =
+ ctxt |> Spec_Rules.get
+ |> filter (curry (op =) Spec_Rules.Equational o fst)
+ |> maps (snd o snd)
+ in
+ Termtab.empty |> add Simp I snd simps
+ |> add Simp atomize snd simps
+ |> add Spec_Eq I I spec_eqs
+ |> add Elim I I elims
+ |> add Intro I I intros
+ end
+
fun needs_quoting reserved s =
Symtab.defined reserved s orelse
exists (not o Lexicon.is_identifier) (Long_Name.explode s)
@@ -123,7 +154,29 @@
val backquote =
raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
-fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
+
+fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
+fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
+
+fun scope_of_thm global assms chained_ths th =
+ if is_chained chained_ths th then Chained
+ else if global then Global
+ else if is_assum assms th then Assum
+ else Local
+
+fun status_of_thm css_table name th =
+ (* FIXME: use structured name *)
+ if String.isSubstring ".induct" name orelse
+ String.isSubstring ".inducts" name then
+ Induct
+ else case Termtab.lookup css_table (prop_of th) of
+ SOME status => status
+ | NONE => General
+
+fun stature_of_thm global assms chained_ths css_table name th =
+ (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
+
+fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
val bracket =
@@ -142,10 +195,10 @@
in
(ths, (0, []))
|-> fold (fn th => fn (j, rest) =>
- (j + 1,
- ((nth_name j,
- (if member Thm.eq_thm_prop chained_ths th then Chained
- else Local (* just in case *), General)), th) :: rest))
+ let val name = nth_name j in
+ (j + 1, ((name, stature_of_thm false [] chained_ths
+ css_table name th), th) :: rest)
+ end)
|> snd
end
@@ -776,35 +829,6 @@
is_that_fact thm
end)
-val crude_zero_vars =
- map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
- #> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S)))
-
-fun clasimpset_rule_table_of ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
- val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
- fun add stature g f =
- fold (Termtab.update o rpair stature o g o crude_zero_vars o prop_of o f)
- val {safeIs, safeEs, hazIs, hazEs, ...} =
- ctxt |> claset_of |> Classical.rep_cs
- val intros = Item_Net.content safeIs @ Item_Net.content hazIs
- val elims =
- Item_Net.content safeEs @ Item_Net.content hazEs
- |> map Classical.classical_rule
- val simps = ctxt |> simpset_of |> dest_ss |> #simps
- val eqs =
- ctxt |> Spec_Rules.get
- |> filter (curry (op =) Spec_Rules.Equational o fst)
- |> maps (snd o snd)
- in
- Termtab.empty |> add Simp I snd simps
- |> add Simp atomize snd simps
- |> add Eq I I eqs
- |> add Elim I I elims
- |> add Intro I I intros
- end
-
fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths =
let
val thy = Proof_Context.theory_of ctxt
@@ -812,22 +836,7 @@
val local_facts = Proof_Context.facts_of ctxt
val named_locals = local_facts |> Facts.dest_static []
val assms = Assumption.all_assms_of ctxt
- fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
- val is_chained = member Thm.eq_thm_prop chained_ths
- val clasimpset_table = clasimpset_rule_table_of ctxt
- fun scope_of_thm global th =
- if is_chained th then Chained
- else if global then Global
- else if is_assum th then Assum
- else Local
- fun status_of_thm name th =
- (* FIXME: use structured name *)
- if String.isSubstring ".induct" name orelse
- String.isSubstring ".inducts" name then
- Induct
- else case Termtab.lookup clasimpset_table (prop_of th) of
- SOME status => status
- | NONE => General
+ val css_table = clasimpset_rule_table_of ctxt
fun is_good_unnamed_local th =
not (Thm.has_name_hint th) andalso
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
@@ -877,8 +886,8 @@
|> (fn SOME name =>
make_name reserved multi j name
| NONE => "")),
- (scope_of_thm global th,
- status_of_thm name0 th)), th)
+ stature_of_thm global assms chained_ths
+ css_table name0 th), th)
in
if multi then (new :: multis, unis)
else (multis, new :: unis)
@@ -906,10 +915,11 @@
Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
|> Object_Logic.atomize_term thy
val ind_stmt_xs = external_frees ind_stmt
+ val css_table = clasimpset_rule_table_of ctxt
in
(if only then
maps (map (fn ((name, stature), th) => ((K name, stature), th))
- o fact_from_ref ctxt reserved chained_ths) add
+ o fact_from_ref ctxt reserved chained_ths css_table) add
else
all_facts ctxt ho_atp reserved false add_ths chained_ths)
|> Config.get ctxt instantiate_inducts
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 05 16:53:20 2012 +0100
@@ -89,6 +89,7 @@
("type_enc", "smart"),
("strict", "false"),
("lam_trans", "smart"),
+ ("uncurried_aliases", "smart"),
("relevance_thresholds", "0.45 0.85"),
("max_relevant", "smart"),
("max_mono_iters", "3"),
@@ -107,14 +108,15 @@
("no_overlord", "overlord"),
("non_blocking", "blocking"),
("non_strict", "strict"),
+ ("no_uncurried_aliases", "uncurried_aliases"),
("no_isar_proof", "isar_proof"),
("dont_slice", "slice"),
("dont_minimize", "minimize")]
val params_for_minimize =
["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
- "max_mono_iters", "max_new_mono_instances", "isar_proof",
- "isar_shrink_factor", "timeout", "preplay_timeout"]
+ "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
+ "isar_proof", "isar_shrink_factor", "timeout", "preplay_timeout"]
val property_dependent_params = ["provers", "timeout"]
@@ -210,7 +212,8 @@
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put SPASS first. *)
fun default_provers_param_value ctxt =
- [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN]
+ [spassN, spass_newN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN,
+ waldmeisterN]
|> map_filter (remotify_prover_if_not_installed ctxt)
|> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
max_default_remote_threads)
@@ -285,6 +288,7 @@
| s => (type_enc_from_string Strict s; SOME s)
val strict = mode = Auto_Try orelse lookup_bool "strict"
val lam_trans = lookup_option lookup_string "lam_trans"
+ val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_option lookup_int "max_relevant"
val max_mono_iters = lookup_int "max_mono_iters"
@@ -303,8 +307,9 @@
in
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
provers = provers, type_enc = type_enc, strict = strict,
- lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
- max_relevant = max_relevant, max_mono_iters = max_mono_iters,
+ lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
+ relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
+ max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slice = slice,
minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Feb 05 16:53:20 2012 +0100
@@ -48,7 +48,8 @@
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
max_new_mono_instances, type_enc, strict, lam_trans,
- isar_proof, isar_shrink_factor, preplay_timeout, ...} : params)
+ uncurried_aliases, isar_proof, isar_shrink_factor,
+ preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state facts =
let
val _ =
@@ -62,8 +63,9 @@
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_enc = type_enc, strict = strict,
- lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
- max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
+ lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
+ relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
+ max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slice = false,
minimize = SOME false, timeout = timeout,
@@ -216,9 +218,10 @@
val ctxt = Proof.context_of state
val reserved = reserved_isar_keyword_table ()
val chained_ths = normalize_chained_theorems (#facts (Proof.goal state))
+ val css_table = clasimpset_rule_table_of ctxt
val facts =
- refs
- |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
+ refs |> maps (map (apsnd single)
+ o fact_from_ref ctxt reserved chained_ths css_table)
in
case subgoal_count state of
0 => Output.urgent_message "No subgoal!"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Feb 05 16:53:20 2012 +0100
@@ -27,6 +27,7 @@
type_enc: string option,
strict: bool,
lam_trans: string option,
+ uncurried_aliases: bool option,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -147,7 +148,7 @@
let val thy = Proof_Context.theory_of ctxt in
case try (get_atp thy) name of
SOME {best_slices, ...} =>
- exists (fn (_, (_, (_, format, _, _, _))) => is_format format)
+ exists (fn (_, (_, ((_, format, _, _, _), _))) => is_format format)
(best_slices ctxt)
| NONE => false
end
@@ -174,7 +175,7 @@
if is_reconstructor name then
reconstructor_default_max_relevant
else if is_atp thy name then
- fold (Integer.max o #1 o snd o snd o snd)
+ fold (Integer.max o #1 o fst o snd o snd o snd)
(get_slices slice (#best_slices (get_atp thy name) ctxt)) 0
else (* is_smt_prover ctxt name *)
SMT_Solver.default_max_relevant ctxt name
@@ -291,6 +292,7 @@
type_enc: string option,
strict: bool,
lam_trans: string option,
+ uncurried_aliases: bool option,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -399,10 +401,10 @@
| _ => "Try this"
fun bunch_of_reconstructors needs_full_types lam_trans =
- [(false, Metis (partial_type_enc, lam_trans true)),
+ [(false, Metis (partial_type_enc, lam_trans false)),
(true, Metis (full_type_enc, lam_trans false)),
- (false, Metis (no_typesN, lam_trans false)),
- (true, Metis (really_full_type_enc, lam_trans false)),
+ (false, Metis (no_typesN, lam_trans true)),
+ (true, Metis (really_full_type_enc, lam_trans true)),
(true, SMT)]
|> map_filter (fn (full_types, reconstr) =>
if needs_full_types andalso not full_types then NONE
@@ -581,9 +583,9 @@
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
(params as {debug, verbose, overlord, type_enc, strict, lam_trans,
- max_relevant, max_mono_iters, max_new_mono_instances,
- isar_proof, isar_shrink_factor, slice, timeout,
- preplay_timeout, ...})
+ uncurried_aliases, max_relevant, max_mono_iters,
+ max_new_mono_instances, isar_proof, isar_shrink_factor,
+ slice, timeout, preplay_timeout, ...})
minimize_command
({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
@@ -651,10 +653,11 @@
|> curry ListPair.zip (map fst facts)
|> maps (fn (name, rths) => map (pair name o snd) rths)
end
- fun run_slice (slice, (time_frac, (complete,
- (best_max_relevant, format, best_type_enc,
- best_lam_trans, extra))))
- time_left =
+ fun run_slice time_left (cache_key, cache_value)
+ (slice, (time_frac, (complete,
+ (key as (best_max_relevant, format, best_type_enc,
+ best_lam_trans, best_uncurried_aliases),
+ extra)))) =
let
val num_facts =
length facts |> is_none max_relevant
@@ -663,14 +666,6 @@
val type_enc =
type_enc |> choose_type_enc soundness best_type_enc format
val fairly_sound = is_type_enc_fairly_sound type_enc
- val facts =
- facts |> map untranslated_fact
- |> not fairly_sound
- ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
- |> take num_facts
- |> polymorphism_of_type_enc type_enc <> Polymorphic
- ? monomorphize_facts
- |> map (apsnd prop_of)
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
((real_ms time_left
@@ -695,20 +690,36 @@
case lam_trans of
SOME s => s
| NONE => best_lam_trans
- val (atp_problem, pool, fact_names, _, sym_tab) =
- prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_enc false lam_trans readable_names true hyp_ts
- concl_t facts
+ val uncurried_aliases =
+ case uncurried_aliases of
+ SOME b => b
+ | NONE => best_uncurried_aliases
+ val value as (atp_problem, _, fact_names, _, _) =
+ if cache_key = SOME key then
+ cache_value
+ else
+ facts
+ |> map untranslated_fact
+ |> not fairly_sound
+ ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
+ |> take num_facts
+ |> polymorphism_of_type_enc type_enc <> Polymorphic
+ ? monomorphize_facts
+ |> map (apsnd prop_of)
+ |> prepare_atp_problem ctxt format conj_sym_kind prem_kind
+ type_enc false lam_trans uncurried_aliases
+ readable_names true hyp_ts concl_t
fun weights () = atp_problem_weights atp_problem
val full_proof = debug orelse isar_proof
- val core =
+ val command =
File.shell_path command ^ " " ^
arguments ctxt full_proof extra slice_timeout weights ^ " " ^
File.shell_path prob_file
- val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1"
- val _ = atp_problem |> lines_for_atp_problem format
- |> cons ("% " ^ command ^ "\n")
- |> File.write_list prob_file
+ |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
+ val _ =
+ atp_problem |> lines_for_atp_problem format
+ |> cons ("% " ^ command ^ "\n")
+ |> File.write_list prob_file
val ((output, run_time), (atp_proof, outcome)) =
TimeLimit.timeLimit generous_slice_timeout
Isabelle_System.bash_output command
@@ -735,8 +746,11 @@
SOME facts =>
let
val failure =
- UnsoundProof (is_type_enc_quasi_sound type_enc,
- facts)
+ if null facts then
+ ProofIncomplete
+ else
+ UnsoundProof (is_type_enc_quasi_sound type_enc,
+ facts)
in
if debug then
(warning (string_for_failure failure); NONE)
@@ -745,27 +759,24 @@
end
| NONE => NONE)
| _ => outcome
- in
- ((pool, fact_names, sym_tab),
- (output, run_time, atp_proof, outcome))
- end
+ in ((SOME key, value), (output, run_time, atp_proof, outcome)) end
val timer = Timer.startRealTimer ()
fun maybe_run_slice slice
- (result as (_, (_, run_time0, _, SOME _))) =
+ (result as (cache, (_, run_time0, _, SOME _))) =
let
val time_left = Time.- (timeout, Timer.checkRealTimer timer)
in
if Time.<= (time_left, Time.zeroTime) then
result
else
- run_slice slice time_left
- |> (fn (stuff, (output, run_time, atp_proof, outcome)) =>
- (stuff, (output, Time.+ (run_time0, run_time),
+ run_slice time_left cache slice
+ |> (fn (cache, (output, run_time, atp_proof, outcome)) =>
+ (cache, (output, Time.+ (run_time0, run_time),
atp_proof, outcome)))
end
| maybe_run_slice _ result = result
in
- ((Symtab.empty, Vector.fromList [], Symtab.empty),
+ ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
("", Time.zeroTime, [], SOME InternalError))
|> fold maybe_run_slice actual_slices
end
@@ -781,7 +792,8 @@
()
else
File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
- val ((pool, fact_names, sym_tab), (output, run_time, atp_proof, outcome)) =
+ val ((_, (_, pool, fact_names, _, sym_tab)),
+ (output, run_time, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
val important_message =
if mode = Normal andalso
@@ -798,8 +810,8 @@
val reconstrs =
bunch_of_reconstructors needs_full_types
(lam_trans_from_atp_proof atp_proof
- o (fn plain =>
- if plain then metis_default_lam_trans else hide_lamsN))
+ o (fn desperate => if desperate then hide_lamsN
+ else metis_default_lam_trans))
in
(used_facts,
fn () =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Feb 05 16:53:20 2012 +0100
@@ -74,9 +74,9 @@
fun adjust_reconstructor_params override_params
({debug, verbose, overlord, blocking, provers, type_enc, strict,
- lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
- max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
- minimize, timeout, preplay_timeout, expect} : params) =
+ lam_trans, uncurried_aliases, relevance_thresholds, max_relevant,
+ max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
+ slice, minimize, timeout, preplay_timeout, expect} : params) =
let
fun lookup_override name default_value =
case AList.lookup (op =) override_params name of
@@ -89,8 +89,8 @@
in
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
provers = provers, type_enc = type_enc, strict = strict,
- lam_trans = lam_trans, max_relevant = max_relevant,
- relevance_thresholds = relevance_thresholds,
+ lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
+ max_relevant = max_relevant, relevance_thresholds = relevance_thresholds,
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slice = slice,
--- a/src/HOL/Tools/list_to_set_comprehension.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/Tools/list_to_set_comprehension.ML Sun Feb 05 16:53:20 2012 +0100
@@ -82,7 +82,7 @@
fun check (i, case_t) s =
(case strip_abs_body case_t of
(Const (@{const_name List.Nil}, _)) => s
- | t => (case s of NONE => SOME i | SOME s => NONE))
+ | _ => (case s of NONE => SOME i | SOME _ => NONE))
in
fold_index check cases NONE
end
@@ -132,7 +132,7 @@
in
(* do case distinction *)
Splitter.split_tac [#split info] 1
- THEN EVERY (map_index (fn (i', case_rewrite) =>
+ THEN EVERY (map_index (fn (i', _) =>
(if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
THEN REPEAT_DETERM (rtac @{thm allI} 1)
THEN rtac @{thm impI} 1
@@ -207,7 +207,7 @@
val eqs' = map reverse_bounds eqs
val pat_eq' = reverse_bounds pat_eq
val inner_t =
- fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy T t)
+ fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
(rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
val lhs = term_of redex
val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Executable_Relation.thy Sun Feb 05 16:53:20 2012 +0100
@@ -0,0 +1,79 @@
+theory Executable_Relation
+imports Main
+begin
+
+text {*
+ Current problem: rtrancl is not executable on an infinite type.
+*}
+
+lemma
+ "(x, (y :: nat)) : rtrancl (R Un S) \<Longrightarrow> (x, y) : (rtrancl R) Un (rtrancl S)"
+(* quickcheck[exhaustive] fails ! *)
+oops
+
+code_thms rtrancl
+
+hide_const (open) rtrancl trancl
+
+quotient_type 'a rel = "('a * 'a) set" / "(op =)"
+morphisms set_of_rel rel_of_set by (metis identity_equivp)
+
+lemma [simp]:
+ "rel_of_set (set_of_rel S) = S"
+by (rule Quotient_abs_rep[OF Quotient_rel])
+
+lemma [simp]:
+ "set_of_rel (rel_of_set R) = R"
+by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl)
+
+no_notation
+ Set.member ("(_/ : _)" [50, 51] 50)
+
+quotient_definition member :: "'a * 'a => 'a rel => bool" where
+ "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool"
+
+notation
+ member ("(_/ : _)" [50, 51] 50)
+
+quotient_definition union :: "'a rel => 'a rel => 'a rel" where
+ "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
+
+quotient_definition rtrancl :: "'a rel => 'a rel" where
+ "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set"
+
+definition reflcl_raw
+where "reflcl_raw R = R \<union> Id"
+
+quotient_definition reflcl :: "('a * 'a) set => 'a rel" where
+ "reflcl" is "reflcl_raw :: ('a * 'a) set => ('a * 'a) set"
+
+code_datatype reflcl rel_of_set
+
+lemma member_code[code]:
+ "(x, y) : rel_of_set R = Set.member (x, y) R"
+ "(x, y) : reflcl R = ((x = y) \<or> Set.member (x, y) R)"
+unfolding member_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def
+by auto
+
+lemma union_code[code]:
+ "union (rel_of_set R) (rel_of_set S) = rel_of_set (Set.union R S)"
+ "union (reflcl R) (rel_of_set S) = reflcl (Set.union R S)"
+ "union (reflcl R) (reflcl S) = reflcl (Set.union R S)"
+ "union (rel_of_set R) (reflcl S) = reflcl (Set.union R S)"
+unfolding union_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def
+by (auto intro: arg_cong[where f=rel_of_set])
+
+lemma rtrancl_code[code]:
+ "rtrancl (rel_of_set R) = reflcl (Transitive_Closure.trancl R)"
+ "rtrancl (reflcl R) = reflcl (Transitive_Closure.trancl R)"
+unfolding rtrancl_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def
+by (auto intro: arg_cong[where f=rel_of_set])
+
+quickcheck_generator rel constructors: rel_of_set
+
+lemma
+ "(x, (y :: nat)) : rtrancl (union R S) \<Longrightarrow> (x, y) : (union (rtrancl R) (rtrancl S))"
+quickcheck[exhaustive]
+oops
+
+end
--- a/src/HOL/ex/Quickcheck_Examples.thy Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Sun Feb 05 16:53:20 2012 +0100
@@ -267,6 +267,19 @@
oops
+subsection {* Examples with sets *}
+
+lemma
+ "{} = A Un - A"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "[| bij_betw f A B; bij_betw f C D |] ==> bij_betw f (A Un C) (B Un D)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+
subsection {* Examples with relations *}
lemma
--- a/src/HOL/ex/ROOT.ML Sun Feb 05 16:53:11 2012 +0100
+++ b/src/HOL/ex/ROOT.ML Sun Feb 05 16:53:20 2012 +0100
@@ -72,7 +72,8 @@
"List_to_Set_Comprehension_Examples",
"Set_Algebras",
"Seq",
- "Simproc_Tests"
+ "Simproc_Tests",
+ "Executable_Relation"
];
if getenv "ISABELLE_GHC" = "" then ()