--- a/src/HOL/Complete_Lattices.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/Complete_Lattices.thy Mon Mar 04 17:32:10 2013 +0100
@@ -89,6 +89,22 @@
by (simp add: fun_eq_iff SUP_def
complete_lattice.INF_def [OF dual_complete_lattice])
+lemma Sup_eqI:
+ "(\<And>y. y \<in> A \<Longrightarrow> y \<le> x) \<Longrightarrow> (\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> \<Squnion>A = x"
+ by (blast intro: antisym Sup_least Sup_upper)
+
+lemma Inf_eqI:
+ "(\<And>i. i \<in> A \<Longrightarrow> x \<le> i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x) \<Longrightarrow> \<Sqinter>A = x"
+ by (blast intro: antisym Inf_greatest Inf_lower)
+
+lemma 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> (\<Squnion>i\<in>A. f i) = x"
+ unfolding SUP_def by (rule Sup_eqI) auto
+
+lemma 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> (\<Sqinter>i\<in>A. f i) = x"
+ unfolding INF_def by (rule Inf_eqI) auto
+
lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
by (auto simp add: INF_def intro: Inf_lower)
@@ -242,6 +258,18 @@
ultimately show ?thesis by (rule Sup_upper2)
qed
+lemma SUPR_eq:
+ assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
+ assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
+ shows "(SUP i:A. f i) = (SUP j:B. g j)"
+ by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
+
+lemma INFI_eq:
+ assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
+ assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
+ shows "(INF i:A. f i) = (INF j:B. g j)"
+ by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
+
lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
by (auto intro: Inf_greatest Inf_lower)
@@ -378,6 +406,12 @@
"(\<Squnion>b. A b) = A True \<squnion> A False"
by (simp add: UNIV_bool SUP_insert sup_commute)
+lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
+ by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
+
+lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
+ unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
+
end
class complete_distrib_lattice = complete_lattice +
@@ -530,9 +564,31 @@
"(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
unfolding INF_def by auto
+lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
+proof safe
+ fix y assume "x \<le> \<Squnion>A" "y < x"
+ then have "y < \<Squnion>A" by auto
+ then show "\<exists>a\<in>A. y < a"
+ unfolding less_Sup_iff .
+qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
+
+lemma 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 Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
+proof safe
+ fix y assume "x \<ge> \<Sqinter>A" "y > x"
+ then have "y > \<Sqinter>A" by auto
+ then show "\<exists>a\<in>A. y > a"
+ unfolding Inf_less_iff .
+qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower)
+
+lemma INF_le_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
+
end
-
subsection {* Complete lattice on @{typ bool} *}
instantiation bool :: complete_lattice
--- a/src/HOL/Int.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/Int.thy Mon Mar 04 17:32:10 2013 +0100
@@ -303,6 +303,18 @@
qed
+instance int :: no_top
+ apply default
+ apply (rule_tac x="x + 1" in exI)
+ apply simp
+ done
+
+instance int :: no_bot
+ apply default
+ apply (rule_tac x="x - 1" in exI)
+ apply simp
+ done
+
subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
--- a/src/HOL/Library/Extended_Real.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy Mon Mar 04 17:32:10 2013 +0100
@@ -18,79 +18,6 @@
*}
-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"
- show "x = bot"
- proof (rule ccontr)
- assume "x \<noteq> bot" then have "bot \<notin> {x..}" by (simp add: le_less)
- then show False using `{x..} = UNIV` by simp
- qed
-qed auto
-
lemma SUPR_pair:
"(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
by (rule antisym) (auto intro!: SUP_least SUP_upper2)
@@ -99,6 +26,18 @@
"(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
by (rule antisym) (auto intro!: INF_greatest INF_lower2)
+lemma le_Sup_iff_less:
+ fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+ shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
+ unfolding le_SUP_iff
+ by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
+
+lemma Inf_le_iff_less:
+ fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+ shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
+ unfolding INF_le_iff
+ by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
+
subsection {* Definition and basic properties *}
datatype ereal = ereal real | PInfty | MInfty
@@ -368,6 +307,12 @@
end
+lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
+ using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
+
+instance ereal :: inner_dense_linorder
+ by default (blast dest: ereal_dense2)
+
instance ereal :: ordered_ab_semigroup_add
proof
fix a b c :: ereal assume "a \<le> b" then show "c + a \<le> c + b"
@@ -462,14 +407,6 @@
fixes a :: ereal shows "-a \<le> 0 \<longleftrightarrow> 0 \<le> a"
by (cases rule: ereal2_cases[of a]) auto
-lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
- using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
-
-lemma ereal_dense:
- fixes x y :: ereal assumes "x < y"
- shows "\<exists>z. x < z \<and> z < y"
- using ereal_dense2[OF `x < y`] by blast
-
lemma ereal_add_strict_mono:
fixes a b c d :: ereal
assumes "a = b" "0 \<le> a" "a \<noteq> \<infinity>" "c < d"
@@ -798,18 +735,6 @@
shows "y <= x"
by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
-lemma ereal_le_ereal:
- fixes x y :: ereal
- assumes "\<And>B. B < x \<Longrightarrow> B <= y"
- shows "x <= y"
-by (metis assms ereal_dense leD linorder_le_less_linear)
-
-lemma ereal_ge_ereal:
- fixes x y :: ereal
- assumes "ALL B. B>x --> B >= y"
- shows "x >= y"
-by (metis assms ereal_dense leD linorder_le_less_linear)
-
lemma setprod_ereal_0:
fixes f :: "'a \<Rightarrow> ereal"
shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
@@ -1199,11 +1124,11 @@
definition "bot = (-\<infinity>::ereal)"
definition "top = (\<infinity>::ereal)"
-definition "Sup S = (LEAST z. \<forall>x\<in>S. x \<le> z :: ereal)"
-definition "Inf S = (GREATEST z. \<forall>x\<in>S. z \<le> x :: ereal)"
+definition "Sup S = (SOME x :: ereal. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z))"
+definition "Inf S = (SOME x :: ereal. (\<forall>y\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x))"
lemma ereal_complete_Sup:
- fixes S :: "ereal set" assumes "S \<noteq> {}"
+ fixes S :: "ereal set"
shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
proof cases
assume "\<exists>x. \<forall>a\<in>S. a \<le> ereal x"
@@ -1211,69 +1136,23 @@
then have "\<infinity> \<notin> S" by force
show ?thesis
proof cases
- assume "S = {-\<infinity>}"
- then show ?thesis by (auto intro!: exI[of _ "-\<infinity>"])
- next
- assume "S \<noteq> {-\<infinity>}"
- with `S \<noteq> {}` `\<infinity> \<notin> S` obtain x where "x \<in> S - {-\<infinity>}" "x \<noteq> \<infinity>" by auto
- with y `\<infinity> \<notin> S` have "\<forall>z\<in>real ` (S - {-\<infinity>}). z \<le> y"
- by (auto simp: real_of_ereal_ord_simps)
- with complete_real[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
- obtain s where s:
- "\<forall>y\<in>S - {-\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S - {-\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z"
- by auto
+ assume "S \<noteq> {-\<infinity>} \<and> S \<noteq> {}"
+ with `\<infinity> \<notin> S` obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>" by auto
+ obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "\<And>z. (\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z"
+ proof (atomize_elim, rule complete_real)
+ show "\<exists>x. x \<in> ereal -` S" using x by auto
+ show "\<exists>z. \<forall>x\<in>ereal -` S. x \<le> z" by (auto dest: y intro!: exI[of _ y])
+ qed
show ?thesis
proof (safe intro!: exI[of _ "ereal s"])
- fix z assume "z \<in> S" with `\<infinity> \<notin> S` show "z \<le> ereal s"
- proof (cases z)
- case (real r)
- then show ?thesis
- using s(1)[rule_format, of z] `z \<in> S` `z = ereal r` by auto
- qed auto
+ fix y assume "y \<in> S" with s `\<infinity> \<notin> S` show "y \<le> ereal s"
+ by (cases y) auto
next
- fix z assume *: "\<forall>y\<in>S. y \<le> z"
- with `S \<noteq> {-\<infinity>}` `S \<noteq> {}` show "ereal s \<le> z"
- proof (cases z)
- case (real u)
- with * have "s \<le> u"
- by (intro s(2)[of u]) (auto simp: real_of_ereal_ord_simps)
- then show ?thesis using real by simp
- qed auto
+ fix z assume "\<forall>y\<in>S. y \<le> z" with `S \<noteq> {-\<infinity>} \<and> S \<noteq> {}` show "ereal s \<le> z"
+ by (cases z) (auto intro!: s)
qed
- qed
-next
- assume *: "\<not> (\<exists>x. \<forall>a\<in>S. a \<le> ereal x)"
- show ?thesis
- proof (safe intro!: exI[of _ \<infinity>])
- fix y assume **: "\<forall>z\<in>S. z \<le> y"
- with * show "\<infinity> \<le> y"
- proof (cases y)
- case MInf with * ** show ?thesis by (force simp: not_le)
- qed auto
- qed simp
-qed
-
-lemma ereal_complete_Inf:
- fixes S :: "ereal set" assumes "S ~= {}"
- shows "EX x. (ALL y:S. x <= y) & (ALL z. (ALL y:S. z <= y) --> z <= x)"
-proof-
-def S1 == "uminus ` S"
-hence "S1 ~= {}" using assms by auto
-then obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
- using ereal_complete_Sup[of S1] by auto
-{ fix z assume "ALL y:S. z <= y"
- hence "ALL y:S1. y <= -z" unfolding S1_def by auto
- hence "x <= -z" using x_def by auto
- hence "z <= -x"
- apply (subst ereal_uminus_uminus[symmetric])
- unfolding ereal_minus_le_minus . }
-moreover have "(ALL y:S. -x <= y)"
- using x_def unfolding S1_def
- apply simp
- apply (subst (3) ereal_uminus_uminus[symmetric])
- unfolding ereal_minus_le_minus by simp
-ultimately show ?thesis by auto
-qed
+ qed (auto intro!: exI[of _ "-\<infinity>"])
+qed (fastforce intro!: exI[of _ \<infinity>] ereal_top intro: order_trans dest: less_imp_le simp: not_le)
lemma ereal_complete_uminus_eq:
fixes S :: "ereal set"
@@ -1281,100 +1160,40 @@
\<longleftrightarrow> (\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -x)"
by simp (metis ereal_minus_le_minus ereal_uminus_uminus)
-lemma ereal_Sup_uminus_image_eq:
- fixes S :: "ereal set"
- shows "Sup (uminus ` S) = - Inf S"
-proof cases
- assume "S = {}"
- moreover have "(THE x. All (op \<le> x)) = (-\<infinity>::ereal)"
- by (rule the_equality) (auto intro!: ereal_bot)
- moreover have "(SOME x. \<forall>y. y \<le> x) = (\<infinity>::ereal)"
- by (rule some_equality) (auto intro!: ereal_top)
- ultimately show ?thesis unfolding Inf_ereal_def Sup_ereal_def
- Least_def Greatest_def GreatestM_def by simp
-next
- assume "S \<noteq> {}"
- with ereal_complete_Sup[of "uminus`S"]
- obtain x where x: "(\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -x)"
- unfolding ereal_complete_uminus_eq by auto
- show "Sup (uminus ` S) = - Inf S"
- unfolding Inf_ereal_def Greatest_def GreatestM_def
- proof (intro someI2[of _ _ "\<lambda>x. Sup (uminus`S) = - x"])
- show "(\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> -x)"
- using x .
- fix x' assume "(\<forall>y\<in>S. x' \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> x')"
- then have "(\<forall>y\<in>uminus`S. y \<le> - x') \<and> (\<forall>y. (\<forall>z\<in>uminus`S. z \<le> y) \<longrightarrow> - x' \<le> y)"
- unfolding ereal_complete_uminus_eq by simp
- then show "Sup (uminus ` S) = -x'"
- unfolding Sup_ereal_def ereal_uminus_eq_iff
- by (intro Least_equality) auto
- qed
-qed
+lemma ereal_complete_Inf:
+ "\<exists>x. (\<forall>y\<in>S::ereal set. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x)"
+ using ereal_complete_Sup[of "uminus ` S"] unfolding ereal_complete_uminus_eq by auto
instance
-proof
- { fix x :: ereal and A
- show "bot <= x" by (cases x) (simp_all add: bot_ereal_def)
- show "x <= top" by (simp add: top_ereal_def) }
-
- { fix x :: ereal and A assume "x : A"
- with ereal_complete_Sup[of A]
- obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto
- hence "x <= s" using `x : A` by auto
- also have "... = Sup A" using s unfolding Sup_ereal_def
- by (auto intro!: Least_equality[symmetric])
- finally show "x <= Sup A" . }
- note le_Sup = this
-
- { fix x :: ereal and A assume *: "!!z. (z : A ==> z <= x)"
- show "Sup A <= x"
- proof (cases "A = {}")
- case True
- hence "Sup A = -\<infinity>" unfolding Sup_ereal_def
- by (auto intro!: Least_equality)
- thus "Sup A <= x" by simp
- next
- case False
- with ereal_complete_Sup[of A]
- obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto
- hence "Sup A = s"
- unfolding Sup_ereal_def by (auto intro!: Least_equality)
- also have "s <= x" using * s by auto
- finally show "Sup A <= x" .
- qed }
- note Sup_le = this
-
- { fix x :: ereal and A assume "x \<in> A"
- with le_Sup[of "-x" "uminus`A"] show "Inf A \<le> x"
- unfolding ereal_Sup_uminus_image_eq by simp }
-
- { fix x :: ereal and A assume *: "!!z. (z : A ==> x <= z)"
- with Sup_le[of "uminus`A" "-x"] show "x \<le> Inf A"
- unfolding ereal_Sup_uminus_image_eq by force }
-qed
+ by default (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
+ simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
end
instance ereal :: complete_linorder ..
+lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
+ by (auto intro!: Sup_eqI
+ simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
+ intro!: complete_lattice_class.Inf_lower2)
+
+lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
+ by (auto intro!: inj_onI)
+
+lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S"
+ using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
+
lemma ereal_SUPR_uminus:
fixes f :: "'a => ereal"
shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
- unfolding SUP_def INF_def
using ereal_Sup_uminus_image_eq[of "f`R"]
- by (simp add: image_image)
+ by (simp add: SUP_def INF_def image_image)
lemma ereal_INFI_uminus:
fixes f :: "'a => ereal"
shows "(INF i : R. -(f i)) = -(SUP i : R. f i)"
using ereal_SUPR_uminus[of _ "\<lambda>x. - f x"] by simp
-lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S) = - Sup (S::ereal set)"
- using ereal_Sup_uminus_image_eq[of "uminus ` S"] by (simp add: image_image)
-
-lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
- by (auto intro!: inj_onI)
-
lemma ereal_image_uminus_shift:
fixes X Y :: "ereal set" shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
proof
@@ -1392,14 +1211,7 @@
lemma Sup_eq_MInfty:
fixes S :: "ereal set" shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
-proof
- assume a: "Sup S = -\<infinity>"
- with complete_lattice_class.Sup_upper[of _ S]
- show "S={} \<or> S={-\<infinity>}" by auto
-next
- assume "S={} \<or> S={-\<infinity>}" then show "Sup S = -\<infinity>"
- unfolding Sup_ereal_def by (auto intro!: Least_equality)
-qed
+ unfolding bot_ereal_def[symmetric] by auto
lemma Inf_eq_PInfty:
fixes S :: "ereal set" shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}"
@@ -1408,13 +1220,11 @@
lemma Inf_eq_MInfty:
fixes S :: "ereal set" shows "-\<infinity> \<in> S \<Longrightarrow> Inf S = -\<infinity>"
- unfolding Inf_ereal_def
- by (auto intro!: Greatest_equality)
+ unfolding bot_ereal_def[symmetric] by auto
lemma Sup_eq_PInfty:
fixes S :: "ereal set" shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
- unfolding Sup_ereal_def
- by (auto intro!: Least_equality)
+ unfolding top_ereal_def[symmetric] by auto
lemma Sup_ereal_close:
fixes e :: ereal
@@ -1447,43 +1257,6 @@
by (auto simp: top_ereal_def)
qed
-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")
-proof-
-{ assume "?rhs"
- { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
- then obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
- then obtain i where "i : A & y <= f i" using `?rhs` by auto
- hence "y <= (SUP i:A. f i)" using SUP_upper[of i A f] by auto
- hence False using y_def by auto
- } hence "?lhs" by auto
-}
-moreover
-{ assume "?lhs" hence "?rhs"
- by (metis less_SUP_iff order_less_imp_le order_less_le_trans)
-} ultimately show ?thesis by auto
-qed
-
-lemma ereal_Inf_le:
- fixes x :: ereal
- shows "((INF i:A. f i) <= x) <-> (ALL y. x < y --> (EX i. i : A & f i <= y))"
-(is "?lhs <-> ?rhs")
-proof-
-{ assume "?rhs"
- { assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le)
- then obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
- then obtain i where "i : A & f i <= y" using `?rhs` by auto
- hence "(INF i:A. f i) <= y" using INF_lower[of i A f] by auto
- hence False using y_def by auto
- } hence "?lhs" by auto
-}
-moreover
-{ assume "?lhs" hence "?rhs"
- by (metis INF_less_iff order_le_less order_less_le_trans)
-} ultimately show ?thesis by auto
-qed
-
lemma Inf_less:
fixes x :: ereal
assumes "(INF i:A. f i) < x"
@@ -1495,44 +1268,6 @@
thus False using assms by auto
qed
-lemma same_INF:
- assumes "ALL e:A. f e = g e"
- shows "(INF e:A. f e) = (INF e:A. g e)"
-proof-
-have "f ` A = g ` A" unfolding image_def using assms by auto
-thus ?thesis unfolding INF_def by auto
-qed
-
-lemma same_SUP:
- assumes "ALL e:A. f e = g e"
- shows "(SUP e:A. f e) = (SUP e:A. g e)"
-proof-
-have "f ` A = g ` A" unfolding image_def using assms by auto
-thus ?thesis unfolding SUP_def by auto
-qed
-
-lemma SUPR_eq:
- assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<le> g j"
- assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<le> f i"
- shows "(SUP i:A. f i) = (SUP j:B. g j)"
-proof (intro antisym)
- show "(SUP i:A. f i) \<le> (SUP j:B. g j)"
- using assms by (metis SUP_least SUP_upper2)
- show "(SUP i:B. g i) \<le> (SUP j:A. f j)"
- 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>"
@@ -2155,39 +1890,6 @@
lemma ereal_real': assumes "\<bar>x\<bar> \<noteq> \<infinity>" shows "ereal (real x) = x"
using assms by auto
-lemma ereal_le_ereal_bounded:
- fixes x y z :: ereal
- assumes "z \<le> y"
- assumes *: "\<And>B. z < B \<Longrightarrow> B < x \<Longrightarrow> B \<le> y"
- shows "x \<le> y"
-proof (rule ereal_le_ereal)
- fix B assume "B < x"
- show "B \<le> y"
- proof cases
- assume "z < B" from *[OF this `B < x`] show "B \<le> y" .
- next
- assume "\<not> z < B" with `z \<le> y` show "B \<le> y" by auto
- qed
-qed
-
-lemma fixes x y :: ereal
- shows Sup_atMost[simp]: "Sup {.. y} = y"
- and Sup_lessThan[simp]: "Sup {..< y} = y"
- and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y"
- and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y"
- and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
- by (auto simp: Sup_ereal_def intro!: Least_equality
- intro: ereal_le_ereal ereal_le_ereal_bounded[of x])
-
-lemma Sup_greaterThanlessThan[simp]:
- fixes x y :: ereal assumes "x < y" shows "Sup { x <..< y} = y"
- unfolding Sup_ereal_def
-proof (intro Least_equality ereal_le_ereal_bounded[of _ _ y])
- fix z assume z: "\<forall>u\<in>{x<..<y}. u \<le> z"
- from ereal_dense[OF `x < y`] guess w .. note w = this
- with z[THEN bspec, of w] show "x \<le> z" by auto
-qed auto
-
lemma real_ereal_id: "real o ereal = id"
proof-
{ fix x have "(real o ereal) x = id x" by auto }
@@ -2257,6 +1959,7 @@
assumes "f ----> f0"
assumes "open S" "f0 : S"
obtains N where "ALL n>=N. f n : S"
+ using assms using tendsto_def
using tendsto_explicit[of f f0] assms by auto
lemma ereal_LimI_finite_iff:
--- a/src/HOL/Limits.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/Limits.thy Mon Mar 04 17:32:10 2013 +0100
@@ -264,6 +264,9 @@
lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
by (rule eventually_False [symmetric])
+lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
+ by (cases P) (simp_all add: eventually_False)
+
subsection {* Map function for filters *}
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Mar 04 17:32:10 2013 +0100
@@ -82,7 +82,7 @@
case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
then obtain b where b_def: "a<b & b<a+e"
- using fin ereal_between ereal_dense[of a "a+e"] by auto
+ using fin ereal_between dense[of a "a+e"] by auto
then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
then show False using b_def e by auto
qed
@@ -157,7 +157,7 @@
{ assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this
then obtain b where b_def: "Inf S-e<b & b<Inf S"
- using fin ereal_between[of "Inf S" e] ereal_dense[of "Inf S-e"] by auto
+ using fin ereal_between[of "Inf S" e] dense[of "Inf S-e"] by auto
then have "b: {Inf S-e <..< Inf S+e}" using e fin ereal_between[of "Inf S" e]
by auto
then have "b:S" using e by auto
@@ -335,7 +335,7 @@
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)
+ proof (rule dense_le)
fix B assume "B < l"
then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
by (intro S[rule_format]) auto
@@ -369,7 +369,7 @@
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)
+ proof (rule dense_ge)
fix B assume "l < B"
then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
by (intro S[rule_format]) auto
--- a/src/HOL/Nat.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/Nat.thy Mon Mar 04 17:32:10 2013 +0100
@@ -455,6 +455,9 @@
end
+instance nat :: no_top
+ by default (auto intro: less_Suc_eq_le[THEN iffD2])
+
subsubsection {* Introduction properties *}
lemma lessI [iff]: "n < Suc n"
--- a/src/HOL/Orderings.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/Orderings.thy Mon Mar 04 17:32:10 2013 +0100
@@ -1135,10 +1135,10 @@
subsection {* Dense orders *}
-class dense_linorder = linorder +
- assumes gt_ex: "\<exists>y. x < y"
- and lt_ex: "\<exists>y. y < x"
- and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
+class inner_dense_order = order +
+ assumes dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
+
+class inner_dense_linorder = linorder + inner_dense_order
begin
lemma dense_le:
@@ -1175,8 +1175,50 @@
qed
qed
+lemma dense_ge:
+ fixes y z :: 'a
+ assumes "\<And>x. z < x \<Longrightarrow> y \<le> x"
+ shows "y \<le> z"
+proof (rule ccontr)
+ assume "\<not> ?thesis"
+ hence "z < y" by simp
+ from dense[OF this]
+ obtain x where "x < y" and "z < x" by safe
+ moreover have "y \<le> x" using assms[OF `z < x`] .
+ ultimately show False by auto
+qed
+
+lemma dense_ge_bounded:
+ fixes x y z :: 'a
+ assumes "z < x"
+ assumes *: "\<And>w. \<lbrakk> z < w ; w < x \<rbrakk> \<Longrightarrow> y \<le> w"
+ shows "y \<le> z"
+proof (rule dense_ge)
+ fix w assume "z < w"
+ from dense[OF `z < x`] obtain u where "z < u" "u < x" by safe
+ from linear[of u w]
+ show "y \<le> w"
+ proof (rule disjE)
+ assume "w \<le> u"
+ from `z < w` le_less_trans[OF `w \<le> u` `u < x`]
+ show "y \<le> w" by (rule *)
+ next
+ assume "u \<le> w"
+ from *[OF `z < u` `u < x`] `u \<le> w`
+ show "y \<le> w" by (rule order_trans)
+ qed
+qed
+
end
+class no_top = order +
+ assumes gt_ex: "\<exists>y. x < y"
+
+class no_bot = order +
+ assumes lt_ex: "\<exists>y. y < x"
+
+class dense_linorder = inner_dense_linorder + no_top + no_bot
+
subsection {* Wellorders *}
class wellorder = linorder +
--- a/src/HOL/Probability/Caratheodory.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Mon Mar 04 17:32:10 2013 +0100
@@ -363,8 +363,7 @@
assumes posf: "positive M f" and ca: "countably_additive M f"
and s: "s \<in> M"
shows "Inf (measure_set M f s) = f s"
- unfolding Inf_ereal_def
-proof (safe intro!: Greatest_equality)
+proof (intro Inf_eqI)
fix z
assume z: "z \<in> measure_set M f s"
from this obtain A where
@@ -394,12 +393,7 @@
qed
also have "... = z" by (rule si)
finally show "f s \<le> z" .
-next
- fix y
- assume y: "\<forall>u \<in> measure_set M f s. y \<le> u"
- thus "y \<le> f s"
- by (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl])
-qed
+qed (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl])
lemma measure_set_pos:
assumes posf: "positive M f" "r \<in> measure_set M f X"
--- a/src/HOL/Probability/Radon_Nikodym.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Mon Mar 04 17:32:10 2013 +0100
@@ -57,7 +57,7 @@
proof
fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)"
using measure[of i] emeasure_nonneg[of M "A i"]
- by (auto intro!: ereal_dense simp: ereal_0_gt_inverse ereal_zero_le_0_iff)
+ by (auto intro!: dense simp: ereal_0_gt_inverse ereal_zero_le_0_iff)
qed
from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
"\<And>i. n i < inverse (2^Suc i * emeasure M (A i))" by auto
--- a/src/HOL/SEQ.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/SEQ.thy Mon Mar 04 17:32:10 2013 +0100
@@ -322,6 +322,16 @@
shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
using trivial_limit_sequentially by (rule tendsto_const_iff)
+lemma LIMSEQ_SUP:
+ "incseq X \<Longrightarrow> X ----> (SUP i. X i :: 'a :: {complete_linorder, linorder_topology})"
+ by (intro increasing_tendsto)
+ (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
+
+lemma LIMSEQ_INF:
+ "decseq X \<Longrightarrow> X ----> (INF i. X i :: 'a :: {complete_linorder, linorder_topology})"
+ by (intro decreasing_tendsto)
+ (auto simp: INF_lower INF_less_iff decseq_def eventually_sequentially intro: le_less_trans)
+
lemma LIMSEQ_ignore_initial_segment:
"f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
apply (rule topological_tendstoI)
--- a/src/HOL/Set_Interval.thy Mon Mar 04 15:03:46 2013 +0100
+++ b/src/HOL/Set_Interval.thy Mon Mar 04 17:32:10 2013 +0100
@@ -267,7 +267,7 @@
end
-context dense_linorder
+context inner_dense_linorder
begin
lemma greaterThanLessThan_empty_iff[simp]:
@@ -310,6 +310,22 @@
end
+context no_top
+begin
+
+lemma greaterThan_non_empty: "{x <..} \<noteq> {}"
+ using gt_ex[of x] by auto
+
+end
+
+context no_bot
+begin
+
+lemma lessThan_non_empty: "{..< x} \<noteq> {}"
+ using lt_ex[of x] by auto
+
+end
+
lemma (in linorder) atLeastLessThan_subset_iff:
"{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
apply (auto simp:subset_eq Ball_def)
@@ -330,6 +346,20 @@
shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
using atLeastLessThan_inj assms by auto
+context complete_lattice
+begin
+
+lemma atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
+ by (auto simp: set_eq_iff intro: le_bot)
+
+lemma atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
+ by (auto simp: set_eq_iff intro: top_le)
+
+lemma atLeastAtMost_eq_UNIV_iff: "{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)"
+ by (auto simp: set_eq_iff intro: top_le le_bot)
+
+end
+
subsubsection {* Intersection *}
context linorder
@@ -364,6 +394,36 @@
end
+context complete_lattice
+begin
+
+lemma
+ shows Sup_atLeast[simp]: "Sup {x ..} = top"
+ and Sup_greaterThanAtLeast[simp]: "x < top \<Longrightarrow> Sup {x <..} = top"
+ and Sup_atMost[simp]: "Sup {.. y} = y"
+ and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y"
+ and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y"
+ by (auto intro!: Sup_eqI)
+
+lemma
+ shows Inf_atMost[simp]: "Inf {.. x} = bot"
+ and Inf_atMostLessThan[simp]: "top < x \<Longrightarrow> Inf {..< x} = bot"
+ and Inf_atLeast[simp]: "Inf {x ..} = x"
+ and Inf_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Inf { x .. y} = x"
+ and Inf_atLeastLessThan[simp]: "x < y \<Longrightarrow> Inf { x ..< y} = x"
+ by (auto intro!: Inf_eqI)
+
+end
+
+lemma
+ fixes x y :: "'a :: {complete_lattice, inner_dense_linorder}"
+ shows Sup_lessThan[simp]: "Sup {..< y} = y"
+ and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
+ and Sup_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Sup { x <..< y} = y"
+ and Inf_greaterThan[simp]: "Inf {x <..} = x"
+ and Inf_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Inf { x <.. y} = x"
+ and Inf_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Inf { x <..< y} = x"
+ by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)
subsection {* Intervals of natural numbers *}
--- a/src/Tools/subtyping.ML Mon Mar 04 15:03:46 2013 +0100
+++ b/src/Tools/subtyping.ML Mon Mar 04 17:32:10 2013 +0100
@@ -20,7 +20,7 @@
(** coercions data **)
datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ;
-datatype coerce_arg = PERMIT | FORBID
+datatype coerce_arg = PERMIT | FORBID | LEAVE
datatype data = Data of
{coes: (term * ((typ list * typ list) * term list)) Symreltab.table, (*coercions table*)
@@ -29,7 +29,7 @@
(*coercions graph restricted to base types - for efficiency reasons strored in the context*)
coes_graph: int Graph.T,
tmaps: (term * variance list) Symtab.table, (*map functions*)
- coerce_args: coerce_arg option list Symtab.table (*special constants with non-coercible arguments*)};
+ coerce_args: coerce_arg list Symtab.table (*special constants with non-coercible arguments*)};
fun make_data (coes, full_graph, coes_graph, tmaps, coerce_args) =
Data {coes = coes, full_graph = full_graph, coes_graph = coes_graph,
@@ -297,8 +297,7 @@
let
val mk_coerce_args = the_default [] o Symtab.lookup (coerce_args_of ctxt);
fun update _ [] = old
- | update 0 (coerce :: _) =
- (case coerce of NONE => old | SOME PERMIT => true | SOME FORBID => false)
+ | update 0 (coerce :: _) = (case coerce of LEAVE => old | PERMIT => true | FORBID => false)
| update n (_ :: cs) = update (n - 1) cs;
val (f, n) = Term.strip_comb (Type.strip_constraints t) ||> length;
in
@@ -1054,9 +1053,7 @@
(* theory setup *)
val parse_coerce_args =
- Args.$$$ "+" >> K (SOME PERMIT) ||
- Args.$$$ "-" >> K (SOME FORBID) ||
- Args.$$$ "0" >> K NONE
+ Args.$$$ "+" >> K PERMIT || Args.$$$ "-" >> K FORBID || Args.$$$ "0" >> K LEAVE
val setup =
Context.theory_map add_term_check #>