--- 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 = (\<forall>v\<in>V. \<forall>w\<in>V. v\<noteq>w \<longrightarrow> {v,w} : E)"
+definition "indep V E = (\<forall>v\<in>V. \<forall>w\<in>V. v\<noteq>w \<longrightarrow> \<not> {v,w} : E)"
+
+lemma ramsey2:
+ "\<exists>r\<ge>1. \<forall> (V::'a set) (E::'a set set). finite V \<and> card V \<ge> r \<longrightarrow>
+ (\<exists> R \<subseteq> V. card R = m \<and> clique R E \<or> card R = n \<and> indep R E)"
+ (is "\<exists>r\<ge>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\<noteq>0" "n\<noteq>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\<ge>1" "r2\<ge>1" "?R (m - 1) n r1" "?R m (n - 1) r2"
+ by auto
+ hence "r1+r2 \<ge> 1" by arith
+ moreover
+ have "?R m n (r1+r2)" (is "ALL V E. _ \<longrightarrow> ?EX V E m n")
+ proof clarify
+ fix V :: "'a set" and E :: "'a set set"
+ assume "finite V" "r1+r2 \<le> card V"
+ with `r1\<ge>1` have "V \<noteq> {}" by auto
+ then obtain v where "v : V" by blast
+ let ?M = "{w : V. w\<noteq>v & {v,w} : E}"
+ let ?N = "{w : V. w\<noteq>v & {v,w} ~: E}"
+ have "V = insert v (?M \<union> ?N)" using `v : V` by auto
+ hence "card V = card(insert v (?M \<union> ?N))" by metis
+ also have "\<dots> = 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 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
+ hence "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
+ moreover
+ { assume "r1 \<le> 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 \<subseteq> ?M" "v ~: R" and
+ CI: "card R = m - 1 \<and> clique R E \<or>
+ card R = n \<and> indep R E" (is "?C \<or> ?I")
+ by blast
+ have "R <= V" using `R <= ?M` by auto
+ have "finite R" using `finite V` `R \<subseteq> 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\<noteq>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 \<le> 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 \<subseteq> ?N" "v ~: R" and
+ CI: "card R = m \<and> clique R E \<or>
+ card R = n - 1 \<and> indep R E" (is "?C \<or> ?I")
+ by blast
+ have "R <= V" using `R <= ?N` by auto
+ have "finite R" using `finite V` `R \<subseteq> 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\<noteq>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 *}
--- 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
--- 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 =
--- 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 ^