# HG changeset patch # User wenzelm # Date 1332275851 -3600 # Node ID 8e1b14bf01905646f20c8dd47a677b33d2a4c3e9 # Parent 6f8dfe6c1aea4987c1f346ae6de6ba7108d6d848# Parent 34761733526c42c7b26ed1b11ebc06a9cca4f91f merged diff -r 34761733526c -r 8e1b14bf0190 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Tue Mar 20 21:34:42 2012 +0100 +++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Mar 20 21:37:31 2012 +0100 @@ -791,8 +791,9 @@ \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} -executable, or install the prebuilt E package from \download. Sledgehammer has -been tested with versions 1.0 to 1.4. +executable and \texttt{E\_VERSION} to the version number (e.g., ``1.4''), or +install the prebuilt E package from \download. Sledgehammer has been tested with +versions 1.0 to 1.4. \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, @@ -815,8 +816,9 @@ \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory -that contains the \texttt{SPASS} executable, or install the prebuilt SPASS -package from \download. Sledgehammer requires version 3.5 or above. +that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the +version number (e.g., ``3.7''), or install the prebuilt SPASS package from +\download. Sledgehammer requires version 3.5 or above. \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution prover developed by Andrei Voronkov and his colleagues diff -r 34761733526c -r 8e1b14bf0190 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Tue Mar 20 21:34:42 2012 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Mar 20 21:37:31 2012 +0100 @@ -117,14 +117,14 @@ fun run_some_atp ctxt format problem = let val thy = Proof_Context.theory_of ctxt - val prob_file = File.tmp_path (Path.explode "prob.tptp") + val prob_file = File.tmp_path (Path.explode "prob") val atp = case format of DFG _ => spass_newN | _ => eN val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp val ord = effective_term_order ctxt atp val _ = problem |> lines_for_atp_problem format ord (K []) |> File.write_list prob_file val command = - File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^ + File.shell_path (Path.explode (getenv (hd (fst exec)) ^ "/" ^ snd exec)) ^ " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^ File.shell_path prob_file in diff -r 34761733526c -r 8e1b14bf0190 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 20 21:34:42 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 20 21:37:31 2012 +0100 @@ -569,29 +569,27 @@ filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat val conjs = filt (formula (curry (op =) Conjecture)) |> separate [""] |> flat - (* The second layer of ")." is a temporary workaround for a quirk in SPASS's - parser. *) val settings = - (if is_lpo then ["set_flag(Ordering, 1).)."] else []) @ + (if is_lpo then ["set_flag(Ordering, 1)."] else []) @ (if gen_prec then [ord_info |> map fst |> rev |> commas |> maybe_enclose "set_precedence(" ")."] else []) - fun list_of _ _ _ [] = [] - | list_of heading bef aft ss = - "list_of_" ^ heading ^ ".\n" :: bef :: map (suffix "\n") ss @ - [aft, "end_of_list.\n\n"] + fun list_of _ [] = [] + | list_of heading ss = + "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @ + ["end_of_list.\n\n"] in "\nbegin_problem(isabelle).\n\n" :: - list_of "descriptions" "" "" + list_of "descriptions" ["name({**}).", "author({**}).", "status(unknown).", "description({**})."] @ - list_of "symbols" "" "" syms @ - list_of "declarations" "" "" decls @ - list_of "formulae(axioms)" "" "" axioms @ - list_of "formulae(conjectures)" "" "" conjs @ - list_of "settings(SPASS)" "{*\n" "*}\n" settings @ + list_of "symbols" syms @ + list_of "declarations" decls @ + list_of "formulae(axioms)" axioms @ + list_of "formulae(conjectures)" conjs @ + list_of "settings(SPASS)" settings @ ["end_problem.\n"] end diff -r 34761733526c -r 8e1b14bf0190 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 20 21:34:42 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 20 21:37:31 2012 +0100 @@ -14,8 +14,8 @@ type slice_spec = int * atp_format * string * string * bool type atp_config = - {exec : string * string, - required_execs : (string * string) list, + {exec : string list * string, + required_vars : string list list, arguments : Proof.context -> bool -> string -> Time.time -> term_order * (unit -> (string * int) list) @@ -51,12 +51,12 @@ val satallaxN : string val snarkN : string val spassN : string + val spass_oldN : string val spass_newN : string val vampireN : string val waldmeisterN : string val z3_tptpN : string val remote_prefix : string - val effective_term_order : Proof.context -> string -> term_order val remote_atp : string -> string -> string list -> (string * string) list -> (failure * string) list -> formula_kind -> formula_kind @@ -66,6 +66,7 @@ val supported_atps : theory -> string list val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit + val effective_term_order : Proof.context -> string -> term_order val setup : theory -> theory end; @@ -81,8 +82,8 @@ type slice_spec = int * atp_format * string * string * bool type atp_config = - {exec : string * string, - required_execs : (string * string) list, + {exec : string list * string, + required_vars : string list list, arguments : Proof.context -> bool -> string -> Time.time -> term_order * (unit -> (string * int) list) @@ -133,7 +134,7 @@ (* named ATPs *) val alt_ergoN = "alt_ergo" -val dummy_thfN = "dummy_thf" (* experimental *) +val dummy_thfN = "dummy_thf" (* for experiments *) val eN = "e" val e_sineN = "e_sine" val e_tofofN = "e_tofof" @@ -143,7 +144,8 @@ val satallaxN = "satallax" val snarkN = "snark" val spassN = "spass" -val spass_newN = "spass_new" (* experimental *) +val spass_oldN = "spass_old" (* for experiments *) +val spass_newN = "spass_new" (* for experiments *) val vampireN = "vampire" val waldmeisterN = "waldmeister" val z3_tptpN = "z3_tptp" @@ -178,30 +180,13 @@ val term_order = Attrib.setup_config_string @{binding atp_term_order} (K smartN) -fun effective_term_order ctxt atp = - let val ord = Config.get ctxt term_order in - if ord = smartN then - if atp = spass_newN then - {is_lpo = false, gen_weights = true, gen_prec = false, gen_simp = true} - else - {is_lpo = false, gen_weights = false, gen_prec = false, - gen_simp = false} - else - let val is_lpo = String.isSubstring lpoN ord in - {is_lpo = is_lpo, - gen_weights = not is_lpo andalso String.isSubstring xweightsN ord, - gen_prec = String.isSubstring xprecN ord, - gen_simp = String.isSubstring xsimpN ord} - end - end - (* Alt-Ergo *) val alt_ergo_tff1 = TFF (TPTP_Polymorphic, TPTP_Explicit) val alt_ergo_config : atp_config = - {exec = ("WHY3_HOME", "why3"), - required_execs = [], + {exec = (["WHY3_HOME"], "why3"), + required_vars = [], arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "--format tff1 --prover alt-ergo --timelimit " ^ @@ -222,7 +207,7 @@ (* E *) -fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.3") = LESS) +fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.2") = GREATER) val tstp_proof_delims = [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"), @@ -300,18 +285,18 @@ end fun effective_e_selection_heuristic ctxt = - if is_old_e_version () then e_autoN else Config.get ctxt e_selection_heuristic + if is_new_e_version () then Config.get ctxt e_selection_heuristic else e_autoN val e_config : atp_config = - {exec = ("E_HOME", "eproof"), - required_execs = [], + {exec = (["E_HOME"], "eproof"), + required_vars = [], arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => "--tstp-in --tstp-out --output-level=5 --silent " ^ e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^ e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^ - "--term-ordering=" ^ (if is_lpo then "LPO4" else "Auto") ^ " " ^ + "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout), proof_delims = tstp_proof_delims, known_failures = @@ -340,8 +325,8 @@ val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice) val leo2_config : atp_config = - {exec = ("LEO2_HOME", "leo"), - required_execs = [], + {exec = (["LEO2_HOME"], "leo"), + required_vars = [], arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) @@ -368,8 +353,8 @@ val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice) val satallax_config : atp_config = - {exec = ("SATALLAX_HOME", "satallax"), - required_execs = [], + {exec = (["SATALLAX_HOME"], "satallax"), + required_vars = [], arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "-p hocore -t " ^ string_of_int (to_secs 1 timeout), @@ -387,11 +372,15 @@ (* SPASS *) -(* The "-VarWeight=3" option helps the higher-order problems, probably by - counteracting the presence of explicit application operators. *) -val spass_config : atp_config = - {exec = ("ISABELLE_ATP", "scripts/spass"), - required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], +fun is_new_spass_version () = + string_ord (getenv "SPASS_VERSION", "3.7") = GREATER orelse + getenv "SPASS_NEW_HOME" <> "" + +(* TODO: Legacy: Remove after planned Isabelle2012 release (and don't forget + "required_vars" and "script/spass"). *) +val spass_old_config : atp_config = + {exec = (["ISABELLE_ATP"], "scripts/spass"), + required_vars = [["SPASS_OLD_HOME", "SPASS_HOME"]], arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) @@ -415,7 +404,7 @@ (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_old = (spass_oldN, spass_old_config) val spass_new_H2 = "-Heuristic=2" val spass_new_H2SOS = "-Heuristic=2 -SOS" @@ -423,17 +412,16 @@ val spass_new_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2" -(* Experimental *) val spass_new_config : atp_config = - {exec = ("SPASS_NEW_HOME", "SPASS"), - required_execs = [], + {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"), + required_vars = [], arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ => ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) |> extra_options <> "" ? prefix (extra_options ^ " "), - proof_delims = #proof_delims spass_config, - known_failures = #known_failures spass_config, - conj_sym_kind = #conj_sym_kind spass_config, - prem_kind = #prem_kind spass_config, + proof_delims = #proof_delims spass_old_config, + known_failures = #known_failures spass_old_config, + conj_sym_kind = #conj_sym_kind spass_old_config, + prem_kind = #prem_kind spass_old_config, best_slices = fn _ => (* FUDGE *) [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))), @@ -447,19 +435,22 @@ val spass_new = (spass_newN, spass_new_config) +fun spass () = + (spassN, if is_new_spass_version () then spass_new_config + else spass_old_config) (* 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") <> GREATER +fun is_new_vampire_version () = + string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit) val vampire_config : atp_config = - {exec = ("VAMPIRE_HOME", "vampire"), - required_execs = [], + {exec = (["VAMPIRE_HOME"], "vampire"), + required_vars = [], arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^ " --proof tptp --output_axiom_names on\ @@ -482,14 +473,14 @@ prem_kind = Conjecture, best_slices = fn ctxt => (* FUDGE *) - (if is_old_vampire_version () then + (if is_new_vampire_version () then + [(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))), + (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))), + (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))] + else [(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, false), sosN))), - (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))), - (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))]) + (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -501,8 +492,8 @@ val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit) val z3_tptp_config : atp_config = - {exec = ("Z3_HOME", "z3"), - required_execs = [], + {exec = (["Z3_HOME"], "z3"), + required_vars = [], arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout), proof_delims = [], @@ -522,8 +513,8 @@ (* Not really a prover: Experimental Polymorphic TFF and THF output *) fun dummy_config format type_enc : atp_config = - {exec = ("ISABELLE_ATP", "scripts/dummy_atp"), - required_execs = [], + {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"), + required_vars = [], arguments = K (K (K (K (K "")))), proof_delims = [], known_failures = known_szs_status_failures, @@ -581,8 +572,8 @@ fun remote_config system_name system_versions proof_delims known_failures conj_sym_kind prem_kind best_slice : atp_config = - {exec = ("ISABELLE_ATP", "scripts/remote_atp"), - required_execs = [], + {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, @@ -663,18 +654,37 @@ val supported_atps = Symtab.keys o Data.get fun is_atp_installed thy name = - let val {exec, required_execs, ...} = get_atp thy name in - forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) + let val {exec, required_vars, ...} = get_atp thy name in + forall (exists (fn var => getenv var <> "")) (fst exec :: required_vars) end fun refresh_systems_on_tptp () = Synchronized.change systems (fn _ => get_systems ()) -val atps = - [alt_ergo, e, leo2, dummy_thf, satallax, spass, spass_new, vampire, z3_tptp, - remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, - remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark, - remote_waldmeister] -val setup = fold add_atp atps +fun effective_term_order ctxt atp = + let val ord = Config.get ctxt term_order in + 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} + else + {is_lpo = false, gen_weights = false, gen_prec = false, + gen_simp = false} + else + let val is_lpo = String.isSubstring lpoN ord in + {is_lpo = is_lpo, + gen_weights = not is_lpo andalso String.isSubstring xweightsN ord, + gen_prec = String.isSubstring xprecN ord, + gen_simp = String.isSubstring xsimpN ord} + end + end + +fun atps () = + [alt_ergo, e, leo2, dummy_thf, satallax, spass_old, spass_new, spass (), + vampire, z3_tptp, remote_e, remote_e_sine, remote_e_tofof, remote_iprover, + remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, + remote_z3_tptp, remote_snark, remote_waldmeister] + +fun setup thy = fold add_atp (atps ()) thy end; diff -r 34761733526c -r 8e1b14bf0190 src/HOL/Tools/ATP/scripts/spass --- a/src/HOL/Tools/ATP/scripts/spass Tue Mar 20 21:34:42 2012 +0100 +++ b/src/HOL/Tools/ATP/scripts/spass Tue Mar 20 21:37:31 2012 +0100 @@ -7,12 +7,13 @@ options=${@:1:$(($#-1))} name=${@:$(($#)):1} +home=${SPASS_OLD_HOME:-$SPASS_HOME} -"$SPASS_HOME/SPASS" -Flotter "$name" \ +"$home/SPASS" -Flotter "$name" \ | sed 's/description({$/description({*/' \ | sed 's/set_ClauseFormulaRelation()\.//' \ > $name.cnf cat $name.cnf -"$SPASS_HOME/SPASS" $options "$name.cnf" \ +"$home/SPASS" $options "$name.cnf" \ | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/' rm -f "$name.cnf" diff -r 34761733526c -r 8e1b14bf0190 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 20 21:34:42 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 20 21:37:31 2012 +0100 @@ -215,8 +215,7 @@ (* 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, spass_newN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, - waldmeisterN] + [spassN, 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) diff -r 34761733526c -r 8e1b14bf0190 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Mar 20 21:34:42 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Mar 20 21:37:31 2012 +0100 @@ -580,7 +580,7 @@ val atp_timeout_slack = seconds 1.0 fun run_atp mode name - ({exec, required_execs, arguments, proof_delims, known_failures, + ({exec, required_vars, arguments, proof_delims, known_failures, conj_sym_kind, prem_kind, best_slices, ...} : atp_config) (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_relevant, max_mono_iters, @@ -605,7 +605,11 @@ Path.append (Path.explode dest_dir) problem_file_name else error ("No such directory: " ^ quote dest_dir ^ ".") - val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) + val command = + case find_first (fn var => getenv var <> "") (fst exec) of + SOME var => Path.explode (getenv var ^ "/" ^ snd exec) + | NONE => error ("The environment variable " ^ quote (hd (fst exec)) ^ + " is not set.") fun split_time s = let val split = String.tokens (fn c => str c = "\n") @@ -622,10 +626,12 @@ as_time t |> Time.fromMilliseconds) end fun run_on prob_file = - case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of - (home_var, _) :: _ => - error ("The environment variable " ^ quote home_var ^ " is not set.") - | [] => + case find_first (forall (fn var => getenv var = "")) + (fst exec :: required_vars) of + SOME home_vars => + error ("The environment variable " ^ quote (hd home_vars) ^ + " is not set.") + | NONE => if File.exists command then let (* If slicing is disabled, we expand the last slice to fill the diff -r 34761733526c -r 8e1b14bf0190 src/ZF/Cardinal_AC.thy --- a/src/ZF/Cardinal_AC.thy Tue Mar 20 21:34:42 2012 +0100 +++ b/src/ZF/Cardinal_AC.thy Tue Mar 20 21:37:31 2012 +0100 @@ -115,24 +115,30 @@ subsection{*Other Applications of AC*} -lemma surj_implies_inj: "f: surj(X,Y) ==> \g. g: inj(Y,X)" -apply (unfold surj_def) -apply (erule CollectE) -apply (rule_tac A1 = Y and B1 = "%y. f-``{y}" in AC_Pi [THEN exE]) -apply (fast elim!: apply_Pair) -apply (blast dest: apply_type Pi_memberD - intro: apply_equality Pi_type f_imp_injective) -done +lemma surj_implies_inj: + assumes f: "f \ surj(X,Y)" shows "\g. g \ inj(Y,X)" +proof - + from f AC_Pi [of Y "%y. f-``{y}"] + obtain z where z: "z \ (\ y\Y. f -`` {y})" + by (auto simp add: surj_def) (fast dest: apply_Pair) + show ?thesis + proof + show "z \ inj(Y, X)" using z surj_is_fun [OF f] + by (blast dest: apply_type Pi_memberD + intro: apply_equality Pi_type f_imp_injective) + qed +qed -(*Kunen's Lemma 10.20*) -lemma surj_implies_cardinal_le: "f: surj(X,Y) ==> |Y| \ |X|" -apply (rule lepoll_imp_Card_le) -apply (erule surj_implies_inj [THEN exE]) -apply (unfold lepoll_def) -apply (erule exI) -done +text{*Kunen's Lemma 10.20*} +lemma surj_implies_cardinal_le: + assumes f: "f \ surj(X,Y)" shows "|Y| \ |X|" +proof (rule lepoll_imp_Card_le) + from f [THEN surj_implies_inj] obtain g where "g \ inj(Y,X)" .. + thus "Y \ X" + by (auto simp add: lepoll_def) +qed -(*Kunen's Lemma 10.21*) +text{*Kunen's Lemma 10.21*} lemma cardinal_UN_le: assumes K: "InfCard(K)" shows "(!!i. i\K ==> |X(i)| \ K) ==> |\i\K. X(i)| \ K" @@ -141,7 +147,7 @@ assume "!!i. i\K ==> X(i) \ K" hence "!!i. i\K ==> \f. f \ inj(X(i), K)" by (simp add: lepoll_def) with AC_Pi obtain f where f: "f \ (\ i\K. inj(X(i), K))" - apply - apply atomize apply auto done + by force { fix z assume z: "z \ (\i\K. X(i))" then obtain i where i: "i \ K" "Ord(i)" "z \ X(i)" @@ -171,8 +177,8 @@ ==> |\i\K. X(i)| < csucc(K)" by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal) -(*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). *) +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); \i\K. j(i) < csucc(K) |] ==> (\i\K. j(i)) < csucc(K)" @@ -203,13 +209,12 @@ finally show "C(x) \ (\y\B. C(if y \ range(f) then converse(f)`y else a))" . qed -(*Simpler to require |W|=K; we'd have a bijection; but the theorem would - be weaker.*) +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| \ K; \w\W. j(w) < csucc(K) |] ==> (\w\W. j(w)) < csucc(K)" -apply (case_tac "W=0") -(*solve the easy 0 case*) +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)