--- a/CONTRIBUTORS Tue Feb 12 17:39:45 2013 +0100
+++ b/CONTRIBUTORS Wed Feb 13 11:46:48 2013 +0100
@@ -3,6 +3,9 @@
who is listed as an author in one of the source files of this Isabelle
distribution.
+Contributions to this Isabelle version
+--------------------------------------
+
Contributions to Isabelle2013
-----------------------------
--- a/NEWS Tue Feb 12 17:39:45 2013 +0100
+++ b/NEWS Wed Feb 13 11:46:48 2013 +0100
@@ -1,6 +1,16 @@
Isabelle NEWS -- history user-relevant changes
==============================================
+New in this Isabelle version
+----------------------------
+
+*** HOL ***
+
+* Theory "RealVector" and "Limits": Introduce type class
+(lin)order_topology. Allows to generalize theorems about limits and
+order. Instances are reals and extended reals.
+
+
New in Isabelle2013 (February 2013)
-----------------------------------
--- a/src/Doc/ProgProve/Logic.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy Wed Feb 13 11:46:48 2013 +0100
@@ -72,6 +72,7 @@
\end{warn}
\subsection{Sets}
+\label{sec:Sets}
Sets of elements of type @{typ 'a} have type @{typ"'a set"}.
They can be finite or infinite. Sets come with the usual notation:
--- a/src/Doc/Sledgehammer/document/root.tex Tue Feb 12 17:39:45 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Feb 13 11:46:48 2013 +0100
@@ -1063,10 +1063,11 @@
variable \texttt{MASH} to \texttt{yes}. Persistent data is stored in the
directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
-\item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh.
+\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
+rankings from MePo and MaSh.
-\item[\labelitemi] \textbf{\textit{smart}:} Use MeSh if MaSh is
-enabled and the target prover is an ATP; otherwise, use MePo.
+\item[\labelitemi] \textbf{\textit{smart}:} A mixture of MePo, MaSh, and MeSh if
+MaSh is enabled; otherwise, MePo.
\end{enum}
\opdefault{max\_facts}{smart\_int}{smart}
--- a/src/HOL/BNF/Examples/Stream.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/BNF/Examples/Stream.thy Wed Feb 13 11:46:48 2013 +0100
@@ -12,7 +12,7 @@
imports "../BNF"
begin
-codata 'a stream = Stream (shd: 'a) (stl: "'a stream")
+codata 'a stream = Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65)
(* TODO: Provide by the package*)
theorem stream_set_induct:
@@ -42,7 +42,7 @@
primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@-" 65) where
"shift [] s = s"
-| "shift (x # xs) s = Stream x (shift xs s)"
+| "shift (x # xs) s = x ## shift xs s"
lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s"
by (induct xs) auto
@@ -71,10 +71,10 @@
thus ?case using stream.unfold[of hd "\<lambda>xs. tl xs @ [hd xs]" u] by (auto simp: cycle_def)
qed auto
-lemma cycle_Cons: "cycle (x # xs) = Stream x (cycle (xs @ [x]))"
-proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = Stream x (cycle (xs @ [x]))"])
+lemma cycle_Cons: "cycle (x # xs) = x ## cycle (xs @ [x])"
+proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])"])
case (2 s1 s2)
- then obtain x xs where "s1 = cycle (x # xs) \<and> s2 = Stream x (cycle (xs @ [x]))" by blast
+ then obtain x xs where "s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])" by blast
thus ?case
by (auto simp: cycle_def intro!: exI[of _ "hd (xs @ [x])"] exI[of _ "tl (xs @ [x])"] stream.unfold)
qed auto
@@ -83,7 +83,7 @@
streams :: "'a set => 'a stream set"
for A :: "'a set"
where
- Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> Stream a s \<in> streams A"
+ Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @- s \<in> streams A"
by (induct w) auto
@@ -91,13 +91,13 @@
lemma stream_set_streams:
assumes "stream_set s \<subseteq> A"
shows "s \<in> streams A"
-proof (coinduct rule: streams.coinduct[of "\<lambda>s'. \<exists>a s. s' = Stream a s \<and> a \<in> A \<and> stream_set s \<subseteq> A"])
+proof (coinduct rule: streams.coinduct[of "\<lambda>s'. \<exists>a s. s' = a ## s \<and> a \<in> A \<and> stream_set s \<subseteq> A"])
case streams from assms show ?case by (cases s) auto
next
- fix s' assume "\<exists>a s. s' = Stream a s \<and> a \<in> A \<and> stream_set s \<subseteq> A"
+ fix s' assume "\<exists>a s. s' = a ## s \<and> a \<in> A \<and> stream_set s \<subseteq> A"
then guess a s by (elim exE)
- with assms show "\<exists>a l. s' = Stream a l \<and>
- a \<in> A \<and> ((\<exists>a s. l = Stream a s \<and> a \<in> A \<and> stream_set s \<subseteq> A) \<or> l \<in> streams A)"
+ with assms show "\<exists>a l. s' = a ## l \<and>
+ a \<in> A \<and> ((\<exists>a s. l = a ## s \<and> a \<in> A \<and> stream_set s \<subseteq> A) \<or> l \<in> streams A)"
by (cases s) auto
qed
@@ -105,17 +105,17 @@
subsection {* flatten a stream of lists *}
definition flat where
- "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else Stream (tl (shd s)) (stl s))"
+ "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else tl (shd s) ## stl s)"
lemma flat_simps[simp]:
"shd (flat ws) = hd (shd ws)"
- "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else Stream (tl (shd ws)) (stl ws))"
+ "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
unfolding flat_def by auto
-lemma flat_Cons[simp]: "flat (Stream (x#xs) w) = Stream x (flat (if xs = [] then w else Stream xs w))"
-unfolding flat_def using stream.unfold[of "hd o shd" _ "Stream (x#xs) w"] by auto
+lemma flat_Cons[simp]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)"
+unfolding flat_def using stream.unfold[of "hd o shd" _ "(x # xs) ## ws"] by auto
-lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (Stream xs ws) = xs @- flat ws"
+lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws"
by (induct xs) auto
lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)"
@@ -132,9 +132,9 @@
"sdrop 0 s = s"
| "sdrop (Suc n) s = sdrop n (stl s)"
-primrec snth :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a" where
- "snth 0 s = shd s"
-| "snth (Suc n) s = snth n (stl s)"
+primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+ "s !! 0 = shd s"
+| "s !! Suc n = stl s !! n"
lemma stake_sdrop: "stake n s @- sdrop n s = s"
by (induct n arbitrary: s) auto
--- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Wed Feb 13 11:46:48 2013 +0100
@@ -46,6 +46,27 @@
or implemented for RBT trees.
*)
-export_code _ checking SML OCaml? Haskell? Scala?
+export_code _ checking SML OCaml? Haskell?
+
+(* Extra setup to make Scala happy *)
+(* If the compilation fails with an error "ambiguous implicit values",
+ read \<section>7.1 in the Code Generation Manual *)
+
+class ccpo_linorder = ccpo + linorder
+
+lemma [code]:
+ "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P =
+ (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
+unfolding admissible_def by blast
+
+lemma [code]:
+ "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
+unfolding gfp_def by blast
+
+lemma [code]:
+ "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
+unfolding lfp_def by blast
+
+export_code _ checking Scala?
end
--- a/src/HOL/Complex.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Complex.thy Wed Feb 13 11:46:48 2013 +0100
@@ -288,8 +288,6 @@
instance proof
fix r :: real and x y :: complex and S :: "complex set"
- show "0 \<le> norm x"
- by (induct x) simp
show "(norm x = 0) = (x = 0)"
by (induct x) simp
show "norm (x + y) \<le> norm x + norm y"
--- a/src/HOL/HOL.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/HOL.thy Wed Feb 13 11:46:48 2013 +0100
@@ -1265,15 +1265,15 @@
val fx_g = Simplifier.rewrite ss (Thm.apply cf cx);
val (_ $ _ $ g) = prop_of fx_g;
val g' = abstract_over (x,g);
+ val abs_g'= Abs (n,xT,g');
in (if (g aconv g')
then
let
val rl =
cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
in SOME (rl OF [fx_g]) end
- else if Term.betapply (f, x) aconv g then NONE (*avoid identity conversion*)
+ else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') then NONE (*avoid identity conversion*)
else let
- val abs_g'= Abs (n,xT,g');
val g'x = abs_g'$x;
val g_g'x = Thm.symmetric (Thm.beta_conversion false (cterm_of thy g'x));
val rl = cterm_instantiate
--- a/src/HOL/IMP/AExp.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/AExp.thy Wed Feb 13 11:46:48 2013 +0100
@@ -32,7 +32,7 @@
syntax
"_State" :: "updbinds => 'a" ("<_>")
translations
- "_State ms" => "_Update <> ms"
+ "_State ms" == "_Update <> ms"
text {* \noindent
We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
--- a/src/HOL/IMP/Abs_Int0.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Wed Feb 13 11:46:48 2013 +0100
@@ -242,9 +242,8 @@
and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
fixes num' :: "val \<Rightarrow> 'av"
and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
- assumes gamma_num': "i : \<gamma>(num' i)"
- and gamma_plus':
- "i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma>(plus' a1 a2)"
+ assumes gamma_num': "i \<in> \<gamma>(num' i)"
+ and gamma_plus': "i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1+i2 \<in> \<gamma>(plus' a1 a2)"
type_synonym 'av st = "(vname \<Rightarrow> 'av)"
@@ -263,7 +262,8 @@
x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}" |
"step' S (C1; C2) = step' S C1; step' (post C1) C2" |
"step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
- IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2 {post C1 \<squnion> post C2}" |
+ IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2
+ {post C1 \<squnion> post C2}" |
"step' S ({I} WHILE b DO {P} C {Q}) =
{S \<squnion> post C} WHILE b DO {I} step' P C {I}"
@@ -290,8 +290,6 @@
lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
by (simp add: Top_option_def)
-(* FIXME (maybe also le \<rightarrow> sqle?) *)
-
lemma mono_gamma_s: "f1 \<sqsubseteq> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
--- a/src/HOL/IMP/Abs_Int1.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Wed Feb 13 11:46:48 2013 +0100
@@ -71,7 +71,7 @@
{S \<squnion> post C} WHILE b DO {I} step' P C {I}"
definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI c = pfp (step' (top c)) (bot c)"
+"AI c = pfp (step' (top(vars c))) (bot c)"
lemma strip_step'[simp]: "strip(step' S C) = strip C"
@@ -110,21 +110,21 @@
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
proof(simp add: CS_def AI_def)
- assume 1: "pfp (step' (top c)) (bot c) = Some C"
+ assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
have "C \<in> L(vars c)"
by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
(erule step'_in_L[OF _ top_in_L])
- have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
- have 2: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+ have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
+ have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
proof(rule order_trans)
- show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (top c) C)"
+ show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (top(vars c)) C)"
by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
- show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C"
+ show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
by(rule mono_gamma_c[OF pfp'])
qed
have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
- have "lfp c (step (\<gamma>\<^isub>o(top c))) \<le> \<gamma>\<^isub>c C"
- by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 2])
+ have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
+ by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
qed
@@ -153,8 +153,8 @@
split: option.split)
done
-lemma mono_step'_top: "C \<in> L(vars c) \<Longrightarrow> C' \<in> L(vars c) \<Longrightarrow>
- C \<sqsubseteq> C' \<Longrightarrow> step' (top c) C \<sqsubseteq> step' (top c) C'"
+lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow>
+ C \<sqsubseteq> C' \<Longrightarrow> step' (top X) C \<sqsubseteq> step' (top X) C'"
by (metis top_in_L mono_step' preord_class.le_refl)
lemma pfp_bot_least:
@@ -167,7 +167,7 @@
by (simp_all add: assms(4,5) bot_least)
lemma AI_least_pfp: assumes "AI c = Some C"
-and "step' (top c) C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)"
+and "step' (top(vars c)) C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)"
shows "C \<sqsubseteq> C'"
apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
by (simp_all add: mono_step'_top)
--- a/src/HOL/IMP/Abs_Int1_const.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Feb 13 11:46:48 2013 +0100
@@ -74,23 +74,23 @@
subsubsection "Tests"
-definition "steps c i = (step_const(top c) ^^ i) (bot c)"
+definition "steps c i = (step_const(top(vars c)) ^^ i) (bot c)"
value "show_acom (steps test1_const 0)"
value "show_acom (steps test1_const 1)"
value "show_acom (steps test1_const 2)"
value "show_acom (steps test1_const 3)"
-value "show_acom_opt (AI_const test1_const)"
+value "show_acom (the(AI_const test1_const))"
-value "show_acom_opt (AI_const test2_const)"
-value "show_acom_opt (AI_const test3_const)"
+value "show_acom (the(AI_const test2_const))"
+value "show_acom (the(AI_const test3_const))"
value "show_acom (steps test4_const 0)"
value "show_acom (steps test4_const 1)"
value "show_acom (steps test4_const 2)"
value "show_acom (steps test4_const 3)"
value "show_acom (steps test4_const 4)"
-value "show_acom_opt (AI_const test4_const)"
+value "show_acom (the(AI_const test4_const))"
value "show_acom (steps test5_const 0)"
value "show_acom (steps test5_const 1)"
@@ -99,7 +99,7 @@
value "show_acom (steps test5_const 4)"
value "show_acom (steps test5_const 5)"
value "show_acom (steps test5_const 6)"
-value "show_acom_opt (AI_const test5_const)"
+value "show_acom (the(AI_const test5_const))"
value "show_acom (steps test6_const 0)"
value "show_acom (steps test6_const 1)"
@@ -115,7 +115,7 @@
value "show_acom (steps test6_const 11)"
value "show_acom (steps test6_const 12)"
value "show_acom (steps test6_const 13)"
-value "show_acom_opt (AI_const test6_const)"
+value "show_acom (the(AI_const test6_const))"
text{* Monotonicity: *}
--- a/src/HOL/IMP/Abs_Int1_parity.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Wed Feb 13 11:46:48 2013 +0100
@@ -121,13 +121,13 @@
definition "test1_parity =
''x'' ::= N 1;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
-value [code] "show_acom_opt (AI_parity test1_parity)"
+value [code] "show_acom (the(AI_parity test1_parity))"
definition "test2_parity =
''x'' ::= N 1;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
-definition "steps c i = (step_parity(top c) ^^ i) (bot c)"
+definition "steps c i = (step_parity(top(vars c)) ^^ i) (bot c)"
value "show_acom (steps test2_parity 0)"
value "show_acom (steps test2_parity 1)"
@@ -136,7 +136,7 @@
value "show_acom (steps test2_parity 4)"
value "show_acom (steps test2_parity 5)"
value "show_acom (steps test2_parity 6)"
-value "show_acom_opt (AI_parity test2_parity)"
+value "show_acom (the(AI_parity test2_parity))"
subsubsection "Termination"
--- a/src/HOL/IMP/Abs_Int2.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy Wed Feb 13 11:46:48 2013 +0100
@@ -105,8 +105,8 @@
(if res then bfilter b1 True (bfilter b2 True S)
else bfilter b1 False S \<squnion> bfilter b2 False S)" |
"bfilter (Less e1 e2) res S =
- (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
- in afilter e1 res1 (afilter e2 res2 S))"
+ (let (a1,a2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
+ in afilter e1 a1 (afilter e2 a2 S))"
lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
by(induction e arbitrary: a S)
@@ -167,7 +167,7 @@
{bfilter b False I}"
definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI c = pfp (step' \<top>\<^bsub>c\<^esub>) (bot c)"
+"AI c = pfp (step' \<top>\<^bsub>vars c\<^esub>) (bot c)"
lemma strip_step'[simp]: "strip(step' S c) = strip c"
by(induct c arbitrary: S) (simp_all add: Let_def)
@@ -209,21 +209,21 @@
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
proof(simp add: CS_def AI_def)
- assume 1: "pfp (step' (top c)) (bot c) = Some C"
+ assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
have "C \<in> L(vars c)"
by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
(erule step'_in_L[OF _ top_in_L])
- have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
- have 2: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+ have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
+ have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
proof(rule order_trans)
- show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (top c) C)"
+ show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (top(vars c)) C)"
by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
- show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C"
+ show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
by(rule mono_gamma_c[OF pfp'])
qed
have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
- have "lfp c (step (\<gamma>\<^isub>o(top c))) \<le> \<gamma>\<^isub>c C"
- by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 2])
+ have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
+ by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
qed
@@ -281,8 +281,8 @@
split: option.split)
done
-lemma mono_step'_top: "C1 \<in> L(vars c) \<Longrightarrow> C2 \<in> L(vars c) \<Longrightarrow>
- C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top c) C1 \<sqsubseteq> step' (top c) C2"
+lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
+ C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top X) C1 \<sqsubseteq> step' (top X) C2"
by (metis top_in_L mono_step' preord_class.le_refl)
end
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Wed Feb 13 11:46:48 2013 +0100
@@ -255,7 +255,7 @@
value "show_acom_opt (AI_ivl test4_const)"
value "show_acom_opt (AI_ivl test6_const)"
-definition "steps c i = (step_ivl(top c) ^^ i) (bot c)"
+definition "steps c i = (step_ivl(top(vars c)) ^^ i) (bot c)"
value "show_acom_opt (AI_ivl test2_ivl)"
value "show_acom (steps test2_ivl 0)"
--- a/src/HOL/IMP/Abs_Int3.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy Wed Feb 13 11:46:48 2013 +0100
@@ -358,24 +358,24 @@
begin
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
-"AI_wn c = pfp_wn (step' (top c)) (bot c)"
+"AI_wn c = pfp_wn (step' (top(vars c))) (bot c)"
lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
proof(simp add: CS_def AI_wn_def)
- assume 1: "pfp_wn (step' (top c)) (bot c) = Some C"
- have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>c\<^esub> C \<sqsubseteq> C"
+ assume 1: "pfp_wn (step' (top(vars c))) (bot c) = Some C"
+ have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<sqsubseteq> C"
by(rule pfp_wn_pfp[where x="bot c"])
(simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
- have pfp: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+ have pfp: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
proof(rule order_trans)
- show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (top c) C)"
+ show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (top(vars c)) C)"
by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] top_in_L])
show "... \<le> \<gamma>\<^isub>c C"
by(rule mono_gamma_c[OF conjunct2[OF 2]])
qed
have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
- have "lfp c (step (\<gamma>\<^isub>o (top c))) \<le> \<gamma>\<^isub>c C"
- by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 pfp])
+ have "lfp c (step (\<gamma>\<^isub>o (top(vars c)))) \<le> \<gamma>\<^isub>c C"
+ by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 pfp])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
qed
@@ -396,9 +396,9 @@
by(rule refl)
definition "step_up_ivl n =
- ((\<lambda>C. C \<nabla> step_ivl (top(strip C)) C)^^n)"
+ ((\<lambda>C. C \<nabla> step_ivl (top(vars(strip C))) C)^^n)"
definition "step_down_ivl n =
- ((\<lambda>C. C \<triangle> step_ivl (top (strip C)) C)^^n)"
+ ((\<lambda>C. C \<triangle> step_ivl (top(vars(strip C))) C)^^n)"
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
the loop took to execute. In contrast, @{const AI_ivl'} converges in a
@@ -629,14 +629,14 @@
lemma iter_winden_step_ivl_termination:
- "\<exists>C. iter_widen (step_ivl (top c)) (bot c) = Some C"
+ "\<exists>C. iter_widen (step_ivl (top(vars c))) (bot c) = Some C"
apply(rule iter_widen_termination[where m = "m_c" and P = "%C. C \<in> Lc c"])
apply (simp_all add: step'_in_Lc m_c_widen)
done
lemma iter_narrow_step_ivl_termination:
- "C0 \<in> Lc c \<Longrightarrow> step_ivl (top c) C0 \<sqsubseteq> C0 \<Longrightarrow>
- \<exists>C. iter_narrow (step_ivl (top c)) C0 = Some C"
+ "C0 \<in> Lc c \<Longrightarrow> step_ivl (top(vars c)) C0 \<sqsubseteq> C0 \<Longrightarrow>
+ \<exists>C. iter_narrow (step_ivl (top(vars c))) C0 = Some C"
apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. C \<in> Lc c"])
apply (simp add: step'_in_Lc)
apply (simp)
@@ -654,7 +654,7 @@
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination
split: option.split)
apply(rule iter_narrow_step_ivl_termination)
-apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>c\<^esub>" and P = "%C. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>c\<^esub>" and c=c, simplified])
+apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>vars c\<^esub>" and P = "%C. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>vars c\<^esub>" and c=c, simplified])
apply(erule iter_widen_pfp)
done
--- a/src/HOL/IMP/Abs_State.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Abs_State.thy Wed Feb 13 11:46:48 2013 +0100
@@ -60,12 +60,12 @@
end
class semilatticeL = join + L +
-fixes top :: "com \<Rightarrow> 'a"
+fixes top :: "vname set \<Rightarrow> 'a"
assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<sqsubseteq> x \<squnion> y"
and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<sqsubseteq> x \<squnion> y"
and join_least[simp]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
-and top[simp]: "x \<in> L(vars c) \<Longrightarrow> x \<sqsubseteq> top c"
-and top_in_L[simp]: "top c \<in> L(vars c)"
+and top[simp]: "x \<in> L X \<Longrightarrow> x \<sqsubseteq> top X"
+and top_in_L[simp]: "top X \<in> L X"
and join_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
notation (input) top ("\<top>\<^bsub>_\<^esub>")
@@ -158,7 +158,7 @@
instantiation st :: (semilattice) semilatticeL
begin
-definition top_st where "top c = FunDom (\<lambda>x. \<top>) (vars c)"
+definition top_st where "top X = FunDom (\<lambda>x. \<top>) X"
instance
proof
@@ -201,8 +201,6 @@
lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"
by (simp add: top_option_def)
-(* FIXME (maybe also le \<rightarrow> sqle?) *)
-
lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)
by (metis mono_gamma subsetD)
--- a/src/HOL/IMP/Collecting.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Collecting.thy Wed Feb 13 11:46:48 2013 +0100
@@ -142,14 +142,14 @@
subsubsection "Collecting semantics"
fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
-"step S (SKIP {P}) = (SKIP {S})" |
-"step S (x ::= e {P}) =
+"step S (SKIP {Q}) = (SKIP {S})" |
+"step S (x ::= e {Q}) =
x ::= e {{s(x := aval e s) |s. s : S}}" |
"step S (C1; C2) = step S C1; step (post C1) C2" |
-"step S (IF b THEN {P1} C1 ELSE {P2} C2 {P}) =
+"step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
IF b THEN {{s:S. bval b s}} step P1 C1 ELSE {{s:S. \<not> bval b s}} step P2 C2
{post C1 \<union> post C2}" |
-"step S ({I} WHILE b DO {P} C {P'}) =
+"step S ({I} WHILE b DO {P} C {Q}) =
{S \<union> post C} WHILE b DO {{s:I. bval b s}} step P C {{s:I. \<not> bval b s}}"
definition CS :: "com \<Rightarrow> state set acom" where
--- a/src/HOL/IMP/Collecting_Examples.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Collecting_Examples.thy Wed Feb 13 11:46:48 2013 +0100
@@ -7,13 +7,20 @@
lemma insert_code [code]: "insert x (set xs) = set (x#xs)"
by simp
+text{* In order to display commands annotated with state sets,
+states must be translated into a printable format as lists of pairs,
+for a given set of variable names. This is what @{text show_acom} does: *}
+
+definition show_acom ::
+ "vname list \<Rightarrow> state set acom \<Rightarrow> (vname*val)list set acom" where
+"show_acom xs = map_acom (\<lambda>S. (\<lambda>s. map (\<lambda>x. (x, s x)) xs) ` S)"
+
+
text{* The example: *}
definition "c = WHILE Less (V ''x'') (N 3)
DO ''x'' ::= Plus (V ''x'') (N 2)"
definition C0 :: "state set acom" where "C0 = anno {} c"
-definition "show_acom xs = map_acom (\<lambda>S. (\<lambda>s. [(x,s x). x \<leftarrow> xs]) ` S)"
-
text{* Collecting semantics: *}
value "show_acom [''x''] (((step {<>}) ^^ 1) C0)"
--- a/src/HOL/IMP/Procs.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Procs.thy Wed Feb 13 11:46:48 2013 +0100
@@ -18,12 +18,11 @@
definition "test_com =
{VAR ''x'';;
- ''x'' ::= N 0;
- {PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');;
+ {PROC ''p'' = ''x'' ::= N 1;;
{PROC ''q'' = CALL ''p'';;
{VAR ''x'';;
- ''x'' ::= N 5;
- {PROC ''p'' = ''x'' ::= Plus (V ''x'') (N 1);;
+ ''x'' ::= N 2;
+ {PROC ''p'' = ''x'' ::= N 3;;
CALL ''q''; ''y'' ::= V ''x''}}}}}"
end
--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Wed Feb 13 11:46:48 2013 +0100
@@ -31,9 +31,6 @@
code_pred big_step .
-values "{map t [''x'',''y'',''z''] |t.
- (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
-
-values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
+values "{map t [''x'',''y''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
end
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Wed Feb 13 11:46:48 2013 +0100
@@ -33,9 +33,6 @@
code_pred big_step .
-values "{map t [''x'', ''y'', ''z''] |t.
- [] \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
-
-values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
+values "{map t [''x'', ''y''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
end
--- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Wed Feb 13 11:46:48 2013 +0100
@@ -32,7 +32,7 @@
e \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
Var: "(pe,ve(x:=f),f+1) \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow>
- (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(f := s f)" |
+ (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t" |
Call1: "((p,c,ve)#pe,ve,f) \<turnstile> (c, s) \<Rightarrow> t \<Longrightarrow>
((p,c,ve)#pe,ve',f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
@@ -45,10 +45,8 @@
code_pred big_step .
-values "{map t [0,1] |t. ([], <>, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
-
-values "{map t [0, 1, 2] |t.
- ([], <''x'' := 0, ''y'' := 1,''z'' := 2>, 0)
+values "{map t [10,11] |t.
+ ([], <''x'' := 10, ''y'' := 11>, 12)
\<turnstile> (test_com, <>) \<Rightarrow> t}"
end
--- a/src/HOL/Library/Extended_Nat.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Wed Feb 13 11:46:48 2013 +0100
@@ -6,7 +6,7 @@
header {* Extended natural numbers (i.e. with infinity) *}
theory Extended_Nat
-imports Main
+imports "~~/src/HOL/Main"
begin
class infinity =
--- a/src/HOL/Library/Extended_Real.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy Wed Feb 13 11:46:48 2013 +0100
@@ -8,7 +8,7 @@
header {* Extended real number line *}
theory Extended_Real
-imports Complex_Main Extended_Nat
+imports "~~/src/HOL/Complex_Main" Extended_Nat
begin
text {*
@@ -18,6 +18,69 @@
*}
+lemma LIMSEQ_SUP:
+ fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
+ assumes "incseq X"
+ shows "X ----> (SUP i. X i)"
+ using `incseq X`
+ by (intro increasing_tendsto)
+ (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
+
+lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
+ by (cases P) (simp_all add: eventually_False)
+
+lemma (in complete_lattice) Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
+ by (metis Sup_upper2 Inf_lower ex_in_conv)
+
+lemma (in complete_lattice) INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
+ unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
+
+lemma (in complete_linorder) le_Sup_iff:
+ "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
+proof safe
+ fix y assume "x \<le> Sup A" "y < x"
+ then have "y < Sup A" by auto
+ then show "\<exists>a\<in>A. y < a"
+ unfolding less_Sup_iff .
+qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] Sup_upper)
+
+lemma (in complete_linorder) le_SUP_iff:
+ "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
+ unfolding le_Sup_iff SUP_def by simp
+
+lemma (in complete_linorder) Inf_le_iff:
+ "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
+proof safe
+ fix y assume "x \<ge> Inf A" "y > x"
+ then have "y > Inf A" by auto
+ then show "\<exists>a\<in>A. y > a"
+ unfolding Inf_less_iff .
+qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] Inf_lower)
+
+lemma (in complete_linorder) le_INF_iff:
+ "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
+ unfolding Inf_le_iff INF_def by simp
+
+lemma (in complete_lattice) Sup_eqI:
+ assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
+ assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
+ shows "Sup A = x"
+ by (metis antisym Sup_least Sup_upper assms)
+
+lemma (in complete_lattice) Inf_eqI:
+ assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
+ assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
+ shows "Inf A = x"
+ by (metis antisym Inf_greatest Inf_lower assms)
+
+lemma (in complete_lattice) SUP_eqI:
+ "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (SUP i:A. f i) = x"
+ unfolding SUP_def by (rule Sup_eqI) auto
+
+lemma (in complete_lattice) INF_eqI:
+ "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (INF i:A. f i) = x"
+ unfolding INF_def by (rule Inf_eqI) auto
+
lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
proof
assume "{x..} = UNIV"
@@ -1353,22 +1416,6 @@
unfolding Sup_ereal_def
by (auto intro!: Least_equality)
-lemma ereal_SUPI:
- fixes x :: ereal
- assumes "!!i. i : A ==> f i <= x"
- assumes "!!y. (!!i. i : A ==> f i <= y) ==> x <= y"
- shows "(SUP i:A. f i) = x"
- unfolding SUP_def Sup_ereal_def
- using assms by (auto intro!: Least_equality)
-
-lemma ereal_INFI:
- fixes x :: ereal
- assumes "!!i. i : A ==> f i >= x"
- assumes "!!y. (!!i. i : A ==> f i >= y) ==> x >= y"
- shows "(INF i:A. f i) = x"
- unfolding INF_def Inf_ereal_def
- using assms by (auto intro!: Greatest_equality)
-
lemma Sup_ereal_close:
fixes e :: ereal
assumes "0 < e" and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}"
@@ -1402,8 +1449,7 @@
lemma ereal_le_Sup:
fixes x :: ereal
- shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))"
-(is "?lhs <-> ?rhs")
+ shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))" (is "?lhs = ?rhs")
proof-
{ assume "?rhs"
{ assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
@@ -1476,6 +1522,17 @@
using assms by (metis SUP_least SUP_upper2)
qed
+lemma INFI_eq:
+ assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<ge> g j"
+ assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<ge> f i"
+ shows "(INF i:A. f i) = (INF j:B. g j)"
+proof (intro antisym)
+ show "(INF i:A. f i) \<le> (INF j:B. g j)"
+ using assms by (metis INF_greatest INF_lower2)
+ show "(INF i:B. g i) \<le> (INF j:A. f j)"
+ using assms by (metis INF_greatest INF_lower2)
+qed
+
lemma SUP_ereal_le_addI:
fixes f :: "'i \<Rightarrow> ereal"
assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
@@ -1491,7 +1548,7 @@
fixes f g :: "nat \<Rightarrow> ereal"
assumes "incseq f" "incseq g" and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
-proof (rule ereal_SUPI)
+proof (rule SUP_eqI)
fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
have f: "SUPR UNIV f \<noteq> -\<infinity>" using pos
unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD)
@@ -1531,7 +1588,7 @@
lemma SUPR_ereal_cmult:
fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" "0 \<le> c"
shows "(SUP i. c * f i) = c * SUPR UNIV f"
-proof (rule ereal_SUPI)
+proof (rule SUP_eqI)
fix i have "f i \<le> SUPR UNIV f" by (rule SUP_upper) auto
then show "c * f i \<le> c * SUPR UNIV f"
using `0 \<le> c` by (rule ereal_mult_left_mono)
@@ -1598,7 +1655,7 @@
qed
from choice[OF this] guess f .. note f = this
have "SUPR UNIV f = Sup A"
- proof (rule ereal_SUPI)
+ proof (rule SUP_eqI)
fix i show "f i \<le> Sup A" using f
by (auto intro!: complete_lattice_class.Sup_upper)
next
@@ -1801,18 +1858,84 @@
subsubsection "Topological space"
-instantiation ereal :: topological_space
+instantiation ereal :: linorder_topology
begin
-definition "open A \<longleftrightarrow> open (ereal -` A)
- \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A))
- \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
+definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
+ open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
+
+instance
+ by default (simp add: open_ereal_generated)
+end
lemma open_PInfty: "open A \<Longrightarrow> \<infinity> \<in> A \<Longrightarrow> (\<exists>x. {ereal x<..} \<subseteq> A)"
- unfolding open_ereal_def by auto
+ unfolding open_ereal_generated
+proof (induct rule: generate_topology.induct)
+ case (Int A B)
+ moreover then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
+ by auto
+ ultimately show ?case
+ by (intro exI[of _ "max x z"]) fastforce
+next
+ { fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" by (cases x) auto }
+ moreover case (Basis S)
+ ultimately show ?case
+ by (auto split: ereal.split)
+qed (fastforce simp add: vimage_Union)+
lemma open_MInfty: "open A \<Longrightarrow> -\<infinity> \<in> A \<Longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A)"
- unfolding open_ereal_def by auto
+ unfolding open_ereal_generated
+proof (induct rule: generate_topology.induct)
+ case (Int A B)
+ moreover then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
+ by auto
+ ultimately show ?case
+ by (intro exI[of _ "min x z"]) fastforce
+next
+ { fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }
+ moreover case (Basis S)
+ ultimately show ?case
+ by (auto split: ereal.split)
+qed (fastforce simp add: vimage_Union)+
+
+lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
+ unfolding open_ereal_generated
+proof (induct rule: generate_topology.induct)
+ case (Int A B) then show ?case by auto
+next
+ { fix x have
+ "ereal -` {..<x} = (case x of PInfty \<Rightarrow> UNIV | MInfty \<Rightarrow> {} | ereal r \<Rightarrow> {..<r})"
+ "ereal -` {x<..} = (case x of PInfty \<Rightarrow> {} | MInfty \<Rightarrow> UNIV | ereal r \<Rightarrow> {r<..})"
+ by (induct x) auto }
+ moreover case (Basis S)
+ ultimately show ?case
+ by (auto split: ereal.split)
+qed (fastforce simp add: vimage_Union)+
+
+lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
+ unfolding open_generated_order[where 'a=real]
+proof (induct rule: generate_topology.induct)
+ case (Basis S)
+ moreover { fix x have "ereal ` {..< x} = { -\<infinity> <..< ereal x }" by auto (case_tac xa, auto) }
+ moreover { fix x have "ereal ` {x <..} = { ereal x <..< \<infinity> }" by auto (case_tac xa, auto) }
+ ultimately show ?case
+ by auto
+qed (auto simp add: image_Union image_Int)
+
+lemma open_ereal_def: "open A \<longleftrightarrow> open (ereal -` A) \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A)) \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
+ (is "open A \<longleftrightarrow> ?rhs")
+proof
+ assume "open A" then show ?rhs
+ using open_PInfty open_MInfty open_ereal_vimage by auto
+next
+ assume "?rhs"
+ then obtain x y where A: "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..< ereal y} \<subseteq> A"
+ by auto
+ have *: "A = ereal ` (ereal -` A) \<union> (if \<infinity> \<in> A then {ereal x<..} else {}) \<union> (if -\<infinity> \<in> A then {..< ereal y} else {})"
+ using A(2,3) by auto
+ from open_ereal[OF A(1)] show "open A"
+ by (subst *) (auto simp: open_Un)
+qed
lemma open_PInfty2: assumes "open A" "\<infinity> \<in> A" obtains x where "{ereal x<..} \<subseteq> A"
using open_PInfty[OF assms] by auto
@@ -1821,85 +1944,17 @@
using open_MInfty[OF assms] by auto
lemma ereal_openE: assumes "open A" obtains x y where
- "open (ereal -` A)"
- "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A"
- "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
+ "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
using assms open_ereal_def by auto
-instance
-proof
- let ?U = "UNIV::ereal set"
- show "open ?U" unfolding open_ereal_def
- by (auto intro!: exI[of _ 0])
-next
- fix S T::"ereal set" assume "open S" and "open T"
- from `open S`[THEN ereal_openE] guess xS yS .
- moreover from `open T`[THEN ereal_openE] guess xT yT .
- ultimately have
- "open (ereal -` (S \<inter> T))"
- "\<infinity> \<in> S \<inter> T \<Longrightarrow> {ereal (max xS xT) <..} \<subseteq> S \<inter> T"
- "-\<infinity> \<in> S \<inter> T \<Longrightarrow> {..< ereal (min yS yT)} \<subseteq> S \<inter> T"
- by auto
- then show "open (S Int T)" unfolding open_ereal_def by blast
-next
- fix K :: "ereal set set" assume "\<forall>S\<in>K. open S"
- then have *: "\<forall>S. \<exists>x y. S \<in> K \<longrightarrow> open (ereal -` S) \<and>
- (\<infinity> \<in> S \<longrightarrow> {ereal x <..} \<subseteq> S) \<and> (-\<infinity> \<in> S \<longrightarrow> {..< ereal y} \<subseteq> S)"
- by (auto simp: open_ereal_def)
- then show "open (Union K)" unfolding open_ereal_def
- proof (intro conjI impI)
- show "open (ereal -` \<Union>K)"
- using *[THEN choice] by (auto simp: vimage_Union)
- qed ((metis UnionE Union_upper subset_trans *)+)
-qed
-end
-
-lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
- by (auto simp: inj_vimage_image_eq open_ereal_def)
-
-lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
- unfolding open_ereal_def by auto
-
-lemma open_ereal_lessThan[intro, simp]: "open {..< a :: ereal}"
-proof -
- have "\<And>x. ereal -` {..<ereal x} = {..< x}"
- "ereal -` {..< \<infinity>} = UNIV" "ereal -` {..< -\<infinity>} = {}" by auto
- then show ?thesis by (cases a) (auto simp: open_ereal_def)
-qed
-
-lemma open_ereal_greaterThan[intro, simp]:
- "open {a :: ereal <..}"
-proof -
- have "\<And>x. ereal -` {ereal x<..} = {x<..}"
- "ereal -` {\<infinity><..} = {}" "ereal -` {-\<infinity><..} = UNIV" by auto
- then show ?thesis by (cases a) (auto simp: open_ereal_def)
-qed
-
-lemma ereal_open_greaterThanLessThan[intro, simp]: "open {a::ereal <..< b}"
- unfolding greaterThanLessThan_def by auto
-
-lemma closed_ereal_atLeast[simp, intro]: "closed {a :: ereal ..}"
-proof -
- have "- {a ..} = {..< a}" by auto
- then show "closed {a ..}"
- unfolding closed_def using open_ereal_lessThan by auto
-qed
-
-lemma closed_ereal_atMost[simp, intro]: "closed {.. b :: ereal}"
-proof -
- have "- {.. b} = {b <..}" by auto
- then show "closed {.. b}"
- unfolding closed_def using open_ereal_greaterThan by auto
-qed
-
-lemma closed_ereal_atLeastAtMost[simp, intro]:
- shows "closed {a :: ereal .. b}"
- unfolding atLeastAtMost_def by auto
-
-lemma closed_ereal_singleton:
- "closed {a :: ereal}"
-by (metis atLeastAtMost_singleton closed_ereal_atLeastAtMost)
-
+lemmas open_ereal_lessThan = open_lessThan[where 'a=ereal]
+lemmas open_ereal_greaterThan = open_greaterThan[where 'a=ereal]
+lemmas ereal_open_greaterThanLessThan = open_greaterThanLessThan[where 'a=ereal]
+lemmas closed_ereal_atLeast = closed_atLeast[where 'a=ereal]
+lemmas closed_ereal_atMost = closed_atMost[where 'a=ereal]
+lemmas closed_ereal_atLeastAtMost = closed_atLeastAtMost[where 'a=ereal]
+lemmas closed_ereal_singleton = closed_singleton[where 'a=ereal]
+
lemma ereal_open_cont_interval:
fixes S :: "ereal set"
assumes "open S" "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
@@ -1928,28 +1983,6 @@
show thesis by auto
qed
-instance ereal :: t2_space
-proof
- fix x y :: ereal assume "x ~= y"
- let "?P x (y::ereal)" = "EX U V. open U & open V & x : U & y : V & U Int V = {}"
-
- { fix x y :: ereal assume "x < y"
- from ereal_dense[OF this] obtain z where z: "x < z" "z < y" by auto
- have "?P x y"
- apply (rule exI[of _ "{..<z}"])
- apply (rule exI[of _ "{z<..}"])
- using z by auto }
- note * = this
-
- from `x ~= y`
- show "EX U V. open U & open V & x : U & y : V & U Int V = {}"
- proof (cases rule: linorder_cases)
- assume "x = y" with `x ~= y` show ?thesis by simp
- next assume "x < y" from *[OF this] show ?thesis by auto
- next assume "y < x" from *[OF this] show ?thesis by auto
- qed
-qed
-
subsubsection {* Convergent sequences *}
lemma lim_ereal[simp]:
@@ -1979,152 +2012,67 @@
by (rule eventually_mono)
qed
-lemma Lim_PInfty: "f ----> \<infinity> <-> (ALL B. EX N. ALL n>=N. f n >= ereal B)" (is "?l = ?r")
-proof
- assume ?r
- show ?l
- apply(rule topological_tendstoI)
- unfolding eventually_sequentially
- proof-
- fix S :: "ereal set" assume "open S" "\<infinity> : S"
- from open_PInfty[OF this] guess B .. note B=this
- from `?r`[rule_format,of "B+1"] guess N .. note N=this
- show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
- proof safe case goal1
- have "ereal B < ereal (B + 1)" by auto
- also have "... <= f n" using goal1 N by auto
- finally show ?case using B by fastforce
- qed
- qed
+lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
+proof -
+ { fix l :: ereal assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
+ from this[THEN spec, of "real l"]
+ have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
+ by (cases l) (auto elim: eventually_elim1) }
+ then show ?thesis
+ by (auto simp: order_tendsto_iff)
+qed
+
+lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
+ unfolding tendsto_def
+proof safe
+ fix S :: "ereal set" assume "open S" "-\<infinity> \<in> S"
+ from open_MInfty[OF this] guess B .. note B = this
+ moreover
+ assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
+ then have "eventually (\<lambda>z. f z \<in> {..< B}) F" by auto
+ ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
next
- assume ?l
- show ?r
- proof fix B::real have "open {ereal B<..}" "\<infinity> : {ereal B<..}" by auto
- from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
- guess N .. note N=this
- show "EX N. ALL n>=N. ereal B <= f n" apply(rule_tac x=N in exI) using N by auto
- qed
+ fix x assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
+ from this[rule_format, of "{..< ereal x}"]
+ show "eventually (\<lambda>y. f y < ereal x) F" by auto
qed
-
-lemma Lim_MInfty: "f ----> (-\<infinity>) <-> (ALL B. EX N. ALL n>=N. f n <= ereal B)" (is "?l = ?r")
-proof
- assume ?r
- show ?l
- apply(rule topological_tendstoI)
- unfolding eventually_sequentially
- proof-
- fix S :: "ereal set"
- assume "open S" "(-\<infinity>) : S"
- from open_MInfty[OF this] guess B .. note B=this
- from `?r`[rule_format,of "B-(1::real)"] guess N .. note N=this
- show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
- proof safe case goal1
- have "ereal (B - 1) >= f n" using goal1 N by auto
- also have "... < ereal B" by auto
- finally show ?case using B by fastforce
- qed
- qed
-next assume ?l show ?r
- proof fix B::real have "open {..<ereal B}" "(-\<infinity>) : {..<ereal B}" by auto
- from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
- guess N .. note N=this
- show "EX N. ALL n>=N. ereal B >= f n" apply(rule_tac x=N in exI) using N by auto
- qed
-qed
-
-
-lemma Lim_bounded_PInfty: assumes lim:"f ----> l" and "!!n. f n <= ereal B" shows "l ~= \<infinity>"
-proof(rule ccontr,unfold not_not) let ?B = "B + 1" assume as:"l=\<infinity>"
- from lim[unfolded this Lim_PInfty,rule_format,of "?B"]
- guess N .. note N=this[rule_format,OF le_refl]
- hence "ereal ?B <= ereal B" using assms(2)[of N] by(rule order_trans)
- hence "ereal ?B < ereal ?B" apply (rule le_less_trans) by auto
- thus False by auto
-qed
-
-
-lemma Lim_bounded_MInfty: assumes lim:"f ----> l" and "!!n. f n >= ereal B" shows "l ~= (-\<infinity>)"
-proof(rule ccontr,unfold not_not) let ?B = "B - 1" assume as:"l=(-\<infinity>)"
- from lim[unfolded this Lim_MInfty,rule_format,of "?B"]
- guess N .. note N=this[rule_format,OF le_refl]
- hence "ereal B <= ereal ?B" using assms(2)[of N] order_trans[of "ereal B" "f N" "ereal(B - 1)"] by blast
- thus False by auto
-qed
-
+lemma Lim_PInfty: "f ----> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
+ unfolding tendsto_PInfty eventually_sequentially
+proof safe
+ fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
+ from this[rule_format, of "r+1"] guess N ..
+ moreover have "ereal r < ereal (r + 1)" by auto
+ ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
+ by (blast intro: less_le_trans)
+qed (blast intro: less_imp_le)
+
+lemma Lim_MInfty: "f ----> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
+ unfolding tendsto_MInfty eventually_sequentially
+proof safe
+ fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
+ from this[rule_format, of "r - 1"] guess N ..
+ moreover have "ereal (r - 1) < ereal r" by auto
+ ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
+ by (blast intro: le_less_trans)
+qed (blast intro: less_imp_le)
+
+lemma Lim_bounded_PInfty: "f ----> l \<Longrightarrow> (\<And>n. f n \<le> ereal B) \<Longrightarrow> l \<noteq> \<infinity>"
+ using LIMSEQ_le_const2[of f l "ereal B"] by auto
+
+lemma Lim_bounded_MInfty: "f ----> l \<Longrightarrow> (\<And>n. ereal B \<le> f n) \<Longrightarrow> l \<noteq> -\<infinity>"
+ using LIMSEQ_le_const[of f l "ereal B"] by auto
lemma tendsto_explicit:
"f ----> f0 <-> (ALL S. open S --> f0 : S --> (EX N. ALL n>=N. f n : S))"
unfolding tendsto_def eventually_sequentially by auto
-
-lemma tendsto_obtains_N:
- assumes "f ----> f0"
- assumes "open S" "f0 : S"
- obtains N where "ALL n>=N. f n : S"
- using tendsto_explicit[of f f0] assms by auto
-
-
-lemma tail_same_limit:
- fixes X Y N
- assumes "X ----> L" "ALL n>=N. X n = Y n"
- shows "Y ----> L"
-proof-
-{ fix S assume "open S" and "L:S"
- then obtain N1 where "ALL n>=N1. X n : S"
- using assms unfolding tendsto_def eventually_sequentially by auto
- hence "ALL n>=max N N1. Y n : S" using assms by auto
- hence "EX N. ALL n>=N. Y n : S" apply(rule_tac x="max N N1" in exI) by auto
-}
-thus ?thesis using tendsto_explicit by auto
-qed
-
-
lemma Lim_bounded_PInfty2:
-assumes lim:"f ----> l" and "ALL n>=N. f n <= ereal B"
-shows "l ~= \<infinity>"
-proof-
- def g == "(%n. if n>=N then f n else ereal B)"
- hence "g ----> l" using tail_same_limit[of f l N g] lim by auto
- moreover have "!!n. g n <= ereal B" using g_def assms by auto
- ultimately show ?thesis using Lim_bounded_PInfty by auto
-qed
-
-lemma Lim_bounded_ereal:
- assumes lim:"f ----> (l :: ereal)"
- and "ALL n>=M. f n <= C"
- shows "l<=C"
-proof-
-{ assume "l=(-\<infinity>)" hence ?thesis by auto }
-moreover
-{ assume "~(l=(-\<infinity>))"
- { assume "C=\<infinity>" hence ?thesis by auto }
- moreover
- { assume "C=(-\<infinity>)" hence "ALL n>=M. f n = (-\<infinity>)" using assms by auto
- hence "l=(-\<infinity>)" using assms
- tendsto_unique[OF trivial_limit_sequentially] tail_same_limit[of "\<lambda>n. -\<infinity>" "-\<infinity>" M f, OF tendsto_const] by auto
- hence ?thesis by auto }
- moreover
- { assume "EX B. C = ereal B"
- then obtain B where B_def: "C=ereal B" by auto
- hence "~(l=\<infinity>)" using Lim_bounded_PInfty2 assms by auto
- then obtain m where m_def: "ereal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
- then obtain N where N_def: "ALL n>=N. f n : {ereal(m - 1) <..< ereal(m+1)}"
- apply (subst tendsto_obtains_N[of f l "{ereal(m - 1) <..< ereal(m+1)}"]) using assms by auto
- { fix n assume "n>=N"
- hence "EX r. ereal r = f n" using N_def by (cases "f n") auto
- } then obtain g where g_def: "ALL n>=N. ereal (g n) = f n" by metis
- hence "(%n. ereal (g n)) ----> l" using tail_same_limit[of f l N] assms by auto
- hence *: "(%n. g n) ----> m" using m_def by auto
- { fix n assume "n>=max N M"
- hence "ereal (g n) <= ereal B" using assms g_def B_def by auto
- hence "g n <= B" by auto
- } hence "EX N. ALL n>=N. g n <= B" by blast
- hence "m<=B" using * LIMSEQ_le_const2[of g m B] by auto
- hence ?thesis using m_def B_def by auto
- } ultimately have ?thesis by (cases C) auto
-} ultimately show ?thesis by blast
-qed
+ "f ----> l \<Longrightarrow> ALL n>=N. f n <= ereal B \<Longrightarrow> l ~= \<infinity>"
+ using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
+
+lemma Lim_bounded_ereal: "f ----> (l :: ereal) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
+ by (intro LIMSEQ_le_const2) auto
lemma real_of_ereal_mult[simp]:
fixes a b :: ereal shows "real (a * b) = real a * real b"
@@ -2204,349 +2152,6 @@
lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
by (cases x) auto
-lemma ereal_LimI_finite:
- fixes x :: ereal
- assumes "\<bar>x\<bar> \<noteq> \<infinity>"
- assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
- shows "u ----> x"
-proof (rule topological_tendstoI, unfold eventually_sequentially)
- obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
- fix S assume "open S" "x : S"
- then have "open (ereal -` S)" unfolding open_ereal_def by auto
- with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
- unfolding open_real_def rx_def by auto
- then obtain n where
- upper: "!!N. n <= N ==> u N < x + ereal r" and
- lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
- show "EX N. ALL n>=N. u n : S"
- proof (safe intro!: exI[of _ n])
- fix N assume "n <= N"
- from upper[OF this] lower[OF this] assms `0 < r`
- have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
- then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
- hence "rx < ra + r" and "ra < rx + r"
- using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
- hence "dist (real (u N)) rx < r"
- using rx_def ra_def
- by (auto simp: dist_real_def abs_diff_less_iff field_simps)
- from dist[OF this] show "u N : S" using `u N ~: {\<infinity>, -\<infinity>}`
- by (auto simp: ereal_real split: split_if_asm)
- qed
-qed
-
-lemma ereal_LimI_finite_iff:
- fixes x :: ereal
- assumes "\<bar>x\<bar> \<noteq> \<infinity>"
- shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
- (is "?lhs <-> ?rhs")
-proof
- assume lim: "u ----> x"
- { fix r assume "(r::ereal)>0"
- then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
- apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
- using lim ereal_between[of x r] assms `r>0` by auto
- hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
- using ereal_minus_less[of r x] by (cases r) auto
- } then show "?rhs" by auto
-next
- assume ?rhs then show "u ----> x"
- using ereal_LimI_finite[of x] assms by auto
-qed
-
-
-subsubsection {* @{text Liminf} and @{text Limsup} *}
-
-definition
- "Liminf net f = (GREATEST l. \<forall>y<l. eventually (\<lambda>x. y < f x) net)"
-
-definition
- "Limsup net f = (LEAST l. \<forall>y>l. eventually (\<lambda>x. f x < y) net)"
-
-lemma Liminf_Sup:
- fixes f :: "'a => 'b::complete_linorder"
- shows "Liminf net f = Sup {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net}"
- by (auto intro!: Greatest_equality complete_lattice_class.Sup_upper simp: less_Sup_iff Liminf_def)
-
-lemma Limsup_Inf:
- fixes f :: "'a => 'b::complete_linorder"
- shows "Limsup net f = Inf {l. \<forall>y>l. eventually (\<lambda>x. f x < y) net}"
- by (auto intro!: Least_equality complete_lattice_class.Inf_lower simp: Inf_less_iff Limsup_def)
-
-lemma ereal_SupI:
- fixes x :: ereal
- assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
- assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
- shows "Sup A = x"
- unfolding Sup_ereal_def
- using assms by (auto intro!: Least_equality)
-
-lemma ereal_InfI:
- fixes x :: ereal
- assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
- assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
- shows "Inf A = x"
- unfolding Inf_ereal_def
- using assms by (auto intro!: Greatest_equality)
-
-lemma Limsup_const:
- fixes c :: "'a::complete_linorder"
- assumes ntriv: "\<not> trivial_limit net"
- shows "Limsup net (\<lambda>x. c) = c"
- unfolding Limsup_Inf
-proof (safe intro!: antisym complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower)
- fix x assume *: "\<forall>y>x. eventually (\<lambda>_. c < y) net"
- show "c \<le> x"
- proof (rule ccontr)
- assume "\<not> c \<le> x" then have "x < c" by auto
- then show False using ntriv * by (auto simp: trivial_limit_def)
- qed
-qed auto
-
-lemma Liminf_const:
- fixes c :: "'a::complete_linorder"
- assumes ntriv: "\<not> trivial_limit net"
- shows "Liminf net (\<lambda>x. c) = c"
- unfolding Liminf_Sup
-proof (safe intro!: antisym complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
- fix x assume *: "\<forall>y<x. eventually (\<lambda>_. y < c) net"
- show "x \<le> c"
- proof (rule ccontr)
- assume "\<not> x \<le> c" then have "c < x" by auto
- then show False using ntriv * by (auto simp: trivial_limit_def)
- qed
-qed auto
-
-definition (in order) mono_set:
- "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
-
-lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
-lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
-lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
-lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
-
-lemma (in complete_linorder) mono_set_iff:
- fixes S :: "'a set"
- defines "a \<equiv> Inf S"
- shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
-proof
- assume "mono_set S"
- then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
- show ?c
- proof cases
- assume "a \<in> S"
- show ?c
- using mono[OF _ `a \<in> S`]
- by (auto intro: Inf_lower simp: a_def)
- next
- assume "a \<notin> S"
- have "S = {a <..}"
- proof safe
- fix x assume "x \<in> S"
- then have "a \<le> x" unfolding a_def by (rule Inf_lower)
- then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
- next
- fix x assume "a < x"
- then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
- with mono[of y x] show "x \<in> S" by auto
- qed
- then show ?c ..
- qed
-qed auto
-
-lemma lim_imp_Liminf:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes ntriv: "\<not> trivial_limit net"
- assumes lim: "(f ---> f0) net"
- shows "Liminf net f = f0"
- unfolding Liminf_Sup
-proof (safe intro!: ereal_SupI)
- fix y assume *: "\<forall>y'<y. eventually (\<lambda>x. y' < f x) net"
- show "y \<le> f0"
- proof (rule ereal_le_ereal)
- fix B assume "B < y"
- { assume "f0 < B"
- then have "eventually (\<lambda>x. f x < B \<and> B < f x) net"
- using topological_tendstoD[OF lim, of "{..<B}"] *[rule_format, OF `B < y`]
- by (auto intro: eventually_conj)
- also have "(\<lambda>x. f x < B \<and> B < f x) = (\<lambda>x. False)" by (auto simp: fun_eq_iff)
- finally have False using ntriv[unfolded trivial_limit_def] by auto
- } then show "B \<le> f0" by (metis linorder_le_less_linear)
- qed
-next
- fix y assume *: "\<forall>z. z \<in> {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net} \<longrightarrow> z \<le> y"
- show "f0 \<le> y"
- proof (safe intro!: *[rule_format])
- fix y assume "y < f0" then show "eventually (\<lambda>x. y < f x) net"
- using lim[THEN topological_tendstoD, of "{y <..}"] by auto
- qed
-qed
-
-lemma ereal_Liminf_le_Limsup:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes ntriv: "\<not> trivial_limit net"
- shows "Liminf net f \<le> Limsup net f"
- unfolding Limsup_Inf Liminf_Sup
-proof (safe intro!: complete_lattice_class.Inf_greatest complete_lattice_class.Sup_least)
- fix u v assume *: "\<forall>y<u. eventually (\<lambda>x. y < f x) net" "\<forall>y>v. eventually (\<lambda>x. f x < y) net"
- show "u \<le> v"
- proof (rule ccontr)
- assume "\<not> u \<le> v"
- then obtain t where "t < u" "v < t"
- using ereal_dense[of v u] by (auto simp: not_le)
- then have "eventually (\<lambda>x. t < f x \<and> f x < t) net"
- using * by (auto intro: eventually_conj)
- also have "(\<lambda>x. t < f x \<and> f x < t) = (\<lambda>x. False)" by (auto simp: fun_eq_iff)
- finally show False using ntriv by (auto simp: trivial_limit_def)
- qed
-qed
-
-lemma Liminf_mono:
- fixes f g :: "'a => ereal"
- assumes ev: "eventually (\<lambda>x. f x \<le> g x) net"
- shows "Liminf net f \<le> Liminf net g"
- unfolding Liminf_Sup
-proof (safe intro!: Sup_mono bexI)
- fix a y assume "\<forall>y<a. eventually (\<lambda>x. y < f x) net" and "y < a"
- then have "eventually (\<lambda>x. y < f x) net" by auto
- then show "eventually (\<lambda>x. y < g x) net"
- by (rule eventually_rev_mp) (rule eventually_mono[OF _ ev], auto)
-qed simp
-
-lemma Liminf_eq:
- fixes f g :: "'a \<Rightarrow> ereal"
- assumes "eventually (\<lambda>x. f x = g x) net"
- shows "Liminf net f = Liminf net g"
- by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
-
-lemma Liminf_mono_all:
- fixes f g :: "'a \<Rightarrow> ereal"
- assumes "\<And>x. f x \<le> g x"
- shows "Liminf net f \<le> Liminf net g"
- using assms by (intro Liminf_mono always_eventually) auto
-
-lemma Limsup_mono:
- fixes f g :: "'a \<Rightarrow> ereal"
- assumes ev: "eventually (\<lambda>x. f x \<le> g x) net"
- shows "Limsup net f \<le> Limsup net g"
- unfolding Limsup_Inf
-proof (safe intro!: Inf_mono bexI)
- fix a y assume "\<forall>y>a. eventually (\<lambda>x. g x < y) net" and "a < y"
- then have "eventually (\<lambda>x. g x < y) net" by auto
- then show "eventually (\<lambda>x. f x < y) net"
- by (rule eventually_rev_mp) (rule eventually_mono[OF _ ev], auto)
-qed simp
-
-lemma Limsup_mono_all:
- fixes f g :: "'a \<Rightarrow> ereal"
- assumes "\<And>x. f x \<le> g x"
- shows "Limsup net f \<le> Limsup net g"
- using assms by (intro Limsup_mono always_eventually) auto
-
-lemma Limsup_eq:
- fixes f g :: "'a \<Rightarrow> ereal"
- assumes "eventually (\<lambda>x. f x = g x) net"
- shows "Limsup net f = Limsup net g"
- by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
-
-abbreviation "liminf \<equiv> Liminf sequentially"
-
-abbreviation "limsup \<equiv> Limsup sequentially"
-
-lemma liminf_SUPR_INFI:
- fixes f :: "nat \<Rightarrow> ereal"
- shows "liminf f = (SUP n. INF m:{n..}. f m)"
- unfolding Liminf_Sup eventually_sequentially
-proof (safe intro!: antisym complete_lattice_class.Sup_least)
- fix x assume *: "\<forall>y<x. \<exists>N. \<forall>n\<ge>N. y < f n" show "x \<le> (SUP n. INF m:{n..}. f m)"
- proof (rule ereal_le_ereal)
- fix y assume "y < x"
- with * obtain N where "\<And>n. N \<le> n \<Longrightarrow> y < f n" by auto
- then have "y \<le> (INF m:{N..}. f m)" by (force simp: le_INF_iff)
- also have "\<dots> \<le> (SUP n. INF m:{n..}. f m)" by (intro SUP_upper) auto
- finally show "y \<le> (SUP n. INF m:{n..}. f m)" .
- qed
-next
- show "(SUP n. INF m:{n..}. f m) \<le> Sup {l. \<forall>y<l. \<exists>N. \<forall>n\<ge>N. y < f n}"
- proof (unfold SUP_def, safe intro!: Sup_mono bexI)
- fix y n assume "y < INFI {n..} f"
- from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. y < f n" by (intro exI[of _ n]) auto
- qed (rule order_refl)
-qed
-
-lemma tail_same_limsup:
- fixes X Y :: "nat => ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n = Y n"
- shows "limsup X = limsup Y"
- using Limsup_eq[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma tail_same_liminf:
- fixes X Y :: "nat => ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n = Y n"
- shows "liminf X = liminf Y"
- using Liminf_eq[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma liminf_mono:
- fixes X Y :: "nat \<Rightarrow> ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
- shows "liminf X \<le> liminf Y"
- using Liminf_mono[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma limsup_mono:
- fixes X Y :: "nat => ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
- shows "limsup X \<le> limsup Y"
- using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma
- fixes X :: "nat \<Rightarrow> ereal"
- shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
- and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
- unfolding incseq_def decseq_def by auto
-
-lemma liminf_bounded:
- fixes X Y :: "nat \<Rightarrow> ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> C \<le> X n"
- shows "C \<le> liminf X"
- using liminf_mono[of N "\<lambda>n. C" X] assms Liminf_const[of sequentially C] by simp
-
-lemma limsup_bounded:
- fixes X Y :: "nat => ereal"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= C"
- shows "limsup X \<le> C"
- using limsup_mono[of N X "\<lambda>n. C"] assms Limsup_const[of sequentially C] by simp
-
-lemma liminf_bounded_iff:
- fixes x :: "nat \<Rightarrow> ereal"
- shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
-proof safe
- fix B assume "B < C" "C \<le> liminf x"
- then have "B < liminf x" by auto
- then obtain N where "B < (INF m:{N..}. x m)"
- unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
- from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
-next
- assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
- { fix B assume "B<C"
- then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
- hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
- also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
- finally have "B \<le> liminf x" .
- } then show "?lhs" by (metis * leD liminf_bounded linorder_le_less_linear)
-qed
-
-lemma liminf_subseq_mono:
- fixes X :: "nat \<Rightarrow> ereal"
- assumes "subseq r"
- shows "liminf X \<le> liminf (X \<circ> r) "
-proof-
- have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
- proof (safe intro!: INF_mono)
- fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
- using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
- qed
- then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
-qed
-
lemma ereal_real': assumes "\<bar>x\<bar> \<noteq> \<infinity>" shows "ereal (real x) = x"
using assms by auto
@@ -2618,6 +2223,399 @@
"[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
by (metis sup_ereal_def sup_least)
+lemma ereal_LimI_finite:
+ fixes x :: ereal
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+ assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
+ shows "u ----> x"
+proof (rule topological_tendstoI, unfold eventually_sequentially)
+ obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
+ fix S assume "open S" "x : S"
+ then have "open (ereal -` S)" unfolding open_ereal_def by auto
+ with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
+ unfolding open_real_def rx_def by auto
+ then obtain n where
+ upper: "!!N. n <= N ==> u N < x + ereal r" and
+ lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
+ show "EX N. ALL n>=N. u n : S"
+ proof (safe intro!: exI[of _ n])
+ fix N assume "n <= N"
+ from upper[OF this] lower[OF this] assms `0 < r`
+ have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
+ then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
+ hence "rx < ra + r" and "ra < rx + r"
+ using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
+ hence "dist (real (u N)) rx < r"
+ using rx_def ra_def
+ by (auto simp: dist_real_def abs_diff_less_iff field_simps)
+ from dist[OF this] show "u N : S" using `u N ~: {\<infinity>, -\<infinity>}`
+ by (auto simp: ereal_real split: split_if_asm)
+ qed
+qed
+
+lemma tendsto_obtains_N:
+ assumes "f ----> f0"
+ assumes "open S" "f0 : S"
+ obtains N where "ALL n>=N. f n : S"
+ using tendsto_explicit[of f f0] assms by auto
+
+lemma ereal_LimI_finite_iff:
+ fixes x :: ereal
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+ shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
+ (is "?lhs <-> ?rhs")
+proof
+ assume lim: "u ----> x"
+ { fix r assume "(r::ereal)>0"
+ then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
+ apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
+ using lim ereal_between[of x r] assms `r>0` by auto
+ hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
+ using ereal_minus_less[of r x] by (cases r) auto
+ } then show "?rhs" by auto
+next
+ assume ?rhs then show "u ----> x"
+ using ereal_LimI_finite[of x] assms by auto
+qed
+
+
+subsubsection {* @{text Liminf} and @{text Limsup} *}
+
+definition
+ "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
+
+definition
+ "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
+
+abbreviation "liminf \<equiv> Liminf sequentially"
+
+abbreviation "limsup \<equiv> Limsup sequentially"
+
+lemma Liminf_eqI:
+ "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>
+ (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
+ unfolding Liminf_def by (auto intro!: SUP_eqI)
+
+lemma Limsup_eqI:
+ "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>
+ (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
+ unfolding Limsup_def by (auto intro!: INF_eqI)
+
+lemma liminf_SUPR_INFI:
+ fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
+ shows "liminf f = (SUP n. INF m:{n..}. f m)"
+ unfolding Liminf_def eventually_sequentially
+ by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
+
+lemma limsup_INFI_SUPR:
+ fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
+ shows "limsup f = (INF n. SUP m:{n..}. f m)"
+ unfolding Limsup_def eventually_sequentially
+ by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
+
+lemma Limsup_const:
+ assumes ntriv: "\<not> trivial_limit F"
+ shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
+proof -
+ have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
+ have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
+ using ntriv by (intro SUP_const) (auto simp: eventually_False *)
+ then show ?thesis
+ unfolding Limsup_def using eventually_True
+ by (subst INF_cong[where D="\<lambda>x. c"])
+ (auto intro!: INF_const simp del: eventually_True)
+qed
+
+lemma Liminf_const:
+ assumes ntriv: "\<not> trivial_limit F"
+ shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
+proof -
+ have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
+ have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
+ using ntriv by (intro INF_const) (auto simp: eventually_False *)
+ then show ?thesis
+ unfolding Liminf_def using eventually_True
+ by (subst SUP_cong[where D="\<lambda>x. c"])
+ (auto intro!: SUP_const simp del: eventually_True)
+qed
+
+lemma Liminf_mono:
+ fixes f g :: "'a => 'b :: complete_lattice"
+ assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
+ shows "Liminf F f \<le> Liminf F g"
+ unfolding Liminf_def
+proof (safe intro!: SUP_mono)
+ fix P assume "eventually P F"
+ with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
+ then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
+ by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
+qed
+
+lemma Liminf_eq:
+ fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+ assumes "eventually (\<lambda>x. f x = g x) F"
+ shows "Liminf F f = Liminf F g"
+ by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
+
+lemma Limsup_mono:
+ fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+ assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
+ shows "Limsup F f \<le> Limsup F g"
+ unfolding Limsup_def
+proof (safe intro!: INF_mono)
+ fix P assume "eventually P F"
+ with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
+ then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
+ by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
+qed
+
+lemma Limsup_eq:
+ fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+ assumes "eventually (\<lambda>x. f x = g x) net"
+ shows "Limsup net f = Limsup net g"
+ by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
+
+lemma Liminf_le_Limsup:
+ fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
+ assumes ntriv: "\<not> trivial_limit F"
+ shows "Liminf F f \<le> Limsup F f"
+ unfolding Limsup_def Liminf_def
+ apply (rule complete_lattice_class.SUP_least)
+ apply (rule complete_lattice_class.INF_greatest)
+proof safe
+ fix P Q assume "eventually P F" "eventually Q F"
+ then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
+ then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
+ using ntriv by (auto simp add: eventually_False)
+ have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
+ by (rule INF_mono) auto
+ also have "\<dots> \<le> SUPR (Collect ?C) f"
+ using not_False by (intro INF_le_SUP) auto
+ also have "\<dots> \<le> SUPR (Collect Q) f"
+ by (rule SUP_mono) auto
+ finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
+qed
+
+lemma
+ fixes X :: "nat \<Rightarrow> ereal"
+ shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
+ and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
+ unfolding incseq_def decseq_def by auto
+
+lemma Liminf_bounded:
+ fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes le: "eventually (\<lambda>n. C \<le> X n) F"
+ shows "C \<le> Liminf F X"
+ using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
+
+lemma Limsup_bounded:
+ fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes le: "eventually (\<lambda>n. X n \<le> C) F"
+ shows "Limsup F X \<le> C"
+ using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
+
+lemma le_Liminf_iff:
+ fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
+ shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
+proof -
+ { fix y P assume "eventually P F" "y < INFI (Collect P) X"
+ then have "eventually (\<lambda>x. y < X x) F"
+ by (auto elim!: eventually_elim1 dest: less_INF_D) }
+ moreover
+ { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
+ have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
+ proof cases
+ assume "\<exists>z. y < z \<and> z < C"
+ then guess z ..
+ moreover then have "z \<le> INFI {x. z < X x} X"
+ by (auto intro!: INF_greatest)
+ ultimately show ?thesis
+ using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
+ next
+ assume "\<not> (\<exists>z. y < z \<and> z < C)"
+ then have "C \<le> INFI {x. y < X x} X"
+ by (intro INF_greatest) auto
+ with `y < C` show ?thesis
+ using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
+ qed }
+ ultimately show ?thesis
+ unfolding Liminf_def le_SUP_iff by auto
+qed
+
+lemma lim_imp_Liminf:
+ fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes lim: "(f ---> f0) F"
+ shows "Liminf F f = f0"
+proof (intro Liminf_eqI)
+ fix P assume P: "eventually P F"
+ then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
+ by eventually_elim (auto intro!: INF_lower)
+ then show "INFI (Collect P) f \<le> f0"
+ by (rule tendsto_le[OF ntriv lim tendsto_const])
+next
+ fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
+ show "f0 \<le> y"
+ proof cases
+ assume "\<exists>z. y < z \<and> z < f0"
+ then guess z ..
+ moreover have "z \<le> INFI {x. z < f x} f"
+ by (rule INF_greatest) simp
+ ultimately show ?thesis
+ using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
+ next
+ assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
+ show ?thesis
+ proof (rule classical)
+ assume "\<not> f0 \<le> y"
+ then have "eventually (\<lambda>x. y < f x) F"
+ using lim[THEN topological_tendstoD, of "{y <..}"] by auto
+ then have "eventually (\<lambda>x. f0 \<le> f x) F"
+ using discrete by (auto elim!: eventually_elim1)
+ then have "INFI {x. f0 \<le> f x} f \<le> y"
+ by (rule upper)
+ moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
+ by (intro INF_greatest) simp
+ ultimately show "f0 \<le> y" by simp
+ qed
+ qed
+qed
+
+lemma lim_imp_Limsup:
+ fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes lim: "(f ---> f0) F"
+ shows "Limsup F f = f0"
+proof (intro Limsup_eqI)
+ fix P assume P: "eventually P F"
+ then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
+ by eventually_elim (auto intro!: SUP_upper)
+ then show "f0 \<le> SUPR (Collect P) f"
+ by (rule tendsto_le[OF ntriv tendsto_const lim])
+next
+ fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
+ show "y \<le> f0"
+ proof cases
+ assume "\<exists>z. f0 < z \<and> z < y"
+ then guess z ..
+ moreover have "SUPR {x. f x < z} f \<le> z"
+ by (rule SUP_least) simp
+ ultimately show ?thesis
+ using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
+ next
+ assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
+ show ?thesis
+ proof (rule classical)
+ assume "\<not> y \<le> f0"
+ then have "eventually (\<lambda>x. f x < y) F"
+ using lim[THEN topological_tendstoD, of "{..< y}"] by auto
+ then have "eventually (\<lambda>x. f x \<le> f0) F"
+ using discrete by (auto elim!: eventually_elim1 simp: not_less)
+ then have "y \<le> SUPR {x. f x \<le> f0} f"
+ by (rule lower)
+ moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
+ by (intro SUP_least) simp
+ ultimately show "y \<le> f0" by simp
+ qed
+ qed
+qed
+
+lemma Liminf_eq_Limsup:
+ fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+ assumes ntriv: "\<not> trivial_limit F"
+ and lim: "Liminf F f = f0" "Limsup F f = f0"
+ shows "(f ---> f0) F"
+proof (rule order_tendstoI)
+ fix a assume "f0 < a"
+ with assms have "Limsup F f < a" by simp
+ then obtain P where "eventually P F" "SUPR (Collect P) f < a"
+ unfolding Limsup_def INF_less_iff by auto
+ then show "eventually (\<lambda>x. f x < a) F"
+ by (auto elim!: eventually_elim1 dest: SUP_lessD)
+next
+ fix a assume "a < f0"
+ with assms have "a < Liminf F f" by simp
+ then obtain P where "eventually P F" "a < INFI (Collect P) f"
+ unfolding Liminf_def less_SUP_iff by auto
+ then show "eventually (\<lambda>x. a < f x) F"
+ by (auto elim!: eventually_elim1 dest: less_INF_D)
+qed
+
+lemma tendsto_iff_Liminf_eq_Limsup:
+ fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+ shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
+ by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
+
+lemma liminf_bounded_iff:
+ fixes x :: "nat \<Rightarrow> ereal"
+ shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
+ unfolding le_Liminf_iff eventually_sequentially ..
+
+lemma liminf_subseq_mono:
+ fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
+ assumes "subseq r"
+ shows "liminf X \<le> liminf (X \<circ> r) "
+proof-
+ have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
+ proof (safe intro!: INF_mono)
+ fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
+ using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
+ qed
+ then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
+qed
+
+lemma limsup_subseq_mono:
+ fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
+ assumes "subseq r"
+ shows "limsup (X \<circ> r) \<le> limsup X"
+proof-
+ have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
+ proof (safe intro!: SUP_mono)
+ fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
+ using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
+ qed
+ then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
+qed
+
+definition (in order) mono_set:
+ "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
+
+lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
+lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
+lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
+lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
+
+lemma (in complete_linorder) mono_set_iff:
+ fixes S :: "'a set"
+ defines "a \<equiv> Inf S"
+ shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
+proof
+ assume "mono_set S"
+ then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
+ show ?c
+ proof cases
+ assume "a \<in> S"
+ show ?c
+ using mono[OF _ `a \<in> S`]
+ by (auto intro: Inf_lower simp: a_def)
+ next
+ assume "a \<notin> S"
+ have "S = {a <..}"
+ proof safe
+ fix x assume "x \<in> S"
+ then have "a \<le> x" unfolding a_def by (rule Inf_lower)
+ then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
+ next
+ fix x assume "a < x"
+ then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
+ with mono[of y x] show "x \<in> S" by auto
+ qed
+ then show ?c ..
+ qed
+qed auto
+
subsubsection {* Tests for code generator *}
(* A small list of simple arithmetic expressions *)
--- a/src/HOL/Library/FrechetDeriv.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy Wed Feb 13 11:46:48 2013 +0100
@@ -5,7 +5,7 @@
header {* Frechet Derivative *}
theory FrechetDeriv
-imports Complex_Main
+imports "~~/src/HOL/Complex_Main"
begin
definition
--- a/src/HOL/Library/Inner_Product.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Library/Inner_Product.thy Wed Feb 13 11:46:48 2013 +0100
@@ -117,8 +117,6 @@
subclass real_normed_vector
proof
fix a :: real and x y :: 'a
- show "0 \<le> norm x"
- unfolding norm_eq_sqrt_inner by simp
show "norm x = 0 \<longleftrightarrow> x = 0"
unfolding norm_eq_sqrt_inner by simp
show "norm (x + y) \<le> norm x + norm y"
--- a/src/HOL/Library/Product_Vector.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Library/Product_Vector.thy Wed Feb 13 11:46:48 2013 +0100
@@ -408,8 +408,6 @@
instance proof
fix r :: real and x y :: "'a \<times> 'b"
- show "0 \<le> norm x"
- unfolding norm_prod_def by simp
show "norm x = 0 \<longleftrightarrow> x = 0"
unfolding norm_prod_def
by (simp add: prod_eq_iff)
--- a/src/HOL/Library/Product_plus.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Library/Product_plus.thy Wed Feb 13 11:46:48 2013 +0100
@@ -5,7 +5,7 @@
header {* Additive group operations on product types *}
theory Product_plus
-imports Main
+imports "~~/src/HOL/Main"
begin
subsection {* Operations *}
--- a/src/HOL/Library/RBT_Set.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Library/RBT_Set.thy Wed Feb 13 11:46:48 2013 +0100
@@ -63,8 +63,6 @@
lemma [code, code del]:
"Bex = Bex" ..
-term can_select
-
lemma [code, code del]:
"can_select = can_select" ..
@@ -526,6 +524,8 @@
code_datatype Set Coset
+declare set.simps[code]
+
lemma empty_Set [code]:
"Set.empty = Set RBT.empty"
by (auto simp: Set_def)
--- a/src/HOL/Limits.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Limits.thy Wed Feb 13 11:46:48 2013 +0100
@@ -832,6 +832,35 @@
"(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
using tendstoI tendstoD by fast
+lemma order_tendstoI:
+ fixes y :: "_ :: order_topology"
+ assumes "\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
+ assumes "\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
+ shows "(f ---> y) F"
+proof (rule topological_tendstoI)
+ fix S assume "open S" "y \<in> S"
+ then show "eventually (\<lambda>x. f x \<in> S) F"
+ unfolding open_generated_order
+ proof induct
+ case (UN K)
+ then obtain k where "y \<in> k" "k \<in> K" by auto
+ with UN(2)[of k] show ?case
+ by (auto elim: eventually_elim1)
+ qed (insert assms, auto elim: eventually_elim2)
+qed
+
+lemma order_tendstoD:
+ fixes y :: "_ :: order_topology"
+ assumes y: "(f ---> y) F"
+ shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
+ and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
+ using topological_tendstoD[OF y, of "{..< a}"] topological_tendstoD[OF y, of "{a <..}"] by auto
+
+lemma order_tendsto_iff:
+ fixes f :: "_ \<Rightarrow> 'a :: order_topology"
+ shows "(f ---> x) F \<longleftrightarrow>(\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
+ by (metis order_tendstoI order_tendstoD)
+
lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
by (simp only: tendsto_iff Zfun_def dist_norm)
@@ -901,6 +930,20 @@
using le_less_trans by (rule eventually_elim2)
qed
+lemma increasing_tendsto:
+ fixes f :: "_ \<Rightarrow> 'a::order_topology"
+ assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
+ and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
+ shows "(f ---> l) F"
+ using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
+
+lemma decreasing_tendsto:
+ fixes f :: "_ \<Rightarrow> 'a::order_topology"
+ assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
+ and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
+ shows "(f ---> l) F"
+ using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
+
subsubsection {* Distance and norms *}
lemma tendsto_dist [tendsto_intros]:
@@ -1002,22 +1045,21 @@
by (simp add: tendsto_const)
qed
-lemma real_tendsto_sandwich:
- fixes f g h :: "'a \<Rightarrow> real"
+lemma tendsto_sandwich:
+ fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
assumes lim: "(f ---> c) net" "(h ---> c) net"
shows "(g ---> c) net"
-proof -
- have "((\<lambda>n. g n - f n) ---> 0) net"
- proof (rule metric_tendsto_imp_tendsto)
- show "eventually (\<lambda>n. dist (g n - f n) 0 \<le> dist (h n - f n) 0) net"
- using ev by (rule eventually_elim2) (simp add: dist_real_def)
- show "((\<lambda>n. h n - f n) ---> 0) net"
- using tendsto_diff[OF lim(2,1)] by simp
- qed
- from tendsto_add[OF this lim(1)] show ?thesis by simp
+proof (rule order_tendstoI)
+ fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net"
+ using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
+next
+ fix a show "c < a \<Longrightarrow> eventually (\<lambda>x. g x < a) net"
+ using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
qed
+lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
+
subsubsection {* Linear operators and multiplication *}
lemma (in bounded_linear) tendsto:
@@ -1082,29 +1124,30 @@
by (simp add: tendsto_const)
qed
-lemma tendsto_le_const:
- fixes f :: "_ \<Rightarrow> real"
+lemma tendsto_le:
+ fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
assumes F: "\<not> trivial_limit F"
- assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
- shows "a \<le> x"
+ assumes x: "(f ---> x) F" and y: "(g ---> y) F"
+ assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
+ shows "y \<le> x"
proof (rule ccontr)
- assume "\<not> a \<le> x"
- with x have "eventually (\<lambda>x. f x < a) F"
- by (auto simp add: tendsto_def elim!: allE[of _ "{..< a}"])
- with a have "eventually (\<lambda>x. False) F"
- by eventually_elim auto
+ assume "\<not> y \<le> x"
+ with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} \<inter> {b<..} = {}"
+ by (auto simp: not_le)
+ then have "eventually (\<lambda>x. f x < a) F" "eventually (\<lambda>x. b < g x) F"
+ using x y by (auto intro: order_tendstoD)
+ with ev have "eventually (\<lambda>x. False) F"
+ by eventually_elim (insert xy, fastforce)
with F show False
by (simp add: eventually_False)
qed
-lemma tendsto_le:
- fixes f g :: "_ \<Rightarrow> real"
+lemma tendsto_le_const:
+ fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
assumes F: "\<not> trivial_limit F"
- assumes x: "(f ---> x) F" and y: "(g ---> y) F"
- assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
- shows "y \<le> x"
- using tendsto_le_const[OF F tendsto_diff[OF x y], of 0] ev
- by (simp add: sign_simps)
+ assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
+ shows "a \<le> x"
+ using F x tendsto_const a by (rule tendsto_le)
subsubsection {* Inverse and division *}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Feb 13 11:46:48 2013 +0100
@@ -456,13 +456,14 @@
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
fun failed failure =
- ({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
+ ({outcome = SOME failure, used_facts = [], used_from = [],
+ run_time = Time.zeroTime,
preplay = Lazy.value (Sledgehammer_Reconstruct.Failed_to_Play
Sledgehammer_Provers.plain_metis),
message = K "", message_tail = ""}, ~1)
- val ({outcome, used_facts, run_time, preplay, message, message_tail}
+ val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
: Sledgehammer_Provers.prover_result,
- time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
+ time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
let
val _ = if is_appropriate_prop concl_t then ()
else raise Fail "inappropriate"
@@ -473,25 +474,20 @@
Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
hyp_ts concl_t
+ val factss =
+ facts
|> filter (is_appropriate_prop o prop_of o snd)
|> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
(the_default default_max_facts max_facts)
Sledgehammer_Fact.no_fact_override hyp_ts concl_t
- |> map (apfst (apfst (fn name => name ())))
- |> tap (fn facts =>
+ |> tap (fn factss =>
"Line " ^ str0 (Position.line_of pos) ^ ": " ^
- (if null facts then
- "Found no relevant facts."
- else
- "Including " ^ string_of_int (length facts) ^
- " relevant fact(s):\n" ^
- (facts |> map (fst o fst) |> space_implode " ") ^ ".")
+ Sledgehammer_Run.string_of_factss factss
|> Output.urgent_message)
val prover = get_prover ctxt prover_name params goal facts
val problem =
{state = st', goal = goal, subgoal = i,
- subgoal_count = Sledgehammer_Util.subgoal_count st,
- facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
+ subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss}
in prover params (K (K (K ""))) problem end)) ()
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Feb 13 11:46:48 2013 +0100
@@ -136,7 +136,7 @@
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params
default_prover (the_default default_max_facts max_facts)
(SOME relevance_fudge) hyp_ts concl_t
- |> map ((fn name => name ()) o fst o fst)
+ |> map (fst o fst)
val (found_facts, lost_facts) =
flat proofs |> sort_distinct string_ord
|> map (fn fact => (find_index (curry (op =) fact) facts, fact))
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Feb 13 11:46:48 2013 +0100
@@ -1,4 +1,3 @@
-
header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}
theory Cartesian_Euclidean_Space
@@ -828,7 +827,7 @@
lemma compact_lemma_cart:
fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
- assumes "bounded s" and "\<forall>n. f n \<in> s"
+ assumes f: "bounded (range f)"
shows "\<forall>d.
\<exists>l r. subseq r \<and>
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
@@ -842,16 +841,17 @@
thus ?case unfolding subseq_def by auto
next
case (insert k d)
- have s': "bounded ((\<lambda>x. x $ k) ` s)"
- using `bounded s` by (rule bounded_component_cart)
obtain l1::"'a^'n" and r1 where r1:"subseq r1"
and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
using insert(3) by auto
- have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` s"
- using `\<forall>n. f n \<in> s` by simp
- obtain l2 r2 where r2: "subseq r2"
+ have s': "bounded ((\<lambda>x. x $ k) ` range f)" using `bounded (range f)`
+ by (auto intro!: bounded_component_cart)
+ have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` range f" by simp
+ have "bounded (range (\<lambda>i. f (r1 i) $ k))"
+ by (metis (lifting) bounded_subset image_subsetI f' s')
+ then obtain l2 r2 where r2: "subseq r2"
and lr2: "((\<lambda>i. f (r1 (r2 i)) $ k) ---> l2) sequentially"
- using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
+ using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) $ k"] by (auto simp: o_def)
def r \<equiv> "r1 \<circ> r2"
have r: "subseq r"
using r1 and r2 unfolding r_def o_def subseq_def by auto
@@ -873,11 +873,11 @@
instance vec :: (heine_borel, finite) heine_borel
proof
- fix s :: "('a ^ 'b) set" and f :: "nat \<Rightarrow> 'a ^ 'b"
- assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
+ fix f :: "nat \<Rightarrow> 'a ^ 'b"
+ assume f: "bounded (range f)"
then obtain l r where r: "subseq r"
and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
- using compact_lemma_cart [OF s f] by blast
+ using compact_lemma_cart [OF f] by blast
let ?d = "UNIV::'b set"
{ fix e::real assume "e>0"
hence "0 < e / (real_of_nat (card ?d))"
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Wed Feb 13 11:46:48 2013 +0100
@@ -288,16 +288,9 @@
assumes lim:"f ----> (l :: ereal)"
and ge: "ALL n>=N. f n >= C"
shows "l>=C"
-proof -
- def g == "(%i. -(f i))"
- { fix n
- assume "n>=N"
- then have "g n <= -C" using assms ereal_minus_le_minus g_def by auto }
- then have "ALL n>=N. g n <= -C" by auto
- moreover have limg: "g ----> (-l)" using g_def ereal_lim_uminus lim by auto
- ultimately have "-l <= -C" using Lim_bounded_ereal[of g "-l" _ "-C"] by auto
- then show ?thesis using ereal_minus_le_minus by auto
-qed
+ using ge
+ by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
+ (auto simp: eventually_sequentially)
lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
proof
@@ -326,54 +319,69 @@
fixes f :: "'a => ereal"
shows "Liminf net f =
Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
- unfolding Liminf_Sup
-proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
- fix l S
- assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono_set S" "l \<in> S"
- then have "S = UNIV \<or> S = {Inf S <..}"
- using ereal_open_mono_set[of S] by auto
- then show "eventually (\<lambda>x. f x \<in> S) net"
- proof
- assume S: "S = {Inf S<..}"
- then have "Inf S < l" using `l \<in> S` by auto
- then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto
- then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
- qed auto
+ (is "_ = Sup ?A")
+proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
+ fix P assume P: "eventually P net"
+ fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
+ { fix x assume "P x"
+ then have "INFI (Collect P) f \<le> f x"
+ by (intro complete_lattice_class.INF_lower) simp
+ with S have "f x \<in> S"
+ by (simp add: mono_set) }
+ with P show "eventually (\<lambda>x. f x \<in> S) net"
+ by (auto elim: eventually_elim1)
next
- fix l y
- assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "y < l"
- have "eventually (\<lambda>x. f x \<in> {y <..}) net"
- using `y < l` by (intro S[rule_format]) auto
- then show "eventually (\<lambda>x. y < f x) net" by auto
+ fix y l
+ assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
+ assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
+ show "l \<le> y"
+ proof (rule ereal_le_ereal)
+ fix B assume "B < l"
+ then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
+ by (intro S[rule_format]) auto
+ then have "INFI {x. B < f x} f \<le> y"
+ using P by auto
+ moreover have "B \<le> INFI {x. B < f x} f"
+ by (intro INF_greatest) auto
+ ultimately show "B \<le> y"
+ by simp
+ qed
qed
lemma ereal_Limsup_Inf_monoset:
fixes f :: "'a => ereal"
shows "Limsup net f =
Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
- unfolding Limsup_Inf
-proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
- fix l S
- assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono_set (uminus`S)" "l \<in> S"
- then have "open (uminus`S) \<and> mono_set (uminus`S)" by (simp add: ereal_open_uminus)
- then have "S = UNIV \<or> S = {..< Sup S}"
- unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp
- then show "eventually (\<lambda>x. f x \<in> S) net"
- proof
- assume S: "S = {..< Sup S}"
- then have "l < Sup S" using `l \<in> S` by auto
- then have "eventually (\<lambda>x. f x < Sup S) net" using ev by auto
- then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
- qed auto
+ (is "_ = Inf ?A")
+proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
+ fix P assume P: "eventually P net"
+ fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
+ { fix x assume "P x"
+ then have "f x \<le> SUPR (Collect P) f"
+ by (intro complete_lattice_class.SUP_upper) simp
+ with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
+ have "f x \<in> S"
+ by (simp add: inj_image_mem_iff) }
+ with P show "eventually (\<lambda>x. f x \<in> S) net"
+ by (auto elim: eventually_elim1)
next
- fix l y
- assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "l < y"
- have "eventually (\<lambda>x. f x \<in> {..< y}) net"
- using `l < y` by (intro S[rule_format]) auto
- then show "eventually (\<lambda>x. f x < y) net" by auto
+ fix y l
+ assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
+ assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
+ show "y \<le> l"
+ proof (rule ereal_ge_ereal, safe)
+ fix B assume "l < B"
+ then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
+ by (intro S[rule_format]) auto
+ then have "y \<le> SUPR {x. f x < B} f"
+ using P by auto
+ moreover have "SUPR {x. f x < B} f \<le> B"
+ by (intro SUP_least) auto
+ ultimately show "y \<le> B"
+ by simp
+ qed
qed
-
lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)"
using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto
@@ -434,21 +442,16 @@
shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
proof (intro lim_imp_Liminf iffI assms)
assume rhs: "Liminf net f = \<infinity>"
- { fix S :: "ereal set"
- assume "open S & \<infinity> : S"
- then obtain m where "{ereal m<..} <= S" using open_PInfty2 by auto
- moreover
- have "eventually (\<lambda>x. f x \<in> {ereal m<..}) net"
- using rhs
- unfolding Liminf_Sup top_ereal_def[symmetric] Sup_eq_top_iff
- by (auto elim!: allE[where x="ereal m"] simp: top_ereal_def)
- ultimately
- have "eventually (%x. f x : S) net"
- apply (subst eventually_mono)
- apply auto
- done
- }
- then show "(f ---> \<infinity>) net" unfolding tendsto_def by auto
+ show "(f ---> \<infinity>) net"
+ unfolding tendsto_PInfty
+ proof
+ fix r :: real
+ have "ereal r < top" unfolding top_ereal_def by simp
+ with rhs obtain P where "eventually P net" "r < INFI (Collect P) f"
+ unfolding Liminf_def SUP_eq_top_iff top_ereal_def[symmetric] by auto
+ then show "eventually (\<lambda>x. ereal r < f x) net"
+ by (auto elim!: eventually_elim1 dest: less_INF_D)
+ qed
qed
lemma Limsup_MInfty:
@@ -474,12 +477,12 @@
show "(f ---> f0) net"
proof (rule topological_tendstoI)
fix S
- assume "open S""f0 \<in> S"
+ assume "open S" "f0 \<in> S"
then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
using ereal_open_cont_interval2[of S f0] real lim by auto
then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
- unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff
- by (auto intro!: eventually_conj)
+ unfolding Liminf_def Limsup_def less_SUP_iff INF_less_iff
+ by (auto intro!: eventually_conj elim: eventually_elim1 dest: less_INF_D SUP_lessD)
with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
by (rule_tac eventually_mono) auto
qed
@@ -518,7 +521,7 @@
assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
and "X ----> x" "Y ----> y"
shows "x <= y"
- by (metis ereal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)
+ using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
lemma incseq_le_ereal:
fixes X :: "nat \<Rightarrow> ereal"
@@ -577,114 +580,24 @@
by (metis abs_less_iff assms leI le_max_iff_disj
less_eq_real_def less_le_not_le less_minus_iff minus_minus)
-lemma bounded_increasing_convergent2:
- fixes f::"nat => real"
- assumes "ALL n. f n <= B" "ALL n m. n>=m --> f n >= f m"
- shows "EX l. (f ---> l) sequentially"
-proof -
- def N == "max (abs (f 0)) (abs B)"
- { fix n
- have "abs (f n) <= N"
- unfolding N_def
- apply (subst bounded_abs)
- using assms apply auto
- done }
- then have "bounded {f n| n::nat. True}"
- unfolding bounded_real by auto
- then show ?thesis
- apply (rule Topology_Euclidean_Space.bounded_increasing_convergent)
- using assms apply auto
- done
-qed
-
lemma lim_ereal_increasing:
- assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
- obtains l where "f ----> (l::ereal)"
-proof (cases "f = (\<lambda>x. - \<infinity>)")
- case True
- then show thesis
- using tendsto_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
-next
- case False
- then obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
- have "ALL n>=N. f n >= f N" using assms by auto
- then have minf: "ALL n>=N. f n > (-\<infinity>)" using N_def by auto
- def Y == "(%n. (if n>=N then f n else f N))"
- then have incy: "!!n m. n>=m ==> Y n >= Y m" using assms by auto
- from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto
- show thesis
- proof (cases "EX B. ALL n. f n < ereal B")
- case False
- then show thesis
- apply -
- apply (rule that[of \<infinity>])
- unfolding Lim_PInfty not_ex not_all
- apply safe
- apply (erule_tac x=B in allE, safe)
- apply (rule_tac x=x in exI, safe)
- apply (rule order_trans[OF _ assms[rule_format]])
- apply auto
- done
- next
- case True
- then guess B ..
- then have "ALL n. Y n < ereal B" using Y_def by auto
- note B = this[rule_format]
- { fix n
- have "Y n < \<infinity>"
- using B[of n]
- apply (subst less_le_trans)
- apply auto
- done
- then have "Y n ~= \<infinity> & Y n ~= (-\<infinity>)" using minfy by auto
- }
- then have *: "ALL n. \<bar>Y n\<bar> \<noteq> \<infinity>" by auto
- { fix n
- have "real (Y n) < B"
- proof -
- case goal1
- then show ?case
- using B[of n] apply-apply(subst(asm) ereal_real'[THEN sym]) defer defer
- unfolding ereal_less using * by auto
- qed
- }
- then have B': "ALL n. (real (Y n) <= B)" using less_imp_le by auto
- have "EX l. (%n. real (Y n)) ----> l"
- apply (rule bounded_increasing_convergent2)
- proof safe
- show "\<And>n. real (Y n) <= B" using B' by auto
- fix n m :: nat
- assume "n<=m"
- then have "ereal (real (Y n)) <= ereal (real (Y m))"
- using incy[rule_format,of n m] apply(subst ereal_real)+
- using *[rule_format, of n] *[rule_format, of m] by auto
- then show "real (Y n) <= real (Y m)" by auto
- qed
- then guess l .. note l=this
- have "Y ----> ereal l"
- using l
- apply -
- apply (subst(asm) lim_ereal[THEN sym])
- unfolding ereal_real
- using * apply auto
- done
- then show thesis
- apply -
- apply (rule that[of "ereal l"])
- apply (subst tail_same_limit[of Y _ N])
- using Y_def apply auto
- done
- qed
+ assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
+ obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
+proof
+ show "f ----> (SUP n. f n)"
+ using assms
+ by (intro increasing_tendsto)
+ (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
qed
lemma lim_ereal_decreasing:
- assumes "\<And>n m. n >= m \<Longrightarrow> f n <= f m"
- obtains l where "f ----> (l::ereal)"
-proof -
- from lim_ereal_increasing[of "\<lambda>x. - f x"] assms
- obtain l where "(\<lambda>x. - f x) ----> l" by auto
- from ereal_lim_mult[OF this, of "- 1"] show thesis
- by (intro that[of "-l"]) (simp add: ereal_uminus_eq_reorder)
+ assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
+ obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
+proof
+ show "f ----> (INF n. f n)"
+ using assms
+ by (intro decreasing_tendsto)
+ (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
qed
lemma compact_ereal:
@@ -711,37 +624,17 @@
by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
lemma SUP_Lim_ereal:
- fixes X :: "nat \<Rightarrow> ereal"
- assumes "incseq X" "X ----> l"
+ fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
+ assumes inc: "incseq X" and l: "X ----> l"
shows "(SUP n. X n) = l"
-proof (rule ereal_SUPI)
- fix n from assms show "X n \<le> l"
- by (intro incseq_le_ereal) (simp add: incseq_def)
-next
- fix y assume "\<And>n. n \<in> UNIV \<Longrightarrow> X n \<le> y"
- with ereal_Sup_lim[OF _ `X ----> l`, of "{..y}"] show "l \<le> y" by auto
-qed
-
-lemma LIMSEQ_ereal_SUPR:
- fixes X :: "nat \<Rightarrow> ereal"
- assumes "incseq X"
- shows "X ----> (SUP n. X n)"
-proof (rule lim_ereal_increasing)
- fix n m :: nat
- assume "m \<le> n"
- then show "X m \<le> X n" using `incseq X` by (simp add: incseq_def)
-next
- fix l
- assume "X ----> l"
- with SUP_Lim_ereal[of X, OF assms this] show ?thesis by simp
-qed
+ using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] by simp
lemma INF_Lim_ereal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::ereal)"
using SUP_Lim_ereal[of "\<lambda>i. - X i" "- l"]
by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
lemma LIMSEQ_ereal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: ereal)"
- using LIMSEQ_ereal_SUPR[of "\<lambda>i. - X i"]
+ using LIMSEQ_SUP[of "\<lambda>i. - X i"]
by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
lemma SUP_eq_LIMSEQ:
@@ -755,165 +648,66 @@
from SUP_Lim_ereal[OF inc this]
show "(SUP n. ereal (f n)) = ereal x" . }
{ assume "(SUP n. ereal (f n)) = ereal x"
- with LIMSEQ_ereal_SUPR[OF inc]
+ with LIMSEQ_SUP[OF inc]
show "f ----> x" by auto }
qed
lemma Liminf_within:
- fixes f :: "'a::metric_space => ereal"
- shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
-proof -
- let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
- { fix T
- assume T_def: "open T & mono_set T & ?l:T"
- have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
- proof -
- { assume "T=UNIV" then have ?thesis by (simp add: gt_ex) }
- moreover
- { assume "~(T=UNIV)"
- then obtain B where "T={B<..}" using T_def ereal_open_mono_set[of T] by auto
- then have "B<?l" using T_def by auto
- then obtain d where d_def: "0<d & B<(INF y:(S Int ball x d - {x}). f y)"
- unfolding less_SUP_iff by auto
- { fix y assume "y:S & 0 < dist y x & dist y x < d"
- then have "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
- then have "f y:T" using d_def INF_lower[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
- } then have ?thesis apply(rule_tac x="d" in exI) using d_def by auto
- }
- ultimately show ?thesis by auto
- qed
- }
- moreover
- { fix z
- assume a: "ALL T. open T --> mono_set T --> z : T -->
- (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
- { fix B
- assume "B<z"
- then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
- using a[rule_format, of "{B<..}"] mono_greaterThan by auto
- { fix y
- assume "y:(S Int ball x d - {x})"
- then have "y:S & 0 < dist y x & dist y x < d"
- unfolding ball_def
- apply (simp add: dist_commute)
- apply (metis dist_eq_0_iff less_le zero_le_dist)
- done
- then have "B <= f y" using d_def by auto
- }
- then have "B <= INFI (S Int ball x d - {x}) f"
- apply (subst INF_greatest)
- apply auto
- done
- also have "...<=?l"
- apply (subst SUP_upper)
- using d_def apply auto
- done
- finally have "B<=?l" by auto
- }
- then have "z <= ?l" using ereal_le_ereal[of z "?l"] by auto
- }
- ultimately show ?thesis
- unfolding ereal_Liminf_Sup_monoset eventually_within
- apply (subst ereal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e - {x}) f)"])
- apply auto
- done
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
+ shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
+ unfolding Liminf_def eventually_within
+proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
+ fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+ then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
+ by (auto simp: zero_less_dist_iff dist_commute)
+ then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
+ by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
+next
+ fix d :: real assume "0 < d"
+ then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+ INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
+ by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
+ (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
qed
lemma Limsup_within:
- fixes f :: "'a::metric_space => ereal"
- shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
-proof -
- let ?l = "(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
- { fix T
- assume T_def: "open T & mono_set (uminus ` T) & ?l:T"
- have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
- proof -
- { assume "T = UNIV"
- then have ?thesis by (simp add: gt_ex) }
- moreover
- { assume "T \<noteq> UNIV"
- then have "~(uminus ` T = UNIV)"
- by (metis Int_UNIV_right Int_absorb1 image_mono ereal_minus_minus_image subset_UNIV)
- then have "uminus ` T = {Inf (uminus ` T)<..}"
- using T_def ereal_open_mono_set[of "uminus ` T"] ereal_open_uminus[of T] by auto
- then obtain B where "T={..<B}"
- unfolding ereal_Inf_uminus_image_eq ereal_uminus_lessThan[symmetric]
- unfolding inj_image_eq_iff[OF ereal_inj_on_uminus] by simp
- then have "?l<B" using T_def by auto
- then obtain d where d_def: "0<d & (SUP y:(S Int ball x d - {x}). f y)<B"
- unfolding INF_less_iff by auto
- { fix y
- assume "y:S & 0 < dist y x & dist y x < d"
- then have "y:(S Int ball x d - {x})"
- unfolding ball_def by (auto simp add: dist_commute)
- then have "f y:T"
- using d_def SUP_upper[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
- }
- then have ?thesis
- apply (rule_tac x="d" in exI)
- using d_def apply auto
- done
- }
- ultimately show ?thesis by auto
- qed
- }
- moreover
- { fix z
- assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T -->
- (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
- { fix B
- assume "z<B"
- then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"
- using a[rule_format, of "{..<B}"] by auto
- { fix y
- assume "y:(S Int ball x d - {x})"
- then have "y:S & 0 < dist y x & dist y x < d"
- unfolding ball_def
- apply (simp add: dist_commute)
- apply (metis dist_eq_0_iff less_le zero_le_dist)
- done
- then have "f y <= B" using d_def by auto
- }
- then have "SUPR (S Int ball x d - {x}) f <= B"
- apply (subst SUP_least)
- apply auto
- done
- moreover
- have "?l<=SUPR (S Int ball x d - {x}) f"
- apply (subst INF_lower)
- using d_def apply auto
- done
- ultimately have "?l<=B" by auto
- } then have "?l <= z" using ereal_ge_ereal[of z "?l"] by auto
- }
- ultimately show ?thesis
- unfolding ereal_Limsup_Inf_monoset eventually_within
- apply (subst ereal_InfI)
- apply auto
- done
+ fixes f :: "'a::metric_space => 'b::complete_lattice"
+ shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
+ unfolding Limsup_def eventually_within
+proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
+ fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+ then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
+ by (auto simp: zero_less_dist_iff dist_commute)
+ then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
+ by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
+next
+ fix d :: real assume "0 < d"
+ then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+ SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
+ by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
+ (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
qed
-
lemma Liminf_within_UNIV:
- fixes f :: "'a::metric_space => ereal"
+ fixes f :: "'a::metric_space => _"
shows "Liminf (at x) f = Liminf (at x within UNIV) f"
by simp (* TODO: delete *)
lemma Liminf_at:
- fixes f :: "'a::metric_space => ereal"
+ fixes f :: "'a::metric_space => _"
shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
using Liminf_within[of x UNIV f] by simp
lemma Limsup_within_UNIV:
- fixes f :: "'a::metric_space => ereal"
+ fixes f :: "'a::metric_space => _"
shows "Limsup (at x) f = Limsup (at x within UNIV) f"
by simp (* TODO: delete *)
lemma Limsup_at:
- fixes f :: "'a::metric_space => ereal"
+ fixes f :: "'a::metric_space => _"
shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
using Limsup_within[of x UNIV f] by simp
@@ -1295,7 +1089,7 @@
proof -
have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)
- from LIMSEQ_ereal_SUPR[OF this]
+ from LIMSEQ_SUP[OF this]
show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)
qed
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Feb 13 11:46:48 2013 +0100
@@ -387,9 +387,6 @@
instance proof
fix a :: real and x y :: "'a ^ 'b"
- show "0 \<le> norm x"
- unfolding norm_vec_def
- by (rule setL2_nonneg)
show "norm x = 0 \<longleftrightarrow> x = 0"
unfolding norm_vec_def
by (simp add: setL2_eq_0_iff vec_eq_iff)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Feb 13 11:46:48 2013 +0100
@@ -47,6 +47,17 @@
definition "topological_basis B =
((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x)))"
+lemma "topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x))"
+ unfolding topological_basis_def
+ apply safe
+ apply fastforce
+ apply fastforce
+ apply (erule_tac x="x" in allE)
+ apply simp
+ apply (rule_tac x="{x}" in exI)
+ apply auto
+ done
+
lemma topological_basis_iff:
assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
shows "topological_basis B \<longleftrightarrow> (\<forall>O'. open O' \<longrightarrow> (\<forall>x\<in>O'. \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'))"
@@ -2143,6 +2154,9 @@
bounded :: "'a set \<Rightarrow> bool" where
"bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
+lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e)"
+ unfolding bounded_def subset_eq by auto
+
lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
unfolding bounded_def
apply safe
@@ -3202,16 +3216,16 @@
class heine_borel = metric_space +
assumes bounded_imp_convergent_subsequence:
- "bounded s \<Longrightarrow> \<forall>n. f n \<in> s
- \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ "bounded (range f) \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
lemma bounded_closed_imp_seq_compact:
fixes s::"'a::heine_borel set"
assumes "bounded s" and "closed s" shows "seq_compact s"
proof (unfold seq_compact_def, clarify)
fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
+ with `bounded s` have "bounded (range f)" by (auto intro: bounded_subset)
obtain l r where r: "subseq r" and l: "((f \<circ> r) ---> l) sequentially"
- using bounded_imp_convergent_subsequence [OF `bounded s` `\<forall>n. f n \<in> s`] by auto
+ using bounded_imp_convergent_subsequence [OF `bounded (range f)`] by auto
from f have fr: "\<forall>n. (f \<circ> r) n \<in> s" by simp
have "l \<in> s" using `closed s` fr l
unfolding closed_sequential_limits by blast
@@ -3239,20 +3253,20 @@
instance real :: heine_borel
proof
- fix s :: "real set" and f :: "nat \<Rightarrow> real"
- assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
+ fix f :: "nat \<Rightarrow> real"
+ assume f: "bounded (range f)"
obtain r where r: "subseq r" "monoseq (f \<circ> r)"
unfolding comp_def by (metis seq_monosub)
moreover
then have "Bseq (f \<circ> r)"
- unfolding Bseq_eq_bounded using s f by (auto intro: bounded_subset)
+ unfolding Bseq_eq_bounded using f by (auto intro: bounded_subset)
ultimately show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
qed
lemma compact_lemma:
fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
- assumes "bounded s" and "\<forall>n. f n \<in> s"
+ assumes "bounded (range f)"
shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. subseq r \<and>
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
proof safe
@@ -3262,14 +3276,16 @@
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
proof(induct d) case empty thus ?case unfolding subseq_def by auto
next case (insert k d) have k[intro]:"k\<in>Basis" using insert by auto
- have s': "bounded ((\<lambda>x. x \<bullet> k) ` s)" using `bounded s`
+ have s': "bounded ((\<lambda>x. x \<bullet> k) ` range f)" using `bounded (range f)`
by (auto intro!: bounded_linear_image bounded_linear_inner_left)
obtain l1::"'a" and r1 where r1:"subseq r1" and
lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
using insert(3) using insert(4) by auto
- have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` s" using `\<forall>n. f n \<in> s` by simp
- obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) ---> l2) sequentially"
- using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
+ have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` range f" by simp
+ have "bounded (range (\<lambda>i. f (r1 i) \<bullet> k))"
+ by (metis (lifting) bounded_subset f' image_subsetI s')
+ then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) ---> l2) sequentially"
+ using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \<bullet> k"] by (auto simp: o_def)
def r \<equiv> "r1 \<circ> r2" have r:"subseq r"
using r1 and r2 unfolding r_def o_def subseq_def by auto
moreover
@@ -3289,11 +3305,11 @@
instance euclidean_space \<subseteq> heine_borel
proof
- fix s :: "'a set" and f :: "nat \<Rightarrow> 'a"
- assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
+ fix f :: "nat \<Rightarrow> 'a"
+ assume f: "bounded (range f)"
then obtain l::'a and r where r: "subseq r"
and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
- using compact_lemma [OF s f] by blast
+ using compact_lemma [OF f] by blast
{ fix e::real assume "e>0"
hence "0 < e / real_of_nat DIM('a)" by (auto intro!: divide_pos_pos DIM_positive)
with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
@@ -3338,19 +3354,16 @@
instance prod :: (heine_borel, heine_borel) heine_borel
proof
- fix s :: "('a * 'b) set" and f :: "nat \<Rightarrow> 'a * 'b"
- assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
- from s have s1: "bounded (fst ` s)" by (rule bounded_fst)
- from f have f1: "\<forall>n. fst (f n) \<in> fst ` s" by simp
- obtain l1 r1 where r1: "subseq r1"
- and l1: "((\<lambda>n. fst (f (r1 n))) ---> l1) sequentially"
- using bounded_imp_convergent_subsequence [OF s1 f1]
- unfolding o_def by fast
- from s have s2: "bounded (snd ` s)" by (rule bounded_snd)
- from f have f2: "\<forall>n. snd (f (r1 n)) \<in> snd ` s" by simp
+ fix f :: "nat \<Rightarrow> 'a \<times> 'b"
+ assume f: "bounded (range f)"
+ from f have s1: "bounded (range (fst \<circ> f))" unfolding image_comp by (rule bounded_fst)
+ obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) ----> l1"
+ using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
+ from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
+ by (auto simp add: image_comp intro: bounded_snd bounded_subset)
obtain l2 r2 where r2: "subseq r2"
and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) ---> l2) sequentially"
- using bounded_imp_convergent_subsequence [OF s2 f2]
+ using bounded_imp_convergent_subsequence [OF s2]
unfolding o_def by fast
have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially"
using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
--- a/src/HOL/Probability/Discrete_Topology.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy Wed Feb 13 11:46:48 2013 +0100
@@ -3,7 +3,7 @@
*)
theory Discrete_Topology
-imports Multivariate_Analysis
+imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
begin
text {* Copy of discrete types with discrete topology. This space is polish. *}
--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Wed Feb 13 11:46:48 2013 +0100
@@ -297,7 +297,7 @@
qed
next
fix x show "(SUP i. ?g i x) = max 0 (u x)"
- proof (rule ereal_SUPI)
+ proof (rule SUP_eqI)
fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
mult_nonpos_nonneg mult_nonneg_nonneg)
@@ -2147,7 +2147,7 @@
assume neq_0: "(\<integral>\<^isup>+ x. max 0 (ereal (2 * w x)) \<partial>M) \<noteq> 0" (is "?wx \<noteq> 0")
have "0 = limsup (\<lambda>n. 0 :: ereal)" by (simp add: Limsup_const)
also have "\<dots> \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
- by (intro limsup_mono positive_integral_positive)
+ by (simp add: Limsup_mono positive_integral_positive)
finally have pos: "0 \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)" .
have "?wx = (\<integral>\<^isup>+ x. liminf (\<lambda>n. max 0 (ereal (?diff n x))) \<partial>M)"
using u'
@@ -2178,11 +2178,11 @@
qed
have "liminf ?f \<le> limsup ?f"
- by (intro ereal_Liminf_le_Limsup trivial_limit_sequentially)
+ by (intro Liminf_le_Limsup trivial_limit_sequentially)
moreover
{ have "0 = liminf (\<lambda>n. 0 :: ereal)" by (simp add: Liminf_const)
also have "\<dots> \<le> liminf ?f"
- by (intro liminf_mono positive_integral_positive)
+ by (simp add: Liminf_mono positive_integral_positive)
finally have "0 \<le> liminf ?f" . }
ultimately have liminf_limsup_eq: "liminf ?f = ereal 0" "limsup ?f = ereal 0"
using `limsup ?f = 0` by auto
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Feb 13 11:46:48 2013 +0100
@@ -698,7 +698,7 @@
have "integral\<^isup>P lebesgue f = ereal (integral UNIV f')"
proof (rule tendsto_unique[OF trivial_limit_sequentially])
have "(\<lambda>i. integral\<^isup>S lebesgue (u i)) ----> (SUP i. integral\<^isup>P lebesgue (u i))"
- unfolding u_eq by (intro LIMSEQ_ereal_SUPR incseq_positive_integral u)
+ unfolding u_eq by (intro LIMSEQ_SUP incseq_positive_integral u)
also note positive_integral_monotone_convergence_SUP
[OF u(2) borel_measurable_simple_function[OF u(1)] u(5), symmetric]
finally show "(\<lambda>k. integral\<^isup>S lebesgue (u k)) ----> integral\<^isup>P lebesgue f"
--- a/src/HOL/Probability/Measure_Space.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Wed Feb 13 11:46:48 2013 +0100
@@ -50,7 +50,7 @@
then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: ereal)"
by (auto simp: setsum_cases)
moreover have "(SUP n. if i < n then f i else 0) = (f i :: ereal)"
- proof (rule ereal_SUPI)
+ proof (rule SUP_eqI)
fix y :: ereal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
from this[of "Suc i"] show "f i \<le> y" by auto
qed (insert assms, simp)
@@ -523,7 +523,7 @@
lemma SUP_emeasure_incseq:
assumes A: "range A \<subseteq> sets M" "incseq A"
shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
- using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
+ using LIMSEQ_SUP[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
by (simp add: LIMSEQ_unique)
lemma decseq_emeasure:
@@ -1570,7 +1570,7 @@
have "incseq (\<lambda>i. ?M (F i))"
using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
then have "(\<lambda>i. ?M (F i)) ----> (SUP n. ?M (F n))"
- by (rule LIMSEQ_ereal_SUPR)
+ by (rule LIMSEQ_SUP)
moreover have "(SUP n. ?M (F n)) = \<infinity>"
proof (rule SUP_PInfty)
--- a/src/HOL/Probability/Regularity.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Probability/Regularity.thy Wed Feb 13 11:46:48 2013 +0100
@@ -16,7 +16,7 @@
assumes f_nonneg: "\<And>i. 0 \<le> f i"
assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
shows "x = (SUP i : A. f i)"
-proof (subst eq_commute, rule ereal_SUPI)
+proof (subst eq_commute, rule SUP_eqI)
show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
next
fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
@@ -45,7 +45,7 @@
assumes f_nonneg: "\<And>i. 0 \<le> f i"
assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
shows "x = (INF i : A. f i)"
-proof (subst eq_commute, rule ereal_INFI)
+proof (subst eq_commute, rule INF_eqI)
show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
next
fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
@@ -79,7 +79,7 @@
from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
ultimately
have "(INF i : A. f i) = x + e" using `e > 0`
- by (intro ereal_INFI)
+ by (intro INF_eqI)
(force, metis add.comm_neutral add_left_mono ereal_less(1)
linorder_not_le not_less_iff_gr_or_eq)
thus False using assms by auto
@@ -97,7 +97,7 @@
from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
ultimately
have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
- by (intro ereal_SUPI)
+ by (intro SUP_eqI)
(metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
thus False using assms by auto
@@ -290,7 +290,7 @@
have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
ultimately show ?thesis by simp
- qed (auto intro!: ereal_INFI)
+ qed (auto intro!: INF_eqI)
note `?inner A` `?outer A` }
note closed_in_D = this
from `B \<in> sets borel`
@@ -299,8 +299,8 @@
then show "?inner B" "?outer B"
proof (induct B rule: sigma_sets_induct_disjoint)
case empty
- { case 1 show ?case by (intro ereal_SUPI[symmetric]) auto }
- { case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
+ { case 1 show ?case by (intro SUP_eqI[symmetric]) auto }
+ { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
next
case (basic B)
{ case 1 from basic closed_in_D show ?case by auto }
--- a/src/HOL/RealVector.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/RealVector.thy Wed Feb 13 11:46:48 2013 +0100
@@ -508,6 +508,56 @@
end
+inductive generate_topology for S where
+ UNIV: "generate_topology S UNIV"
+| Int: "generate_topology S a \<Longrightarrow> generate_topology S b \<Longrightarrow> generate_topology S (a \<inter> b)"
+| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)"
+| Basis: "s \<in> S \<Longrightarrow> generate_topology S s"
+
+hide_fact (open) UNIV Int UN Basis
+
+lemma generate_topology_Union:
+ "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
+ unfolding SUP_def by (intro generate_topology.UN) auto
+
+lemma topological_space_generate_topology:
+ "class.topological_space (generate_topology S)"
+ by default (auto intro: generate_topology.intros)
+
+class order_topology = order + "open" +
+ assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
+begin
+
+subclass topological_space
+ unfolding open_generated_order
+ by (rule topological_space_generate_topology)
+
+lemma open_greaterThan [simp]: "open {a <..}"
+ unfolding open_generated_order by (auto intro: generate_topology.Basis)
+
+lemma open_lessThan [simp]: "open {..< a}"
+ unfolding open_generated_order by (auto intro: generate_topology.Basis)
+
+lemma open_greaterThanLessThan [simp]: "open {a <..< b}"
+ unfolding greaterThanLessThan_eq by (simp add: open_Int)
+
+end
+
+class linorder_topology = linorder + order_topology
+
+lemma closed_atMost [simp]: "closed {.. a::'a::linorder_topology}"
+ by (simp add: closed_open)
+
+lemma closed_atLeast [simp]: "closed {a::'a::linorder_topology ..}"
+ by (simp add: closed_open)
+
+lemma closed_atLeastAtMost [simp]: "closed {a::'a::linorder_topology .. b}"
+proof -
+ have "{a .. b} = {a ..} \<inter> {.. b}"
+ by auto
+ then show ?thesis
+ by (simp add: closed_Int)
+qed
subsection {* Metric spaces *}
@@ -621,10 +671,20 @@
assumes dist_norm: "dist x y = norm (x - y)"
class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
- assumes norm_ge_zero [simp]: "0 \<le> norm x"
- and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
+ assumes norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
+begin
+
+lemma norm_ge_zero [simp]: "0 \<le> norm x"
+proof -
+ have "0 = norm (x + -1 *\<^sub>R x)"
+ using scaleR_add_left[of 1 "-1" x] norm_scaleR[of 0 x] by (simp add: scaleR_one)
+ also have "\<dots> \<le> norm x + norm (-1 *\<^sub>R x)" by (rule norm_triangle_ineq)
+ finally show ?thesis by simp
+qed
+
+end
class real_normed_algebra = real_algebra + real_normed_vector +
assumes norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
@@ -850,7 +910,6 @@
apply (rule dist_real_def)
apply (rule open_real_def)
apply (simp add: sgn_real_def)
-apply (rule abs_ge_zero)
apply (rule abs_eq_0)
apply (rule abs_triangle_ineq)
apply (rule abs_mult)
@@ -859,46 +918,46 @@
end
-lemma open_real_lessThan [simp]:
- fixes a :: real shows "open {..<a}"
-unfolding open_real_def dist_real_def
-proof (clarify)
- fix x assume "x < a"
- hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
- thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
-qed
-
-lemma open_real_greaterThan [simp]:
- fixes a :: real shows "open {a<..}"
-unfolding open_real_def dist_real_def
-proof (clarify)
- fix x assume "a < x"
- hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
- thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" ..
+instance real :: linorder_topology
+proof
+ show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
+ proof (rule ext, safe)
+ fix S :: "real set" assume "open S"
+ then guess f unfolding open_real_def bchoice_iff ..
+ then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
+ by (fastforce simp: dist_real_def)
+ show "generate_topology (range lessThan \<union> range greaterThan) S"
+ apply (subst *)
+ apply (intro generate_topology_Union generate_topology.Int)
+ apply (auto intro: generate_topology.Basis)
+ done
+ next
+ fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
+ moreover have "\<And>a::real. open {..<a}"
+ unfolding open_real_def dist_real_def
+ proof clarify
+ fix x a :: real assume "x < a"
+ hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
+ thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
+ qed
+ moreover have "\<And>a::real. open {a <..}"
+ unfolding open_real_def dist_real_def
+ proof clarify
+ fix x a :: real assume "a < x"
+ hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
+ thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" ..
+ qed
+ ultimately show "open S"
+ by induct auto
+ qed
qed
-lemma open_real_greaterThanLessThan [simp]:
- fixes a b :: real shows "open {a<..<b}"
-proof -
- have "{a<..<b} = {a<..} \<inter> {..<b}" by auto
- thus "open {a<..<b}" by (simp add: open_Int)
-qed
-
-lemma closed_real_atMost [simp]:
- fixes a :: real shows "closed {..a}"
-unfolding closed_open by simp
-
-lemma closed_real_atLeast [simp]:
- fixes a :: real shows "closed {a..}"
-unfolding closed_open by simp
-
-lemma closed_real_atLeastAtMost [simp]:
- fixes a b :: real shows "closed {a..b}"
-proof -
- have "{a..b} = {a..} \<inter> {..b}" by auto
- thus "closed {a..b}" by (simp add: closed_Int)
-qed
-
+lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
+lemmas open_real_lessThan = open_lessThan[where 'a=real]
+lemmas open_real_greaterThanLessThan = open_greaterThanLessThan[where 'a=real]
+lemmas closed_real_atMost = closed_atMost[where 'a=real]
+lemmas closed_real_atLeast = closed_atLeast[where 'a=real]
+lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real]
subsection {* Extra type constraints *}
@@ -1172,6 +1231,30 @@
instance t2_space \<subseteq> t1_space
proof qed (fast dest: hausdorff)
+lemma (in linorder) less_separate:
+ assumes "x < y"
+ shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
+proof cases
+ assume "\<exists>z. x < z \<and> z < y"
+ then guess z ..
+ then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
+ by auto
+ then show ?thesis by blast
+next
+ assume "\<not> (\<exists>z. x < z \<and> z < y)"
+ with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"
+ by auto
+ then show ?thesis by blast
+qed
+
+instance linorder_topology \<subseteq> t2_space
+proof
+ fix x y :: 'a
+ from less_separate[of x y] less_separate[of y x]
+ show "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+ by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+
+qed
+
instance metric_space \<subseteq> t2_space
proof
fix x y :: "'a::metric_space"
--- a/src/HOL/SEQ.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/SEQ.thy Wed Feb 13 11:46:48 2013 +0100
@@ -368,19 +368,16 @@
and bdd: "\<And>n. f n \<le> l"
and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
shows "f ----> l"
- unfolding LIMSEQ_def
-proof safe
- fix r :: real assume "0 < r"
- with bdd en[of "r / 2"] obtain n where n: "dist (f n) l \<le> r / 2"
- by (auto simp add: field_simps dist_real_def)
- { fix N assume "n \<le> N"
- then have "dist (f N) l \<le> dist (f n) l"
- using incseq_SucI[of f] inc bdd by (auto dest!: incseqD simp: dist_real_def)
- then have "dist (f N) l < r"
- using `0 < r` n by simp }
- with `0 < r` show "\<exists>no. \<forall>n\<ge>no. dist (f n) l < r"
- by (auto simp add: LIMSEQ_def field_simps intro!: exI[of _ n])
-qed
+proof (rule increasing_tendsto)
+ fix x assume "x < l"
+ with dense[of 0 "l - x"] obtain e where "0 < e" "e < l - x"
+ by auto
+ from en[OF `0 < e`] obtain n where "l - e \<le> f n"
+ by (auto simp: field_simps)
+ with `e < l - x` `0 < e` have "x < f n" by simp
+ with incseq_SucI[of f, OF inc] show "eventually (\<lambda>n. x < f n) sequentially"
+ by (auto simp: eventually_sequentially incseq_def intro: less_le_trans)
+qed (insert bdd, auto)
lemma Bseq_inverse_lemma:
fixes x :: "'a::real_normed_div_algebra"
@@ -437,15 +434,15 @@
by auto
lemma LIMSEQ_le_const:
- "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
+ "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
lemma LIMSEQ_le:
- "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
+ "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)"
using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
lemma LIMSEQ_le_const2:
- "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
+ "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
subsection {* Convergence *}
--- a/src/HOL/Series.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Series.thy Wed Feb 13 11:46:48 2013 +0100
@@ -367,7 +367,7 @@
lemma pos_summable:
fixes f:: "nat \<Rightarrow> real"
- assumes pos: "!!n. 0 \<le> f n" and le: "!!n. setsum f {0..<n} \<le> x"
+ assumes pos: "\<And>n. 0 \<le> f n" and le: "\<And>n. setsum f {0..<n} \<le> x"
shows "summable f"
proof -
have "convergent (\<lambda>n. setsum f {0..<n})"
@@ -386,35 +386,65 @@
qed
lemma series_pos_le:
- fixes f :: "nat \<Rightarrow> real"
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
-apply (drule summable_sums)
-apply (simp add: sums_def)
-apply (cut_tac k = "setsum f {0..<n}" in tendsto_const)
-apply (erule LIMSEQ_le, blast)
-apply (rule_tac x="n" in exI, clarify)
-apply (rule setsum_mono2)
-apply auto
-done
+ apply (drule summable_sums)
+ apply (simp add: sums_def)
+ apply (rule LIMSEQ_le_const)
+ apply assumption
+ apply (intro exI[of _ n])
+ apply (auto intro!: setsum_mono2)
+ done
lemma series_pos_less:
- fixes f :: "nat \<Rightarrow> real"
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_ab_semigroup_add_imp_le, ordered_comm_monoid_add, linorder_topology}"
shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 < f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} < suminf f"
-apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)
-apply simp
-apply (erule series_pos_le)
-apply (simp add: order_less_imp_le)
-done
+ apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)
+ using add_less_cancel_left [of "setsum f {0..<n}" 0 "f n"]
+ apply simp
+ apply (erule series_pos_le)
+ apply (simp add: order_less_imp_le)
+ done
+
+lemma suminf_eq_zero_iff:
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
+ shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
+proof
+ assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
+ then have "f sums 0"
+ by (simp add: sums_iff)
+ then have f: "(\<lambda>n. \<Sum>i<n. f i) ----> 0"
+ by (simp add: sums_def atLeast0LessThan)
+ have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
+ proof (rule LIMSEQ_le_const[OF f])
+ fix i show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}"
+ using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto
+ qed
+ with pos show "\<forall>n. f n = 0"
+ by (auto intro!: antisym)
+next
+ assume "\<forall>n. f n = 0"
+ then have "f = (\<lambda>n. 0)"
+ by auto
+ then show "suminf f = 0"
+ by simp
+qed
+
+lemma suminf_gt_zero_iff:
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
+ shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
+ using series_pos_le[of f 0] suminf_eq_zero_iff[of f]
+ by (simp add: less_le)
lemma suminf_gt_zero:
- fixes f :: "nat \<Rightarrow> real"
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
shows "\<lbrakk>summable f; \<forall>n. 0 < f n\<rbrakk> \<Longrightarrow> 0 < suminf f"
-by (drule_tac n="0" in series_pos_less, simp_all)
+ using suminf_gt_zero_iff[of f] by (simp add: less_imp_le)
lemma suminf_ge_zero:
- fixes f :: "nat \<Rightarrow> real"
+ fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
shows "\<lbrakk>summable f; \<forall>n. 0 \<le> f n\<rbrakk> \<Longrightarrow> 0 \<le> suminf f"
-by (drule_tac n="0" in series_pos_le, simp_all)
+ by (drule_tac n="0" in series_pos_le, simp_all)
lemma sumr_pos_lt_pair:
fixes f :: "nat \<Rightarrow> real"
@@ -493,9 +523,14 @@
done
lemma suminf_le:
- fixes x :: real
+ fixes x :: "'a :: {ordered_comm_monoid_add, linorder_topology}"
shows "summable f \<Longrightarrow> (!!n. setsum f {0..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
- by (simp add: summable_convergent_sumr_iff suminf_eq_lim lim_le)
+ apply (drule summable_sums)
+ apply (simp add: sums_def)
+ apply (rule LIMSEQ_le_const2)
+ apply assumption
+ apply auto
+ done
lemma summable_Cauchy:
"summable (f::nat \<Rightarrow> 'a::banach) =
@@ -575,7 +610,7 @@
text{*Limit comparison property for series (c.f. jrh)*}
lemma summable_le:
- fixes f g :: "nat \<Rightarrow> real"
+ fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
shows "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
apply (drule summable_sums)+
apply (simp only: sums_def, erule (1) LIMSEQ_le)
@@ -597,15 +632,7 @@
fixes f::"nat\<Rightarrow>real"
assumes gt0: "\<forall>n. 0 \<le> f n" and sm: "summable f"
shows "0 \<le> suminf f"
-proof -
- let ?g = "(\<lambda>n. (0::real))"
- from gt0 have "\<forall>n. ?g n \<le> f n" by simp
- moreover have "summable ?g" by (rule summable_zero)
- moreover from sm have "summable f" .
- ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
- then show "0 \<le> suminf f" by simp
-qed
-
+ using suminf_ge_zero[OF sm gt0] by simp
text{*Absolute convergence imples normal convergence*}
lemma summable_norm_cancel:
--- a/src/HOL/Set_Interval.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Set_Interval.thy Wed Feb 13 11:46:48 2013 +0100
@@ -117,6 +117,11 @@
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
by (blast intro: order_antisym)
+lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \<inter> { b <..} = { max a b <..}"
+ by auto
+
+lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \<inter> {..< b} = {..< min a b}"
+ by auto
subsection {* Logical Equivalences for Set Inclusion and Equality *}
@@ -190,6 +195,9 @@
breaks many proofs. Since it only helps blast, it is better to leave well
alone *}
+lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
+ by auto
+
end
subsubsection{* Emptyness, singletons, subset *}
--- a/src/HOL/TPTP/MaSh_Export.thy Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Wed Feb 13 11:46:48 2013 +0100
@@ -16,6 +16,8 @@
declare [[sledgehammer_instantiate_inducts = false]]
+hide_fact (open) HOL.ext
+
ML {*
!Multithreading.max_threads
*}
--- a/src/HOL/TPTP/mash_eval.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Wed Feb 13 11:46:48 2013 +0100
@@ -30,11 +30,10 @@
open Sledgehammer_Provers
open Sledgehammer_Isar
-val MePoN = "MePo"
-val MaSh_IsarN = "MaSh-Isar"
-val MaSh_ProverN = "MaSh-Prover"
-val MeSh_IsarN = "MeSh-Isar"
-val MeSh_ProverN = "MeSh-Prover"
+val MaSh_IsarN = MaShN ^ "-Isar"
+val MaSh_ProverN = MaShN ^ "-Prover"
+val MeSh_IsarN = MeShN ^ "-Isar"
+val MeSh_ProverN = MeShN ^ "-Prover"
val IsarN = "Isar"
fun in_range (from, to) j =
@@ -44,6 +43,7 @@
mepo_file_name mash_isar_file_name mash_prover_file_name
mesh_isar_file_name mesh_prover_file_name report_file_name =
let
+ val zeros = [0, 0, 0, 0, 0, 0]
val report_path = report_file_name |> Path.explode
val _ = File.write report_path ""
fun print s = File.append report_path (s ^ "\n")
@@ -71,7 +71,7 @@
val str_of_method = enclose " " ": "
fun str_of_result method facts ({outcome, run_time, used_facts, ...}
: prover_result) =
- let val facts = facts |> map (fn ((name, _), _) => name ()) in
+ let val facts = facts |> map (fst o fst) in
str_of_method method ^
(if is_none outcome then
"Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
@@ -111,7 +111,7 @@
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val isar_deps = isar_dependencies_of name_tabs th
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
- val find_suggs = find_suggested_facts facts
+ val find_suggs = find_suggested_facts facts #> map fact_of_raw_fact
fun get_facts [] compute = compute facts
| get_facts suggs _ = find_suggs suggs
val mepo_facts =
@@ -121,7 +121,8 @@
|> weight_mepo_facts
fun mash_of suggs =
get_facts suggs (fn _ =>
- find_mash_suggestions slack_max_facts suggs facts [] [] |> fst)
+ find_mash_suggestions slack_max_facts suggs facts [] []
+ |> fst |> map fact_of_raw_fact)
|> weight_mash_facts
val mash_isar_facts = mash_of mash_isar_suggs
val mash_prover_facts = mash_of mash_prover_suggs
@@ -160,6 +161,7 @@
|> map (get #> nickify)
|> maybe_instantiate_inducts ctxt hyp_ts concl_t
|> take (the max_facts)
+ |> map fact_of_raw_fact
val ctxt = ctxt |> set_file_name method prob_dir_name
val res as {outcome, ...} =
run_prover_for_mash ctxt params prover facts goal
@@ -179,11 +181,11 @@
map snd ress
end
else
- [0, 0, 0, 0, 0, 0]
+ zeros
fun total_of method ok n =
str_of_method method ^ string_of_int ok ^ " (" ^
Real.fmt (StringCvt.FIX (SOME 1))
- (100.0 * Real.fromInt ok / Real.fromInt n) ^ "%)"
+ (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
val inst_inducts = Config.get ctxt instantiate_inducts
val options =
["prover = " ^ prover,
@@ -199,7 +201,7 @@
val n = length oks
val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok,
isar_ok] =
- map Integer.sum (map_transpose I oks)
+ if n = 0 then zeros else map Integer.sum (map_transpose I oks)
in
["Successes (of " ^ string_of_int n ^ " goals)",
total_of MePoN mepo_ok n,
--- a/src/HOL/TPTP/mash_export.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML Wed Feb 13 11:46:48 2013 +0100
@@ -83,15 +83,31 @@
in File.append path s end
in List.app do_fact facts end
-fun isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
- isar_deps_opt =
- case params_opt of
- SOME (params as {provers = prover :: _, ...}) =>
- prover_dependencies_of ctxt params prover 0 facts name_tabs th |> snd
- | NONE =>
- case isar_deps_opt of
- SOME deps => deps
- | NONE => isar_dependencies_of name_tabs th
+val prover_marker = "$a"
+val isar_marker = "$i"
+val omitted_marker = "$o"
+val unprovable_marker = "$u" (* axiom or definition or characteristic theorem *)
+val prover_failed_marker = "$x"
+
+fun smart_dependencies_of ctxt params_opt facts name_tabs th isar_deps_opt =
+ let
+ val (marker, deps) =
+ case params_opt of
+ SOME (params as {provers = prover :: _, ...}) =>
+ prover_dependencies_of ctxt params prover 0 facts name_tabs th
+ |>> (fn true => prover_marker | false => prover_failed_marker)
+ | NONE =>
+ let
+ val deps =
+ case isar_deps_opt of
+ SOME deps => deps
+ | NONE => isar_dependencies_of name_tabs th
+ in (if null deps then unprovable_marker else isar_marker, deps) end
+ in
+ case trim_dependencies th deps of
+ SOME deps => (marker, deps)
+ | NONE => (omitted_marker, [])
+ end
fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
file_name =
@@ -105,10 +121,9 @@
let
val name = nickname_of_thm th
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
- val deps =
- isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
- NONE
- in encode_str name ^ ": " ^ encode_strs deps ^ "\n" end
+ val (marker, deps) =
+ smart_dependencies_of ctxt params_opt facts name_tabs th NONE
+ in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end
else
""
val lines = Par_List.map do_fact (tag_list 1 facts)
@@ -123,7 +138,7 @@
fun is_bad_query ctxt ho_atp step j th isar_deps =
j mod step <> 0 orelse
Thm.legacy_get_kind th = "" orelse
- null (these (trim_dependencies th isar_deps)) orelse
+ null isar_deps orelse
is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
@@ -141,9 +156,9 @@
val feats =
features_of ctxt prover (theory_of_thm th) stature [prop_of th]
val isar_deps = isar_dependencies_of name_tabs th
- val deps =
- isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
- (SOME isar_deps)
+ val (marker, deps) =
+ smart_dependencies_of ctxt params_opt facts name_tabs th
+ (SOME isar_deps)
val core =
encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^
encode_features (sort_wrt fst feats)
@@ -151,8 +166,7 @@
if is_bad_query ctxt ho_atp step j th isar_deps then ""
else "? " ^ core ^ "\n"
val update =
- "! " ^ core ^ "; " ^
- encode_strs (these (trim_dependencies th deps)) ^ "\n"
+ "! " ^ core ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
in query ^ update end
else
""
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed Feb 13 11:46:48 2013 +0100
@@ -42,15 +42,15 @@
|> relevant_facts ctxt params name
(the_default default_max_facts max_facts) fact_override hyp_ts
concl_t
+ |> hd |> snd
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts |> map (apfst (apfst (fn name => name ())))
- |> map Untranslated_Fact}
+ factss = [("", facts)]}
in
(case prover params (K (K (K ""))) problem of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
| _ => NONE)
- handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
+ handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
end
fun sledgehammer_with_metis_tac ctxt override_params fact_override i th =
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Feb 13 11:46:48 2013 +0100
@@ -201,9 +201,7 @@
fun step_name_ord p =
let val q = pairself fst p in
- (* The "unprefix" part is to cope with remote Vampire's output. The proper
- solution would be to perform a topological sort, e.g. using the nice
- "Graph" functor. *)
+ (* The "unprefix" part is to cope with remote Vampire's output. *)
case pairself (Int.fromString
o perhaps (try (unprefix vampire_fact_prefix))) q of
(NONE, NONE) => string_ord q
@@ -229,6 +227,8 @@
|| Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
>> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
+val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) >> implode
+
val skip_term =
let
fun skip _ accum [] = (accum, [])
@@ -264,9 +264,13 @@
(Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
--| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
-- parse_dependencies --| $$ "]" --| $$ ")") x
+and skip_introduced x =
+ (Scan.this_string "introduced" |-- $$ "(" |-- skip_term --| $$ ")") x
and parse_source x =
(parse_file_source >> File_Source
|| parse_inference_source >> Inference_Source
+ || skip_introduced >> K dummy_inference (* for Vampire *)
+ || scan_nat >> (fn s => Inference_Source ("", [s])) (* for E *)
|| skip_term >> K dummy_inference) x
fun list_app (f, args) =
@@ -508,7 +512,7 @@
| atp_proof_from_tstplike_proof problem tstp =
tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof problem
- |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *)
+ |> sort (step_name_ord o pairself step_name)
fun clean_up_dependencies _ [] = []
| clean_up_dependencies seen
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Feb 13 11:46:48 2013 +0100
@@ -39,7 +39,8 @@
val string_of_ref_graph : ref_graph -> string
val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent
val direct_graph : direct_sequent list -> direct_graph
- val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof
+ val redirect_graph :
+ atom list -> atom list -> atom -> ref_graph -> direct_proof
val succedent_of_cases : (clause * direct_inference list) list -> clause
val string_of_direct_proof : direct_proof -> string
end;
@@ -147,17 +148,11 @@
| zones_of n (bs :: bss) =
(fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs])
-fun redirect_graph axioms tainted ref_graph =
+fun redirect_graph axioms tainted bot ref_graph =
let
- val bot =
- case Atom_Graph.maximals ref_graph of
- [bot] => bot
- | bots => raise Fail ("malformed refutation graph with " ^
- string_of_int (length bots) ^ " maximal nodes")
val seqs =
map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)
val direct_graph = direct_graph seqs
-
fun redirect c proved seqs =
if null seqs then
[]
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 13 11:46:48 2013 +0100
@@ -12,7 +12,7 @@
type formula_role = ATP_Problem.formula_role
type failure = ATP_Proof.failure
- type slice_spec = int * atp_format * string * string * bool
+ type slice_spec = (int * string) * atp_format * string * string * bool
type atp_config =
{exec : string list * string list,
arguments :
@@ -91,7 +91,7 @@
val default_max_mono_iters = 3 (* FUDGE *)
val default_max_new_mono_instances = 200 (* FUDGE *)
-type slice_spec = int * atp_format * string * string * bool
+type slice_spec = (int * string) * atp_format * string * string * bool
type atp_config =
{exec : string list * string list,
@@ -107,18 +107,26 @@
best_max_new_mono_instances : int}
(* "best_slices" must be found empirically, taking a wholistic approach since
- the ATPs are run in parallel. The "real" component gives the faction of the
- time available given to the slice and should add up to 1.0. The "int"
- component indicates the preferred number of facts to pass; the first
- "string", the preferred type system (which should be sound or quasi-sound);
- the second "string", the preferred lambda translation scheme; the "bool",
- whether uncurried aliased should be generated; the third "string", extra
- information to the prover (e.g., SOS or no SOS).
+ the ATPs are run in parallel. Each slice has the format
+
+ (time_frac, ((max_facts, fact_filter), format, type_enc,
+ lam_trans, uncurried_aliases), extra)
+
+ where
+
+ time_frac = faction of the time available given to the slice (which should
+ add up to 1.0)
+
+ extra = extra information to the prover (e.g., SOS or no SOS).
The last slice should be the most "normal" one, because it will get all the
time available if the other slices fail early and also because it is used if
slicing is disabled (e.g., by the minimizer). *)
+val mepoN = "mepo"
+val mashN = "mash"
+val meshN = "mesh"
+
val known_perl_failures =
[(CantConnect, "HTTP error"),
(NoPerl, "env: perl"),
@@ -209,7 +217,7 @@
prem_role = Hypothesis,
best_slices = fn _ =>
(* FUDGE *)
- [(1.0, ((100, alt_ergo_tff1, "poly_native", liftingN, false), ""))],
+ [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -328,11 +336,14 @@
let val heuristic = effective_e_selection_heuristic ctxt in
(* FUDGE *)
if heuristic = e_smartN then
- [(0.333, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN)),
- (0.334, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN)),
- (0.333, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN))]
+ [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
+ (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)),
+ (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)),
+ (0.15, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN)),
+ (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)),
+ (0.25, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN))]
else
- [(1.0, ((500, FOF, "mono_tags??", combsN, false), heuristic))]
+ [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))]
end,
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -351,8 +362,10 @@
prem_role = Conjecture,
best_slices =
(* FUDGE *)
- K [(0.5, ((1000, FOF, "mono_tags??", combsN, false), "")),
- (0.5, ((1000, FOF, "mono_guards??", combsN, false), ""))],
+ K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")),
+ (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")),
+ (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")),
+ (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -390,7 +403,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, ((150, FOF, "mono_guards??", liftingN, false), ""))],
+ K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -434,7 +447,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, ((40, leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((40, ""), leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
@@ -456,7 +469,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, ((60, satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
@@ -497,14 +510,14 @@
prem_role = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.1667, ((150, DFG Monomorphic, "mono_native", combsN, true), "")),
- (0.1667, ((500, DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
- (0.1666, ((50, DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)),
- (0.1000, ((250, DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)),
- (0.1000, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
- (0.1000, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
- (0.1000, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
- (0.1000, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))]
+ [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")),
+ (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
+ (0.1666, (((50, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)),
+ (0.1000, (((250, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)),
+ (0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
+ (0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
+ (0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
+ (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))]
|> (case Config.get ctxt spass_extra_options of
"" => I
| opts => map (apsnd (apsnd (K opts)))),
@@ -551,13 +564,13 @@
best_slices = fn ctxt =>
(* FUDGE *)
(if is_vampire_beyond_1_8 () then
- [(0.333, ((500, vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
- (0.333, ((150, vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
- (0.334, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
+ [(0.333, (((500, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
+ (0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
+ (0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
else
- [(0.333, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
- (0.333, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN)),
- (0.334, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))])
+ [(0.333, (((150, meshN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
+ (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)),
+ (0.334, (((50, meshN), FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I),
best_max_mono_iters = default_max_mono_iters,
@@ -580,10 +593,10 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(0.5, ((250, z3_tff0, "mono_native", combsN, false), "")),
- (0.25, ((125, z3_tff0, "mono_native", combsN, false), "")),
- (0.125, ((62, z3_tff0, "mono_native", combsN, false), "")),
- (0.125, ((31, z3_tff0, "mono_native", combsN, false), ""))],
+ K [(0.5, (((250, meshN), z3_tff0, "mono_native", combsN, false), "")),
+ (0.25, (((125, mepoN), z3_tff0, "mono_native", combsN, false), "")),
+ (0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")),
+ (0.125, (((31, meshN), z3_tff0, "mono_native", combsN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -599,7 +612,7 @@
known_failures = known_szs_status_failures,
prem_role = Hypothesis,
best_slices =
- K [(1.0, ((200, format, type_enc,
+ K [(1.0, (((200, ""), format, type_enc,
if is_format_higher_order format then keep_lamsN
else combsN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
@@ -692,32 +705,32 @@
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_iprover =
remotify_atp iprover "iProver" []
- (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
+ (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
val remote_iprover_eq =
remotify_atp iprover_eq "iProver-Eq" []
- (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
+ (K (((150, ""), FOF, "mono_guards??", liftingN, 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.3", "2.2", "2"]
- (K ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
+ (K (((100, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["2.6", "2.5", "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_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
- (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
+ (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] 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) 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:")]
@@ -725,7 +738,7 @@
(Inappropriate, "**** Unexpected end of file."),
(Crashed, "Unrecoverable Segmentation Fault")]
Hypothesis
- (K ((50, CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
+ (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
(* Setup *)
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py Wed Feb 13 11:46:48 2013 +0100
@@ -34,15 +34,13 @@
"""
for d in trainData:
dFeatureCounts = {}
- # Give p |- p a higher weight
+ # Add p proves p with weight self.defaultPriorWeight
if not self.defaultPriorWeight == 0:
for f,_w in dicts.featureDict[d]:
dFeatureCounts[f] = self.defaultPriorWeight
self.counts[d] = [self.defaultPriorWeight,dFeatureCounts]
- for key in dicts.dependenciesDict.keys():
- # Add p proves p
- keyDeps = [key]+dicts.dependenciesDict[key]
+ for key,keyDeps in dicts.dependenciesDict.iteritems():
for dep in keyDeps:
self.counts[dep][0] += 1
depFeatures = dicts.featureDict[key]
@@ -105,7 +103,7 @@
resultA = log(posA)
for f,w in features:
# DEBUG
- #w = 1
+ #w = 1.0
if f in fA:
if fWeightsA[f] == 0:
resultA += w*self.defVal
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Feb 13 11:46:48 2013 +0100
@@ -10,7 +10,8 @@
type status = ATP_Problem_Generate.status
type stature = ATP_Problem_Generate.stature
- type fact = ((unit -> string) * stature) * thm
+ type raw_fact = ((unit -> string) * stature) * thm
+ type fact = (string * stature) * thm
type fact_override =
{add : (Facts.ref * Attrib.src list) list,
@@ -33,12 +34,13 @@
Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
-> (((unit -> string) * 'a) * thm) list
val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
+ val fact_of_raw_fact : raw_fact -> fact
val all_facts :
Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
- -> status Termtab.table -> fact list
+ -> status Termtab.table -> raw_fact list
val nearly_all_facts :
Proof.context -> bool -> fact_override -> unit Symtab.table
- -> status Termtab.table -> thm list -> term list -> term -> fact list
+ -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
end;
structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
@@ -49,7 +51,8 @@
open Metis_Tactic
open Sledgehammer_Util
-type fact = ((unit -> string) * stature) * thm
+type raw_fact = ((unit -> string) * stature) * thm
+type fact = (string * stature) * thm
type fact_override =
{add : (Facts.ref * Attrib.src list) list,
@@ -419,6 +422,8 @@
fun maybe_filter_no_atps ctxt =
not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
+fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
+
fun all_facts ctxt generous ho_atp reserved add_ths chained css =
let
val thy = Proof_Context.theory_of ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Feb 13 11:46:48 2013 +0100
@@ -7,6 +7,7 @@
signature SLEDGEHAMMER_MASH =
sig
type stature = ATP_Problem_Generate.stature
+ type raw_fact = Sledgehammer_Fact.raw_fact
type fact = Sledgehammer_Fact.fact
type fact_override = Sledgehammer_Fact.fact_override
type params = Sledgehammer_Provers.params
@@ -14,7 +15,10 @@
type prover_result = Sledgehammer_Provers.prover_result
val trace : bool Config.T
+ val snow : bool Config.T
+ val MePoN : string
val MaShN : string
+ val MeShN : string
val mepoN : string
val mashN : string
val meshN : string
@@ -62,7 +66,7 @@
val isar_dependencies_of :
string Symtab.table * string Symtab.table -> thm -> string list
val prover_dependencies_of :
- Proof.context -> params -> string -> int -> fact list
+ Proof.context -> params -> string -> int -> raw_fact list
-> string Symtab.table * string Symtab.table -> thm
-> bool * string list
val weight_mepo_facts : 'a list -> ('a * real) list
@@ -71,8 +75,8 @@
int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list
-> ('b * thm) list * ('b * thm) list
val mash_suggested_facts :
- Proof.context -> params -> string -> int -> term list -> term -> fact list
- -> fact list * fact list
+ Proof.context -> params -> string -> int -> term list -> term
+ -> raw_fact list -> fact list * fact list
val mash_learn_proof :
Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
-> unit
@@ -85,7 +89,7 @@
val mash_weight : real
val relevant_facts :
Proof.context -> params -> string -> int -> fact_override -> term list
- -> term -> fact list -> fact list
+ -> term -> raw_fact list -> (string * fact list) list
val kill_learners : unit -> unit
val running_learners : unit -> unit
end;
@@ -103,9 +107,14 @@
val trace =
Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
+val snow =
+ Attrib.setup_config_bool @{binding sledgehammer_mash_snow} (K false)
+
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
+val MePoN = "MePo"
val MaShN = "MaSh"
+val MeShN = "MeSh"
val mepoN = "mepo"
val mashN = "mash"
@@ -146,13 +155,20 @@
val sugg_path = Path.explode sugg_file
val cmd_file = temp_dir ^ "/mash_commands" ^ serial
val cmd_path = Path.explode cmd_file
+ val model_dir = File.shell_path (mash_model_dir ())
val core =
"--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
" --numberOfPredictions " ^ string_of_int max_suggs ^
(* " --learnTheories" ^ *) (if save then " --saveModel" else "")
val command =
- "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^
- File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
+ "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; " ^
+ "./mash.py --quiet" ^
+ (if Config.get ctxt snow then " --snow" else "") ^
+ " --outputDir " ^ model_dir ^
+ " --modelFile=" ^ model_dir ^ "/model.pickle" ^
+ " --dictsFile=" ^ model_dir ^ "/dict.pickle" ^
+ " --theoryFile=" ^ model_dir ^ "/theory.pickle" ^
+ " --log " ^ log_file ^ " " ^ core ^
" >& " ^ err_file
fun run_on () =
(Isabelle_System.bash command
@@ -200,7 +216,7 @@
fun encode_feature (name, weight) =
encode_str name ^
- (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
+ (if Real.== (weight, 1.0) then "" else "=" ^ smart_string_of_real weight)
val encode_features = map encode_feature #> space_implode " "
@@ -320,7 +336,7 @@
local
-val version = "*** MaSh version 20130113a ***"
+val version = "*** MaSh version 20130207a ***"
exception Too_New of unit
@@ -457,9 +473,8 @@
map fst (take max_facts sels) @ take (max_facts - length sels) unks
| mesh_facts fact_eq max_facts mess =
let
- val mess =
- mess |> map (apsnd (apfst (normalize_scores max_facts #> `length)))
- fun score_in fact (global_weight, ((sel_len, sels), unks)) =
+ val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
+ fun score_in fact (global_weight, (sels, unks)) =
let
fun score_at j =
case try (nth sels) j of
@@ -474,8 +489,7 @@
end
fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
val facts =
- fold (union fact_eq o map fst o take max_facts o snd o fst o snd) mess
- []
+ fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
in
facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
|> map snd |> take max_facts
@@ -526,8 +540,7 @@
let
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
- facts = facts |> map (apfst (apfst (fn name => name ())))
- |> map Untranslated_Fact}
+ factss = [("", facts)]}
in
get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
problem
@@ -659,9 +672,7 @@
if length deps > max_dependencies then NONE else SOME deps
fun isar_dependencies_of name_tabs th =
- let
- val deps = thms_in_proof (SOME name_tabs) th
- in
+ let val deps = thms_in_proof (SOME name_tabs) th in
if deps = [typedef_dep] orelse
deps = [class_some_dep] orelse
exists (member (op =) fundef_ths) deps orelse
@@ -682,14 +693,13 @@
val goal = goal_of_thm thy th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
- fun nickify ((_, stature), th) =
- ((fn () => nickname_of_thm th, stature), th)
+ fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
fun is_dep dep (_, th) = nickname_of_thm th = dep
fun add_isar_dep facts dep accum =
if exists (is_dep dep) accum then
accum
else case find_first (is_dep dep) facts of
- SOME ((name, status), th) => accum @ [((name, status), th)]
+ SOME ((_, status), th) => accum @ [(("", status), th)]
| NONE => accum (* shouldn't happen *)
val facts =
facts
@@ -820,7 +830,10 @@
(parents, feats, hints))
end)
val unknown = facts |> filter_out (is_fact_in_graph access_G snd)
- in find_mash_suggestions max_facts suggs facts chained unknown end
+ in
+ find_mash_suggestions max_facts suggs facts chained unknown
+ |> pairself (map fact_of_raw_fact)
+ end
fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) =
let
@@ -1094,9 +1107,11 @@
if not (subset (op =) (the_list fact_filter, fact_filters)) then
error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
else if only then
- facts
+ let val facts = facts |> map fact_of_raw_fact in
+ [("", facts)]
+ end
else if max_facts <= 0 orelse null facts then
- []
+ [("", [])]
else
let
fun maybe_learn () =
@@ -1112,21 +1127,22 @@
end
else
()
- val fact_filter =
+ val effective_fact_filter =
case fact_filter of
SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
| NONE =>
- if is_smt_prover ctxt prover then
- mepoN
- else if is_mash_enabled () then
+ if is_mash_enabled () then
(maybe_learn ();
if mash_can_suggest_facts ctxt then meshN else mepoN)
else
mepoN
val add_ths = Attrib.eval_thms ctxt add
- fun prepend_facts ths accepts =
- ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
- (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
+ fun in_add (_, th) = member Thm.eq_thm_prop add_ths th
+ fun add_and_take accepts =
+ (case add_ths of
+ [] => accepts
+ | _ => (facts |> filter in_add |> map fact_of_raw_fact) @
+ (accepts |> filter_out in_add))
|> take max_facts
fun mepo () =
mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
@@ -1137,13 +1153,24 @@
hyp_ts concl_t facts
|>> weight_mash_facts
val mess =
- [] |> (if fact_filter <> mashN then cons (mepo_weight, (mepo (), []))
- else I)
- |> (if fact_filter <> mepoN then cons (mash_weight, (mash ()))
- else I)
+ (* the order is important for the "case" expression below *)
+ [] |> (if effective_fact_filter <> mepoN then
+ cons (mash_weight, (mash ()))
+ else
+ I)
+ |> (if effective_fact_filter <> mashN then
+ cons (mepo_weight, (mepo (), []))
+ else
+ I)
+ val mesh =
+ mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess
+ |> add_and_take
in
- mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess
- |> not (null add_ths) ? prepend_facts add_ths
+ case (fact_filter, mess) of
+ (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
+ [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
+ (mashN, mash |> map fst |> add_and_take)]
+ | _ => [("", mesh)]
end
fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Feb 13 11:46:48 2013 +0100
@@ -8,6 +8,7 @@
signature SLEDGEHAMMER_MEPO =
sig
type stature = ATP_Problem_Generate.stature
+ type raw_fact = Sledgehammer_Fact.raw_fact
type fact = Sledgehammer_Fact.fact
type params = Sledgehammer_Provers.params
type relevance_fudge = Sledgehammer_Provers.relevance_fudge
@@ -20,7 +21,7 @@
-> string list
val mepo_suggested_facts :
Proof.context -> params -> string -> int -> relevance_fudge option
- -> term list -> term -> fact list -> fact list
+ -> term list -> term -> raw_fact list -> fact list
end;
structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
@@ -337,7 +338,7 @@
fun take_most_relevant ctxt max_facts remaining_max
({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
- (candidates : ((fact * (string * ptype) list) * real) list) =
+ (candidates : ((raw_fact * (string * ptype) list) * real) list) =
let
val max_imperfect =
Real.ceil (Math.pow (max_imperfect,
@@ -497,10 +498,10 @@
|> chop special_fact_index
in bef @ add @ after end
fun insert_special_facts accepts =
- (* FIXME: get rid of "ext" here once it is treated as a helper *)
- [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
- |> add_set_const_thms accepts
- |> insert_into_facts accepts
+ (* FIXME: get rid of "ext" here once it is treated as a helper *)
+ [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
+ |> add_set_const_thms accepts
+ |> insert_into_facts accepts
in
facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
|> iter 0 max_facts thres0 goal_const_tab []
@@ -533,6 +534,7 @@
relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
facts hyp_ts
(concl_t |> theory_constify fudge (Context.theory_name thy)))
+ |> map fact_of_raw_fact
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 13 11:46:48 2013 +0100
@@ -68,8 +68,7 @@
else
"") ^ "...")
val {goal, ...} = Proof.goal state
- val facts =
- facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
+ val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_enc = type_enc, strict = strict,
@@ -82,7 +81,7 @@
preplay_timeout = preplay_timeout, expect = ""}
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts}
+ factss = [("", facts)]}
val result as {outcome, used_facts, run_time, ...} =
prover params (K (K (K ""))) problem
in
@@ -268,8 +267,8 @@
fun maybe_minimize ctxt mode do_learn name
(params as {verbose, isar_proofs, minimize, ...})
- ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
- (result as {outcome, used_facts, run_time, preplay, message,
+ ({state, subgoal, subgoal_count, ...} : prover_problem)
+ (result as {outcome, used_facts, used_from, run_time, preplay, message,
message_tail} : prover_result) =
if is_some outcome orelse null used_facts then
result
@@ -309,18 +308,17 @@
val (used_facts, (preplay, message, _)) =
if minimize then
minimize_facts do_learn minimize_name params
- (mode <> Normal orelse not verbose) subgoal
- subgoal_count state
- (filter_used_facts true used_facts
- (map (apsnd single o untranslated_fact) facts))
+ (mode <> Normal orelse not verbose) subgoal subgoal_count state
+ (filter_used_facts true used_facts (map (apsnd single) used_from))
|>> Option.map (map fst)
else
(SOME used_facts, (preplay, message, ""))
in
case used_facts of
SOME used_facts =>
- {outcome = NONE, used_facts = used_facts, run_time = run_time,
- preplay = preplay, message = message, message_tail = message_tail}
+ {outcome = NONE, used_facts = used_facts, used_from = used_from,
+ run_time = run_time, preplay = preplay, message = message,
+ message_tail = message_tail}
| NONE => result
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Feb 13 11:46:48 2013 +0100
@@ -11,6 +11,7 @@
type failure = ATP_Proof.failure
type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
+ type fact = Sledgehammer_Fact.fact
type reconstructor = Sledgehammer_Reconstruct.reconstructor
type play = Sledgehammer_Reconstruct.play
type minimize_command = Sledgehammer_Reconstruct.minimize_command
@@ -62,20 +63,17 @@
threshold_divisor : real,
ridiculous_threshold : real}
- datatype prover_fact =
- Untranslated_Fact of (string * stature) * thm |
- SMT_Weighted_Fact of (string * stature) * (int option * thm)
-
type prover_problem =
{state : Proof.state,
goal : thm,
subgoal : int,
subgoal_count : int,
- facts : prover_fact list}
+ factss : (string * fact list) list}
type prover_result =
{outcome : failure option,
used_facts : (string * stature) list,
+ used_from : fact list,
run_time : Time.time,
preplay : play Lazy.lazy,
message : play -> string,
@@ -123,10 +121,6 @@
val weight_smt_fact :
Proof.context -> int -> ((string * stature) * thm) * int
-> (string * stature) * (int option * thm)
- val untranslated_fact : prover_fact -> (string * stature) * thm
- val smt_weighted_fact :
- Proof.context -> int -> prover_fact * int
- -> (string * stature) * (int option * thm)
val supported_provers : Proof.context -> unit
val kill_provers : unit -> unit
val running_provers : unit -> unit
@@ -149,6 +143,7 @@
open ATP_Proof_Reconstruct
open Metis_Tactic
open Sledgehammer_Util
+open Sledgehammer_Fact
open Sledgehammer_Reconstruct
@@ -201,7 +196,7 @@
if is_reconstructor name then
reconstructor_default_max_facts
else if is_atp thy name then
- fold (Integer.max o #1 o fst o snd o snd)
+ fold (Integer.max o fst o #1 o fst o snd o snd)
(get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0
else (* is_smt_prover ctxt name *)
SMT_Solver.default_max_relevant ctxt name
@@ -355,20 +350,17 @@
threshold_divisor : real,
ridiculous_threshold : real}
-datatype prover_fact =
- Untranslated_Fact of (string * stature) * thm |
- SMT_Weighted_Fact of (string * stature) * (int option * thm)
-
type prover_problem =
{state : Proof.state,
goal : thm,
subgoal : int,
subgoal_count : int,
- facts : prover_fact list}
+ factss : (string * fact list) list}
type prover_result =
{outcome : failure option,
used_facts : (string * stature) list,
+ used_from : fact list,
run_time : Time.time,
preplay : play Lazy.lazy,
message : play -> string,
@@ -430,12 +422,6 @@
(info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
end
-fun untranslated_fact (Untranslated_Fact p) = p
- | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
-fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
- | smt_weighted_fact ctxt num_facts (fact, j) =
- (untranslated_fact fact, j) |> weight_smt_fact ctxt num_facts
-
fun overlord_file_location_for_prover prover =
(getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
@@ -544,6 +530,12 @@
clearly inconsistent facts such as X = a | X = b, though it by no means
guarantees soundness. *)
+fun get_facts_for_filter _ [(_, facts)] = facts
+ | get_facts_for_filter fact_filter factss =
+ case AList.lookup (op =) factss fact_filter of
+ SOME facts => facts
+ | NONE => snd (hd factss)
+
(* Unwanted equalities are those between a (bound or schematic) variable that
does not properly occur in the second operand. *)
val is_exhaustive_finite =
@@ -642,11 +634,11 @@
({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
(params as {debug, verbose, overlord, type_enc, strict, lam_trans,
- uncurried_aliases, max_facts, max_mono_iters,
+ uncurried_aliases, fact_filter, max_facts, max_mono_iters,
max_new_mono_instances, isar_proofs, isar_shrink,
slice, timeout, preplay_timeout, ...})
minimize_command
- ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
+ ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
@@ -723,10 +715,14 @@
end
fun run_slice time_left (cache_key, cache_value)
(slice, (time_frac,
- (key as (best_max_facts, format, best_type_enc,
- best_lam_trans, best_uncurried_aliases),
+ (key as ((best_max_facts, best_fact_filter), format,
+ best_type_enc, best_lam_trans,
+ best_uncurried_aliases),
extra))) =
let
+ val effective_fact_filter =
+ fact_filter |> the_default best_fact_filter
+ val facts = get_facts_for_filter effective_fact_filter factss
val num_facts =
length facts |> is_none max_facts ? Integer.min best_max_facts
val soundness = if strict then Strict else Non_Strict
@@ -773,7 +769,6 @@
cache_value
else
facts
- |> map untranslated_fact
|> not sound
? filter_out (is_dangerous_prop ctxt o prop_of o snd)
|> take num_facts
@@ -798,7 +793,7 @@
|> lines_for_atp_problem format ord ord_info
|> cons ("% " ^ command ^ "\n")
|> File.write_list prob_path
- val ((output, run_time), (atp_proof, outcome)) =
+ val ((output, run_time), used_from, (atp_proof, outcome)) =
time_limit generous_slice_timeout Isabelle_System.bash_output
command
|>> (if overlord then
@@ -807,14 +802,14 @@
I)
|> fst |> split_time
|> (fn accum as (output, _) =>
- (accum,
+ (accum, facts,
extract_tstplike_proof_and_outcome verbose proof_delims
known_failures output
|>> atp_proof_from_tstplike_proof atp_problem
handle UNRECOGNIZED_ATP_PROOF () =>
([], SOME ProofIncomplete)))
handle TimeLimit.TimeOut =>
- (("", the slice_timeout), ([], SOME TimedOut))
+ (("", the slice_timeout), [], ([], SOME TimedOut))
val outcome =
case outcome of
NONE =>
@@ -830,10 +825,12 @@
end
| NONE => NONE)
| _ => outcome
- in ((SOME key, value), (output, run_time, atp_proof, outcome)) end
+ in
+ ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
+ end
val timer = Timer.startRealTimer ()
fun maybe_run_slice slice
- (result as (cache, (_, run_time0, _, SOME _))) =
+ (result as (cache, (_, run_time0, _, _, SOME _))) =
let
val time_left =
Option.map
@@ -845,25 +842,26 @@
result
else
run_slice time_left cache slice
- |> (fn (cache, (output, run_time, atp_proof, outcome)) =>
- (cache, (output, Time.+ (run_time0, run_time),
+ |> (fn (cache, (output, run_time, used_from, atp_proof,
+ outcome)) =>
+ (cache, (output, Time.+ (run_time0, run_time), used_from,
atp_proof, outcome)))
end
| maybe_run_slice _ result = result
in
((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
- ("", Time.zeroTime, [], SOME InternalError))
+ ("", Time.zeroTime, [], [], SOME InternalError))
|> fold maybe_run_slice actual_slices
end
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
fun clean_up () =
if dest_dir = "" then (try File.rm prob_path; ()) else ()
- fun export (_, (output, _, _, _)) =
+ fun export (_, (output, _, _, _, _)) =
if dest_dir = "" then ()
else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
val ((_, (_, pool, fact_names, _, sym_tab)),
- (output, run_time, atp_proof, outcome)) =
+ (output, run_time, used_from, atp_proof, outcome)) =
with_cleanup clean_up run () |> tap export
val important_message =
if mode = Normal andalso
@@ -887,8 +885,7 @@
Lazy.lazy (fn () =>
let
val used_pairs =
- facts |> map untranslated_fact
- |> filter_used_facts false used_facts
+ used_from |> filter_used_facts false used_facts
in
play_one_line_proof mode debug verbose preplay_timeout
used_pairs state subgoal (hd reconstrs) reconstrs
@@ -926,10 +923,15 @@
([], Lazy.value (Failed_to_Play plain_metis),
fn _ => string_for_failure failure, "")
in
- {outcome = outcome, used_facts = used_facts, run_time = run_time,
- preplay = preplay, message = message, message_tail = message_tail}
+ {outcome = outcome, used_facts = used_facts, used_from = used_from,
+ run_time = run_time, preplay = preplay, message = message,
+ message_tail = message_tail}
end
+fun rotate_one (x :: xs) = xs @ [x]
+
+fun app_hd f (x :: xs) = f x :: xs
+
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
these are sorted out properly in the SMT module, we have to interpret these
ourselves. *)
@@ -962,11 +964,12 @@
val smt_max_slices =
Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
val smt_slice_fact_frac =
- Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.5)
+ Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac}
+ (K 0.667)
val smt_slice_time_frac =
- Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.5)
+ Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
val smt_slice_min_secs =
- Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5)
+ Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
fun smt_filter_loop name
({debug, verbose, overlord, max_mono_iters,
@@ -987,7 +990,8 @@
val ctxt = Proof.context_of state |> repair_context
val state = state |> Proof.map_context (K ctxt)
val max_slices = if slice then Config.get ctxt smt_max_slices else 1
- fun do_slice timeout slice outcome0 time_so_far facts =
+ fun do_slice timeout slice outcome0 time_so_far
+ (weighted_factss as (fact_filter, weighted_facts) :: _) =
let
val timer = Timer.startRealTimer ()
val state =
@@ -1006,7 +1010,7 @@
end
else
timeout
- val num_facts = length facts
+ val num_facts = length weighted_facts
val _ =
if debug then
quote name ^ " slice " ^ string_of_int slice ^ " with " ^
@@ -1022,7 +1026,8 @@
if debug then Output.urgent_message "Invoking SMT solver..." else ()
val state_facts = these (try (#facts o Proof.goal) state)
val (outcome, used_facts) =
- SMT_Solver.smt_filter_preprocess ctxt state_facts goal facts i
+ SMT_Solver.smt_filter_preprocess ctxt state_facts goal weighted_facts
+ i
|> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
|> (fn {outcome, used_facts} => (outcome, used_facts))
handle exn => if Exn.is_interrupt exn then
@@ -1053,36 +1058,48 @@
val new_num_facts =
Real.ceil (Config.get ctxt smt_slice_fact_frac
* Real.fromInt num_facts)
+ val weighted_factss as (new_fact_filter, _) :: _ =
+ weighted_factss
+ |> rotate_one
+ |> app_hd (apsnd (take new_num_facts))
+ val show_filter = fact_filter <> new_fact_filter
+ fun num_of_facts fact_filter num_facts =
+ string_of_int num_facts ^
+ (if show_filter then " " ^ quote fact_filter else "") ^
+ " fact" ^ plural_s num_facts
val _ =
if verbose andalso is_some outcome then
- quote name ^ " invoked with " ^ string_of_int num_facts ^
- " fact" ^ plural_s num_facts ^ ": " ^
+ quote name ^ " invoked with " ^
+ num_of_facts fact_filter num_facts ^ ": " ^
string_for_failure (failure_from_smt_failure (the outcome)) ^
- " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^
- plural_s new_num_facts ^ "..."
+ " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
+ "..."
|> Output.urgent_message
else
()
in
- facts |> take new_num_facts
- |> do_slice timeout (slice + 1) outcome0 time_so_far
+ do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
end
else
{outcome = if is_none outcome then NONE else the outcome0,
- used_facts = used_facts, run_time = time_so_far}
+ used_facts = used_facts, used_from = map (apsnd snd) weighted_facts,
+ run_time = time_so_far}
end
in do_slice timeout 1 NONE Time.zeroTime end
fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
minimize_command
- ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
+ ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val ctxt = Proof.context_of state
- val num_facts = length facts
- val facts = facts ~~ (0 upto num_facts - 1)
- |> map (smt_weighted_fact ctxt num_facts)
- val {outcome, used_facts = used_pairs, run_time} =
- smt_filter_loop name params state goal subgoal facts
+ fun weight_facts facts =
+ let val num_facts = length facts in
+ facts ~~ (0 upto num_facts - 1)
+ |> map (weight_smt_fact ctxt num_facts)
+ end
+ val weighted_factss = factss |> map (apsnd weight_facts)
+ val {outcome, used_facts = used_pairs, used_from, run_time} =
+ smt_filter_loop name params state goal subgoal weighted_factss
val used_facts = used_pairs |> map fst
val outcome = outcome |> Option.map failure_from_smt_failure
val (preplay, message, message_tail) =
@@ -1109,14 +1126,16 @@
(Lazy.value (Failed_to_Play plain_metis),
fn _ => string_for_failure failure, "")
in
- {outcome = outcome, used_facts = used_facts, run_time = run_time,
- preplay = preplay, message = message, message_tail = message_tail}
+ {outcome = outcome, used_facts = used_facts, used_from = used_from,
+ run_time = run_time, preplay = preplay, message = message,
+ message_tail = message_tail}
end
fun run_reconstructor mode name
(params as {debug, verbose, timeout, type_enc, lam_trans, ...})
minimize_command
- ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
+ ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...}
+ : prover_problem) =
let
val reconstr =
if name = metisN then
@@ -1126,15 +1145,14 @@
SMT
else
raise Fail ("unknown reconstructor: " ^ quote name)
- val used_pairs = facts |> map untranslated_fact
- val used_facts = used_pairs |> map fst
+ val used_facts = facts |> map fst
in
case play_one_line_proof (if mode = Minimize then Normal else mode) debug
- verbose timeout used_pairs state subgoal reconstr
+ verbose timeout facts state subgoal reconstr
[reconstr] of
play as Played (_, time) =>
- {outcome = NONE, used_facts = used_facts, run_time = time,
- preplay = Lazy.value play,
+ {outcome = NONE, used_facts = used_facts, used_from = facts,
+ run_time = time, preplay = Lazy.value play,
message =
fn play =>
let
@@ -1150,8 +1168,8 @@
let
val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
in
- {outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
- preplay = Lazy.value play,
+ {outcome = SOME failure, used_facts = [], used_from = [],
+ run_time = Time.zeroTime, preplay = Lazy.value play,
message = fn _ => string_for_failure failure, message_tail = ""}
end
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 13 11:46:48 2013 +0100
@@ -131,6 +131,7 @@
val is_typed_helper_name =
String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
+
fun is_typed_helper_used_in_atp_proof atp_proof =
is_axiom_used_in_proof is_typed_helper_name atp_proof
@@ -145,7 +146,7 @@
fun ext_name ctxt =
if Thm.eq_thm_prop (@{thm ext},
- singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
+ singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
isa_short_ext
else
isa_ext
@@ -158,8 +159,8 @@
insert (op =) (ext_name ctxt, (Global, General))
else if rule = leo2_unfold_def_rule then
(* LEO 1.3.3 does not record definitions properly, leading to missing
- dependencies in the TSTP proof. Remove the next line once this is
- fixed. *)
+ dependencies in the TSTP proof. Remove the next line once this is
+ fixed. *)
add_non_rec_defs fact_names
else if rule = satallax_coreN then
(fn [] =>
@@ -169,8 +170,7 @@
| facts => facts)
else
I)
- #> (if null deps then union (op =) (resolve_fact fact_names ss)
- else I)
+ #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
| add_fact _ _ _ = I
fun used_facts_in_atp_proof ctxt fact_names atp_proof =
@@ -678,6 +678,7 @@
val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
val axioms = axioms_of_ref_graph ref_graph conjs
val tainted = tainted_atoms_of_ref_graph ref_graph conjs
+ val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
val steps =
Symtab.empty
|> fold (fn Definition_Step _ => I (* FIXME *)
@@ -743,7 +744,7 @@
map (isar_step_of_direct_inf outer) infs
val (isar_proof, (preplay_fail, preplay_time)) =
ref_graph
- |> redirect_graph axioms tainted
+ |> redirect_graph axioms tainted bot
|> map (isar_step_of_direct_inf true)
|> append assms
|> (if not preplay andalso isar_shrink <= 1.0 then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Feb 13 11:46:48 2013 +0100
@@ -8,6 +8,7 @@
signature SLEDGEHAMMER_RUN =
sig
+ type fact = Sledgehammer_Fact.fact
type fact_override = Sledgehammer_Fact.fact_override
type minimize_command = Sledgehammer_Reconstruct.minimize_command
type mode = Sledgehammer_Provers.mode
@@ -17,6 +18,7 @@
val noneN : string
val timeoutN : string
val unknownN : string
+ val string_of_factss : (string * fact list) list -> string
val run_sledgehammer :
params -> mode -> int -> fact_override
-> ((string * string list) list -> string -> minimize_command)
@@ -64,8 +66,8 @@
fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
timeout, expect, ...})
- mode minimize_command only learn
- {state, goal, subgoal, subgoal_count, facts} name =
+ mode minimize_command only learn
+ {state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
let
val ctxt = Proof.context_of state
val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
@@ -79,14 +81,15 @@
val problem =
{state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count,
- facts = facts
- |> not (Sledgehammer_Provers.is_ho_atp ctxt name)
- ? filter_out (curry (op =) Induction o snd o snd o fst
- o untranslated_fact)
- |> take num_facts}
- fun print_used_facts used_facts =
- tag_list 1 facts
- |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
+ factss =
+ factss
+ |> map (apsnd ((not (is_ho_atp ctxt name)
+ ? filter_out (fn ((_, (_, Induction)), _) => true
+ | _ => false))
+ #> take num_facts))}
+ fun print_used_facts used_facts used_from =
+ tag_list 1 used_from
+ |> map (fn (j, fact) => fact |> apsnd (K j))
|> filter_used_facts false used_facts
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
|> commas
@@ -96,9 +99,10 @@
fun really_go () =
problem
|> get_minimizing_isar_prover ctxt mode learn name params minimize_command
- |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} =>
- print_used_facts used_facts
- | _ => ())
+ |> verbose
+ ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
+ print_used_facts used_facts used_from
+ | _ => ())
|> (fn {outcome, preplay, message, message_tail, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
@@ -160,11 +164,24 @@
(unknownN, state))
end
-fun class_of_smt_solver ctxt name =
- ctxt |> select_smt_solver name
- |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
+val auto_try_max_facts_divisor = 2 (* FUDGE *)
+
+fun eq_facts p = eq_list (op = o pairself fst) p
+
+fun string_of_facts facts =
+ "Including " ^ string_of_int (length facts) ^
+ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
+ (facts |> map (fst o fst) |> space_implode " ") ^ "."
-val auto_try_max_facts_divisor = 2 (* FUDGE *)
+fun string_of_factss factss =
+ if forall (null o snd) factss then
+ "Found no relevant facts."
+ else case factss of
+ [(_, facts)] => string_of_facts facts
+ | _ =>
+ factss
+ |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
+ |> space_implode "\n\n"
fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts,
slice, ...})
@@ -182,7 +199,7 @@
val ctxt = Proof.context_of state
val {facts = chained, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
- val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
+ val ho_atp = exists (is_ho_atp ctxt) provers
val reserved = reserved_isar_keyword_table ()
val css = clasimpset_rule_table_of ctxt
val all_facts =
@@ -196,15 +213,36 @@
val (smts, (ueq_atps, full_atps)) =
provers |> List.partition (is_smt_prover ctxt)
||> List.partition (is_unit_equational_atp ctxt)
- fun launch_provers state get_facts translate provers =
+ fun get_factss label is_appropriate_prop provers =
let
- val facts = get_facts ()
- val num_facts = length facts
- val facts = facts ~~ (0 upto num_facts - 1)
- |> map (translate num_facts)
+ val max_max_facts =
+ case max_facts of
+ SOME n => n
+ | NONE =>
+ 0 |> fold (Integer.max o default_max_facts_for_prover ctxt slice)
+ provers
+ |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
+ in
+ all_facts
+ |> (case is_appropriate_prop of
+ SOME is_app => filter (is_app o prop_of o snd)
+ | NONE => I)
+ |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
+ hyp_ts concl_t
+ |> tap (fn factss =>
+ if verbose then
+ label ^ plural_s (length provers) ^ ": " ^
+ string_of_factss factss
+ |> print
+ else
+ ())
+ end
+ fun launch_provers state label is_appropriate_prop provers =
+ let
+ val factss = get_factss label is_appropriate_prop provers
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts}
+ factss = factss}
fun learn prover =
mash_learn_proof ctxt params prover (prop_of goal) all_facts
val launch = launch_prover params mode minimize_command only learn
@@ -220,36 +258,6 @@
|> (if blocking then Par_List.map else map) (launch problem #> fst)
|> max_outcome_code |> rpair state
end
- fun get_facts label is_appropriate_prop provers =
- let
- val max_max_facts =
- case max_facts of
- SOME n => n
- | NONE =>
- 0 |> fold (Integer.max o default_max_facts_for_prover ctxt slice)
- provers
- |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
- in
- all_facts
- |> (case is_appropriate_prop of
- SOME is_app => filter (is_app o prop_of o snd)
- | NONE => I)
- |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
- hyp_ts concl_t
- |> map (apfst (apfst (fn name => name ())))
- |> tap (fn facts =>
- if verbose then
- label ^ plural_s (length provers) ^ ": " ^
- (if null facts then
- "Found no relevant facts."
- else
- "Including " ^ string_of_int (length facts) ^
- " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
- (facts |> map (fst o fst) |> space_implode " ") ^ ".")
- |> print
- else
- ())
- end
fun launch_atps label is_appropriate_prop atps accum =
if null atps then
accum
@@ -263,21 +271,9 @@
();
accum)
else
- launch_provers state (get_facts label is_appropriate_prop o K atps)
- (K (Untranslated_Fact o fst)) atps
+ launch_provers state label is_appropriate_prop atps
fun launch_smts accum =
- if null smts then
- accum
- else
- let
- val facts = get_facts "SMT solver" NONE smts
- val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
- in
- smts |> map (`(class_of_smt_solver ctxt))
- |> AList.group (op =)
- |> map (snd #> launch_provers state (K facts) weight #> fst)
- |> max_outcome_code |> rpair state
- end
+ if null smts then accum else launch_provers state "SMT solver" NONE smts
val launch_full_atps = launch_atps "ATP" NONE full_atps
val launch_ueq_atps =
launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps
--- a/src/Pure/Isar/attrib.ML Tue Feb 12 17:39:45 2013 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Feb 13 11:46:48 2013 +0100
@@ -420,7 +420,7 @@
setup (Binding.name "abs_def")
(Scan.succeed (Thm.rule_attribute (fn context =>
Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
- "abstract over free variables of definitionial theorem"));
+ "abstract over free variables of definitional theorem"));