--- a/src/HOL/List.thy Fri Aug 26 08:56:29 2011 -0700
+++ b/src/HOL/List.thy Fri Aug 26 10:38:29 2011 -0700
@@ -4703,7 +4703,7 @@
qed
-text{* Accessible part of @{term listrel1} relations: *}
+text{* Accessible part and wellfoundedness: *}
lemma Cons_acc_listrel1I [intro!]:
"x \<in> acc r \<Longrightarrow> xs \<in> acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> acc (listrel1 r)"
@@ -4729,6 +4729,9 @@
apply (fastsimp dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
done
+lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
+by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff)
+
subsubsection {* Lifting Relations to Lists: all elements *}
--- a/src/HOL/Quotient_Examples/FSet.thy Fri Aug 26 08:56:29 2011 -0700
+++ b/src/HOL/Quotient_Examples/FSet.thy Fri Aug 26 10:38:29 2011 -0700
@@ -196,7 +196,11 @@
lemma member_rsp [quot_respect]:
shows "(op \<approx> ===> op =) List.member List.member"
- by (auto intro!: fun_relI simp add: mem_def)
+proof
+ fix x y assume "x \<approx> y"
+ then show "List.member x = List.member y"
+ unfolding fun_eq_iff by simp
+qed
lemma nil_rsp [quot_respect]:
shows "(op \<approx>) Nil Nil"
--- a/src/HOL/Tools/ATP/atp_problem.ML Fri Aug 26 08:56:29 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Aug 26 10:38:29 2011 -0700
@@ -19,12 +19,13 @@
datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
+ datatype tff_flavor = Implicit | Explicit
datatype thf_flavor = Without_Choice | With_Choice
datatype format =
CNF |
CNF_UEQ |
FOF |
- TFF |
+ TFF of tff_flavor |
THF of thf_flavor
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
@@ -118,12 +119,14 @@
datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
+datatype tff_flavor = Implicit | Explicit
datatype thf_flavor = Without_Choice | With_Choice
+
datatype format =
CNF |
CNF_UEQ |
FOF |
- TFF |
+ TFF of tff_flavor |
THF of thf_flavor
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
@@ -199,10 +202,10 @@
fun formula_fold pos f =
let
- fun aux pos (AQuant (_, _, phi)) = aux pos phi
- | aux pos (AConn conn) = aconn_fold pos aux conn
- | aux pos (AAtom tm) = f pos tm
- in aux pos end
+ fun fld pos (AQuant (_, _, phi)) = fld pos phi
+ | fld pos (AConn conn) = aconn_fold pos fld conn
+ | fld pos (AAtom tm) = f pos tm
+ in fld pos end
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
@@ -210,7 +213,7 @@
fun is_format_thf (THF _) = true
| is_format_thf _ = false
-fun is_format_typed TFF = true
+fun is_format_typed (TFF _) = true
| is_format_typed (THF _) = true
| is_format_typed _ = false
@@ -232,7 +235,7 @@
aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2
|> not rhs ? enclose "(" ")"
in aux true ty end
- | string_for_type TFF ty =
+ | string_for_type (TFF _) ty =
(case strip_tff_type ty of
([], s) => s
| ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
@@ -320,7 +323,7 @@
fun string_for_format CNF = tptp_cnf
| string_for_format CNF_UEQ = tptp_cnf
| string_for_format FOF = tptp_fof
- | string_for_format TFF = tptp_tff
+ | string_for_format (TFF _) = tptp_tff
| string_for_format (THF _) = tptp_thf
fun string_for_problem_line format (Decl (ident, sym, ty)) =
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 26 08:56:29 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 26 10:38:29 2011 -0700
@@ -304,8 +304,10 @@
(* Vampire *)
+(* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on
+ SystemOnTPTP. *)
fun is_old_vampire_version () =
- string_ord (getenv "VAMPIRE_VERSION", "1.8") = LESS
+ string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
@@ -335,12 +337,12 @@
(* FUDGE *)
(if is_old_vampire_version () then
[(0.333, (false, (150, FOF, "poly_guards", sosN))),
- (0.334, (true, (50, FOF, "mono_guards?", no_sosN))),
- (0.333, (false, (500, FOF, "mono_tags?", sosN)))]
+ (0.333, (false, (500, FOF, "mono_tags?", sosN))),
+ (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
else
- [(0.333, (false, (150, TFF, "poly_guards", sosN))),
- (0.334, (true, (50, TFF, "simple", no_sosN))),
- (0.333, (false, (500, TFF, "simple", sosN)))])
+ [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))),
+ (0.333, (false, (500, TFF Implicit, "simple", sosN))),
+ (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -368,8 +370,8 @@
(* FUDGE *)
K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
(0.25, (false, (125, FOF, "mono_guards?", ""))),
- (0.125, (false, (62, TFF, "simple", ""))),
- (0.125, (false, (31, TFF, "simple", "")))]}
+ (0.125, (false, (62, TFF Implicit, "simple", ""))),
+ (0.125, (false, (31, TFF Implicit, "simple", "")))]}
val z3_tptp = (z3_tptpN, z3_tptp_config)
@@ -457,19 +459,21 @@
remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
(K (100, THF With_Choice, "simple_higher") (* FUDGE *))
val remote_vampire =
- remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *))
+ remotify_atp vampire "Vampire" ["1.8"]
+ (K (250, TFF Implicit, "simple") (* FUDGE *))
val remote_z3_tptp =
- remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *))
+ remotify_atp z3_tptp "Z3" ["3.0"]
+ (K (250, TFF Implicit, "simple") (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
- (K (100, TFF, "simple") (* FUDGE *))
+ (K (100, TFF Explicit, "simple") (* FUDGE *))
val remote_e_tofof =
remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
- Axiom Hypothesis (K (150, TFF, "simple") (* FUDGE *))
+ Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
[("#START OF PROOF", "Proved Goals:")]
--- a/src/HOL/Tools/ATP/atp_translate.ML Fri Aug 26 08:56:29 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Aug 26 10:38:29 2011 -0700
@@ -621,7 +621,7 @@
| is_type_level_monotonicity_based _ = false
fun adjust_type_enc (THF _) type_enc = type_enc
- | adjust_type_enc TFF (Simple_Types (_, level)) =
+ | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
Simple_Types (First_Order, level)
| adjust_type_enc format (Simple_Types (_, level)) =
adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
@@ -1020,7 +1020,7 @@
fun preprocess_abstractions_in_terms trans_lambdas facts =
let
val (facts, lambda_ts) =
- facts |> map (snd o snd) |> trans_lambdas
+ facts |> map (snd o snd) |> trans_lambdas
|>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
val lambda_facts =
map2 (fn t => fn j =>
@@ -1095,12 +1095,9 @@
val known_infinite_types =
[@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
-fun is_type_surely_infinite' ctxt soundness cached_Ts T =
- (* Unlike virtually any other polymorphic fact whose type variables can be
- instantiated by a known infinite type, extensionality actually encodes a
- cardinality constraints. *)
+fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
soundness <> Sound andalso
- is_type_surely_infinite ctxt (soundness = Unsound) cached_Ts T
+ is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
@@ -1114,7 +1111,7 @@
exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
not (exists (type_instance ctxt T) surely_infinite_Ts orelse
(not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
- is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
+ is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
| should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
maybe_nonmono_Ts, ...}
Fin_Nonmono_Types T =
@@ -1249,14 +1246,15 @@
end
in add true end
fun add_fact_syms_to_table ctxt explicit_apply =
- formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply))
- |> fact_lift
+ K (add_iterm_syms_to_table ctxt explicit_apply)
+ |> formula_fold NONE |> fact_lift
val tvar_a = TVar (("'a", 0), HOLogic.typeS)
val default_sym_tab_entries : (string * sym_info) list =
(prefixed_predicator_name,
- {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
+ {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
+ (* FIXME: needed? *) ::
(make_fixed_const NONE @{const_name undefined},
{pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
([tptp_false, tptp_true]
@@ -1674,8 +1672,7 @@
else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
let
val var = ATerm (name, [])
- val tagged_var =
- ATerm (type_tag, [ho_term_from_typ format type_enc T, var])
+ val tagged_var = var |> tag_with_type ctxt format mono type_enc pos T
in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
else
NONE
@@ -1792,7 +1789,7 @@
#> fold (add_iterm_syms in_conj) args
end
fun add_fact_syms in_conj =
- fact_lift (formula_fold NONE (K (add_iterm_syms in_conj)))
+ K (add_iterm_syms in_conj) |> formula_fold NONE |> fact_lift
fun add_formula_var_types (AQuant (_, xs, phi)) =
fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
#> add_formula_var_types phi
@@ -1844,8 +1841,8 @@
if exists (type_instance ctxt T) surely_infinite_Ts orelse
member (type_aconv ctxt) maybe_finite_Ts T then
mono
- else if is_type_surely_infinite' ctxt soundness surely_infinite_Ts
- T then
+ else if is_type_kind_of_surely_infinite ctxt soundness
+ surely_infinite_Ts T then
{maybe_finite_Ts = maybe_finite_Ts,
surely_finite_Ts = surely_finite_Ts,
maybe_infinite_Ts = maybe_infinite_Ts,
@@ -1888,6 +1885,22 @@
? fold (add_fact_mononotonicity_info ctxt level) facts
end
+fun add_iformula_monotonic_types ctxt mono type_enc =
+ let
+ val level = level_of_type_enc type_enc
+ val should_encode = should_encode_type ctxt mono level
+ fun add_type T = not (should_encode T) ? insert_type ctxt I T
+ fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
+ | add_args _ = I
+ and add_term tm = add_type (ityp_of tm) #> add_args tm
+ in formula_fold NONE (K add_term) end
+fun add_fact_monotonic_types ctxt mono type_enc =
+ add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
+fun monotonic_types_for_facts ctxt mono type_enc facts =
+ [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
+ is_type_level_monotonicity_based (level_of_type_enc type_enc))
+ ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
+
fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
Formula (guards_sym_formula_prefix ^
ascii_of (mangled_type format type_enc T),
@@ -2049,17 +2062,9 @@
end)
fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
- sym_decl_tab =
+ mono_Ts sym_decl_tab =
let
val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
- val mono_Ts =
- if polymorphism_of_type_enc type_enc = Polymorphic then
- syms |> maps (map result_type_of_decl o snd)
- |> filter_out (should_encode_type ctxt mono
- (level_of_type_enc type_enc))
- |> rpair [] |-> fold (insert_type ctxt I)
- else
- []
val mono_lines =
problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
val decl_lines =
@@ -2134,11 +2139,14 @@
val helpers =
repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
|> map repair
+ val mono_Ts =
+ helpers @ conjs @ facts
+ |> monotonic_types_for_facts ctxt mono type_enc
val sym_decl_lines =
(conjs, helpers @ facts)
|> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
|> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
- type_enc
+ type_enc mono_Ts
val helper_lines =
0 upto length helpers - 1 ~~ helpers
|> map (formula_line_for_fact ctxt format helper_prefix I false true mono
@@ -2168,7 +2176,7 @@
CNF => ensure_cnf_problem
| CNF_UEQ => filter_cnf_ueq_problem
| _ => I)
- |> (if is_format_typed format then
+ |> (if is_format_typed format andalso format <> TFF Implicit then
declare_undeclared_syms_in_atp_problem type_decl_prefix
implicit_declsN
else
--- a/src/HOL/Tools/ATP/atp_util.ML Fri Aug 26 08:56:29 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_util.ML Fri Aug 26 10:38:29 2011 -0700
@@ -161,16 +161,14 @@
0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
cardinality 2 or more. The specified default cardinality is returned if the
cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt inst_tvars assigns default_card T =
+fun tiny_card_of_type ctxt sound assigns default_card T =
let
val thy = Proof_Context.theory_of ctxt
val max = 2 (* 1 would be too small for the "fun" case *)
- val type_cmp =
- if inst_tvars then uncurry (type_generalization ctxt) else type_aconv ctxt
fun aux slack avoid T =
if member (op =) avoid T then
0
- else case AList.lookup type_cmp assigns T of
+ else case AList.lookup (type_aconv ctxt) assigns T of
SOME k => k
| NONE =>
case T of
@@ -218,13 +216,14 @@
(* Very slightly unsound: Type variables are assumed not to be
constrained to cardinality 1. (In practice, the user would most
likely have used "unit" directly anyway.) *)
- | TFree _ => if default_card = 1 then 2 else default_card
+ | TFree _ =>
+ if not sound andalso default_card = 1 then 2 else default_card
| TVar _ => default_card
in Int.min (max, aux false [] T) end
-fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt false [] 0 T <> 0
-fun is_type_surely_infinite ctxt inst_tvars infinite_Ts T =
- tiny_card_of_type ctxt inst_tvars (map (rpair 0) infinite_Ts) 1 T = 0
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt true [] 0 T <> 0
+fun is_type_surely_infinite ctxt sound infinite_Ts T =
+ tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0
(* Simple simplifications to ensure that sort annotations don't leave a trail of
spurious "True"s. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Aug 26 08:56:29 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Aug 26 10:38:29 2011 -0700
@@ -536,6 +536,11 @@
#> Config.put Monomorph.max_new_instances max_new_instances
#> Config.put Monomorph.keep_partial_instances false
+fun suffix_for_mode Auto_Try = "_auto_try"
+ | suffix_for_mode Try = "_try"
+ | suffix_for_mode Normal = ""
+ | suffix_for_mode Minimize = "_min"
+
(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
Linux appears to be the only ATP that does not honor its time limit. *)
val atp_timeout_slack = seconds 1.0
@@ -557,7 +562,7 @@
else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
val problem_file_name =
Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
- "_" ^ string_of_int subgoal)
+ suffix_for_mode mode ^ "_" ^ string_of_int subgoal)
val problem_path_name =
if dest_dir = "" then
File.tmp_path problem_file_name