--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Mar 21 23:41:58 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Mar 21 23:41:22 2012 +0100
@@ -282,12 +282,12 @@
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\
+Sledgehammer: ``\textit{remote\_satallax\/}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
\postw
-Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
+Sledgehammer ran E, Satallax, SPASS, Vampire, Waldmeister, and Z3 in parallel.
Depending on which provers are installed and how many processor cores are
available, some of the provers might be missing or present with a
\textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
@@ -858,8 +858,8 @@
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
-developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
-E-SInE runs on Geoff Sutcliffe's Miami servers.
+developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff
+Sutcliffe's Miami servers.
\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
@@ -905,7 +905,7 @@
with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
+By default, Sledgehammer runs E, Satallax, SPASS, Vampire, Z3 (or whatever
the SMT module's \textit{smt\_solver} configuration option is set to), and (if
appropriate) Waldmeister in parallel---either locally or remotely, depending on
the number of processor cores available. For historical reasons, the default
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Mar 21 23:41:58 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Mar 21 23:41:22 2012 +0100
@@ -85,6 +85,7 @@
val extract_isabelle_status : (string, 'a) ho_term list -> string option
val extract_isabelle_rank : (string, 'a) ho_term list -> int
val introN : string
+ val spec_introN : string
val elimN : string
val simpN : string
val spec_eqN : string
@@ -217,6 +218,7 @@
val isabelle_info_prefix = "isabelle_"
val introN = "intro"
+val spec_introN = "spec_intro"
val elimN = "elim"
val simpN = "simp"
val spec_eqN = "spec_eq"
@@ -551,8 +553,8 @@
(if gen_weights then ord_info else [])
|> map spair |> commas |> maybe_enclose "weights [" "]."
val syms =
- [func_aries] @ (if sorted then [do_term_order_weights ()] else []) @
- [pred_aries] @ (if sorted then [sorts ()] else [])
+ [func_aries, pred_aries] @
+ (if sorted then [do_term_order_weights (), sorts ()] else [])
fun func_sigs () =
filt (fn Decl (_, sym, ty) =>
if is_function_type ty then SOME (fun_typ sym ty) else NONE
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Mar 21 23:41:58 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Mar 21 23:41:22 2012 +0100
@@ -16,7 +16,8 @@
type 'a problem = 'a ATP_Problem.problem
datatype scope = Global | Local | Assum | Chained
- datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
+ datatype status =
+ General | Induct | Intro | Spec_Intro | Elim | Simp | Spec_Eq
type stature = scope * status
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
@@ -547,7 +548,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 | Spec_Eq
+datatype status = General | Induct | Intro | Spec_Intro | Elim | Simp | Spec_Eq
type stature = scope * status
datatype order = First_Order | Higher_Order
@@ -1413,7 +1414,11 @@
{pred_sym = true, min_ary = 1, max_ary = 1, types = [],
in_conj = false})
-datatype app_op_level = Incomplete_Apply | Sufficient_Apply | Full_Apply
+datatype app_op_level =
+ Min_App_Op |
+ Sufficient_App_Op |
+ Sufficient_App_Op_And_Predicator |
+ Full_App_Op_And_Predicator
fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
let
@@ -1428,10 +1433,14 @@
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 app_op_level = Sufficient_Apply andalso
- (can dest_funT T orelse T = @{typ bool}) then
+ if (app_op_level = Sufficient_App_Op andalso can dest_funT T) orelse
+ (app_op_level = Sufficient_App_Op_And_Predicator andalso
+ (can dest_funT T orelse T = @{typ bool})) then
let
- val bool_vars' = bool_vars orelse body_type T = @{typ bool}
+ val bool_vars' =
+ bool_vars orelse
+ (app_op_level = Sufficient_App_Op_And_Predicator andalso
+ body_type T = @{typ bool})
fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
{pred_sym = pred_sym andalso not bool_vars',
min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
@@ -1468,8 +1477,9 @@
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
+ if (app_op_level = Sufficient_App_Op orelse
+ app_op_level = Sufficient_App_Op_And_Predicator)
+ andalso not (pointer_eq (types', types)) then
fold (consider_var_ary T) fun_var_Ts min_ary
else
min_ary
@@ -1496,10 +1506,9 @@
| NONE => ary
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
+ Min_App_Op => ary
+ | Full_App_Op_And_Predicator => 0
+ | _ => fold (consider_var_ary T) fun_var_Ts ary
in
Symtab.update_new (s,
{pred_sym = pred_sym, min_ary = min_ary,
@@ -1984,6 +1993,7 @@
let val rank = rank j in
case snd stature of
Intro => isabelle_info introN rank
+ | Spec_Intro => isabelle_info spec_introN rank
| Elim => isabelle_info elimN rank
| Simp => isabelle_info simpN rank
| Spec_Eq => isabelle_info spec_eqN rank
@@ -2000,7 +2010,7 @@
type_class_formula type_enc superclass ty_arg])
|> mk_aquant AForall
[(tvar_a_name, atype_of_type_vars type_enc)],
- NONE, isabelle_info introN helper_rank)
+ NONE, isabelle_info spec_introN helper_rank)
end
fun formula_from_arity_atom type_enc (class, t, args) =
@@ -2014,7 +2024,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 introN helper_rank)
+ NONE, isabelle_info spec_introN helper_rank)
fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
({name, kind, iformula, atomic_types, ...} : translated_formula) =
@@ -2223,7 +2233,7 @@
always_guard_var_in_formula (SOME true)
|> close_formula_universally
|> bound_tvars type_enc true (atomic_types_of T),
- NONE, isabelle_info introN helper_rank)
+ NONE, isabelle_info spec_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
@@ -2303,7 +2313,7 @@
|> close_formula_universally
|> bound_tvars type_enc (n > 1) (atomic_types_of T)
|> maybe_negate,
- NONE, isabelle_info introN helper_rank)
+ NONE, isabelle_info spec_introN helper_rank)
end
fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
@@ -2552,7 +2562,7 @@
|> List.partition is_poly_constr
|> pairself (map fst)
-val app_op_threshold = 50
+val app_op_and_predicator_threshold = 50
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
lam_trans uncurried_aliases readable_names preproc
@@ -2565,11 +2575,13 @@
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 >= app_op_threshold then
- Incomplete_Apply
+ if length facts > app_op_and_predicator_threshold then
+ if polymorphism_of_type_enc type_enc = Polymorphic then
+ Min_App_Op
+ else
+ Sufficient_App_Op
else
- Sufficient_Apply
+ Sufficient_App_Op_And_Predicator
val lam_trans =
if lam_trans = keep_lamsN andalso
not (is_type_enc_higher_order type_enc) then
@@ -2590,7 +2602,7 @@
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 sym_tab = sym_table_for_facts ctxt type_enc Min_App_Op conjs facts
val helpers =
sym_tab |> helper_facts_for_sym_table ctxt format type_enc
|> map (firstorderize true)
@@ -2693,14 +2705,34 @@
|> sort (prod_ord Real.compare string_ord o pairself swap)
end
-fun make_head_roll (ATerm (s, args)) =
- (* ugly hack: may make innocent victims (collateral damage) *)
- if String.isPrefix app_op_name s andalso length args = 2 then
- make_head_roll (hd args) ||> append (tl args)
- else
- (s, args)
+(* Ugly hack: may make innocent victims (collateral damage) *)
+fun may_be_app s args = String.isPrefix app_op_name s andalso length args = 2
+fun may_be_predicator s =
+ member (op =) [predicator_name, prefixed_predicator_name] s
+
+fun strip_predicator (tm as ATerm (s, [tm'])) =
+ if may_be_predicator s then tm' else tm
+ | strip_predicator tm = tm
+
+fun make_head_roll (ATerm (s, tms)) =
+ if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms)
+ else (s, tms)
| make_head_roll _ = ("", [])
+fun strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
+ | strip_up_to_predicator (AConn (_, phis)) = maps strip_up_to_predicator phis
+ | strip_up_to_predicator (AAtom tm) = [strip_predicator tm]
+
+fun strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
+ | strip_ahorn_etc (AConn (AImplies, [phi1, phi2])) =
+ strip_ahorn_etc phi2 |>> append (strip_up_to_predicator phi1)
+ | strip_ahorn_etc phi = ([], hd (strip_up_to_predicator phi))
+
+fun strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
+ | strip_iff_etc (AConn (AIff, [phi1, phi2])) =
+ pairself strip_up_to_predicator (phi1, phi2)
+ | strip_iff_etc _ = ([], [])
+
val max_term_order_weight = 2147483647
fun atp_problem_term_order_info problem =
@@ -2710,31 +2742,50 @@
#> Graph.default_node (s', ())
#> Graph.add_edge_acyclic (s, s')
fun add_term_deps head (ATerm (s, args)) =
- is_tptp_user_symbol s ? perhaps (try (add_edge s head))
- #> fold (add_term_deps head) args
+ if is_tptp_user_symbol head then
+ (if is_tptp_user_symbol s then perhaps (try (add_edge s head)) else I)
+ #> fold (add_term_deps head) args
+ else
+ I
| add_term_deps head (AAbs (_, tm)) = add_term_deps head tm
- fun add_eq_deps (SOME true) (ATerm (s, [lhs as _, rhs])) =
+ fun add_intro_deps pred (Formula (_, role, phi, _, info)) =
+ if pred (role, info) then
+ let val (hyps, concl) = strip_ahorn_etc phi in
+ case make_head_roll concl of
+ (head, args as _ :: _) => fold (add_term_deps head) (hyps @ args)
+ | _ => I
+ end
+ else
+ I
+ | add_intro_deps _ _ = I
+ fun add_atom_eq_deps (SOME true) (ATerm (s, [lhs as _, rhs])) =
if is_tptp_equal s then
case make_head_roll lhs of
- (head, rest as _ :: _) =>
- is_tptp_user_symbol head ? fold (add_term_deps head) (rhs :: rest)
+ (head, args as _ :: _) => fold (add_term_deps head) (rhs :: args)
| _ => I
else
I
- | add_eq_deps _ _ = I
- fun add_deps pred (Formula (_, role, phi, _, info)) =
+ | add_atom_eq_deps _ _ = I
+ fun add_eq_deps pred (Formula (_, role, phi, _, info)) =
if pred (role, info) then
- formula_fold (SOME (role <> Conjecture)) add_eq_deps phi
+ case strip_iff_etc phi of
+ ([lhs], rhs) =>
+ (case make_head_roll lhs of
+ (head, args as _ :: _) => fold (add_term_deps head) (rhs @ args)
+ | _ => I)
+ | _ => formula_fold (SOME (role <> Conjecture)) add_atom_eq_deps phi
else
I
- | add_deps _ _ = I
+ | add_eq_deps _ _ = I
fun has_status status (_, info) =
extract_isabelle_status info = SOME status
fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
val graph =
Graph.empty
- |> fold (fold (add_deps (has_status spec_eqN)) o snd) problem
- |> fold (fold (add_deps (has_status simpN orf is_conj)) o snd) problem
+ |> fold (fold (add_eq_deps (has_status spec_eqN)) o snd) problem
+ |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem
+ |> fold (fold (add_intro_deps (has_status spec_introN)) o snd) problem
+ |> fold (fold (add_intro_deps (has_status introN)) o snd) problem
fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
fun add_weights _ [] = I
| add_weights weight syms =
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Mar 21 23:41:58 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Mar 21 23:41:22 2012 +0100
@@ -60,7 +60,7 @@
val remote_atp :
string -> string -> string list -> (string * string) list
-> (failure * string) list -> formula_kind -> formula_kind
- -> (Proof.context -> slice_spec) -> string * atp_config
+ -> (Proof.context -> slice_spec * string) -> string * atp_config
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
@@ -169,7 +169,7 @@
val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
val smartN = "smart"
-val kboN = "kbo"
+(* val kboN = "kbo" *)
val lpoN = "lpo"
val xweightsN = "_weights"
val xprecN = "_prec"
@@ -574,14 +574,15 @@
conj_sym_kind prem_kind best_slice : atp_config =
{exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
required_vars = [],
- 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,
+ arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
+ (if command <> "" then "-c " ^ quote command ^ " " else "") ^
+ "-s " ^ the_system system_name system_versions ^ " " ^
+ "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
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 => [(1.0, (false, (best_slice ctxt, "")))]}
+ 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, ...}
@@ -602,44 +603,43 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
- (K (750, FOF, "mono_tags??", combsN, false) (* 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_native_higher", liftingN, false) (* FUDGE *))
+ (K ((100, leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
val remote_satallax =
- remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
- (K (100, satallax_thf0, "mono_native_higher", keep_lamsN, false)
- (* FUDGE *))
+ remotify_atp satallax "Satallax" ["2.3", "2.2", "2"]
+ (K ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["1.8"]
- (K (250, vampire_tff0, "mono_native", combs_or_liftingN, false) (* FUDGE *))
+ (K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
val remote_z3_tptp =
remotify_atp z3_tptp "Z3" ["3.0"]
- (K (250, z3_tff0, "mono_native", combsN, false) (* FUDGE *))
+ (K ((250, z3_tff0, "mono_native", 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, false) (* FUDGE *))
+ remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom Conjecture
+ (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
val remote_iprover =
remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
- (K (150, FOF, "mono_guards??", liftingN, false) (* 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, false) (* 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_native", liftingN, false) (* FUDGE *))
+ (K ((100, explicit_tff0, "mono_native", 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_native", liftingN, false) (* FUDGE *))
+ (K ((150, explicit_tff0, "mono_native", 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, false) (* FUDGE *))
+ (K ((50, CNF_UEQ, "mono_tags??", combsN, false), "") (* FUDGE *))
(* Setup *)
@@ -666,7 +666,7 @@
if ord = smartN then
if atp = spass_newN orelse
(atp = spassN andalso is_new_spass_version ()) then
- {is_lpo = false, gen_weights = true, gen_prec = false, gen_simp = true}
+ {is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false}
else
{is_lpo = false, gen_weights = false, gen_prec = false,
gen_simp = false}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Mar 21 23:41:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Mar 21 23:41:22 2012 +0100
@@ -128,31 +128,32 @@
fold (fn normalize => Termtab.update (normalize t, stature))
(I :: normalizers)
end)
-(*
- TODO: "intro" and "elim" rules are not exploited yet by SPASS (or any other
- prover). Reintroduce this code when it becomes useful. It costs about 50 ms
- per Sledgehammer invocation.
-
- val {safeIs, safeEs, hazIs, hazEs, ...} =
+ val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
ctxt |> claset_of |> Classical.rep_cs
val intros = Item_Net.content safeIs @ Item_Net.content hazIs
+(* Add once it is used:
val elims =
Item_Net.content safeEs @ Item_Net.content hazEs
|> map Classical.classical_rule
*)
val simps = ctxt |> simpset_of |> dest_ss |> #simps
+ val specs = ctxt |> Spec_Rules.get
val spec_eqs =
- ctxt |> Spec_Rules.get
- |> filter (curry (op =) Spec_Rules.Equational o fst)
- |> maps (snd o snd)
- |> filter_out (member Thm.eq_thm_prop risky_spec_eqs)
+ specs |> filter (curry (op =) Spec_Rules.Equational o fst)
+ |> maps (snd o snd)
+ |> filter_out (member Thm.eq_thm_prop risky_spec_eqs)
+ val spec_intros =
+ specs |> filter (member (op =) [Spec_Rules.Inductive,
+ Spec_Rules.Co_Inductive] o fst)
+ |> maps (snd o snd)
in
Termtab.empty |> add Simp [atomize] snd simps
|> add Spec_Eq [] I spec_eqs
-(*
+(* Add once it is used:
|> add Elim [] I elims
+*)
|> add Intro [] I intros
-*)
+ |> add Spec_Intro [] I spec_intros
end
fun needs_quoting reserved s =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 21 23:41:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 21 23:41:22 2012 +0100
@@ -215,7 +215,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, eN, vampireN, SMT_Solver.solver_name_of ctxt, satallaxN,
+ waldmeisterN]
|> map_filter (remotify_prover_if_not_installed ctxt)
|> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
max_default_remote_threads)
--- a/src/ZF/Cardinal_AC.thy Wed Mar 21 23:41:58 2012 +0100
+++ b/src/ZF/Cardinal_AC.thy Wed Mar 21 23:41:22 2012 +0100
@@ -173,14 +173,14 @@
text{*The same again, using @{term csucc}*}
lemma cardinal_UN_lt_csucc:
- "[| InfCard(K); \<forall>i\<in>K. |X(i)| < csucc(K) |]
+ "[| InfCard(K); \<And>i. i\<in>K \<Longrightarrow> |X(i)| < csucc(K) |]
==> |\<Union>i\<in>K. X(i)| < csucc(K)"
by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
text{*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i),
the least ordinal j such that i:Vfrom(A,j). *}
lemma cardinal_UN_Ord_lt_csucc:
- "[| InfCard(K); \<forall>i\<in>K. j(i) < csucc(K) |]
+ "[| InfCard(K); \<And>i. i\<in>K \<Longrightarrow> j(i) < csucc(K) |]
==> (\<Union>i\<in>K. j(i)) < csucc(K)"
apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
@@ -189,11 +189,11 @@
done
-(** Main result for infinite-branching datatypes. As above, but the index
- set need not be a cardinal. Surprisingly complicated proof!
-**)
+subsection{*The Main Result for Infinite-Branching Datatypes*}
-text{*Work backwards along the injection from @{term W} into @{term K}, given that @{term"W\<noteq>0"}.*}
+text{*As above, but the index set need not be a cardinal. Work
+backwards along the injection from @{term W} into @{term K}, given
+that @{term"W\<noteq>0"}.*}
lemma inj_UN_subset:
assumes f: "f \<in> inj(A,B)" and a: "a \<in> A"
@@ -209,20 +209,35 @@
finally show "C(x) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))" .
qed
-text{*Simpler to require |W|=K; we'd have a bijection; but the theorem would
- be weaker.*}
-lemma le_UN_Ord_lt_csucc:
- "[| InfCard(K); |W| \<le> K; \<forall>w\<in>W. j(w) < csucc(K) |]
- ==> (\<Union>w\<in>W. j(w)) < csucc(K)"
-apply (case_tac "W=0") --{*solve the easy 0 case*}
- apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc]
- Card_is_Ord Ord_0_lt_csucc)
-apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)
-apply (safe intro!: equalityI)
-apply (erule swap)
-apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+)
- apply (simp add: inj_converse_fun [THEN apply_type])
-apply (blast intro!: Ord_UN elim: ltE)
-done
+theorem le_UN_Ord_lt_csucc:
+ assumes IK: "InfCard(K)" and WK: "|W| \<le> K" and j: "\<And>w. w\<in>W \<Longrightarrow> j(w) < csucc(K)"
+ shows "(\<Union>w\<in>W. j(w)) < csucc(K)"
+proof -
+ have CK: "Card(K)"
+ by (simp add: InfCard_is_Card IK)
+ then obtain f where f: "f \<in> inj(W, K)" using WK
+ by(auto simp add: le_Card_iff lepoll_def)
+ have OU: "Ord(\<Union>w\<in>W. j(w))" using j
+ by (blast elim: ltE)
+ note lt_subset_trans [OF _ _ OU, trans]
+ show ?thesis
+ proof (cases "W=0")
+ case True --{*solve the easy 0 case*}
+ thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)
+ next
+ case False
+ then obtain x where x: "x \<in> W" by blast
+ have "(\<Union>x\<in>W. j(x)) \<subseteq> (\<Union>k\<in>K. j(if k \<in> range(f) then converse(f) ` k else x))"
+ by (rule inj_UN_subset [OF f x])
+ also have "... < csucc(K)" using IK
+ proof (rule cardinal_UN_Ord_lt_csucc)
+ fix k
+ assume "k \<in> K"
+ thus "j(if k \<in> range(f) then converse(f) ` k else x) < csucc(K)" using f x j
+ by (simp add: inj_converse_fun [THEN apply_type])
+ qed
+ finally show ?thesis .
+ qed
+qed
end
--- a/src/ZF/Constructible/AC_in_L.thy Wed Mar 21 23:41:58 2012 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy Wed Mar 21 23:41:22 2012 +0100
@@ -444,16 +444,16 @@
done
-text{*Locale for proving results under the assumption @{text "V=L"}*}
-locale V_equals_L =
- assumes VL: "L(x)"
-
-text{*The Axiom of Choice holds in @{term L}! Or, to be precise, the
-Wellordering Theorem.*}
-theorem (in V_equals_L) AC: "\<exists>r. well_ord(x,r)"
-apply (insert Transset_Lset VL [of x])
+text{*Every constructible set is well-ordered! Therefore the Wellordering Theorem and
+ the Axiom of Choice hold in @{term L}!!*}
+theorem L_implies_AC: assumes x: "L(x)" shows "\<exists>r. well_ord(x,r)"
+ using Transset_Lset x
apply (simp add: Transset_def L_def)
apply (blast dest!: well_ord_L_r intro: well_ord_subset)
done
+text{*In order to prove @{term" \<exists>r[L]. wellordered(L, A, r)"}, it's necessary to know
+that @{term r} is actually constructible. Of course, it follows from the assumption ``@{term V} equals @{term L''},
+but this reasoning doesn't appear to work in Isabelle.*}
+
end
--- a/src/ZF/Constructible/DPow_absolute.thy Wed Mar 21 23:41:58 2012 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy Wed Mar 21 23:41:22 2012 +0100
@@ -613,15 +613,14 @@
subsection{*The Notion of Constructible Set*}
-
definition
constructible :: "[i=>o,i] => o" where
"constructible(M,x) ==
\<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
theorem V_equals_L_in_L:
- "L(x) ==> constructible(L,x)"
-apply (simp add: constructible_def Lset_abs Lset_closed)
+ "L(x) \<longleftrightarrow> constructible(L,x)"
+apply (simp add: constructible_def Lset_abs Lset_closed)
apply (simp add: L_def)
apply (blast intro: Ord_in_L)
done
--- a/src/ZF/Constructible/Wellorderings.thy Wed Mar 21 23:41:58 2012 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy Wed Mar 21 23:41:22 2012 +0100
@@ -109,7 +109,7 @@
lemma (in M_basic) wellfounded_induct:
"[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));
\<forall>x. M(x) & (\<forall>y. <y,x> \<in> r \<longrightarrow> P(y)) \<longrightarrow> P(x) |]
- ==> P(a)";
+ ==> P(a)"
apply (simp (no_asm_use) add: wellfounded_def)
apply (drule_tac x="{z \<in> domain(r). ~P(z)}" in rspec)
apply (blast dest: transM)+
@@ -119,7 +119,7 @@
"[| a\<in>A; wellfounded_on(M,A,r); M(A);
separation(M, \<lambda>x. x\<in>A \<longrightarrow> ~P(x));
\<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r \<longrightarrow> P(y)) \<longrightarrow> P(x) |]
- ==> P(a)";
+ ==> P(a)"
apply (simp (no_asm_use) add: wellfounded_on_def)
apply (drule_tac x="{z\<in>A. z\<in>A \<longrightarrow> ~P(z)}" in rspec)
apply (blast intro: transM)+
@@ -153,6 +153,9 @@
by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def
linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized)
+text{*The property being well founded (and hence of being well ordered) is not absolute:
+the set that doesn't contain a minimal element may not exist in the class M.
+However, every set that is well founded in a transitive model M is well founded (page 124).*}
subsection{* Relativized versions of order-isomorphisms and order types *}
--- a/src/ZF/InfDatatype.thy Wed Mar 21 23:41:58 2012 +0100
+++ b/src/ZF/InfDatatype.thy Wed Mar 21 23:41:22 2012 +0100
@@ -11,21 +11,38 @@
Limit_VfromE [OF apply_funtype InfCard_csucc [THEN InfCard_is_Limit]]
lemma fun_Vcsucc_lemma:
- "[| f: D -> Vfrom(A,csucc(K)); |D| \<le> K; InfCard(K) |]
- ==> \<exists>j. f: D -> Vfrom(A,j) & j < csucc(K)"
-apply (rule_tac x = "\<Union>d\<in>D. LEAST i. f`d \<in> Vfrom (A,i) " in exI)
-apply (rule conjI)
-apply (rule_tac [2] le_UN_Ord_lt_csucc)
-apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all)
- prefer 2 apply (fast elim: Least_le [THEN lt_trans1] ltE)
-apply (rule Pi_type)
-apply (rename_tac [2] d)
-apply (erule_tac [2] fun_Limit_VfromE, simp_all)
-apply (subgoal_tac "f`d \<in> Vfrom (A, LEAST i. f`d \<in> Vfrom (A,i))")
- apply (erule Vfrom_mono [OF subset_refl UN_upper, THEN subsetD])
- apply assumption
-apply (fast elim: LeastI ltE)
-done
+ assumes f: "f \<in> D -> Vfrom(A,csucc(K))" and DK: "|D| \<le> K" and ICK: "InfCard(K)"
+ shows "\<exists>j. f \<in> D -> Vfrom(A,j) & j < csucc(K)"
+proof (rule exI, rule conjI)
+ show "f \<in> D \<rightarrow> Vfrom(A, \<Union>z\<in>D. \<mu> i. f`z \<in> Vfrom (A,i))"
+ proof (rule Pi_type [OF f])
+ fix d
+ assume d: "d \<in> D"
+ show "f ` d \<in> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))"
+ proof (rule fun_Limit_VfromE [OF f d ICK])
+ fix x
+ assume "x < csucc(K)" "f ` d \<in> Vfrom(A, x)"
+ hence "f`d \<in> Vfrom(A, \<mu> i. f`d \<in> Vfrom (A,i))" using d
+ by (fast elim: LeastI ltE)
+ also have "... \<subseteq> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))"
+ by (rule Vfrom_mono) (auto intro: d)
+ finally show "f`d \<in> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))" .
+ qed
+ qed
+next
+ show "(\<Union>d\<in>D. \<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
+ proof (rule le_UN_Ord_lt_csucc [OF ICK DK])
+ fix d
+ assume d: "d \<in> D"
+ show "(\<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
+ proof (rule fun_Limit_VfromE [OF f d ICK])
+ fix x
+ assume "x < csucc(K)" "f ` d \<in> Vfrom(A, x)"
+ thus "(\<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
+ by (blast intro: Least_le lt_trans1 lt_Ord)
+ qed
+ qed
+qed
lemma subset_Vcsucc:
"[| D \<subseteq> Vfrom(A,csucc(K)); |D| \<le> K; InfCard(K) |]