# HG changeset patch # User haftmann # Date 1290696041 -3600 # Node ID fed0251b7939a1ad28508d8df0803bf4b3fda85c # Parent af30b887573365abb7b9ee85cc849582082a220a# Parent 03f1266a066e4c14567e018a756b38fb4a7ac07a merged diff -r 03f1266a066e -r fed0251b7939 src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Thu Nov 25 15:40:15 2010 +0100 +++ b/src/HOL/Library/Ramsey.thy Thu Nov 25 15:40:41 2010 +0100 @@ -8,6 +8,113 @@ imports Main Infinite_Set begin +subsection{* Finite Ramsey theorem(s) *} + +text{* To distinguish the finite and infinite ones, lower and upper case +names are used. + +This is the most basic version in terms of cliques and independent +sets, i.e. the version for graphs and 2 colours. *} + +definition "clique V E = (\v\V. \w\V. v\w \ {v,w} : E)" +definition "indep V E = (\v\V. \w\V. v\w \ \ {v,w} : E)" + +lemma ramsey2: + "\r\1. \ (V::'a set) (E::'a set set). finite V \ card V \ r \ + (\ R \ V. card R = m \ clique R E \ card R = n \ indep R E)" + (is "\r\1. ?R m n r") +proof(induct k == "m+n" arbitrary: m n) + case 0 + show ?case (is "EX r. ?R r") + proof + show "?R 1" using 0 + by (clarsimp simp: indep_def)(metis card.empty emptyE empty_subsetI) + qed +next + case (Suc k) + { assume "m=0" + have ?case (is "EX r. ?R r") + proof + show "?R 1" using `m=0` + by (simp add:clique_def)(metis card.empty emptyE empty_subsetI) + qed + } moreover + { assume "n=0" + have ?case (is "EX r. ?R r") + proof + show "?R 1" using `n=0` + by (simp add:indep_def)(metis card.empty emptyE empty_subsetI) + qed + } moreover + { assume "m\0" "n\0" + hence "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto + from Suc(1)[OF this(1)] Suc(1)[OF this(2)] + obtain r1 r2 where "r1\1" "r2\1" "?R (m - 1) n r1" "?R m (n - 1) r2" + by auto + hence "r1+r2 \ 1" by arith + moreover + have "?R m n (r1+r2)" (is "ALL V E. _ \ ?EX V E m n") + proof clarify + fix V :: "'a set" and E :: "'a set set" + assume "finite V" "r1+r2 \ card V" + with `r1\1` have "V \ {}" by auto + then obtain v where "v : V" by blast + let ?M = "{w : V. w\v & {v,w} : E}" + let ?N = "{w : V. w\v & {v,w} ~: E}" + have "V = insert v (?M \ ?N)" using `v : V` by auto + hence "card V = card(insert v (?M \ ?N))" by metis + also have "\ = card ?M + card ?N + 1" using `finite V` + by(fastsimp intro: card_Un_disjoint) + finally have "card V = card ?M + card ?N + 1" . + hence "r1+r2 \ card ?M + card ?N + 1" using `r1+r2 \ card V` by simp + hence "r1 \ card ?M \ r2 \ card ?N" by arith + moreover + { assume "r1 \ card ?M" + moreover have "finite ?M" using `finite V` by auto + ultimately have "?EX ?M E (m - 1) n" using `?R (m - 1) n r1` by blast + then obtain R where "R \ ?M" "v ~: R" and + CI: "card R = m - 1 \ clique R E \ + card R = n \ indep R E" (is "?C \ ?I") + by blast + have "R <= V" using `R <= ?M` by auto + have "finite R" using `finite V` `R \ V` by (metis finite_subset) + { assume "?I" + with `R <= V` have "?EX V E m n" by blast + } moreover + { assume "?C" + hence "clique (insert v R) E" using `R <= ?M` + by(auto simp:clique_def insert_commute) + moreover have "card(insert v R) = m" + using `?C` `finite R` `v ~: R` `m\0` by simp + ultimately have "?EX V E m n" using `R <= V` `v : V` by blast + } ultimately have "?EX V E m n" using CI by blast + } moreover + { assume "r2 \ card ?N" + moreover have "finite ?N" using `finite V` by auto + ultimately have "?EX ?N E m (n - 1)" using `?R m (n - 1) r2` by blast + then obtain R where "R \ ?N" "v ~: R" and + CI: "card R = m \ clique R E \ + card R = n - 1 \ indep R E" (is "?C \ ?I") + by blast + have "R <= V" using `R <= ?N` by auto + have "finite R" using `finite V` `R \ V` by (metis finite_subset) + { assume "?C" + with `R <= V` have "?EX V E m n" by blast + } moreover + { assume "?I" + hence "indep (insert v R) E" using `R <= ?N` + by(auto simp:indep_def insert_commute) + moreover have "card(insert v R) = n" + using `?I` `finite R` `v ~: R` `n\0` by simp + ultimately have "?EX V E m n" using `R <= V` `v : V` by blast + } ultimately have "?EX V E m n" using CI by blast + } ultimately show "?EX V E m n" by blast + qed + ultimately have ?case by blast + } ultimately show ?case by blast +qed + + subsection {* Preliminaries *} subsubsection {* ``Axiom'' of Dependent Choice *} diff -r 03f1266a066e -r fed0251b7939 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Nov 25 15:40:15 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Nov 25 15:40:41 2010 +0100 @@ -526,12 +526,10 @@ val (prover_name, _) = get_prover ctxt args val minimize = AList.defined (op =) args minimizeK val metis_ft = AList.defined (op =) args metis_ftK - val trivial = false -(* FIXME + val trivial = TimeLimit.timeLimit try_outer_timeout (Try.invoke_try (SOME try_inner_timeout)) pre handle TimeLimit.TimeOut => false -*) fun apply_reconstructor m1 m2 = if metis_ft then diff -r 03f1266a066e -r fed0251b7939 src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Thu Nov 25 15:40:15 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_translate.ML Thu Nov 25 15:40:41 2010 +0100 @@ -402,6 +402,9 @@ | NONE => transs h T ts)) | (h as Free (_, T), ts) => transs h T ts | (Bound i, []) => pair (SVar i) + | (Abs (_, _, t1 $ Bound 0), []) => + if not (loose_bvar1 (t1, 0)) then trans t1 (* eta-reduce on the fly *) + else raise TERM ("smt_translate", [t]) | _ => raise TERM ("smt_translate", [t])) and transs t T ts = diff -r 03f1266a066e -r fed0251b7939 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 25 15:40:15 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 25 15:40:41 2010 +0100 @@ -104,8 +104,9 @@ else is_atp_installed thy name end -val smt_default_max_relevant = 200 (* FUDGE *) -val auto_max_relevant_divisor = 2 (* FUDGE *) +(* FUDGE *) +val smt_default_max_relevant = 200 +val auto_max_relevant_divisor = 2 fun default_max_relevant_for_prover thy name = if is_smt_prover name then smt_default_max_relevant @@ -432,6 +433,7 @@ | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources | failure_from_smt_failure _ = UnknownError +(* FUDGE *) val smt_max_iter = 8 val smt_iter_fact_divisor = 2 val smt_iter_min_msecs = 5000 @@ -482,9 +484,9 @@ | SOME (SMT_Failure.Abnormal_Termination code) => (if verbose then "The SMT solver invoked with " ^ string_of_int num_facts ^ - " fact" ^ plural_s num_facts ^ " terminated abnormally with exit\ - \code " ^ string_of_int code ^ "." - |> (if debug then error else warning) + " fact" ^ plural_s num_facts ^ " terminated abnormally with \ + \exit code " ^ string_of_int code ^ "." + |> warning else (); true (* kind of *)) @@ -516,16 +518,16 @@ val smt_metis_timeout = seconds 0.5 -fun can_apply_metis state i ths = - can_apply smt_metis_timeout (fn ctxt => Metis_Tactics.metis_tac ctxt ths) - state i +fun can_apply_metis debug state i ths = + can_apply smt_metis_timeout + (Config.put Metis_Tactics.verbose debug + #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i fun run_smt_solver auto remote (params as {debug, ...}) minimize_command ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = let val repair_context = - Config.put Metis_Tactics.verbose debug - #> Config.put SMT_Config.verbose debug + Config.put SMT_Config.verbose debug #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit val state = state |> Proof.map_context repair_context val thy = Proof.theory_of state @@ -538,8 +540,10 @@ NONE => let val method = - if can_apply_metis state subgoal (map snd used_facts) then "metis" - else "smt" + if can_apply_metis debug state subgoal (map snd used_facts) then + "metis" + else + "smt" in try_command_line (proof_banner auto) (apply_on_subgoal subgoal subgoal_count ^