--- a/NEWS Tue Oct 16 23:12:38 2007 +0200
+++ b/NEWS Tue Oct 16 23:12:45 2007 +0200
@@ -109,6 +109,24 @@
*** Pure ***
+* Class-context aware syntax for class target ("user space type system"):
+Local operations in class context (fixes, definitions, axiomatizations,
+abbreviations) are identified with their global counterparts during reading and
+printing of terms. Practically, this allows to use the same syntax for
+both local *and* global operations. Syntax declarations referring directly to
+local fixes, definitions, axiomatizations and abbreviations are applied to their
+global counterparts instead (but explicit notation declarations still are local);
+the special treatment of \<^loc> in local syntax declarations has been abandoned.
+INCOMPATIBILITY. Most affected theories shall work after the following
+purgatory:
+
+ perl -i -pe 's/\\<\^loc>//g;' THYFILENAME1 THYFILENAME2 ...
+
+Current limitations:
+- printing of local abbreviations sometimes yields unexpected results.
+- some facilities (e.g. attribute of, legacy tac-methods) still do not use
+canonical interfaces for printing and reading terms.
+
* Code generator: consts in 'consts_code' Isar commands are now
referred to by usual term syntax (including optional type
annotations).
@@ -116,7 +134,7 @@
* Code generator: basic definitions (from 'definition', 'constdefs',
or primitive 'instance' definitions) are added automatically to the
table of defining equations. Primitive defs are not used as defining
-equations by default any longer. defining equations are now definitly
+equations by default any longer. Defining equations are now definitly
restricted to meta "==" and object equality "=".
* The 'class' package offers a combination of axclass and locale to
--- a/src/HOL/Dense_Linear_Order.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy Tue Oct 16 23:12:45 2007 +0200
@@ -22,153 +22,153 @@
context linorder
begin
-lemma less_not_permute: "\<not> (x \<^loc>< y \<and> y \<^loc>< x)" by (simp add: not_less linear)
+lemma less_not_permute: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear)
lemma gather_simps:
shows
- "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> x \<^loc>< u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> (insert u U). x \<^loc>< y) \<and> P x)"
- and "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> l \<^loc>< x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> P x)"
- "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> x \<^loc>< u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> (insert u U). x \<^loc>< y))"
- and "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> l \<^loc>< x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y))" by auto
+ "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y) \<and> P x)"
+ and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y) \<and> P x)"
+ "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y))"
+ and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y))" by auto
lemma
- gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y\<in> {}. x \<^loc>< y) \<and> P x)"
+ gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)"
by simp
-text{* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
-lemma minf_lt: "\<exists>z . \<forall>x. x \<^loc>< z \<longrightarrow> (x \<^loc>< t \<longleftrightarrow> True)" by auto
-lemma minf_gt: "\<exists>z . \<forall>x. x \<^loc>< z \<longrightarrow> (t \<^loc>< x \<longleftrightarrow> False)"
+text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
+lemma minf_lt: "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
+lemma minf_gt: "\<exists>z . \<forall>x. x < z \<longrightarrow> (t < x \<longleftrightarrow> False)"
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
-lemma minf_le: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x \<^loc>\<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
-lemma minf_ge: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (t \<^loc>\<le> x \<longleftrightarrow> False)"
+lemma minf_le: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma minf_ge: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
by (auto simp add: less_le not_less not_le)
-lemma minf_eq: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
-lemma minf_neq: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
-lemma minf_P: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
+lemma minf_eq: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
+lemma minf_neq: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
+lemma minf_P: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
-text{* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
-lemma pinf_gt: "\<exists>z . \<forall>x. z \<^loc>< x \<longrightarrow> (t \<^loc>< x \<longleftrightarrow> True)" by auto
-lemma pinf_lt: "\<exists>z . \<forall>x. z \<^loc>< x \<longrightarrow> (x \<^loc>< t \<longleftrightarrow> False)"
+text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
+lemma pinf_gt: "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
+lemma pinf_lt: "\<exists>z . \<forall>x. z < x \<longrightarrow> (x < t \<longleftrightarrow> False)"
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
-lemma pinf_ge: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (t \<^loc>\<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
-lemma pinf_le: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x \<^loc>\<le> t \<longleftrightarrow> False)"
+lemma pinf_ge: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma pinf_le: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
by (auto simp add: less_le not_less not_le)
-lemma pinf_eq: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
-lemma pinf_neq: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
-lemma pinf_P: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
+lemma pinf_eq: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
+lemma pinf_neq: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
+lemma pinf_P: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
-lemma nmi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<^loc>< t \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
-lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t \<^loc>< x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)"
+lemma nmi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x < t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)"
by (auto simp add: le_less)
-lemma nmi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<^loc>\<le> t \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
-lemma nmi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<^loc>\<le> x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
-lemma nmi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
-lemma nmi_neq: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
-lemma nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
-lemma nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x) ;
- \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)\<rbrakk> \<Longrightarrow>
- \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
-lemma nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x) ;
- \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)\<rbrakk> \<Longrightarrow>
- \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
+lemma nmi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<le> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<le> x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_neq: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ;
+ \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
+ \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ;
+ \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
+ \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
-lemma npi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<^loc>< t \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by (auto simp add: le_less)
-lemma npi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<^loc>< x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
-lemma npi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<^loc>\<le> t \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
-lemma npi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<^loc>\<le> x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
-lemma npi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
-lemma npi_neq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u )" by auto
-lemma npi_P: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
-lemma npi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)\<rbrakk>
- \<Longrightarrow> \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
-lemma npi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)\<rbrakk>
- \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
+lemma npi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x < t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by (auto simp add: le_less)
+lemma npi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t < x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<le> t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<le> x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_neq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. x \<le> u )" by auto
+lemma npi_P: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
+ \<Longrightarrow> \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
+ \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
-lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x \<^loc>< t \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y \<^loc>< t)"
+lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x < t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y < t)"
proof(clarsimp)
- fix x l u y assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x"
- and xu: "x\<^loc><u" and px: "x \<^loc>< t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
+ fix x l u y assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x"
+ and xu: "x<u" and px: "x < t" and ly: "l<y" and yu:"y < u"
from tU noU ly yu have tny: "t\<noteq>y" by auto
- {assume H: "t \<^loc>< y"
+ {assume H: "t < y"
from less_trans[OF lx px] less_trans[OF H yu]
- have "l \<^loc>< t \<and> t \<^loc>< u" by simp
+ have "l < t \<and> t < u" by simp
with tU noU have "False" by auto}
- hence "\<not> t \<^loc>< y" by auto hence "y \<^loc>\<le> t" by (simp add: not_less)
- thus "y \<^loc>< t" using tny by (simp add: less_le)
+ hence "\<not> t < y" by auto hence "y \<le> t" by (simp add: not_less)
+ thus "y < t" using tny by (simp add: less_le)
qed
-lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l \<^loc>< x \<and> x \<^loc>< u \<and> t \<^loc>< x \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> t \<^loc>< y)"
+lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t < x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t < y)"
proof(clarsimp)
fix x l u y
- assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x" and xu: "x\<^loc><u"
- and px: "t \<^loc>< x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
+ assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
+ and px: "t < x" and ly: "l<y" and yu:"y < u"
from tU noU ly yu have tny: "t\<noteq>y" by auto
- {assume H: "y\<^loc>< t"
- from less_trans[OF ly H] less_trans[OF px xu] have "l \<^loc>< t \<and> t \<^loc>< u" by simp
+ {assume H: "y< t"
+ from less_trans[OF ly H] less_trans[OF px xu] have "l < t \<and> t < u" by simp
with tU noU have "False" by auto}
- hence "\<not> y\<^loc><t" by auto hence "t \<^loc>\<le> y" by (auto simp add: not_less)
- thus "t \<^loc>< y" using tny by (simp add:less_le)
+ hence "\<not> y<t" by auto hence "t \<le> y" by (auto simp add: not_less)
+ thus "t < y" using tny by (simp add:less_le)
qed
-lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x \<^loc>\<le> t \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y\<^loc>\<le> t)"
+lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<le> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<le> t)"
proof(clarsimp)
fix x l u y
- assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x" and xu: "x\<^loc><u"
- and px: "x \<^loc>\<le> t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
+ assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
+ and px: "x \<le> t" and ly: "l<y" and yu:"y < u"
from tU noU ly yu have tny: "t\<noteq>y" by auto
- {assume H: "t \<^loc>< y"
+ {assume H: "t < y"
from less_le_trans[OF lx px] less_trans[OF H yu]
- have "l \<^loc>< t \<and> t \<^loc>< u" by simp
+ have "l < t \<and> t < u" by simp
with tU noU have "False" by auto}
- hence "\<not> t \<^loc>< y" by auto thus "y \<^loc>\<le> t" by (simp add: not_less)
+ hence "\<not> t < y" by auto thus "y \<le> t" by (simp add: not_less)
qed
-lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> t \<^loc>\<le> x \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> t \<^loc>\<le> y)"
+lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> t \<le> x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t \<le> y)"
proof(clarsimp)
fix x l u y
- assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x" and xu: "x\<^loc><u"
- and px: "t \<^loc>\<le> x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
+ assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
+ and px: "t \<le> x" and ly: "l<y" and yu:"y < u"
from tU noU ly yu have tny: "t\<noteq>y" by auto
- {assume H: "y\<^loc>< t"
+ {assume H: "y< t"
from less_trans[OF ly H] le_less_trans[OF px xu]
- have "l \<^loc>< t \<and> t \<^loc>< u" by simp
+ have "l < t \<and> t < u" by simp
with tU noU have "False" by auto}
- hence "\<not> y\<^loc><t" by auto thus "t \<^loc>\<le> y" by (simp add: not_less)
+ hence "\<not> y<t" by auto thus "t \<le> y" by (simp add: not_less)
qed
-lemma lin_dense_eq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x = t \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y= t)" by auto
-lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x \<noteq> t \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y\<noteq> t)" by auto
-lemma lin_dense_P: "\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P)" by auto
+lemma lin_dense_eq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x = t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y= t)" by auto
+lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<noteq> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<noteq> t)" by auto
+lemma lin_dense_P: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P)" by auto
lemma lin_dense_conj:
- "\<lbrakk>\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P1 x
- \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P1 y) ;
- \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P2 x
- \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
- \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> (P1 x \<and> P2 x)
- \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> (P1 y \<and> P2 y))"
+ "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
+ \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
+ \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
+ \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
+ \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<and> P2 x)
+ \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
by blast
lemma lin_dense_disj:
- "\<lbrakk>\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P1 x
- \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P1 y) ;
- \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P2 x
- \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
- \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> (P1 x \<or> P2 x)
- \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> (P1 y \<or> P2 y))"
+ "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
+ \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
+ \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
+ \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
+ \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<or> P2 x)
+ \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
by blast
-lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)\<rbrakk>
- \<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u')"
+lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
+ \<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')"
by auto
lemma finite_set_intervals:
- assumes px: "P x" and lx: "l \<^loc>\<le> x" and xu: "x \<^loc>\<le> u" and linS: "l\<in> S"
- and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<^loc>\<le> x" and Su: "\<forall> x\<in> S. x \<^loc>\<le> u"
- shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<^loc>< y \<and> y \<^loc>< b \<longrightarrow> y \<notin> S) \<and> a \<^loc>\<le> x \<and> x \<^loc>\<le> b \<and> P x"
+ assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
+ and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
+ shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x"
proof-
- let ?Mx = "{y. y\<in> S \<and> y \<^loc>\<le> x}"
- let ?xM = "{y. y\<in> S \<and> x \<^loc>\<le> y}"
+ let ?Mx = "{y. y\<in> S \<and> y \<le> x}"
+ let ?xM = "{y. y\<in> S \<and> x \<le> y}"
let ?a = "Max ?Mx"
let ?b = "Min ?xM"
have MxS: "?Mx \<subseteq> S" by blast
@@ -179,31 +179,31 @@
hence fxM: "finite ?xM" using fS finite_subset by auto
from xu uinS have linxM: "u \<in> ?xM" by blast
hence xMne: "?xM \<noteq> {}" by blast
- have ax:"?a \<^loc>\<le> x" using Mxne fMx by auto
- have xb:"x \<^loc>\<le> ?b" using xMne fxM by auto
+ have ax:"?a \<le> x" using Mxne fMx by auto
+ have xb:"x \<le> ?b" using xMne fxM by auto
have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
- have noy:"\<forall> y. ?a \<^loc>< y \<and> y \<^loc>< ?b \<longrightarrow> y \<notin> S"
+ have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
proof(clarsimp)
- fix y assume ay: "?a \<^loc>< y" and yb: "y \<^loc>< ?b" and yS: "y \<in> S"
+ fix y assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear)
- moreover {assume "y \<in> ?Mx" hence "y \<^loc>\<le> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])}
- moreover {assume "y \<in> ?xM" hence "?b \<^loc>\<le> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])}
+ moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])}
+ moreover {assume "y \<in> ?xM" hence "?b \<le> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])}
ultimately show "False" by blast
qed
from ainS binS noy ax xb px show ?thesis by blast
qed
lemma finite_set_intervals2:
- assumes px: "P x" and lx: "l \<^loc>\<le> x" and xu: "x \<^loc>\<le> u" and linS: "l\<in> S"
- and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<^loc>\<le> x" and Su: "\<forall> x\<in> S. x \<^loc>\<le> u"
- shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<^loc>< y \<and> y \<^loc>< b \<longrightarrow> y \<notin> S) \<and> a \<^loc>< x \<and> x \<^loc>< b \<and> P x)"
+ assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
+ and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
+ shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)"
proof-
from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
obtain a and b where
- as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a \<^loc>< y \<and> y \<^loc>< b \<longrightarrow> y \<notin> S"
- and axb: "a \<^loc>\<le> x \<and> x \<^loc>\<le> b \<and> P x" by auto
- from axb have "x= a \<or> x= b \<or> (a \<^loc>< x \<and> x \<^loc>< b)" by (auto simp add: le_less)
+ as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S"
+ and axb: "a \<le> x \<and> x \<le> b \<and> P x" by auto
+ from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by (auto simp add: le_less)
thus ?thesis using px as bs noS by blast
qed
@@ -216,45 +216,45 @@
lemma dlo_qe_bnds:
assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
- shows "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l \<^loc>< u)"
+ shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l < u)"
proof (simp only: atomize_eq, rule iffI)
- assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)"
- then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast
+ assume H: "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)"
+ then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y" by blast
{fix l u assume l: "l \<in> L" and u: "u \<in> U"
from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]]
- have "l \<^loc>< u" .}
- thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
+ have "l < u" .}
+ thus "\<forall>l\<in>L. \<forall>u\<in>U. l < u" by blast
next
- assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
+ assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l < u"
let ?ML = "Max L"
let ?MU = "Min U"
- from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<^loc>\<le> ?ML" by auto
- from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<^loc>\<le> u" by auto
- from th1 th2 H have "?ML \<^loc>< ?MU" by auto
- with dense obtain w where th3: "?ML \<^loc>< w" and th4: "w \<^loc>< ?MU" by blast
- from th3 th1' have "\<forall>l \<in> L. l \<^loc>< w" by auto
- moreover from th4 th2' have "\<forall>u \<in> U. w \<^loc>< u" by auto
- ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
+ from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<le> ?ML" by auto
+ from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<le> u" by auto
+ from th1 th2 H have "?ML < ?MU" by auto
+ with dense obtain w where th3: "?ML < w" and th4: "w < ?MU" by blast
+ from th3 th1' have "\<forall>l \<in> L. l < w" by auto
+ moreover from th4 th2' have "\<forall>u \<in> U. w < u" by auto
+ ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto
qed
lemma dlo_qe_noub:
assumes ne: "L \<noteq> {}" and fL: "finite L"
- shows "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> {}. x \<^loc>< y)) \<equiv> True"
+ shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True"
proof(simp add: atomize_eq)
- from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<^loc>< M" by blast
- from ne fL have "\<forall>x \<in> L. x \<^loc>\<le> Max L" by simp
- with M have "\<forall>x\<in>L. x \<^loc>< M" by (auto intro: le_less_trans)
- thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast
+ from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L < M" by blast
+ from ne fL have "\<forall>x \<in> L. x \<le> Max L" by simp
+ with M have "\<forall>x\<in>L. x < M" by (auto intro: le_less_trans)
+ thus "\<exists>x. \<forall>y\<in>L. y < x" by blast
qed
lemma dlo_qe_nolb:
assumes ne: "U \<noteq> {}" and fU: "finite U"
- shows "(\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y)) \<equiv> True"
+ shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True"
proof(simp add: atomize_eq)
- from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<^loc>< Min U" by blast
- from ne fU have "\<forall>x \<in> U. Min U \<^loc>\<le> x" by simp
- with M have "\<forall>x\<in>U. M \<^loc>< x" by (auto intro: less_le_trans)
- thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast
+ from lt_ex[rule_format, of "Min U"] obtain M where M: "M < Min U" by blast
+ from ne fU have "\<forall>x \<in> U. Min U \<le> x" by simp
+ with M have "\<forall>x\<in>U. M < x" by (auto intro: less_le_trans)
+ thus "\<exists>x. \<forall>y\<in>U. x < y" by blast
qed
lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x"
@@ -263,7 +263,7 @@
lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq
le_less neq_iff linear less_not_permute
-lemma axiom: "dense_linear_order (op \<^loc>\<le>) (op \<^loc><)" .
+lemma axiom: "dense_linear_order (op \<le>) (op <)" .
lemma atoms:
includes meta_term_syntax
shows "TERM (less :: 'a \<Rightarrow> _)"
@@ -303,22 +303,22 @@
text {* Linear order without upper bounds *}
class linorder_no_ub = linorder +
- assumes gt_ex: "\<exists>y. x \<^loc>< y"
+ assumes gt_ex: "\<exists>y. x < y"
begin
-lemma ge_ex: "\<exists>y. x \<^loc>\<le> y" using gt_ex by auto
+lemma ge_ex: "\<exists>y. x \<le> y" using gt_ex by auto
-text {* Theorems for @{text "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
+text {* Theorems for @{text "\<exists>z. \<forall>x. z < x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
lemma pinf_conj:
- assumes ex1: "\<exists>z1. \<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and ex2: "\<exists>z2. \<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
- shows "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
+ assumes ex1: "\<exists>z1. \<forall>x. z1 < x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+ and ex2: "\<exists>z2. \<forall>x. z2 < x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+ shows "\<exists>z. \<forall>x. z < x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
proof-
- from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and z2: "\<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
- from gt_ex obtain z where z:"max z1 z2 \<^loc>< z" by blast
- from z have zz1: "z1 \<^loc>< z" and zz2: "z2 \<^loc>< z" by simp_all
- {fix x assume H: "z \<^loc>< x"
+ from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 < x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+ and z2: "\<forall>x. z2 < x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+ from gt_ex obtain z where z:"max z1 z2 < z" by blast
+ from z have zz1: "z1 < z" and zz2: "z2 < z" by simp_all
+ {fix x assume H: "z < x"
from less_trans[OF zz1 H] less_trans[OF zz2 H]
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto
}
@@ -326,25 +326,25 @@
qed
lemma pinf_disj:
- assumes ex1: "\<exists>z1. \<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and ex2: "\<exists>z2. \<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
- shows "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
+ assumes ex1: "\<exists>z1. \<forall>x. z1 < x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+ and ex2: "\<exists>z2. \<forall>x. z2 < x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+ shows "\<exists>z. \<forall>x. z < x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
proof-
- from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and z2: "\<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
- from gt_ex obtain z where z:"max z1 z2 \<^loc>< z" by blast
- from z have zz1: "z1 \<^loc>< z" and zz2: "z2 \<^loc>< z" by simp_all
- {fix x assume H: "z \<^loc>< x"
+ from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 < x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+ and z2: "\<forall>x. z2 < x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+ from gt_ex obtain z where z:"max z1 z2 < z" by blast
+ from z have zz1: "z1 < z" and zz2: "z2 < z" by simp_all
+ {fix x assume H: "z < x"
from less_trans[OF zz1 H] less_trans[OF zz2 H]
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto
}
thus ?thesis by blast
qed
-lemma pinf_ex: assumes ex:"\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
+lemma pinf_ex: assumes ex:"\<exists>z. \<forall>x. z < x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
proof-
- from ex obtain z where z: "\<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
- from gt_ex obtain x where x: "z \<^loc>< x" by blast
+ from ex obtain z where z: "\<forall>x. z < x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
+ from gt_ex obtain x where x: "z < x" by blast
from z x p1 show ?thesis by blast
qed
@@ -353,22 +353,22 @@
text {* Linear order without upper bounds *}
class linorder_no_lb = linorder +
- assumes lt_ex: "\<exists>y. y \<^loc>< x"
+ assumes lt_ex: "\<exists>y. y < x"
begin
-lemma le_ex: "\<exists>y. y \<^loc>\<le> x" using lt_ex by auto
+lemma le_ex: "\<exists>y. y \<le> x" using lt_ex by auto
-text {* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
+text {* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
lemma minf_conj:
- assumes ex1: "\<exists>z1. \<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and ex2: "\<exists>z2. \<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
- shows "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
+ assumes ex1: "\<exists>z1. \<forall>x. x < z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+ and ex2: "\<exists>z2. \<forall>x. x < z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+ shows "\<exists>z. \<forall>x. x < z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
proof-
- from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
- from lt_ex obtain z where z:"z \<^loc>< min z1 z2" by blast
- from z have zz1: "z \<^loc>< z1" and zz2: "z \<^loc>< z2" by simp_all
- {fix x assume H: "x \<^loc>< z"
+ from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x < z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x < z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+ from lt_ex obtain z where z:"z < min z1 z2" by blast
+ from z have zz1: "z < z1" and zz2: "z < z2" by simp_all
+ {fix x assume H: "x < z"
from less_trans[OF H zz1] less_trans[OF H zz2]
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto
}
@@ -376,24 +376,24 @@
qed
lemma minf_disj:
- assumes ex1: "\<exists>z1. \<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and ex2: "\<exists>z2. \<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
- shows "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
+ assumes ex1: "\<exists>z1. \<forall>x. x < z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+ and ex2: "\<exists>z2. \<forall>x. x < z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+ shows "\<exists>z. \<forall>x. x < z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
proof-
- from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
- from lt_ex obtain z where z:"z \<^loc>< min z1 z2" by blast
- from z have zz1: "z \<^loc>< z1" and zz2: "z \<^loc>< z2" by simp_all
- {fix x assume H: "x \<^loc>< z"
+ from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x < z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x < z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+ from lt_ex obtain z where z:"z < min z1 z2" by blast
+ from z have zz1: "z < z1" and zz2: "z < z2" by simp_all
+ {fix x assume H: "x < z"
from less_trans[OF H zz1] less_trans[OF H zz2]
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto
}
thus ?thesis by blast
qed
-lemma minf_ex: assumes ex:"\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
+lemma minf_ex: assumes ex:"\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
proof-
- from ex obtain z where z: "\<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
- from lt_ex obtain x where x: "x \<^loc>< z" by blast
+ from ex obtain z where z: "\<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
+ from lt_ex obtain x where x: "x < z" by blast
from z x p1 show ?thesis by blast
qed
@@ -402,7 +402,7 @@
class constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
fixes between
- assumes between_less: "x \<^loc>< y \<Longrightarrow> x \<^loc>< between x y \<and> between x y \<^loc>< y"
+ assumes between_less: "x < y \<Longrightarrow> x < between x y \<and> between x y < y"
and between_same: "between x x = x"
begin
@@ -413,41 +413,41 @@
lemma rinf_U:
assumes fU: "finite U"
- and lin_dense: "\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P x
- \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P y )"
- and nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u')"
+ and lin_dense: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P x
+ \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P y )"
+ and nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')"
and nmi: "\<not> MP" and npi: "\<not> PP" and ex: "\<exists> x. P x"
shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')"
proof-
from ex obtain x where px: "P x" by blast
- from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u'" by auto
- then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<^loc>\<le> x" and xu':"x \<^loc>\<le> u'" by auto
+ from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u'" by auto
+ then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<le> x" and xu':"x \<le> u'" by auto
from uU have Une: "U \<noteq> {}" by auto
let ?l = "Min U"
let ?u = "Max U"
have linM: "?l \<in> U" using fU Une by simp
have uinM: "?u \<in> U" using fU Une by simp
- have lM: "\<forall> t\<in> U. ?l \<^loc>\<le> t" using Une fU by auto
- have Mu: "\<forall> t\<in> U. t \<^loc>\<le> ?u" using Une fU by auto
- have th:"?l \<^loc>\<le> u" using uU Une lM by auto
- from order_trans[OF th ux] have lx: "?l \<^loc>\<le> x" .
- have th: "u' \<^loc>\<le> ?u" using uU' Une Mu by simp
- from order_trans[OF xu' th] have xu: "x \<^loc>\<le> ?u" .
+ have lM: "\<forall> t\<in> U. ?l \<le> t" using Une fU by auto
+ have Mu: "\<forall> t\<in> U. t \<le> ?u" using Une fU by auto
+ have th:"?l \<le> u" using uU Une lM by auto
+ from order_trans[OF th ux] have lx: "?l \<le> x" .
+ have th: "u' \<le> ?u" using uU' Une Mu by simp
+ from order_trans[OF xu' th] have xu: "x \<le> ?u" .
from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu]
have "(\<exists> s\<in> U. P s) \<or>
- (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U) \<and> t1 \<^loc>< x \<and> x \<^loc>< t2 \<and> P x)" .
+ (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U) \<and> t1 < x \<and> x < t2 \<and> P x)" .
moreover { fix u assume um: "u\<in>U" and pu: "P u"
have "between u u = u" by (simp add: between_same)
with um pu have "P (between u u)" by simp
with um have ?thesis by blast}
moreover{
- assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U) \<and> t1 \<^loc>< x \<and> x \<^loc>< t2 \<and> P x"
+ assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U) \<and> t1 < x \<and> x < t2 \<and> P x"
then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U"
- and noM: "\<forall> y. t1 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U" and t1x: "t1 \<^loc>< x" and xt2: "x \<^loc>< t2" and px: "P x"
+ and noM: "\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U" and t1x: "t1 < x" and xt2: "x < t2" and px: "P x"
by blast
- from less_trans[OF t1x xt2] have t1t2: "t1 \<^loc>< t2" .
+ from less_trans[OF t1x xt2] have t1t2: "t1 < t2" .
let ?u = "between t1 t2"
- from between_less t1t2 have t1lu: "t1 \<^loc>< ?u" and ut2: "?u \<^loc>< t2" by auto
+ from between_less t1t2 have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto
from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast
with t1M t2M have ?thesis by blast}
ultimately show ?thesis by blast
@@ -455,11 +455,11 @@
theorem fr_eq:
assumes fU: "finite U"
- and lin_dense: "\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P x
- \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P y )"
- and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)"
- and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)"
- and mi: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x = MP)" and pi: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x = PP)"
+ and lin_dense: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P x
+ \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P y )"
+ and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)"
+ and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)"
+ and mi: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x = MP)" and pi: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P x = PP)"
shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))"
(is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D")
proof-
@@ -469,7 +469,7 @@
moreover {assume "MP \<or> PP" hence "?D" by blast}
moreover {assume nmi: "\<not> MP" and npi: "\<not> PP"
from npmibnd[OF nmibnd npibnd]
- have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u')" .
+ have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')" .
from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast}
ultimately have "?D" by blast}
moreover
@@ -504,7 +504,7 @@
fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
fun generic_whatis phi =
let
- val [lt, le] = map (Morphism.term phi) [@{term "op \<^loc><"}, @{term "op \<^loc>\<le>"}]
+ val [lt, le] = map (Morphism.term phi) [@{term "op <"}, @{term "op \<le>"}]
fun h x t =
case term_of t of
Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
--- a/src/HOL/Divides.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Divides.thy Tue Oct 16 23:12:45 2007 +0200
@@ -12,8 +12,8 @@
begin
class div = times +
- fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>div" 70)
- fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>mod" 70)
+ fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
+ fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
instance nat :: Divides.div
div_def: "m div n == wfrec (pred_nat^+)
@@ -22,12 +22,12 @@
(%f j. if j<n | n=0 then j else f (j-n)) m" ..
definition (in div)
- dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>dvd" 50)
+ dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
where
- [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
+ [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
class dvd_mod = div + zero + -- {* for code generation *}
- assumes dvd_def_mod [code func]: "x \<^loc>dvd y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
+ assumes dvd_def_mod [code func]: "x dvd y \<longleftrightarrow> y mod x = 0"
definition
quorem :: "(nat*nat) * (nat*nat) => bool" where
--- a/src/HOL/Finite_Set.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Finite_Set.thy Tue Oct 16 23:12:45 2007 +0200
@@ -2026,6 +2026,20 @@
and strict_below_def: "less x y \<longleftrightarrow> less_eq x y \<and> x \<noteq> y"
begin
+notation
+ less_eq ("op \<^loc><=") and
+ less_eq ("(_/ \<^loc><= _)" [51, 51] 50) and
+ less ("op \<^loc><") and
+ less ("(_/ \<^loc>< _)" [51, 51] 50)
+
+notation (xsymbols)
+ less_eq ("op \<^loc>\<le>") and
+ less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50)
+
+notation (HTML output)
+ less_eq ("op \<^loc>\<le>") and
+ less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50)
+
lemma below_refl [simp]: "x \<^loc>\<le> x"
by (simp add: below_def idem)
@@ -2242,27 +2256,27 @@
over (non-empty) sets by means of @{text fold1}.
*}
-lemma (in lower_semilattice) ACf_inf: "ACf (op \<sqinter>)"
+lemma (in lower_semilattice) ACf_inf: "ACf inf"
by (blast intro: ACf.intro inf_commute inf_assoc)
-lemma (in upper_semilattice) ACf_sup: "ACf (op \<squnion>)"
+lemma (in upper_semilattice) ACf_sup: "ACf sup"
by (blast intro: ACf.intro sup_commute sup_assoc)
-lemma (in lower_semilattice) ACIf_inf: "ACIf (op \<sqinter>)"
+lemma (in lower_semilattice) ACIf_inf: "ACIf inf"
apply(rule ACIf.intro)
apply(rule ACf_inf)
apply(rule ACIf_axioms.intro)
apply(rule inf_idem)
done
-lemma (in upper_semilattice) ACIf_sup: "ACIf (op \<squnion>)"
+lemma (in upper_semilattice) ACIf_sup: "ACIf sup"
apply(rule ACIf.intro)
apply(rule ACf_sup)
apply(rule ACIf_axioms.intro)
apply(rule sup_idem)
done
-lemma (in lower_semilattice) ACIfSL_inf: "ACIfSL (op \<^loc>\<le>) (op \<^loc><) (op \<sqinter>)"
+lemma (in lower_semilattice) ACIfSL_inf: "ACIfSL (op \<le>) (op <) inf"
apply(rule ACIfSL.intro)
apply(rule ACIf.intro)
apply(rule ACf_inf)
@@ -2275,7 +2289,7 @@
apply(rule less_le)
done
-lemma (in upper_semilattice) ACIfSL_sup: "ACIfSL (%x y. y \<^loc>\<le> x) (%x y. y \<^loc>< x) (op \<squnion>)"
+lemma (in upper_semilattice) ACIfSL_sup: "ACIfSL (%x y. y \<le> x) (%x y. y < x) sup"
apply(rule ACIfSL.intro)
apply(rule ACIf.intro)
apply(rule ACf_sup)
@@ -2294,14 +2308,14 @@
definition
Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
where
- "Inf_fin = fold1 (op \<sqinter>)"
+ "Inf_fin = fold1 inf"
definition
Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
where
- "Sup_fin = fold1 (op \<squnion>)"
-
-lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<^loc>\<le> \<Squnion>\<^bsub>fin\<^esub>A"
+ "Sup_fin = fold1 sup"
+
+lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
apply(unfold Sup_fin_def Inf_fin_def)
apply(subgoal_tac "EX a. a:A")
prefer 2 apply blast
@@ -2312,13 +2326,13 @@
done
lemma sup_Inf_absorb [simp]:
- "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>\<^bsub>fin\<^esub>A) = a"
+ "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (sup a (\<Sqinter>\<^bsub>fin\<^esub>A)) = a"
apply(subst sup_commute)
apply(simp add: Inf_fin_def sup_absorb2 ACIfSL.fold1_belowI [OF ACIfSL_inf])
done
lemma inf_Sup_absorb [simp]:
- "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>\<^bsub>fin\<^esub>A) = a"
+ "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (inf a (\<Squnion>\<^bsub>fin\<^esub>A)) = a"
by(simp add: Sup_fin_def inf_absorb1 ACIfSL.fold1_belowI [OF ACIfSL_sup])
end
@@ -2327,7 +2341,7 @@
begin
lemma sup_Inf1_distrib:
- "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<squnion> \<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{x \<squnion> a|a. a \<in> A}"
+ "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
apply(simp add: Inf_fin_def image_def
ACIf.hom_fold1_commute[OF ACIf_inf, where h="sup x", OF sup_inf_distrib1])
apply(rule arg_cong, blast)
@@ -2335,38 +2349,38 @@
lemma sup_Inf2_distrib:
assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
- shows "(\<Sqinter>\<^bsub>fin\<^esub>A \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
+ shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
using A proof (induct rule: finite_ne_induct)
case singleton thus ?case
by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
next
case (insert x A)
- have finB: "finite {x \<squnion> b |b. b \<in> B}"
- by(rule finite_surj[where f = "%b. x \<squnion> b", OF B(1)], auto)
- have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
+ have finB: "finite {sup x b |b. b \<in> B}"
+ by(rule finite_surj[where f = "sup x", OF B(1)], auto)
+ have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
proof -
- have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
+ have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
by blast
thus ?thesis by(simp add: insert(1) B(1))
qed
- have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
- have "\<Sqinter>\<^bsub>fin\<^esub>(insert x A) \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B = (x \<sqinter> \<Sqinter>\<^bsub>fin\<^esub>A) \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B"
+ have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
+ have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
using insert
by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_fin_def])
- also have "\<dots> = (x \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B) \<sqinter> (\<Sqinter>\<^bsub>fin\<^esub>A \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B)" by(rule sup_inf_distrib2)
- also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>{x \<squnion> b|b. b \<in> B} \<sqinter> \<Sqinter>\<^bsub>fin\<^esub>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
+ also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
+ also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
using insert by(simp add:sup_Inf1_distrib[OF B])
- also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
+ also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
(is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
using B insert
by (simp add: Inf_fin_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
- also have "?M = {a \<squnion> b |a b. a \<in> insert x A \<and> b \<in> B}"
+ also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
by blast
finally show ?case .
qed
lemma inf_Sup1_distrib:
- "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<sqinter> \<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{x \<sqinter> a|a. a \<in> A}"
+ "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
apply (simp add: Sup_fin_def image_def
ACIf.hom_fold1_commute[OF ACIf_sup, where h="inf x", OF inf_sup_distrib1])
apply (rule arg_cong, blast)
@@ -2374,31 +2388,31 @@
lemma inf_Sup2_distrib:
assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
- shows "(\<Squnion>\<^bsub>fin\<^esub>A \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
+ shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}"
using A proof (induct rule: finite_ne_induct)
case singleton thus ?case
by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
next
case (insert x A)
- have finB: "finite {x \<sqinter> b |b. b \<in> B}"
- by(rule finite_surj[where f = "%b. x \<sqinter> b", OF B(1)], auto)
- have finAB: "finite {a \<sqinter> b |a b. a \<in> A \<and> b \<in> B}"
+ have finB: "finite {inf x b |b. b \<in> B}"
+ by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
+ have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
proof -
- have "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<sqinter> b})"
+ have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
by blast
thus ?thesis by(simp add: insert(1) B(1))
qed
- have ne: "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
- have "\<Squnion>\<^bsub>fin\<^esub>(insert x A) \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B = (x \<squnion> \<Squnion>\<^bsub>fin\<^esub>A) \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B"
+ have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
+ have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
using insert by (simp add: ACIf.fold1_insert_idem_def [OF ACIf_sup Sup_fin_def])
- also have "\<dots> = (x \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B) \<squnion> (\<Squnion>\<^bsub>fin\<^esub>A \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B)" by(rule inf_sup_distrib2)
- also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>{x \<sqinter> b|b. b \<in> B} \<squnion> \<Squnion>\<^bsub>fin\<^esub>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
+ also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
+ also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
using insert by(simp add:inf_Sup1_distrib[OF B])
- also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({x\<sqinter>b |b. b \<in> B} \<union> {a\<sqinter>b |a b. a \<in> A \<and> b \<in> B})"
+ also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
(is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
using B insert
by (simp add: Sup_fin_def ACIf.fold1_Un2[OF ACIf_sup finB _ finAB ne])
- also have "?M = {a \<sqinter> b |a b. a \<in> insert x A \<and> b \<in> B}"
+ also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
by blast
finally show ?case .
qed
@@ -2413,12 +2427,12 @@
*}
lemma Inf_fin_Inf:
- "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A = \<Sqinter>A"
+ "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
unfolding Inf_fin_def by (induct A set: finite)
(simp_all add: Inf_insert_simp ACIf.fold1_insert_idem [OF ACIf_inf])
lemma Sup_fin_Sup:
- "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>\<^bsub>fin\<^esub>A = \<Squnion>A"
+ "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>\<^bsub>fin\<^esub>A = Sup A"
unfolding Sup_fin_def by (induct A set: finite)
(simp_all add: Sup_insert_simp ACIf.fold1_insert_idem [OF ACIf_sup])
@@ -2462,13 +2476,13 @@
rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
-lemma ACIfSL_min: "ACIfSL (op \<^loc>\<le>) (op \<^loc><) min"
+lemma ACIfSL_min: "ACIfSL (op \<le>) (op <) min"
by (rule lower_semilattice.ACIfSL_inf,
rule lattice.axioms,
rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
-lemma ACIfSLlin_min: "ACIfSLlin (op \<^loc>\<le>) (op \<^loc><) min"
+lemma ACIfSLlin_min: "ACIfSLlin (op \<le>) (op <) min"
by (rule ACIfSLlin.intro,
rule lower_semilattice.ACIfSL_inf,
rule lattice.axioms,
@@ -2488,13 +2502,13 @@
rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
-lemma ACIfSL_max: "ACIfSL (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x) max"
+lemma ACIfSL_max: "ACIfSL (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) max"
by (rule upper_semilattice.ACIfSL_sup,
rule lattice.axioms,
rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
-lemma ACIfSLlin_max: "ACIfSLlin (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x) max"
+lemma ACIfSLlin_max: "ACIfSLlin (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) max"
by (rule ACIfSLlin.intro,
rule upper_semilattice.ACIfSL_sup,
rule lattice.axioms,
@@ -2517,48 +2531,48 @@
using ACf.fold1_in [OF ACf_max]
by (fastsimp simp: Max_def max_def)
-lemma Min_antimono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Min N \<^loc>\<le> Min M"
+lemma Min_antimono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Min N \<le> Min M"
by (simp add: Min_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_min])
-lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<^loc>\<le> Max N"
+lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<le> Max N"
by (simp add: Max_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_max])
-lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x"
+lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
by (simp add: Min_def ACIfSL.fold1_belowI [OF ACIfSL_min])
-lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A"
+lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
by (simp add: Max_def ACIfSL.fold1_belowI [OF ACIfSL_max])
lemma Min_ge_iff [simp,noatp]:
- "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<^loc>\<le> a)"
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
by (simp add: Min_def ACIfSL.below_fold1_iff [OF ACIfSL_min])
lemma Max_le_iff [simp,noatp]:
- "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<^loc>\<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<^loc>\<le> x)"
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
by (simp add: Max_def ACIfSL.below_fold1_iff [OF ACIfSL_max])
lemma Min_gr_iff [simp,noatp]:
- "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>< Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<^loc>< a)"
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
by (simp add: Min_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_min])
lemma Max_less_iff [simp,noatp]:
- "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<^loc>< x \<longleftrightarrow> (\<forall>a\<in>A. a \<^loc>< x)"
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
by (simp add: Max_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_max])
lemma Min_le_iff [noatp]:
- "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<^loc>\<le> x)"
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
by (simp add: Min_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_min])
lemma Max_ge_iff [noatp]:
- "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<^loc>\<le> a)"
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
by (simp add: Max_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_max])
lemma Min_less_iff [noatp]:
- "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<^loc>< x \<longleftrightarrow> (\<exists>a\<in>A. a \<^loc>< x)"
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
by (simp add: Min_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_min])
lemma Max_gr_iff [noatp]:
- "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>< Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<^loc>< a)"
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
by (simp add: Max_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_max])
lemma Min_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
@@ -2586,23 +2600,29 @@
lemma add_Min_commute:
fixes k
- shows "finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> k \<^loc>+ Min N = Min {k \<^loc>+ m | m. m \<in> N}"
- apply (subgoal_tac "\<And>x y. k \<^loc>+ min x y = min (k \<^loc>+ x) (k \<^loc>+ y)")
- using hom_Min_commute [of "(op \<^loc>+) k" N]
- apply simp apply (rule arg_cong [where f = Min]) apply blast
- apply (simp add: min_def not_le)
- apply (blast intro: antisym less_imp_le add_left_mono)
- done
+ assumes "finite N" and "N \<noteq> {}"
+ shows "k + Min N = Min {k + m | m. m \<in> N}"
+proof -
+ have "\<And>x y. k + min x y = min (k + x) (k + y)"
+ by (simp add: min_def not_le)
+ (blast intro: antisym less_imp_le add_left_mono)
+ with assms show ?thesis
+ using hom_Min_commute [of "plus k" N]
+ by simp (blast intro: arg_cong [where f = Min])
+qed
lemma add_Max_commute:
fixes k
- shows "finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> k \<^loc>+ Max N = Max {k \<^loc>+ m | m. m \<in> N}"
- apply (subgoal_tac "\<And>x y. k \<^loc>+ max x y = max (k \<^loc>+ x) (k \<^loc>+ y)")
- using hom_Max_commute [of "(op \<^loc>+) k" N]
- apply simp apply (rule arg_cong [where f = Max]) apply blast
- apply (simp add: max_def not_le)
- apply (blast intro: antisym less_imp_le add_left_mono)
- done
+ assumes "finite N" and "N \<noteq> {}"
+ shows "k + Max N = Max {k + m | m. m \<in> N}"
+proof -
+ have "\<And>x y. k + max x y = max (k + x) (k + y)"
+ by (simp add: max_def not_le)
+ (blast intro: antisym less_imp_le add_left_mono)
+ with assms show ?thesis
+ using hom_Max_commute [of "plus k" N]
+ by simp (blast intro: arg_cong [where f = Max])
+qed
end
--- a/src/HOL/HOL.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/HOL.thy Tue Oct 16 23:12:45 2007 +0200
@@ -208,75 +208,55 @@
fixes default :: 'a
class zero = type +
- fixes zero :: 'a ("\<^loc>0")
+ fixes zero :: 'a ("0")
class one = type +
- fixes one :: 'a ("\<^loc>1")
+ fixes one :: 'a ("1")
hide (open) const zero one
class plus = type +
- fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>+" 65)
+ fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
class minus = type +
- fixes uminus :: "'a \<Rightarrow> 'a"
- and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>-" 65)
+ fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
+ and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
class times = type +
- fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>*" 70)
+ fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
class inverse = type +
fixes inverse :: "'a \<Rightarrow> 'a"
- and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>'/" 70)
+ and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
class abs = type +
fixes abs :: "'a \<Rightarrow> 'a"
-class sgn = type +
- fixes sgn :: "'a \<Rightarrow> 'a"
-
-notation
- uminus ("- _" [81] 80)
-
notation (xsymbols)
abs ("\<bar>_\<bar>")
notation (HTML output)
abs ("\<bar>_\<bar>")
+class sgn = type +
+ fixes sgn :: "'a \<Rightarrow> 'a"
+
class ord = type +
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
begin
-notation
- less_eq ("op \<^loc><=") and
- less_eq ("(_/ \<^loc><= _)" [51, 51] 50) and
- less ("op \<^loc><") and
- less ("(_/ \<^loc>< _)" [51, 51] 50)
-
-notation (xsymbols)
- less_eq ("op \<^loc>\<le>") and
- less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50)
-
-notation (HTML output)
- less_eq ("op \<^loc>\<le>") and
- less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50)
+abbreviation (input)
+ greater_eq (infix ">=" 50) where
+ "x >= y \<equiv> less_eq y x"
abbreviation (input)
- greater_eq (infix "\<^loc>>=" 50) where
- "x \<^loc>>= y \<equiv> y \<^loc><= x"
-
-notation (input)
- greater_eq (infix "\<^loc>\<ge>" 50)
-
-abbreviation (input)
- greater (infix "\<^loc>>" 50) where
- "x \<^loc>> y \<equiv> y \<^loc>< x"
+ greater (infix ">" 50) where
+ "x > y \<equiv> less y x"
definition
- Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "\<^loc>LEAST " 10)
+ Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10)
where
- "Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<^loc>\<le> y))"
+ "Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> less_eq x y))"
end
--- a/src/HOL/Hyperreal/HDeriv.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Hyperreal/HDeriv.thy Tue Oct 16 23:12:45 2007 +0200
@@ -369,7 +369,7 @@
subsubsection {* Equivalence of NS and Standard definitions *}
-lemma divideR_eq_divide: "x /# y = x / y"
+lemma divideR_eq_divide: "x /\<^sub>R y = x / y"
by (simp add: real_scaleR_def divide_inverse mult_commute)
text{*Now equivalence between NSDERIV and DERIV*}
--- a/src/HOL/Hyperreal/HLim.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Hyperreal/HLim.thy Tue Oct 16 23:12:45 2007 +0200
@@ -52,12 +52,12 @@
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
lemma starfun_scaleR [simp]:
- "starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
+ "starfun (\<lambda>x. f x *\<^sub>R g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
by transfer (rule refl)
lemma NSLIM_scaleR:
"[| f -- x --NS> l; g -- x --NS> m |]
- ==> (%x. f(x) *# g(x)) -- x --NS> (l *# m)"
+ ==> (%x. f(x) *\<^sub>R g(x)) -- x --NS> (l *\<^sub>R m)"
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
lemma NSLIM_add:
--- a/src/HOL/Hyperreal/NSA.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Tue Oct 16 23:12:45 2007 +0200
@@ -87,7 +87,7 @@
lemma hnorm_scaleR:
"\<And>x::'a::real_normed_vector star.
- hnorm (a *# x) = \<bar>star_of a\<bar> * hnorm x"
+ hnorm (a *\<^sub>R x) = \<bar>star_of a\<bar> * hnorm x"
by transfer (rule norm_scaleR)
lemma hnorm_scaleHR:
@@ -429,7 +429,7 @@
done
lemma Infinitesimal_scaleR2:
- "x \<in> Infinitesimal ==> a *# x \<in> Infinitesimal"
+ "x \<in> Infinitesimal ==> a *\<^sub>R x \<in> Infinitesimal"
apply (case_tac "a = 0", simp)
apply (rule InfinitesimalI)
apply (drule InfinitesimalD)
@@ -853,7 +853,7 @@
by transfer (rule scaleR_left_diff_distrib)
lemma approx_scaleR1:
- "[| a @= star_of b; c: HFinite|] ==> scaleHR a c @= b *# c"
+ "[| a @= star_of b; c: HFinite|] ==> scaleHR a c @= b *\<^sub>R c"
apply (unfold approx_def)
apply (drule (1) Infinitesimal_HFinite_scaleHR)
apply (simp only: scaleHR_left_diff_distrib)
@@ -861,12 +861,12 @@
done
lemma approx_scaleR2:
- "a @= b ==> c *# a @= c *# b"
+ "a @= b ==> c *\<^sub>R a @= c *\<^sub>R b"
by (simp add: approx_def Infinitesimal_scaleR2
scaleR_right_diff_distrib [symmetric])
lemma approx_scaleR_HFinite:
- "[|a @= star_of b; c @= d; d: HFinite|] ==> scaleHR a c @= b *# d"
+ "[|a @= star_of b; c @= d; d: HFinite|] ==> scaleHR a c @= b *\<^sub>R d"
apply (rule approx_trans)
apply (rule_tac [2] approx_scaleR2)
apply (rule approx_scaleR1)
--- a/src/HOL/Hyperreal/Transcendental.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Tue Oct 16 23:12:45 2007 +0200
@@ -437,7 +437,7 @@
definition
exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where
- "exp x = (\<Sum>n. x ^ n /# real (fact n))"
+ "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
definition
sin :: "real => real" where
@@ -451,10 +451,10 @@
lemma summable_exp_generic:
fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
- defines S_def: "S \<equiv> \<lambda>n. x ^ n /# real (fact n)"
+ defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
shows "summable S"
proof -
- have S_Suc: "\<And>n. S (Suc n) = (x * S n) /# real (Suc n)"
+ have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)"
unfolding S_def by (simp add: power_Suc del: mult_Suc)
obtain r :: real where r0: "0 < r" and r1: "r < 1"
using dense [OF zero_less_one] by fast
@@ -481,12 +481,12 @@
lemma summable_norm_exp:
fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
- shows "summable (\<lambda>n. norm (x ^ n /# real (fact n)))"
+ shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
proof (rule summable_norm_comparison_test [OF exI, rule_format])
- show "summable (\<lambda>n. norm x ^ n /# real (fact n))"
+ show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
by (rule summable_exp_generic)
next
- fix n show "norm (x ^ n /# real (fact n)) \<le> norm x ^ n /# real (fact n)"
+ fix n show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
by (simp add: norm_scaleR norm_power_ineq)
qed
@@ -536,7 +536,7 @@
apply (case_tac [2] "n", auto)
done
-lemma exp_converges: "(\<lambda>n. x ^ n /# real (fact n)) sums exp x"
+lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x"
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
lemma sin_converges:
@@ -604,7 +604,7 @@
else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
by (auto intro!: sums_unique sums_minus sin_converges)
-lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /# real (fact n))"
+lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
by (auto intro!: ext simp add: exp_def)
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
@@ -680,7 +680,7 @@
lemma exp_series_add:
fixes x y :: "'a::{real_field,recpower}"
- defines S_def: "S \<equiv> \<lambda>x n. x ^ n /# real (fact n)"
+ defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
proof (induct n)
case 0
@@ -688,12 +688,12 @@
unfolding S_def by simp
next
case (Suc n)
- have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /# real (Suc n)"
+ have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)"
unfolding S_def by (simp add: power_Suc del: mult_Suc)
- hence times_S: "\<And>x n. x * S x n = real (Suc n) *# S x (Suc n)"
+ hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
by simp
- have "real (Suc n) *# S (x + y) (Suc n) = (x + y) * S (x + y) n"
+ have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
by (simp only: times_S)
also have "\<dots> = (x + y) * (\<Sum>i=0..n. S x i * S y (n-i))"
by (simp only: Suc)
@@ -703,21 +703,21 @@
also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
+ (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
by (simp only: setsum_right_distrib mult_ac)
- also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *# (S x (Suc i) * S y (n-i)))
- + (\<Sum>i=0..n. real (Suc n-i) *# (S x i * S y (Suc n-i)))"
+ also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
+ + (\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
by (simp add: times_S Suc_diff_le)
- also have "(\<Sum>i=0..n. real (Suc i) *# (S x (Suc i) * S y (n-i))) =
- (\<Sum>i=0..Suc n. real i *# (S x i * S y (Suc n-i)))"
+ also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
+ (\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
by (subst setsum_cl_ivl_Suc2, simp)
- also have "(\<Sum>i=0..n. real (Suc n-i) *# (S x i * S y (Suc n-i))) =
- (\<Sum>i=0..Suc n. real (Suc n-i) *# (S x i * S y (Suc n-i)))"
+ also have "(\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
+ (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
by (subst setsum_cl_ivl_Suc, simp)
- also have "(\<Sum>i=0..Suc n. real i *# (S x i * S y (Suc n-i))) +
- (\<Sum>i=0..Suc n. real (Suc n-i) *# (S x i * S y (Suc n-i))) =
- (\<Sum>i=0..Suc n. real (Suc n) *# (S x i * S y (Suc n-i)))"
+ also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
+ (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
+ (\<Sum>i=0..Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
real_of_nat_add [symmetric], simp)
- also have "\<dots> = real (Suc n) *# (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
+ also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
by (simp only: scaleR_right.setsum)
finally show
"S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
--- a/src/HOL/Lattices.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Lattices.thy Tue Oct 16 23:12:45 2007 +0200
@@ -33,18 +33,20 @@
lemmas antisym_intro [intro!] = antisym
lemmas (in -) [rule del] = antisym_intro
-lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
-apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
- apply(blast intro: order_trans)
-apply simp
-done
+lemma le_infI1[intro]:
+ assumes "a \<sqsubseteq> x"
+ shows "a \<sqinter> b \<sqsubseteq> x"
+proof (rule order_trans)
+ show "a \<sqinter> b \<sqsubseteq> a" and "a \<sqsubseteq> x" using assms by simp
+qed
lemmas (in -) [rule del] = le_infI1
-lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
-apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
- apply(blast intro: order_trans)
-apply simp
-done
+lemma le_infI2[intro]:
+ assumes "b \<sqsubseteq> x"
+ shows "a \<sqinter> b \<sqsubseteq> x"
+proof (rule order_trans)
+ show "a \<sqinter> b \<sqsubseteq> b" and "b \<sqsubseteq> x" using assms by simp
+qed
lemmas (in -) [rule del] = le_infI2
lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
@@ -75,17 +77,11 @@
lemmas (in -) [rule del] = antisym_intro
lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
-apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
- apply(blast intro: order_trans)
-apply simp
-done
+ by (rule order_trans) auto
lemmas (in -) [rule del] = le_supI1
lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
-apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
- apply(blast intro: order_trans)
-apply simp
-done
+ by (rule order_trans) auto
lemmas (in -) [rule del] = le_supI2
lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
@@ -255,26 +251,26 @@
lemma (in lower_semilattice) inf_unique:
fixes f (infixl "\<triangle>" 70)
- assumes le1: "\<And>x y. x \<triangle> y \<^loc>\<le> x" and le2: "\<And>x y. x \<triangle> y \<^loc>\<le> y"
- and greatest: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z"
+ assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
+ and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
shows "x \<sqinter> y = x \<triangle> y"
proof (rule antisym)
- show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
+ show "x \<triangle> y \<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
next
- have leI: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z" by (blast intro: greatest)
- show "x \<sqinter> y \<^loc>\<le> x \<triangle> y" by (rule leI) simp_all
+ have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
+ show "x \<sqinter> y \<le> x \<triangle> y" by (rule leI) simp_all
qed
lemma (in upper_semilattice) sup_unique:
fixes f (infixl "\<nabla>" 70)
- assumes ge1 [simp]: "\<And>x y. x \<^loc>\<le> x \<nabla> y" and ge2: "\<And>x y. y \<^loc>\<le> x \<nabla> y"
- and least: "\<And>x y z. y \<^loc>\<le> x \<Longrightarrow> z \<^loc>\<le> x \<Longrightarrow> y \<nabla> z \<^loc>\<le> x"
+ assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
+ and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
shows "x \<squnion> y = x \<nabla> y"
proof (rule antisym)
- show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
+ show "x \<squnion> y \<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
next
- have leI: "\<And>x y z. x \<^loc>\<le> z \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<nabla> y \<^loc>\<le> z" by (blast intro: least)
- show "x \<nabla> y \<^loc>\<le> x \<squnion> y" by (rule leI) simp_all
+ have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
+ show "x \<nabla> y \<le> x \<squnion> y" by (rule leI) simp_all
qed
@@ -282,9 +278,9 @@
special case of @{const inf}/@{const sup} *}
lemma (in linorder) distrib_lattice_min_max:
- "distrib_lattice (op \<^loc>\<le>) (op \<^loc><) min max"
+ "distrib_lattice (op \<le>) (op <) min max"
proof unfold_locales
- have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
+ have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
by (auto simp add: less_le antisym)
fix x y z
show "max x (min y z) = min (max x y) (max x z)"
@@ -333,10 +329,10 @@
and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
begin
-lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<^loc>\<le> a}"
+lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
-lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
+lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
@@ -411,10 +407,10 @@
where
"bot = Sup {}"
-lemma top_greatest [simp]: "x \<^loc>\<le> top"
+lemma top_greatest [simp]: "x \<le> top"
by (unfold top_def, rule Inf_greatest, simp)
-lemma bot_least [simp]: "bot \<^loc>\<le> x"
+lemma bot_least [simp]: "bot \<le> x"
by (unfold bot_def, rule Sup_least, simp)
definition
@@ -584,4 +580,16 @@
lemmas inf_aci = inf_ACI
lemmas sup_aci = sup_ACI
+no_notation
+ inf (infixl "\<sqinter>" 70)
+
+no_notation
+ sup (infixl "\<squnion>" 65)
+
+no_notation
+ Inf ("\<Sqinter>_" [900] 900)
+
+no_notation
+ Sup ("\<Squnion>_" [900] 900)
+
end
--- a/src/HOL/Library/Kleene_Algebras.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Library/Kleene_Algebras.thy Tue Oct 16 23:12:45 2007 +0200
@@ -15,15 +15,15 @@
fixes star :: "'a \<Rightarrow> 'a"
class idem_add = ab_semigroup_add +
- assumes add_idem [simp]: "x \<^loc>+ x = x"
+ assumes add_idem [simp]: "x + x = x"
lemma add_idem2[simp]: "(x::'a::idem_add) + (x + y) = x + y"
unfolding add_assoc[symmetric]
by simp
class order_by_add = idem_add + ord +
- assumes order_def: "a \<^loc>\<le> b \<longleftrightarrow> a \<^loc>+ b = b"
- assumes strict_order_def: "a \<^loc>< b \<longleftrightarrow> a \<^loc>\<le> b \<and> a \<noteq> b"
+ assumes order_def: "a \<le> b \<longleftrightarrow> a + b = b"
+ assumes strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> a \<noteq> b"
lemma ord_simp1[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> x + y = y"
unfolding order_def .
@@ -82,14 +82,14 @@
qed
class kleene = pre_kleene + star +
- assumes star1: "\<^loc>1 \<^loc>+ a \<^loc>* star a \<^loc>\<le> star a"
- and star2: "\<^loc>1 \<^loc>+ star a \<^loc>* a \<^loc>\<le> star a"
- and star3: "a \<^loc>* x \<^loc>\<le> x \<Longrightarrow> star a \<^loc>* x \<^loc>\<le> x"
- and star4: "x \<^loc>* a \<^loc>\<le> x \<Longrightarrow> x \<^loc>* star a \<^loc>\<le> x"
+ assumes star1: "1 + a * star a \<le> star a"
+ and star2: "1 + star a * a \<le> star a"
+ and star3: "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
+ and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
class kleene_by_complete_lattice = pre_kleene
+ complete_lattice + recpower + star +
- assumes star_cont: "a \<^loc>* star b \<^loc>* c = SUPR UNIV (\<lambda>n. a \<^loc>* b \<^loc>^ n \<^loc>* c)"
+ assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
lemma plus_leI:
fixes x :: "'a :: order_by_add"
--- a/src/HOL/Library/Quicksort.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Library/Quicksort.thy Tue Oct 16 23:12:45 2007 +0200
@@ -14,7 +14,7 @@
function quicksort :: "'a list \<Rightarrow> 'a list" where
"quicksort [] = []" |
-"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<^loc>\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<^loc>\<le>y])"
+"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
by pat_completeness auto
termination
--- a/src/HOL/Library/Quotient.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Library/Quotient.thy Tue Oct 16 23:12:45 2007 +0200
@@ -22,12 +22,12 @@
*}
class eqv = type +
- fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>\<sim>" 50)
+ fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50)
class equiv = eqv +
- assumes equiv_refl [intro]: "x \<^loc>\<sim> x"
- assumes equiv_trans [trans]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> z \<Longrightarrow> x \<^loc>\<sim> z"
- assumes equiv_sym [sym]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> x"
+ assumes equiv_refl [intro]: "x \<sim> x"
+ assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
+ assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
proof -
--- a/src/HOL/List.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/List.thy Tue Oct 16 23:12:45 2007 +0200
@@ -218,11 +218,11 @@
fun (in linorder) sorted :: "'a list \<Rightarrow> bool" where
"sorted [] \<longleftrightarrow> True" |
"sorted [x] \<longleftrightarrow> True" |
-"sorted (x#y#zs) \<longleftrightarrow> x \<^loc><= y \<and> sorted (y#zs)"
+"sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
fun (in linorder) insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"insort x [] = [x]" |
-"insort x (y#ys) = (if x \<^loc><= y then (x#y#ys) else y#(insort x ys))"
+"insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
fun (in linorder) sort :: "'a list \<Rightarrow> 'a list" where
"sort [] = []" |
@@ -1816,11 +1816,11 @@
by (induct k arbitrary: a b l) simp_all
lemma (in semigroup_add) foldl_assoc:
-shows "foldl op\<^loc>+ (x\<^loc>+y) zs = x \<^loc>+ (foldl op\<^loc>+ y zs)"
+shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
by (induct zs arbitrary: y) (simp_all add:add_assoc)
lemma (in monoid_add) foldl_absorb0:
-shows "x \<^loc>+ (foldl op\<^loc>+ \<^loc>0 zs) = foldl op\<^loc>+ x zs"
+shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
by (induct zs) (simp_all add:foldl_assoc)
@@ -1843,7 +1843,7 @@
lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
-lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op \<^loc>+ xs a = foldl op \<^loc>+ a xs"
+lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
by (induct xs, auto simp add: foldl_assoc add_commute)
text {*
@@ -2526,12 +2526,12 @@
context linorder
begin
-lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x \<^loc><= y))"
+lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
apply(induct xs arbitrary: x) apply simp
by simp (blast intro: order_trans)
lemma sorted_append:
- "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<^loc>\<le>y))"
+ "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
by (induct xs) (auto simp add:sorted_Cons)
lemma set_insort: "set(insort x xs) = insert x (set xs)"
@@ -2583,32 +2583,32 @@
class finite_intvl_succ = linorder +
fixes successor :: "'a \<Rightarrow> 'a"
-assumes finite_intvl: "finite(ord.atLeastAtMost (op \<^loc>\<le>) a b)" (* FIXME should be finite({a..b}) *)
-and successor_incr: "a \<^loc>< successor a"
-and ord_discrete: "\<not>(\<exists>x. a \<^loc>< x & x \<^loc>< successor a)"
+assumes finite_intvl: "finite(ord.atLeastAtMost (op \<le>) a b)" (* FIXME should be finite({a..b}) *)
+and successor_incr: "a < successor a"
+and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
context finite_intvl_succ
begin
definition
- upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1\<^loc>[_../_])") where
-"upto i j == THE is. set is = \<^loc>{i..j} & sorted is & distinct is"
-
-lemma set_upto[simp]: "set\<^loc>[a..b] = \<^loc>{a..b}"
+ upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
+"upto i j == THE is. set is = {i..j} & sorted is & distinct is"
+
+lemma set_upto[simp]: "set[a..b] = {a..b}"
apply(simp add:upto_def)
apply(rule the1I2)
apply(simp_all add: finite_sorted_distinct_unique finite_intvl)
done
-lemma insert_intvl: "i \<^loc>\<le> j \<Longrightarrow> insert i \<^loc>{successor i..j} = \<^loc>{i..j}"
+lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
apply(insert successor_incr[of i])
apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
apply (metis ord_discrete less_le not_le)
done
-lemma upto_rec[code]: "\<^loc>[i..j] = (if i \<^loc>\<le> j then i # \<^loc>[successor i..j] else [])"
+lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
proof cases
- assume "i \<^loc>\<le> j" thus ?thesis
+ assume "i \<le> j" thus ?thesis
apply(simp add:upto_def)
apply (rule the1_equality[OF finite_sorted_distinct_unique])
apply (simp add:finite_intvl)
@@ -2618,7 +2618,7 @@
apply (metis successor_incr leD less_imp_le order_trans)
done
next
- assume "~ i \<^loc>\<le> j" thus ?thesis
+ assume "~ i \<le> j" thus ?thesis
by(simp add:upto_def atLeastAtMost_empty cong:conj_cong)
qed
--- a/src/HOL/Nat.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Nat.thy Tue Oct 16 23:12:45 2007 +0200
@@ -1154,7 +1154,7 @@
begin
definition
- of_nat_def: "of_nat = nat_rec \<^loc>0 (\<lambda>_. (op \<^loc>+) \<^loc>1)"
+ of_nat_def: "of_nat = nat_rec 0 (\<lambda>_. (op +) 1)"
end
@@ -1340,8 +1340,8 @@
begin
lemma of_nat_simps [simp, code]:
- shows of_nat_0: "of_nat 0 = \<^loc>0"
- and of_nat_Suc: "of_nat (Suc m) = \<^loc>1 \<^loc>+ of_nat m"
+ shows of_nat_0: "of_nat 0 = 0"
+ and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
unfolding of_nat_def by simp_all
end
@@ -1405,7 +1405,7 @@
class semiring_char_0 = semiring_1 +
assumes of_nat_eq_iff [simp]:
- "(Nat.semiring_1.of_nat \<^loc>1 \<^loc>0 (op \<^loc>+) m = Nat.semiring_1.of_nat \<^loc>1 \<^loc>0 (op \<^loc>+) n) = (m = n)"
+ "of_nat m = of_nat n \<longleftrightarrow> m = n"
text{*Every @{text ordered_semidom} has characteristic zero.*}
instance ordered_semidom < semiring_char_0
--- a/src/HOL/OrderedGroup.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/OrderedGroup.thy Tue Oct 16 23:12:45 2007 +0200
@@ -27,58 +27,75 @@
subsection {* Semigroups and Monoids *}
class semigroup_add = plus +
- assumes add_assoc: "(a \<^loc>+ b) \<^loc>+ c = a \<^loc>+ (b \<^loc>+ c)"
+ assumes add_assoc: "(a + b) + c = a + (b + c)"
class ab_semigroup_add = semigroup_add +
- assumes add_commute: "a \<^loc>+ b = b \<^loc>+ a"
+ assumes add_commute: "a + b = b + a"
+begin
-lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ab_semigroup_add))"
- by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
+lemma add_left_commute: "a + (b + c) = b + (a + c)"
+ by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
+ (*FIXME term_check*)
+
+theorems add_ac = add_assoc add_commute add_left_commute
+
+end
theorems add_ac = add_assoc add_commute add_left_commute
class semigroup_mult = times +
- assumes mult_assoc: "(a \<^loc>* b) \<^loc>* c = a \<^loc>* (b \<^loc>* c)"
+ assumes mult_assoc: "(a * b) * c = a * (b * c)"
class ab_semigroup_mult = semigroup_mult +
- assumes mult_commute: "a \<^loc>* b = b \<^loc>* a"
+ assumes mult_commute: "a * b = b * a"
begin
-lemma mult_left_commute: "a \<^loc>* (b \<^loc>* c) = b \<^loc>* (a \<^loc>* c)"
- by (rule mk_left_commute [of "op \<^loc>*", OF mult_assoc mult_commute])
+lemma mult_left_commute: "a * (b * c) = b * (a * c)"
+ by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
+ (*FIXME term_check*)
+
+theorems mult_ac = mult_assoc mult_commute mult_left_commute
end
theorems mult_ac = mult_assoc mult_commute mult_left_commute
class monoid_add = zero + semigroup_add +
- assumes add_0_left [simp]: "\<^loc>0 \<^loc>+ a = a" and add_0_right [simp]: "a \<^loc>+ \<^loc>0 = a"
+ assumes add_0_left [simp]: "0 + a = a"
+ and add_0_right [simp]: "a + 0 = a"
class comm_monoid_add = zero + ab_semigroup_add +
- assumes add_0: "\<^loc>0 \<^loc>+ a = a"
+ assumes add_0: "0 + a = a"
+begin
-instance comm_monoid_add < monoid_add
-by intro_classes (insert comm_monoid_add_class.zero_plus.add_0, simp_all add: add_commute, auto)
+subclass monoid_add
+ by unfold_locales (insert add_0, simp_all add: add_commute)
+
+end
class monoid_mult = one + semigroup_mult +
- assumes mult_1_left [simp]: "\<^loc>1 \<^loc>* a = a"
- assumes mult_1_right [simp]: "a \<^loc>* \<^loc>1 = a"
+ assumes mult_1_left [simp]: "1 * a = a"
+ assumes mult_1_right [simp]: "a * 1 = a"
class comm_monoid_mult = one + ab_semigroup_mult +
- assumes mult_1: "\<^loc>1 \<^loc>* a = a"
+ assumes mult_1: "1 * a = a"
+begin
-instance comm_monoid_mult \<subseteq> monoid_mult
- by intro_classes (insert mult_1, simp_all add: mult_commute, auto)
+subclass monoid_mult
+ by unfold_locales (insert mult_1, simp_all add: mult_commute)
+
+end
class cancel_semigroup_add = semigroup_add +
- assumes add_left_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"
- assumes add_right_imp_eq: "b \<^loc>+ a = c \<^loc>+ a \<Longrightarrow> b = c"
+ assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
+ assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
class cancel_ab_semigroup_add = ab_semigroup_add +
- assumes add_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"
+ assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
+begin
-instance cancel_ab_semigroup_add \<subseteq> cancel_semigroup_add
-proof intro_classes
+subclass cancel_semigroup_add
+proof unfold_locales
fix a b c :: 'a
assume "a + b = a + c"
then show "b = c" by (rule add_imp_eq)
@@ -89,60 +106,50 @@
then show "b = c" by (rule add_imp_eq)
qed
+end context cancel_ab_semigroup_add begin
+
lemma add_left_cancel [simp]:
- "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
+ "a + b = a + c \<longleftrightarrow> b = c"
by (blast dest: add_left_imp_eq)
lemma add_right_cancel [simp]:
- "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
+ "b + a = c + a \<longleftrightarrow> b = c"
by (blast dest: add_right_imp_eq)
+end
+
subsection {* Groups *}
-class ab_group_add = minus + comm_monoid_add +
- assumes ab_left_minus: "uminus a \<^loc>+ a = \<^loc>0"
- assumes ab_diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
-
class group_add = minus + monoid_add +
- assumes left_minus [simp]: "uminus a \<^loc>+ a = \<^loc>0"
- assumes diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
-
-instance ab_group_add < group_add
-by intro_classes (simp_all add: ab_left_minus ab_diff_minus)
+ assumes left_minus [simp]: "- a + a = 0"
+ assumes diff_minus: "a - b = a + (- b)"
+begin
-instance ab_group_add \<subseteq> cancel_ab_semigroup_add
-proof intro_classes
- fix a b c :: 'a
- assume "a + b = a + c"
- then have "uminus a + a + b = uminus a + a + c" unfolding add_assoc by simp
- then show "b = c" by simp
-qed
+lemma minus_add_cancel: "- a + (a + b) = b"
+ by (simp add: add_assoc[symmetric])
-lemma minus_add_cancel: "-(a::'a::group_add) + (a+b) = b"
-by(simp add:add_assoc[symmetric])
-
-lemma minus_zero[simp]: "-(0::'a::group_add) = 0"
+lemma minus_zero [simp]: "- 0 = 0"
proof -
- have "-(0::'a::group_add) = - 0 + (0+0)" by(simp only: add_0_right)
- also have "\<dots> = 0" by(rule minus_add_cancel)
+ have "- 0 = - 0 + (0 + 0)" by (simp only: add_0_right)
+ also have "\<dots> = 0" by (rule minus_add_cancel)
finally show ?thesis .
qed
-lemma minus_minus[simp]: "- (-(a::'a::group_add)) = a"
+lemma minus_minus [simp]: "- (- a) = a"
proof -
- have "-(-a) = -(-a) + (-a + a)" by simp
- also have "\<dots> = a" by(rule minus_add_cancel)
+ have "- (- a) = - (- a) + (- a + a)" by simp
+ also have "\<dots> = a" by (rule minus_add_cancel)
finally show ?thesis .
qed
-lemma right_minus[simp]: "a + - a = (0::'a::group_add)"
+lemma right_minus [simp]: "a + - a = 0"
proof -
- have "a + -a = -(-a) + -a" by simp
- also have "\<dots> = 0" thm group_add.left_minus by(rule left_minus)
+ have "a + - a = - (- a) + - a" by simp
+ also have "\<dots> = 0" by (rule left_minus)
finally show ?thesis .
qed
-lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::group_add))"
+lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
proof
assume "a - b = 0"
have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
@@ -152,154 +159,173 @@
assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
qed
-lemma equals_zero_I: assumes "a+b = 0" shows "-a = (b::'a::group_add)"
+lemma equals_zero_I:
+ assumes "a + b = 0"
+ shows "- a = b"
proof -
- have "- a = -a + (a+b)" using assms by simp
- also have "\<dots> = b" by(simp add:add_assoc[symmetric])
+ have "- a = - a + (a + b)" using assms by simp
+ also have "\<dots> = b" by (simp add: add_assoc[symmetric])
finally show ?thesis .
qed
-lemma diff_self[simp]: "(a::'a::group_add) - a = 0"
-by(simp add: diff_minus)
+lemma diff_self [simp]: "a - a = 0"
+ by (simp add: diff_minus)
-lemma diff_0 [simp]: "(0::'a::group_add) - a = -a"
-by (simp add: diff_minus)
+lemma diff_0 [simp]: "0 - a = - a"
+ by (simp add: diff_minus)
-lemma diff_0_right [simp]: "a - (0::'a::group_add) = a"
-by (simp add: diff_minus)
+lemma diff_0_right [simp]: "a - 0 = a"
+ by (simp add: diff_minus)
-lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::group_add)"
-by (simp add: diff_minus)
+lemma diff_minus_eq_add [simp]: "a - - b = a + b"
+ by (simp add: diff_minus)
-lemma uminus_add_conv_diff: "-a + b = b - (a::'a::ab_group_add)"
-by(simp add:diff_minus add_commute)
-
-lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::group_add))"
+lemma neg_equal_iff_equal [simp]:
+ "- a = - b \<longleftrightarrow> a = b"
proof
assume "- a = - b"
hence "- (- a) = - (- b)"
by simp
- thus "a=b" by simp
+ thus "a = b" by simp
next
- assume "a=b"
- thus "-a = -b" by simp
+ assume "a = b"
+ thus "- a = - b" by simp
qed
-lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::group_add))"
-by (subst neg_equal_iff_equal [symmetric], simp)
+lemma neg_equal_0_iff_equal [simp]:
+ "- a = 0 \<longleftrightarrow> a = 0"
+ by (subst neg_equal_iff_equal [symmetric], simp)
-lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::group_add))"
-by (subst neg_equal_iff_equal [symmetric], simp)
+lemma neg_0_equal_iff_equal [simp]:
+ "0 = - a \<longleftrightarrow> 0 = a"
+ by (subst neg_equal_iff_equal [symmetric], simp)
text{*The next two equations can make the simplifier loop!*}
-lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::group_add))"
+lemma equation_minus_iff:
+ "a = - b \<longleftrightarrow> b = - a"
proof -
- have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
+ have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
+ thus ?thesis by (simp add: eq_commute)
+qed
+
+lemma minus_equation_iff:
+ "- a = b \<longleftrightarrow> - b = a"
+proof -
+ have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
thus ?thesis by (simp add: eq_commute)
qed
-lemma minus_equation_iff: "(- a = b) = (- (b::'a::group_add) = a)"
-proof -
- have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
- thus ?thesis by (simp add: eq_commute)
+end
+
+class ab_group_add = minus + comm_monoid_add +
+ assumes ab_left_minus: "- a + a = 0"
+ assumes ab_diff_minus: "a - b = a + (- b)"
+
+subclass (in ab_group_add) group_add
+ by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)
+
+subclass (in ab_group_add) cancel_semigroup_add
+proof unfold_locales
+ fix a b c :: 'a
+ assume "a + b = a + c"
+ then have "- a + a + b = - a + a + c"
+ unfolding add_assoc by simp
+ then show "b = c" by simp
+next
+ fix a b c :: 'a
+ assume "b + a = c + a"
+ then have "b + (a + - a) = c + (a + - a)"
+ unfolding add_assoc [symmetric] by simp
+ then show "b = c" by simp
qed
-lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ab_group_add)"
-apply (rule equals_zero_I)
-apply (simp add: add_ac)
-done
+subclass (in ab_group_add) cancel_ab_semigroup_add
+proof unfold_locales
+ fix a b c :: 'a
+ assume "a + b = a + c"
+ then have "- a + a + b = - a + a + c"
+ unfolding add_assoc by simp
+ then show "b = c" by simp
+qed
+
+context ab_group_add
+begin
-lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ab_group_add)"
-by (simp add: diff_minus add_commute)
+lemma uminus_add_conv_diff:
+ "- a + b = b - a"
+ by (simp add:diff_minus add_commute)
+
+lemma minus_add_distrib [simp]:
+ "- (a + b) = - a + - b"
+ by (rule equals_zero_I) (simp add: add_ac)
+
+lemma minus_diff_eq [simp]:
+ "- (a - b) = b - a"
+ by (simp add: diff_minus add_commute)
+
+end
subsection {* (Partially) Ordered Groups *}
class pordered_ab_semigroup_add = order + ab_semigroup_add +
- assumes add_left_mono: "a \<^loc>\<le> b \<Longrightarrow> c \<^loc>+ a \<^loc>\<le> c \<^loc>+ b"
-
-class pordered_cancel_ab_semigroup_add =
- pordered_ab_semigroup_add + cancel_ab_semigroup_add
-
-class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
- assumes add_le_imp_le_left: "c \<^loc>+ a \<^loc>\<le> c \<^loc>+ b \<Longrightarrow> a \<^loc>\<le> b"
-
-class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
-
-instance pordered_ab_group_add \<subseteq> pordered_ab_semigroup_add_imp_le
-proof
- fix a b c :: 'a
- assume "c + a \<le> c + b"
- hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
- hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
- thus "a \<le> b" by simp
-qed
-
-class ordered_ab_semigroup_add =
- linorder + pordered_ab_semigroup_add
+ assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
+begin
-class ordered_cancel_ab_semigroup_add =
- linorder + pordered_cancel_ab_semigroup_add
-
-instance ordered_cancel_ab_semigroup_add \<subseteq> ordered_ab_semigroup_add ..
-
-instance ordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add_imp_le
-proof
- fix a b c :: 'a
- assume le: "c + a <= c + b"
- show "a <= b"
- proof (rule ccontr)
- assume w: "~ a \<le> b"
- hence "b <= a" by (simp add: linorder_not_le)
- hence le2: "c+b <= c+a" by (rule add_left_mono)
- have "a = b"
- apply (insert le)
- apply (insert le2)
- apply (drule order_antisym, simp_all)
- done
- with w show False
- by (simp add: linorder_not_le [symmetric])
- qed
-qed
-
-lemma add_right_mono: "a \<le> (b::'a::pordered_ab_semigroup_add) ==> a + c \<le> b + c"
+lemma add_right_mono:
+ "a \<le> b \<Longrightarrow> a + c \<le> b + c"
by (simp add: add_commute [of _ c] add_left_mono)
text {* non-strict, in both arguments *}
lemma add_mono:
- "[|a \<le> b; c \<le> d|] ==> a + c \<le> b + (d::'a::pordered_ab_semigroup_add)"
+ "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
apply (erule add_right_mono [THEN order_trans])
apply (simp add: add_commute add_left_mono)
done
+end
+
+class pordered_cancel_ab_semigroup_add =
+ pordered_ab_semigroup_add + cancel_ab_semigroup_add
+begin
+
lemma add_strict_left_mono:
- "a < b ==> c + a < c + (b::'a::pordered_cancel_ab_semigroup_add)"
- by (simp add: order_less_le add_left_mono)
+ "a < b \<Longrightarrow> c + a < c + b"
+ by (auto simp add: less_le add_left_mono)
lemma add_strict_right_mono:
- "a < b ==> a + c < b + (c::'a::pordered_cancel_ab_semigroup_add)"
- by (simp add: add_commute [of _ c] add_strict_left_mono)
+ "a < b \<Longrightarrow> a + c < b + c"
+ by (simp add: add_commute [of _ c] add_strict_left_mono)
text{*Strict monotonicity in both arguments*}
-lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
-apply (erule add_strict_right_mono [THEN order_less_trans])
+lemma add_strict_mono:
+ "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
+apply (erule add_strict_right_mono [THEN less_trans])
apply (erule add_strict_left_mono)
done
lemma add_less_le_mono:
- "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
-apply (erule add_strict_right_mono [THEN order_less_le_trans])
-apply (erule add_left_mono)
+ "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
+apply (erule add_strict_right_mono [THEN less_le_trans])
+apply (erule add_left_mono)
done
lemma add_le_less_mono:
- "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
-apply (erule add_right_mono [THEN order_le_less_trans])
+ "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
+apply (erule add_right_mono [THEN le_less_trans])
apply (erule add_strict_left_mono)
done
+end
+
+class pordered_ab_semigroup_add_imp_le =
+ pordered_cancel_ab_semigroup_add +
+ assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
+begin
+
lemma add_less_imp_less_left:
- assumes less: "c + a < c + b" shows "a < (b::'a::pordered_ab_semigroup_add_imp_le)"
+ assumes less: "c + a < c + b"
+ shows "a < b"
proof -
from less have le: "c + a <= c + b" by (simp add: order_le_less)
have "a <= b"
@@ -317,30 +343,90 @@
qed
lemma add_less_imp_less_right:
- "a + c < b + c ==> a < (b::'a::pordered_ab_semigroup_add_imp_le)"
+ "a + c < b + c \<Longrightarrow> a < b"
apply (rule add_less_imp_less_left [of c])
apply (simp add: add_commute)
done
lemma add_less_cancel_left [simp]:
- "(c+a < c+b) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))"
-by (blast intro: add_less_imp_less_left add_strict_left_mono)
+ "c + a < c + b \<longleftrightarrow> a < b"
+ by (blast intro: add_less_imp_less_left add_strict_left_mono)
lemma add_less_cancel_right [simp]:
- "(a+c < b+c) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))"
-by (blast intro: add_less_imp_less_right add_strict_right_mono)
+ "a + c < b + c \<longleftrightarrow> a < b"
+ by (blast intro: add_less_imp_less_right add_strict_right_mono)
lemma add_le_cancel_left [simp]:
- "(c+a \<le> c+b) = (a \<le> (b::'a::pordered_ab_semigroup_add_imp_le))"
-by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
+ "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
+ by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
lemma add_le_cancel_right [simp]:
- "(a+c \<le> b+c) = (a \<le> (b::'a::pordered_ab_semigroup_add_imp_le))"
-by (simp add: add_commute[of a c] add_commute[of b c])
+ "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
+ by (simp add: add_commute [of a c] add_commute [of b c])
lemma add_le_imp_le_right:
- "a + c \<le> b + c ==> a \<le> (b::'a::pordered_ab_semigroup_add_imp_le)"
-by simp
+ "a + c \<le> b + c \<Longrightarrow> a \<le> b"
+ by simp
+
+end
+
+class pordered_ab_group_add =
+ ab_group_add + pordered_ab_semigroup_add
+begin
+
+subclass pordered_cancel_ab_semigroup_add
+ by unfold_locales
+
+subclass pordered_ab_semigroup_add_imp_le
+proof unfold_locales
+ fix a b c :: 'a
+ assume "c + a \<le> c + b"
+ hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
+ hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
+ thus "a \<le> b" by simp
+qed
+
+end
+
+class ordered_ab_semigroup_add =
+ linorder + pordered_ab_semigroup_add
+
+class ordered_cancel_ab_semigroup_add =
+ linorder + pordered_cancel_ab_semigroup_add
+
+subclass (in ordered_cancel_ab_semigroup_add) ordered_ab_semigroup_add
+ by unfold_locales
+
+subclass (in ordered_cancel_ab_semigroup_add) pordered_ab_semigroup_add_imp_le
+proof unfold_locales
+ fix a b c :: 'a
+ assume le: "c + a <= c + b"
+ show "a <= b"
+ proof (rule ccontr)
+ assume w: "~ a \<le> b"
+ hence "b <= a" by (simp add: linorder_not_le)
+ hence le2: "c + b <= c + a" by (rule add_left_mono)
+ have "a = b"
+ apply (insert le)
+ apply (insert le2)
+ apply (drule antisym, simp_all)
+ done
+ with w show False
+ by (simp add: linorder_not_le [symmetric])
+ qed
+qed
+
+-- {* FIXME continue localization here *}
+
+lemma max_add_distrib_left:
+ fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
+ shows "(max x y) + z = max (x+z) (y+z)"
+by (rule max_of_mono [THEN sym], rule add_le_cancel_right)
+
+lemma min_add_distrib_left:
+ fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
+ shows "(min x y) + z = min (x+z) (y+z)"
+by (rule min_of_mono [THEN sym], rule add_le_cancel_right)
lemma add_increasing:
fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
@@ -362,16 +448,6 @@
shows "[|0\<le>a; b<c|] ==> b < a + c"
by (insert add_le_less_mono [of 0 a b c], simp)
-lemma max_add_distrib_left:
- fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
- shows "(max x y) + z = max (x+z) (y+z)"
-by (rule max_of_mono [THEN sym], rule add_le_cancel_right)
-
-lemma min_add_distrib_left:
- fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
- shows "(min x y) + z = min (x+z) (y+z)"
-by (rule min_of_mono [THEN sym], rule add_le_cancel_right)
-
lemma max_diff_distrib_left:
fixes z :: "'a::pordered_ab_group_add"
shows "(max x y) - z = max (x-z) (y-z)"
--- a/src/HOL/Orderings.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Orderings.thy Tue Oct 16 23:12:45 2007 +0200
@@ -14,10 +14,10 @@
subsection {* Partial orders *}
class order = ord +
- assumes less_le: "x \<^loc>< y \<longleftrightarrow> x \<^loc>\<le> y \<and> x \<noteq> y"
- and order_refl [iff]: "x \<^loc>\<le> x"
- and order_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> z"
- assumes antisym: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
+ assumes less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
+ and order_refl [iff]: "x \<le> x"
+ and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
+ assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
begin
@@ -28,94 +28,94 @@
text {* Reflexivity. *}
-lemma eq_refl: "x = y \<Longrightarrow> x \<^loc>\<le> y"
+lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
-- {* This form is useful with the classical reasoner. *}
by (erule ssubst) (rule order_refl)
-lemma less_irrefl [iff]: "\<not> x \<^loc>< x"
+lemma less_irrefl [iff]: "\<not> x < x"
by (simp add: less_le)
-lemma le_less: "x \<^loc>\<le> y \<longleftrightarrow> x \<^loc>< y \<or> x = y"
+lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
-- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
by (simp add: less_le) blast
-lemma le_imp_less_or_eq: "x \<^loc>\<le> y \<Longrightarrow> x \<^loc>< y \<or> x = y"
+lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
unfolding less_le by blast
-lemma less_imp_le: "x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y"
+lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
unfolding less_le by blast
-lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
+lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
by (erule contrapos_pn, erule subst, rule less_irrefl)
text {* Useful for simplification, but too risky to include by default. *}
-lemma less_imp_not_eq: "x \<^loc>< y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
+lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
by auto
-lemma less_imp_not_eq2: "x \<^loc>< y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
+lemma less_imp_not_eq2: "x < y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
by auto
text {* Transitivity rules for calculational reasoning *}
-lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<^loc>\<le> b \<Longrightarrow> a \<^loc>< b"
+lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
by (simp add: less_le)
-lemma le_neq_trans: "a \<^loc>\<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<^loc>< b"
+lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b"
by (simp add: less_le)
text {* Asymmetry. *}
-lemma less_not_sym: "x \<^loc>< y \<Longrightarrow> \<not> (y \<^loc>< x)"
+lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
by (simp add: less_le antisym)
-lemma less_asym: "x \<^loc>< y \<Longrightarrow> (\<not> P \<Longrightarrow> y \<^loc>< x) \<Longrightarrow> P"
+lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
by (drule less_not_sym, erule contrapos_np) simp
-lemma eq_iff: "x = y \<longleftrightarrow> x \<^loc>\<le> y \<and> y \<^loc>\<le> x"
+lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
by (blast intro: antisym)
-lemma antisym_conv: "y \<^loc>\<le> x \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
+lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
by (blast intro: antisym)
-lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
+lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
by (erule contrapos_pn, erule subst, rule less_irrefl)
text {* Transitivity. *}
-lemma less_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
+lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
by (simp add: less_le) (blast intro: order_trans antisym)
-lemma le_less_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
+lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
by (simp add: less_le) (blast intro: order_trans antisym)
-lemma less_le_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>< z"
+lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
by (simp add: less_le) (blast intro: order_trans antisym)
text {* Useful for simplification, but too risky to include by default. *}
-lemma less_imp_not_less: "x \<^loc>< y \<Longrightarrow> (\<not> y \<^loc>< x) \<longleftrightarrow> True"
+lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
by (blast elim: less_asym)
-lemma less_imp_triv: "x \<^loc>< y \<Longrightarrow> (y \<^loc>< x \<longrightarrow> P) \<longleftrightarrow> True"
+lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
by (blast elim: less_asym)
text {* Transitivity rules for calculational reasoning *}
-lemma less_asym': "a \<^loc>< b \<Longrightarrow> b \<^loc>< a \<Longrightarrow> P"
+lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
by (rule less_asym)
text {* Reverse order *}
lemma order_reverse:
- "order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+ "order (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
by unfold_locales
(simp add: less_le, auto intro: antisym order_trans)
@@ -128,67 +128,67 @@
assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
begin
-lemma less_linear: "x \<^loc>< y \<or> x = y \<or> y \<^loc>< x"
+lemma less_linear: "x < y \<or> x = y \<or> y < x"
unfolding less_le using less_le linear by blast
-lemma le_less_linear: "x \<^loc>\<le> y \<or> y \<^loc>< x"
+lemma le_less_linear: "x \<le> y \<or> y < x"
by (simp add: le_less less_linear)
lemma le_cases [case_names le ge]:
- "(x \<^loc>\<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>\<le> x \<Longrightarrow> P) \<Longrightarrow> P"
+ "(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
using linear by blast
lemma linorder_cases [case_names less equal greater]:
- "(x \<^loc>< y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> P) \<Longrightarrow> P"
+ "(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P"
using less_linear by blast
-lemma not_less: "\<not> x \<^loc>< y \<longleftrightarrow> y \<^loc>\<le> x"
+lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x"
apply (simp add: less_le)
using linear apply (blast intro: antisym)
done
lemma not_less_iff_gr_or_eq:
- "\<not>(x \<^loc>< y) \<longleftrightarrow> (x \<^loc>> y | x = y)"
+ "\<not>(x < y) \<longleftrightarrow> (x > y | x = y)"
apply(simp add:not_less le_less)
apply blast
done
-lemma not_le: "\<not> x \<^loc>\<le> y \<longleftrightarrow> y \<^loc>< x"
+lemma not_le: "\<not> x \<le> y \<longleftrightarrow> y < x"
apply (simp add: less_le)
using linear apply (blast intro: antisym)
done
-lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x \<^loc>< y \<or> y \<^loc>< x"
+lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x < y \<or> y < x"
by (cut_tac x = x and y = y in less_linear, auto)
-lemma neqE: "x \<noteq> y \<Longrightarrow> (x \<^loc>< y \<Longrightarrow> R) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> R) \<Longrightarrow> R"
+lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R"
by (simp add: neq_iff) blast
-lemma antisym_conv1: "\<not> x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
+lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
by (blast intro: antisym dest: not_less [THEN iffD1])
-lemma antisym_conv2: "x \<^loc>\<le> y \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
+lemma antisym_conv2: "x \<le> y \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
by (blast intro: antisym dest: not_less [THEN iffD1])
-lemma antisym_conv3: "\<not> y \<^loc>< x \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
+lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
by (blast intro: antisym dest: not_less [THEN iffD1])
text{*Replacing the old Nat.leI*}
-lemma leI: "\<not> x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x"
+lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x"
unfolding not_less .
-lemma leD: "y \<^loc>\<le> x \<Longrightarrow> \<not> x \<^loc>< y"
+lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
unfolding not_less .
(*FIXME inappropriate name (or delete altogether)*)
-lemma not_leE: "\<not> y \<^loc>\<le> x \<Longrightarrow> x \<^loc>< y"
+lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y"
unfolding not_le .
text {* Reverse order *}
lemma linorder_reverse:
- "linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+ "linorder (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
by unfold_locales
(simp add: less_le, auto intro: antisym order_trans simp add: linear)
@@ -199,42 +199,42 @@
definition (in ord)
min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- [code unfold, code inline del]: "min a b = (if a \<^loc>\<le> b then a else b)"
+ [code unfold, code inline del]: "min a b = (if a \<le> b then a else b)"
definition (in ord)
max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- [code unfold, code inline del]: "max a b = (if a \<^loc>\<le> b then b else a)"
+ [code unfold, code inline del]: "max a b = (if a \<le> b then b else a)"
lemma min_le_iff_disj:
- "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
+ "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
unfolding min_def using linear by (auto intro: order_trans)
lemma le_max_iff_disj:
- "z \<^loc>\<le> max x y \<longleftrightarrow> z \<^loc>\<le> x \<or> z \<^loc>\<le> y"
+ "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
unfolding max_def using linear by (auto intro: order_trans)
lemma min_less_iff_disj:
- "min x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<or> y \<^loc>< z"
+ "min x y < z \<longleftrightarrow> x < z \<or> y < z"
unfolding min_def le_less using less_linear by (auto intro: less_trans)
lemma less_max_iff_disj:
- "z \<^loc>< max x y \<longleftrightarrow> z \<^loc>< x \<or> z \<^loc>< y"
+ "z < max x y \<longleftrightarrow> z < x \<or> z < y"
unfolding max_def le_less using less_linear by (auto intro: less_trans)
lemma min_less_iff_conj [simp]:
- "z \<^loc>< min x y \<longleftrightarrow> z \<^loc>< x \<and> z \<^loc>< y"
+ "z < min x y \<longleftrightarrow> z < x \<and> z < y"
unfolding min_def le_less using less_linear by (auto intro: less_trans)
lemma max_less_iff_conj [simp]:
- "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z"
+ "max x y < z \<longleftrightarrow> x < z \<and> y < z"
unfolding max_def le_less using less_linear by (auto intro: less_trans)
lemma split_min [noatp]:
- "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)"
+ "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
by (simp add: min_def)
lemma split_max [noatp]:
- "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)"
+ "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
by (simp add: max_def)
end
@@ -371,109 +371,109 @@
(* The type constraint on @{term op =} below is necessary since the operation
is not a parameter of the locale. *)
lemmas (in order)
- [order add less_reflE: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add less_reflE: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_irrefl [THEN notE]
lemmas (in order)
- [order add le_refl: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
order_refl
lemmas (in order)
- [order add less_imp_le: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_imp_le
lemmas (in order)
- [order add eqI: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
antisym
lemmas (in order)
- [order add eqD1: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
eq_refl
lemmas (in order)
- [order add eqD2: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
sym [THEN eq_refl]
lemmas (in order)
- [order add less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_trans
lemmas (in order)
- [order add less_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_le_trans
lemmas (in order)
- [order add le_less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
le_less_trans
lemmas (in order)
- [order add le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
order_trans
lemmas (in order)
- [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
le_neq_trans
lemmas (in order)
- [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
neq_le_trans
lemmas (in order)
- [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_imp_neq
lemmas (in order)
- [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
eq_neq_eq_imp_neq
lemmas (in order)
- [order add not_sym: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_sym
-lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = _
+lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
lemmas (in linorder)
- [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_irrefl [THEN notE]
lemmas (in linorder)
- [order add le_refl: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
order_refl
lemmas (in linorder)
- [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_imp_le
lemmas (in linorder)
- [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_less [THEN iffD2]
lemmas (in linorder)
- [order add not_leI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_le [THEN iffD2]
lemmas (in linorder)
- [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_less [THEN iffD1]
lemmas (in linorder)
- [order add not_leD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_le [THEN iffD1]
lemmas (in linorder)
- [order add eqI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
antisym
lemmas (in linorder)
- [order add eqD1: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
eq_refl
lemmas (in linorder)
- [order add eqD2: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
sym [THEN eq_refl]
lemmas (in linorder)
- [order add less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_trans
lemmas (in linorder)
- [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_le_trans
lemmas (in linorder)
- [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
le_less_trans
lemmas (in linorder)
- [order add le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
order_trans
lemmas (in linorder)
- [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
le_neq_trans
lemmas (in linorder)
- [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
neq_le_trans
lemmas (in linorder)
- [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_imp_neq
lemmas (in linorder)
- [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
eq_neq_eq_imp_neq
lemmas (in linorder)
- [order add not_sym: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+ [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_sym
--- a/src/HOL/Power.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Power.thy Tue Oct 16 23:12:45 2007 +0200
@@ -12,13 +12,13 @@
begin
class power = type +
- fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "\<^loc>^" 80)
+ fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80)
subsection{*Powers for Arbitrary Monoids*}
class recpower = monoid_mult + power +
- assumes power_0 [simp]: "a \<^loc>^ 0 = \<^loc>1"
- assumes power_Suc: "a \<^loc>^ Suc n = a \<^loc>* (a \<^loc>^ n)"
+ assumes power_0 [simp]: "a ^ 0 = 1"
+ assumes power_Suc: "a ^ Suc n = a * (a ^ n)"
lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
by (simp add: power_Suc)
--- a/src/HOL/Real/RealVector.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Real/RealVector.thy Tue Oct 16 23:12:45 2007 +0200
@@ -44,32 +44,28 @@
subsection {* Real vector spaces *}
class scaleR = type +
- fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<^loc>*#" 75)
+ fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
begin
abbreviation
- divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "\<^loc>'/#" 70)
+ divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "'/\<^sub>R" 70)
where
- "x \<^loc>/# r == scaleR (inverse r) x"
+ "x /\<^sub>R r == scaleR (inverse r) x"
end
-notation (xsymbols)
- scaleR (infixr "*\<^sub>R" 75) and
- divideR (infixl "'/\<^sub>R" 70)
-
instance real :: scaleR
real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" ..
class real_vector = scaleR + ab_group_add +
- assumes scaleR_right_distrib: "scaleR a (x \<^loc>+ y) = scaleR a x \<^loc>+ scaleR a y"
- and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x \<^loc>+ scaleR b x"
+ assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
+ and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
and scaleR_one [simp]: "scaleR 1 x = x"
class real_algebra = real_vector + ring +
- assumes mult_scaleR_left [simp]: "scaleR a x \<^loc>* y = scaleR a (x \<^loc>* y)"
- and mult_scaleR_right [simp]: "x \<^loc>* scaleR a y = scaleR a (x \<^loc>* y)"
+ assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
+ and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
class real_algebra_1 = real_algebra + ring_1
@@ -379,22 +375,22 @@
real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
class sgn_div_norm = scaleR + norm + sgn +
- assumes sgn_div_norm: "sgn x = x \<^loc>/# norm x"
+ assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
class real_normed_vector = real_vector + sgn_div_norm +
assumes norm_ge_zero [simp]: "0 \<le> norm x"
- and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = \<^loc>0"
- and norm_triangle_ineq: "norm (x \<^loc>+ y) \<le> norm x + norm y"
+ and 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: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
class real_normed_algebra = real_algebra + real_normed_vector +
- assumes norm_mult_ineq: "norm (x \<^loc>* y) \<le> norm x * norm y"
+ assumes norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
- assumes norm_one [simp]: "norm \<^loc>1 = 1"
+ assumes norm_one [simp]: "norm 1 = 1"
class real_normed_div_algebra = real_div_algebra + real_normed_vector +
- assumes norm_mult: "norm (x \<^loc>* y) = norm x * norm y"
+ assumes norm_mult: "norm (x * y) = norm x * norm y"
class real_normed_field = real_field + real_normed_div_algebra
--- a/src/HOL/Ring_and_Field.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy Tue Oct 16 23:12:45 2007 +0200
@@ -24,12 +24,12 @@
*}
class semiring = ab_semigroup_add + semigroup_mult +
- assumes left_distrib: "(a \<^loc>+ b) \<^loc>* c = a \<^loc>* c \<^loc>+ b \<^loc>* c"
- assumes right_distrib: "a \<^loc>* (b \<^loc>+ c) = a \<^loc>* b \<^loc>+ a \<^loc>* c"
+ assumes left_distrib: "(a + b) * c = a * c + b * c"
+ assumes right_distrib: "a * (b + c) = a * b + a * c"
class mult_zero = times + zero +
- assumes mult_zero_left [simp]: "\<^loc>0 \<^loc>* a = \<^loc>0"
- assumes mult_zero_right [simp]: "a \<^loc>* \<^loc>0 = \<^loc>0"
+ assumes mult_zero_left [simp]: "0 * a = 0"
+ assumes mult_zero_right [simp]: "a * 0 = 0"
class semiring_0 = semiring + comm_monoid_add + mult_zero
@@ -50,7 +50,7 @@
qed
class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
- assumes distrib: "(a \<^loc>+ b) \<^loc>* c = a \<^loc>* c \<^loc>+ b \<^loc>* c"
+ assumes distrib: "(a + b) * c = a * c + b * c"
instance comm_semiring \<subseteq> semiring
proof
@@ -73,7 +73,7 @@
instance comm_semiring_0_cancel \<subseteq> comm_semiring_0 ..
class zero_neq_one = zero + one +
- assumes zero_neq_one [simp]: "\<^loc>0 \<noteq> \<^loc>1"
+ assumes zero_neq_one [simp]: "0 \<noteq> 1"
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
@@ -83,7 +83,7 @@
instance comm_semiring_1 \<subseteq> semiring_1 ..
class no_zero_divisors = zero + times +
- assumes no_zero_divisors: "a \<noteq> \<^loc>0 \<Longrightarrow> b \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* b \<noteq> \<^loc>0"
+ assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
+ cancel_ab_semigroup_add + monoid_mult
@@ -131,8 +131,8 @@
instance idom \<subseteq> ring_1_no_zero_divisors ..
class division_ring = ring_1 + inverse +
- assumes left_inverse [simp]: "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
- assumes right_inverse [simp]: "a \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* inverse a = \<^loc>1"
+ assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
+ assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
instance division_ring \<subseteq> ring_1_no_zero_divisors
proof
@@ -153,8 +153,8 @@
qed
class field = comm_ring_1 + inverse +
- assumes field_inverse: "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
- assumes divide_inverse: "a \<^loc>/ b = a \<^loc>* inverse b"
+ assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
+ assumes divide_inverse: "a / b = a * inverse b"
instance field \<subseteq> division_ring
proof
@@ -167,7 +167,7 @@
instance field \<subseteq> idom ..
class division_by_zero = zero + inverse +
- assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0"
+ assumes inverse_zero [simp]: "inverse 0 = 0"
subsection {* Distribution rules *}
@@ -211,8 +211,8 @@
lemmas ring_simps = group_simps ring_distribs
class mult_mono = times + zero + ord +
- assumes mult_left_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"
- assumes mult_right_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> a \<^loc>* c \<^loc>\<le> b \<^loc>* c"
+ assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
+ assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add
@@ -228,8 +228,8 @@
instance ordered_semiring \<subseteq> pordered_cancel_semiring ..
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
- assumes mult_strict_left_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"
- assumes mult_strict_right_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> a \<^loc>* c \<^loc>< b \<^loc>* c"
+ assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
+ assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
@@ -246,7 +246,7 @@
qed
class mult_mono1 = times + zero + ord +
- assumes mult_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"
+ assumes mult_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
class pordered_comm_semiring = comm_semiring_0
+ pordered_ab_semigroup_add + mult_mono1
@@ -257,7 +257,7 @@
instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
- assumes mult_strict_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"
+ assumes mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
instance pordered_comm_semiring \<subseteq> pordered_semiring
proof
@@ -297,10 +297,10 @@
instance lordered_ring \<subseteq> lordered_ab_group_join ..
class abs_if = minus + ord + zero + abs +
- assumes abs_if: "abs a = (if a \<^loc>< \<^loc>0 then (uminus a) else a)"
+ assumes abs_if: "abs a = (if a < 0 then (uminus a) else a)"
class sgn_if = sgn + zero + one + minus + ord +
- assumes sgn_if: "sgn x = (if x = \<^loc>0 then \<^loc>0 else if \<^loc>0 \<^loc>< x then \<^loc>1 else uminus \<^loc>1)"
+ assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else uminus 1)"
(* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
@@ -327,7 +327,7 @@
class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
(*previously ordered_semiring*)
- assumes zero_less_one [simp]: "\<^loc>0 \<^loc>< \<^loc>1"
+ assumes zero_less_one [simp]: "0 < 1"
lemma pos_add_strict:
fixes a b c :: "'a\<Colon>ordered_semidom"
--- a/src/HOL/SetInterval.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/SetInterval.thy Tue Oct 16 23:12:45 2007 +0200
@@ -16,36 +16,36 @@
context ord
begin
definition
- lessThan :: "'a => 'a set" ("(1\<^loc>{..<_})") where
- "\<^loc>{..<u} == {x. x \<^loc>< u}"
+ lessThan :: "'a => 'a set" ("(1{..<_})") where
+ "{..<u} == {x. x < u}"
definition
- atMost :: "'a => 'a set" ("(1\<^loc>{.._})") where
- "\<^loc>{..u} == {x. x \<^loc>\<le> u}"
+ atMost :: "'a => 'a set" ("(1{.._})") where
+ "{..u} == {x. x \<le> u}"
definition
- greaterThan :: "'a => 'a set" ("(1\<^loc>{_<..})") where
- "\<^loc>{l<..} == {x. l\<^loc><x}"
+ greaterThan :: "'a => 'a set" ("(1{_<..})") where
+ "{l<..} == {x. l<x}"
definition
- atLeast :: "'a => 'a set" ("(1\<^loc>{_..})") where
- "\<^loc>{l..} == {x. l\<^loc>\<le>x}"
+ atLeast :: "'a => 'a set" ("(1{_..})") where
+ "{l..} == {x. l\<le>x}"
definition
- greaterThanLessThan :: "'a => 'a => 'a set" ("(1\<^loc>{_<..<_})") where
- "\<^loc>{l<..<u} == \<^loc>{l<..} Int \<^loc>{..<u}"
+ greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where
+ "{l<..<u} == {l<..} Int {..<u}"
definition
- atLeastLessThan :: "'a => 'a => 'a set" ("(1\<^loc>{_..<_})") where
- "\<^loc>{l..<u} == \<^loc>{l..} Int \<^loc>{..<u}"
+ atLeastLessThan :: "'a => 'a => 'a set" ("(1{_..<_})") where
+ "{l..<u} == {l..} Int {..<u}"
definition
- greaterThanAtMost :: "'a => 'a => 'a set" ("(1\<^loc>{_<.._})") where
- "\<^loc>{l<..u} == \<^loc>{l<..} Int \<^loc>{..u}"
+ greaterThanAtMost :: "'a => 'a => 'a set" ("(1{_<.._})") where
+ "{l<..u} == {l<..} Int {..u}"
definition
- atLeastAtMost :: "'a => 'a => 'a set" ("(1\<^loc>{_.._})") where
- "\<^loc>{l..u} == \<^loc>{l..} Int \<^loc>{..u}"
+ atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where
+ "{l..u} == {l..} Int {..u}"
end
(*
@@ -106,7 +106,7 @@
subsection {* Various equivalences *}
-lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i\<^loc><k)"
+lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
by (simp add: lessThan_def)
lemma Compl_lessThan [simp]:
@@ -117,7 +117,7 @@
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
by auto
-lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k\<^loc><i)"
+lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
by (simp add: greaterThan_def)
lemma Compl_greaterThan [simp]:
@@ -130,7 +130,7 @@
apply (rule double_complement)
done
-lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k\<^loc><=i)"
+lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
by (simp add: atLeast_def)
lemma Compl_atLeast [simp]:
@@ -138,7 +138,7 @@
apply (simp add: lessThan_def atLeast_def le_def, auto)
done
-lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i\<^loc><=k)"
+lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)"
by (simp add: atMost_def)
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
@@ -194,19 +194,19 @@
begin
lemma greaterThanLessThan_iff [simp,noatp]:
- "(i : \<^loc>{l<..<u}) = (l \<^loc>< i & i \<^loc>< u)"
+ "(i : {l<..<u}) = (l < i & i < u)"
by (simp add: greaterThanLessThan_def)
lemma atLeastLessThan_iff [simp,noatp]:
- "(i : \<^loc>{l..<u}) = (l \<^loc><= i & i \<^loc>< u)"
+ "(i : {l..<u}) = (l <= i & i < u)"
by (simp add: atLeastLessThan_def)
lemma greaterThanAtMost_iff [simp,noatp]:
- "(i : \<^loc>{l<..u}) = (l \<^loc>< i & i \<^loc><= u)"
+ "(i : {l<..u}) = (l < i & i <= u)"
by (simp add: greaterThanAtMost_def)
lemma atLeastAtMost_iff [simp,noatp]:
- "(i : \<^loc>{l..u}) = (l \<^loc><= i & i \<^loc><= u)"
+ "(i : {l..u}) = (l <= i & i <= u)"
by (simp add: atLeastAtMost_def)
text {* The above four lemmas could be declared as iffs.
@@ -219,19 +219,19 @@
context order
begin
-lemma atLeastAtMost_empty [simp]: "n \<^loc>< m ==> \<^loc>{m..n} = {}";
+lemma atLeastAtMost_empty [simp]: "n < m ==> {m..n} = {}";
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
-lemma atLeastLessThan_empty[simp]: "n \<^loc>\<le> m ==> \<^loc>{m..<n} = {}"
+lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n} = {}"
by (auto simp add: atLeastLessThan_def)
-lemma greaterThanAtMost_empty[simp]:"l \<^loc>\<le> k ==> \<^loc>{k<..l} = {}"
+lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..l} = {}"
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
-lemma greaterThanLessThan_empty[simp]:"l \<^loc>\<le> k ==> \<^loc>{k<..l} = {}"
+lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..l} = {}"
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
-lemma atLeastAtMost_singleton [simp]: "\<^loc>{a..a} = {a}"
+lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
end
--- a/src/HOL/Wellfounded_Relations.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Wellfounded_Relations.thy Tue Oct 16 23:12:45 2007 +0200
@@ -113,15 +113,15 @@
lemma (in linorder)
finite_linorder_induct[consumes 1, case_names empty insert]:
"finite A \<Longrightarrow> P {} \<Longrightarrow>
- (!!A b. finite A \<Longrightarrow> ALL a:A. a \<^loc>< b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
+ (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
\<Longrightarrow> P A"
proof (induct A rule: measure_induct[where f=card])
fix A :: "'a set"
assume IH: "ALL B. card B < card A \<longrightarrow> finite B \<longrightarrow> P {} \<longrightarrow>
- (\<forall>A b. finite A \<longrightarrow> (\<forall>a\<in>A. a\<^loc><b) \<longrightarrow> P A \<longrightarrow> P (insert b A))
+ (\<forall>A b. finite A \<longrightarrow> (\<forall>a\<in>A. a<b) \<longrightarrow> P A \<longrightarrow> P (insert b A))
\<longrightarrow> P B"
and "finite A" and "P {}"
- and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a \<^loc>< b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
+ and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
show "P A"
proof cases
assume "A = {}" thus "P A" using `P {}` by simp
@@ -133,7 +133,7 @@
note card_Diff1_less[OF `finite A` `Max A : A`]
moreover have "finite ?B" using `finite A` by simp
ultimately have "P ?B" using `P {}` step IH by blast
- moreover have "\<forall>a\<in>?B. a \<^loc>< Max A"
+ moreover have "\<forall>a\<in>?B. a < Max A"
using Max_ge[OF `finite A` `A \<noteq> {}`] by fastsimp
ultimately show "P A"
using A insert_Diff_single step[OF `finite ?B`] by fastsimp
--- a/src/HOL/ex/Classpackage.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy Tue Oct 16 23:12:45 2007 +0200
@@ -9,8 +9,8 @@
begin
class semigroup = type +
- fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70)
- assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
+ fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
+ assumes assoc: "x \<otimes> y \<otimes> z = x \<otimes> (y \<otimes> z)"
instance nat :: semigroup
"m \<otimes> n \<equiv> m + n"
@@ -43,8 +43,8 @@
qed
class monoidl = semigroup +
- fixes one :: 'a ("\<^loc>\<one>")
- assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
+ fixes one :: 'a ("\<one>")
+ assumes neutl: "\<one> \<otimes> x = x"
instance nat :: monoidl and int :: monoidl
"\<one> \<equiv> 0"
@@ -74,66 +74,66 @@
qed
class monoid = monoidl +
- assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
+ assumes neutr: "x \<otimes> \<one> = x"
begin
definition
units :: "'a set" where
- "units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}"
+ "units = {y. \<exists>x. x \<otimes> y = \<one> \<and> y \<otimes> x = \<one>}"
lemma inv_obtain:
assumes "x \<in> units"
- obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
+ obtains y where "y \<otimes> x = \<one>" and "x \<otimes> y = \<one>"
proof -
from assms units_def obtain y
- where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto
+ where "y \<otimes> x = \<one>" and "x \<otimes> y = \<one>" by auto
thus ?thesis ..
qed
lemma inv_unique:
- assumes "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
+ assumes "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>"
shows "y = y'"
proof -
- from assms neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
- also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp
+ from assms neutr have "y = y \<otimes> (x \<otimes> y')" by simp
+ also with assoc have "... = (y \<otimes> x) \<otimes> y'" by simp
also with assms neutl have "... = y'" by simp
finally show ?thesis .
qed
lemma units_inv_comm:
- assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>"
+ assumes inv: "x \<otimes> y = \<one>"
and G: "x \<in> units"
- shows "y \<^loc>\<otimes> x = \<^loc>\<one>"
+ shows "y \<otimes> x = \<one>"
proof -
from G inv_obtain obtain z
- where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast
- from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp
- with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp
+ where z_choice: "z \<otimes> x = \<one>" by blast
+ from inv neutl neutr have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by simp
+ with assoc have "z \<otimes> x \<otimes> y \<otimes> x = z \<otimes> x \<otimes> \<one>" by simp
with neutl z_choice show ?thesis by simp
qed
fun
npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
where
- "npow 0 x = \<^loc>\<one>"
- | "npow (Suc n) x = x \<^loc>\<otimes> npow n x"
+ "npow 0 x = \<one>"
+ | "npow (Suc n) x = x \<otimes> npow n x"
abbreviation
- npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
- "x \<^loc>\<up> n \<equiv> npow n x"
+ npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<up>" 75) where
+ "x \<up> n \<equiv> npow n x"
lemma nat_pow_one:
- "\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>"
+ "\<one> \<up> n = \<one>"
using neutl by (induct n) simp_all
-lemma nat_pow_mult: "x \<^loc>\<up> n \<^loc>\<otimes> x \<^loc>\<up> m = x \<^loc>\<up> (n + m)"
+lemma nat_pow_mult: "x \<up> n \<otimes> x \<up> m = x \<up> (n + m)"
proof (induct n)
case 0 with neutl show ?case by simp
next
case (Suc n) with Suc.hyps assoc show ?case by simp
qed
-lemma nat_pow_pow: "(x \<^loc>\<up> m) \<^loc>\<up> n = x \<^loc>\<up> (n * m)"
+lemma nat_pow_pow: "(x \<up> m) \<up> n = x \<up> (n * m)"
using nat_pow_mult by (induct n) simp_all
end
@@ -153,7 +153,7 @@
qed
class monoid_comm = monoid +
- assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x"
+ assumes comm: "x \<otimes> y = y \<otimes> x"
instance nat :: monoid_comm and int :: monoid_comm
proof
@@ -174,30 +174,30 @@
by default (simp_all add: split_paired_all mult_prod_def comm)
class group = monoidl +
- fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80)
- assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>"
+ fixes inv :: "'a \<Rightarrow> 'a" ("\<div> _" [81] 80)
+ assumes invl: "\<div> x \<otimes> x = \<one>"
begin
lemma cancel:
- "(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)"
+ "(x \<otimes> y = x \<otimes> z) = (y = z)"
proof
fix x y z :: 'a
- assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
- hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
- with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp
+ assume eq: "x \<otimes> y = x \<otimes> z"
+ hence "\<div> x \<otimes> (x \<otimes> y) = \<div> x \<otimes> (x \<otimes> z)" by simp
+ with assoc have "\<div> x \<otimes> x \<otimes> y = \<div> x \<otimes> x \<otimes> z" by simp
with neutl invl show "y = z" by simp
next
fix x y z :: 'a
assume eq: "y = z"
- thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
+ thus "x \<otimes> y = x \<otimes> z" by simp
qed
subclass monoid
proof unfold_locales
fix x
- from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp
- with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp
- with cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
+ from invl have "\<div> x \<otimes> x = \<one>" by simp
+ with assoc [symmetric] neutl invl have "\<div> x \<otimes> (x \<otimes> \<one>) = \<div> x \<otimes> x" by simp
+ with cancel show "x \<otimes> \<one> = x" by simp
qed
end context group begin
@@ -205,11 +205,11 @@
find_theorems name: neut
lemma invr:
- "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>"
+ "x \<otimes> \<div> x = \<one>"
proof -
- from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp
- with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
- with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
+ from neutl invl have "\<div> x \<otimes> x \<otimes> \<div> x = \<div> x" by simp
+ with neutr have "\<div> x \<otimes> x \<otimes> \<div> x = \<div> x \<otimes> \<one> " by simp
+ with assoc have "\<div> x \<otimes> (x \<otimes> \<div> x) = \<div> x \<otimes> \<one> " by simp
with cancel show ?thesis ..
qed
@@ -218,72 +218,72 @@
unfolding units_def
proof -
fix x :: "'a"
- from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" .
- then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" ..
- hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast
- thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}" by simp
+ from invl invr have "\<div> x \<otimes> x = \<one>" and "x \<otimes> \<div> x = \<one>" .
+ then obtain y where "y \<otimes> x = \<one>" and "x \<otimes> y = \<one>" ..
+ hence "\<exists>y\<Colon>'a. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by blast
+ thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<otimes> y = \<one> \<and> y \<otimes> x = \<one>}" by simp
qed
lemma cancer:
- "(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)"
+ "(y \<otimes> x = z \<otimes> x) = (y = z)"
proof
- assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x"
- with assoc [symmetric] have "y \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = z \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x)" by (simp del: invr)
+ assume eq: "y \<otimes> x = z \<otimes> x"
+ with assoc [symmetric] have "y \<otimes> (x \<otimes> \<div> x) = z \<otimes> (x \<otimes> \<div> x)" by (simp del: invr)
with invr neutr show "y = z" by simp
next
assume eq: "y = z"
- thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp
+ thus "y \<otimes> x = z \<otimes> x" by simp
qed
lemma inv_one:
- "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>"
+ "\<div> \<one> = \<one>"
proof -
- from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" ..
- moreover from invr have "... = \<^loc>\<one>" by simp
+ from neutl have "\<div> \<one> = \<one> \<otimes> (\<div> \<one>)" ..
+ moreover from invr have "... = \<one>" by simp
finally show ?thesis .
qed
lemma inv_inv:
- "\<^loc>\<div> (\<^loc>\<div> x) = x"
+ "\<div> (\<div> x) = x"
proof -
from invl invr neutr
- have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x" by simp
+ have "\<div> (\<div> x) \<otimes> \<div> x \<otimes> x = x \<otimes> \<div> x \<otimes> x" by simp
with assoc [symmetric]
- have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x) = x \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x)" by simp
+ have "\<div> (\<div> x) \<otimes> (\<div> x \<otimes> x) = x \<otimes> (\<div> x \<otimes> x)" by simp
with invl neutr show ?thesis by simp
qed
lemma inv_mult_group:
- "\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x"
+ "\<div> (x \<otimes> y) = \<div> y \<otimes> \<div> x"
proof -
- from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp
- with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp
- with neutl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
- with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> (y \<^loc>\<otimes> \<^loc>\<div> y) \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
+ from invl have "\<div> (x \<otimes> y) \<otimes> (x \<otimes> y) = \<one>" by simp
+ with assoc have "\<div> (x \<otimes> y) \<otimes> x \<otimes> y = \<one>" by simp
+ with neutl have "\<div> (x \<otimes> y) \<otimes> x \<otimes> y \<otimes> \<div> y \<otimes> \<div> x = \<div> y \<otimes> \<div> x" by simp
+ with assoc have "\<div> (x \<otimes> y) \<otimes> (x \<otimes> (y \<otimes> \<div> y) \<otimes> \<div> x) = \<div> y \<otimes> \<div> x" by simp
with invr neutr show ?thesis by simp
qed
lemma inv_comm:
- "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x"
+ "x \<otimes> \<div> x = \<div> x \<otimes> x"
using invr invl by simp
definition
pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a"
where
- "pow k x = (if k < 0 then \<^loc>\<div> (npow (nat (-k)) x)
+ "pow k x = (if k < 0 then \<div> (npow (nat (-k)) x)
else (npow (nat k) x))"
abbreviation
- pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>\<up>" 75)
+ pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<up>\<up>" 75)
where
- "x \<^loc>\<up>\<up> k \<equiv> pow k x"
+ "x \<up>\<up> k \<equiv> pow k x"
lemma int_pow_zero:
- "x \<^loc>\<up>\<up> (0\<Colon>int) = \<^loc>\<one>"
+ "x \<up>\<up> (0\<Colon>int) = \<one>"
using pow_def by simp
lemma int_pow_one:
- "\<^loc>\<one> \<^loc>\<up>\<up> (k\<Colon>int) = \<^loc>\<one>"
+ "\<one> \<up>\<up> (k\<Colon>int) = \<one>"
using pow_def nat_pow_one inv_one by simp
end
--- a/src/Pure/Isar/class.ML Tue Oct 16 23:12:38 2007 +0200
+++ b/src/Pure/Isar/class.ML Tue Oct 16 23:12:45 2007 +0200
@@ -7,7 +7,7 @@
signature CLASS =
sig
- val fork_mixfix: bool -> bool -> mixfix -> mixfix * mixfix
+ val fork_mixfix: bool -> bool -> mixfix -> (mixfix * mixfix) * mixfix
val axclass_cmd: bstring * xstring list
-> ((bstring * Attrib.src list) * string list) list
@@ -19,9 +19,9 @@
val class_cmd: bstring -> xstring list -> Element.context Locale.element list
-> xstring list -> theory -> string * Proof.context
val init: class -> Proof.context -> Proof.context
- val add_const_in_class: string -> (string * mixfix) * (string * term)
+ val add_const_in_class: string -> (string * mixfix) * term
-> theory -> string * theory
- val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * (string * term)
+ val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * term
-> theory -> string * theory
val remove_constraint: class -> string -> Proof.context -> Proof.context
val is_class: theory -> class -> bool
@@ -54,13 +54,15 @@
(** auxiliary **)
-fun fork_mixfix is_locale is_class mx =
- let
- val mx' = Syntax.unlocalize_mixfix mx;
- val mx_global = if not is_locale orelse (is_class andalso not (mx = mx'))
- then mx' else NoSyn;
- val mx_local = if is_locale then mx else NoSyn;
- in (mx_global, mx_local) end;
+val classN = "class";
+val introN = "intro";
+
+fun fork_mixfix false _ mx = ((NoSyn, NoSyn), mx)
+ | fork_mixfix true false mx = ((NoSyn, mx), NoSyn)
+ | fork_mixfix true true mx = ((mx, NoSyn), NoSyn);
+ (*let
+ val mx' = Syntax.unlocalize_mixfix mx;
+ in if mx' = mx then ((NoSyn, mx), NoSyn) else ((mx', mx), NoSyn) end;*)
fun prove_interpretation tac prfx_atts expr inst =
Locale.interpretation_i I prfx_atts expr inst
@@ -315,36 +317,36 @@
datatype class_data = ClassData of {
consts: (string * string) list
(*locale parameter ~> constant name*),
- local_sort: sort,
+ base_sort: sort,
inst: (typ option list * term option list) * term Symtab.table
(*canonical interpretation FIXME*),
+ morphism: morphism,
+ (*partial morphism of canonical interpretation*)
intro: thm,
defs: thm list,
- operations: (string * (term * (typ * int))) list
- (*constant name ~> (locale term, (constant constraint, instantiaton index of class typ))*),
- operations_rev: (string * string) list
- (*locale operation ~> constant name*)
+ operations: (string * ((term * typ) * (typ * int))) list
+ (*constant name ~> (locale term & typ,
+ (constant constraint, instantiaton index of class typ))*)
};
fun rep_class_data (ClassData d) = d;
-fun mk_class_data ((consts, local_sort, inst, intro),
- (defs, operations, operations_rev)) =
- ClassData { consts = consts, local_sort = local_sort, inst = inst,
- intro = intro, defs = defs, operations = operations,
- operations_rev = operations_rev };
-fun map_class_data f (ClassData { consts, local_sort, inst, intro,
- defs, operations, operations_rev }) =
- mk_class_data (f ((consts, local_sort, inst, intro),
- (defs, operations, operations_rev)));
+fun mk_class_data ((consts, base_sort, inst, morphism, intro),
+ (defs, operations)) =
+ ClassData { consts = consts, base_sort = base_sort, inst = inst,
+ morphism = morphism, intro = intro, defs = defs,
+ operations = operations };
+fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro,
+ defs, operations }) =
+ mk_class_data (f ((consts, base_sort, inst, morphism, intro),
+ (defs, operations)));
fun merge_class_data _ (ClassData { consts = consts,
- local_sort = local_sort, inst = inst, intro = intro,
- defs = defs1, operations = operations1, operations_rev = operations_rev1 },
- ClassData { consts = _, local_sort = _, inst = _, intro = _,
- defs = defs2, operations = operations2, operations_rev = operations_rev2 }) =
- mk_class_data ((consts, local_sort, inst, intro),
+ base_sort = base_sort, inst = inst, morphism = morphism, intro = intro,
+ defs = defs1, operations = operations1 },
+ ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _,
+ defs = defs2, operations = operations2 }) =
+ mk_class_data ((consts, base_sort, inst, morphism, intro),
(Thm.merge_thms (defs1, defs2),
- AList.merge (op =) (K true) (operations1, operations2),
- AList.merge (op =) (K true) (operations_rev1, operations_rev2)));
+ AList.merge (op =) (K true) (operations1, operations2)));
structure ClassData = TheoryDataFun
(
@@ -381,6 +383,8 @@
fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
+fun morphism thy = #morphism o the_class_data thy;
+
fun these_intros thy =
Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
(ClassData.get thy) [];
@@ -388,26 +392,21 @@
fun these_operations thy =
maps (#operations o the_class_data thy) o ancestry thy;
-fun these_operations_rev thy =
- maps (#operations_rev o the_class_data thy) o ancestry thy;
-
fun local_operation thy = AList.lookup (op =) o these_operations thy;
-fun global_operation thy = AList.lookup (op =) o these_operations_rev thy;
-
-fun sups_local_sort thy sort =
+fun sups_base_sort thy sort =
let
- val sups = filter (is_some o lookup_class_data thy) sort
+ val sups = filter (is_class thy) sort
|> Sign.minimize_sort thy;
- val local_sort = case sups
- of sup :: _ => #local_sort (the_class_data thy sup)
+ val base_sort = case sups
+ of _ :: _ => maps (#base_sort o the_class_data thy) sups
+ |> Sign.minimize_sort thy
| [] => sort;
- in (sups, local_sort) end;
+ in (sups, base_sort) end;
fun print_classes thy =
let
val ctxt = ProofContext.init thy;
-
val algebra = Sign.classes_of thy;
val arities =
Symtab.empty
@@ -422,11 +421,13 @@
fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
- (SOME o Pretty.str) ("class " ^ class ^ ":"),
+ (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
(SOME o Pretty.block) [Pretty.str "supersort: ",
(Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
- if is_class thy class then (SOME o Pretty.str) ("locale: " ^ class) else NONE,
- ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
+ if is_class thy class then (SOME o Pretty.str)
+ ("locale: " ^ Locale.extern thy class) else NONE,
+ ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
+ (Pretty.str "parameters:" :: ps)) o map mk_param
o these o Option.map #params o try (AxClass.get_info thy)) class,
(SOME o Pretty.block o Pretty.breaks) [
Pretty.str "instances:",
@@ -441,7 +442,7 @@
(* updaters *)
-fun add_class_data ((class, superclasses), (cs, local_sort, inst, intro)) thy =
+fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
let
(*FIXME*)
val is_empty = null (fold (fn ((_, ty), _) => fold_atyps cons ty) cs [])
@@ -453,26 +454,50 @@
(Locale.parameters_of_expr thy (Locale.Locale class));
val instT = if is_empty then [] else [SOME (TFree (Name.aT, [class]))];
val inst' = ((instT, inst_params), inst);
- val operations = map (fn (v_ty, (c, ty)) => (c, (Free v_ty, (ty, 0)))) cs;
+ val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
+ (c, ((Free v_ty, ty'), (Logic.varifyT ty, 0)))) cs;
val cs = (map o pairself) fst cs;
val add_class = Graph.new_node (class,
- mk_class_data ((cs, local_sort, inst', intro), ([], operations, [])))
+ mk_class_data ((cs, base_sort, inst', phi, intro), ([], operations)))
#> fold (curry Graph.add_edge class) superclasses;
in
ClassData.map add_class thy
end;
-fun register_operation class (entry, some_def) =
- (ClassData.map o Graph.map_node class o map_class_data o apsnd)
- (fn (defs, operations, operations_rev) =>
- (case some_def of NONE => defs | SOME def => def :: defs,
- entry :: operations, (*FIXME*)operations_rev));
+fun register_operation class ((c, rhs), some_def) thy =
+ let
+ val ty = Sign.the_const_constraint thy c;
+ val typargs = Sign.const_typargs thy (c, ty);
+ val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs;
+ val ty' = Term.fastype_of rhs;
+ in
+ thy
+ |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
+ (fn (defs, operations) =>
+ (case some_def of NONE => defs | SOME def => def :: defs,
+ (c, ((rhs, ty'), (ty, typidx))) :: operations))
+ end;
(** rule calculation, tactics and methods **)
val class_prefix = Logic.const_of_class o Sign.base_name;
+fun calculate_morphism class cs =
+ let
+ val subst_typ = Term.map_type_tfree (fn var as (v, sort) =>
+ if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort));
+ fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
+ of SOME (c, _) => Const (c, ty)
+ | NONE => t)
+ | subst_aterm t = t;
+ val subst_term = map_aterms subst_aterm #> map_types subst_typ;
+ in
+ Morphism.identity
+ $> Morphism.term_morphism subst_term
+ $> Morphism.typ_morphism subst_typ
+ end;
+
fun class_intro thy class sups =
let
fun class_elim class =
@@ -506,8 +531,6 @@
let
val params = these_params thy [class];
val { inst = ((_, inst), _), ... } = the_class_data thy class;
- (*val _ = tracing ("interpreting with " ^ cat_lines (map (setmp show_sorts true makestring)
- (map_filter I inst)));*)
val tac = ALLGOALS (ProofContext.fact_tac facts);
val prfx = class_prefix class;
in
@@ -548,82 +571,86 @@
(* class context syntax *)
-fun internal_remove_constraint local_sort (c, (_, (ty, typidx))) ctxt =
+fun internal_remove_constraint base_sort (c, (_, (ty, _))) ctxt =
let
- val consts = ProofContext.consts_of ctxt;
- val typargs = Consts.typargs consts (c, ty);
- val typargs' = nth_map typidx (K (TVar ((Name.aT, 0), local_sort))) typargs;
- val ty' = Consts.instance consts (c, typargs');
- in ProofContext.add_const_constraint (c, SOME ty') ctxt end;
+ val ty' = ty
+ |> map_atyps (fn ty as TVar ((v, 0), _) =>
+ if v = Name.aT then TVar ((v, 0), base_sort) else ty)
+ |> SOME;
+ in ProofContext.add_const_constraint (c, ty') ctxt end;
fun remove_constraint class c ctxt =
let
val thy = ProofContext.theory_of ctxt;
+ val base_sort = (#base_sort o the_class_data thy) class;
val SOME entry = local_operation thy [class] c;
in
- internal_remove_constraint
- ((#local_sort o the_class_data thy) class) (c, entry) ctxt
+ internal_remove_constraint base_sort (c, entry) ctxt
end;
-fun sort_term_check sups local_sort ts ctxt =
+fun sort_term_check sups base_sort ts ctxt =
let
val thy = ProofContext.theory_of ctxt;
- val local_operation = local_operation thy sups;
+ val local_operation = local_operation thy sups o fst;
+ val typargs = Consts.typargs (ProofContext.consts_of ctxt);
val constraints = these_operations thy sups |> (map o apsnd) (fst o snd);
- val consts = ProofContext.consts_of ctxt;
- fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx
- of TFree (v, _) => if v = Name.aT
- then apfst (AList.update (op =) ((c, ty), t')) else I
- | TVar (vi, _) => if TypeInfer.is_param vi
- then apfst (AList.update (op =) ((c, ty), t'))
+ fun check_typ (c, ty) (TFree (v, _)) t = if v = Name.aT
+ then apfst (AList.update (op =) ((c, ty), t)) else I
+ | check_typ (c, ty) (TVar (vi, _)) t = if TypeInfer.is_param vi
+ then apfst (AList.update (op =) ((c, ty), t))
#> apsnd (insert (op =) vi) else I
- | _ => I;
- fun add_const (Const (c, ty)) = (case local_operation c
- of SOME (t', (_, idx)) => check_typ (c, ty) (t', idx)
- | NONE => I)
+ | check_typ _ _ _ = I;
+ fun check_const (c, ty) ((t, _), (_, idx)) =
+ check_typ (c, ty) (nth (typargs (c, ty)) idx) t;
+ fun add_const (Const c_ty) = Option.map (check_const c_ty) (local_operation c_ty)
+ |> the_default I
| add_const _ = I;
val (cs, typarams) = (fold o fold_aterms) add_const ts ([], []);
- val ts' = map (map_aterms
+ val subst_typ = map_type_tvar (fn var as (vi, _) =>
+ if member (op =) typarams vi then TFree (Name.aT, base_sort) else TVar var);
+ val subst_term = map_aterms
(fn t as Const (c, ty) => the_default t (AList.lookup (op =) cs (c, ty)) | t => t)
- #> (map_types o map_type_tvar) (fn var as (vi, _) => if member (op =) typarams vi
- then TFree (Name.aT, local_sort) else TVar var)) ts;
+ #> map_types subst_typ;
+ val ts' = map subst_term ts;
val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt') end;
-val uncheck = ref false;
+val uncheck = ref true;
fun sort_term_uncheck sups ts ctxt =
let
+ (*FIXME abbreviations*)
val thy = ProofContext.theory_of ctxt;
- val global_param = AList.lookup (op =) (these_params thy sups) #> Option.map fst;
- val global_operation = global_operation thy sups;
- fun globalize (t as Free (v, ty)) = (case global_param v
- of SOME c => Const (c, ty)
- | NONE => t)
- | globalize (t as Const (c, ty)) = (case global_operation c
- of SOME c => Const (c, ty)
- | NONE => t)
- | globalize t = t;
- val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts;
+ fun rew_app f (t1 $ t2) = rew_app f t1 $ f t2
+ | rew_app f t = t;
+ val rews = map (fn (c, ((t, ty), _)) => (t, Const (c, ty))) (these_operations thy sups);
+ val rews' = (map o apfst o rew_app) (Pattern.rewrite_term thy rews []) rews;
+ val _ = map (Thm.cterm_of thy o Logic.mk_equals) rews';
+ val ts' = if ! uncheck
+ then map (Pattern.rewrite_term thy rews' []) ts else ts;
in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
-fun init_class_ctxt sups local_sort ctxt =
+fun init_class_ctxt sups base_sort ctxt =
let
val operations = these_operations (ProofContext.theory_of ctxt) sups;
+ fun standard_infer_types ts ctxt =
+ let
+ val ts' = ProofContext.standard_infer_types ctxt ts;
+ in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
in
ctxt
|> Variable.declare_term
- (Logic.mk_type (TFree (Name.aT, local_sort)))
- |> fold (internal_remove_constraint local_sort) operations
- |> Context.proof_map (Syntax.add_term_check 50 "class"
- (sort_term_check sups local_sort)
- #> Syntax.add_term_uncheck 50 "class"
- (sort_term_uncheck sups))
+ (Logic.mk_type (TFree (Name.aT, base_sort)))
+ |> fold (internal_remove_constraint base_sort) operations
+ |> Context.proof_map (Syntax.add_term_check 1 "class"
+ (sort_term_check sups base_sort)
+ #> Syntax.add_term_check 1 "standard" standard_infer_types
+ #> Syntax.add_term_uncheck (~10) "class" (sort_term_uncheck sups))
end;
fun init class ctxt =
init_class_ctxt [class]
- ((#local_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt;
+ ((#base_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt;
(* class definition *)
@@ -633,7 +660,7 @@
fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
let
val supclasses = map (prep_class thy) raw_supclasses;
- val (sups, local_sort) = sups_local_sort thy supclasses;
+ val (sups, base_sort) = sups_base_sort thy supclasses;
val supsort = Sign.minimize_sort thy supclasses;
val suplocales = map Locale.Locale sups;
val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
@@ -649,10 +676,10 @@
ProofContext.init thy
|> Locale.cert_expr supexpr [constrain]
|> snd
- |> init_class_ctxt sups local_sort
+ |> init_class_ctxt sups base_sort
|> process_expr Locale.empty raw_elems
|> fst
- |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)),
+ |> (fn elems => ((((sups, supconsts), (supsort, base_sort, mergeexpr)),
(*FIXME*) if null includes then constrain :: elems else elems)))
end;
@@ -688,26 +715,26 @@
raw_supclasses raw_includes_elems raw_other_consts thy =
let
val class = Sign.full_name thy bname;
- val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) =
+ val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) =
prep_spec thy raw_supclasses raw_includes_elems;
val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
fun mk_inst class param_names cs =
Symtab.empty
|> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
(c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
+ fun fork_syntax (Element.Fixes xs) =
+ fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
+ #>> Element.Fixes
+ | fork_syntax x = pair x;
+ val (elems, global_syn) = fold_map fork_syntax elems_syn [];
+ fun globalize (c, ty) =
+ ((c, Term.map_type_tfree (K (TFree (Name.aT, base_sort))) ty),
+ (the_default NoSyn o AList.lookup (op =) global_syn) c);
fun extract_params thy =
let
- val params = Locale.parameters_of thy class;
- val _ = if Sign.subsort thy (supsort, local_sort) then () else error
- ("Sort " ^ Sign.string_of_sort thy local_sort
- ^ " is less general than permitted least general sort "
- ^ Sign.string_of_sort thy supsort);
+ val params = map fst (Locale.parameters_of thy class);
in
- (map fst params, params
- |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (Name.aT, local_sort)))
- |> (map o apsnd) (fork_mixfix true true #> fst)
- |> chop (length supconsts)
- |> snd)
+ (params, (map globalize o snd o chop (length supconsts)) params)
end;
fun extract_assumes params thy cs =
let
@@ -722,28 +749,26 @@
Locale.global_asms_of thy class
|> map prep_asm
end;
- fun note_intro class_intro =
- PureThy.note_thmss_qualified "" (class_prefix class)
- [(("intro", []), [([class_intro], [])])]
- #> snd
in
thy
|> Locale.add_locale_i (SOME "") bname mergeexpr elems
|> snd
|> ProofContext.theory (`extract_params
- #-> (fn (globals, params) =>
+ #-> (fn (all_params, params) =>
define_class_params (bname, supsort) params
(extract_assumes params) other_consts
#-> (fn (_, (consts, axioms)) =>
`(fn thy => class_intro thy class sups)
#-> (fn class_intro =>
+ PureThy.note_thmss_qualified "" (NameSpace.append class classN)
+ [((introN, []), [([class_intro], [])])]
+ #-> (fn [(_, [class_intro])] =>
add_class_data ((class, sups),
- (map fst params ~~ consts, local_sort,
- mk_inst class (map fst globals) (map snd supconsts @ consts),
- class_intro))
- #> note_intro class_intro
+ (map fst params ~~ consts, base_sort,
+ mk_inst class (map fst all_params) (map snd supconsts @ consts),
+ calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
#> class_interpretation class axioms []
- ))))
+ )))))
|> pair class
end;
@@ -757,56 +782,29 @@
(* definition in class target *)
-fun export_fixes thy class =
+fun add_const_in_class class ((c, mx), rhs) thy =
let
- val cs = these_params thy [class];
- fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
- of SOME (c, _) => Const (c, ty)
- | NONE => t)
- | subst_aterm t = t;
- in Term.map_aterms subst_aterm end;
-
-fun mk_operation_entry thy (c, rhs) =
- let
- val ty = Logic.unvarifyT (Sign.the_const_constraint thy c);
- val typargs = Sign.const_typargs thy (c, ty);
- val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
- in (c, (rhs, (ty, typidx))) end;
-
-fun add_const_in_class class ((c, mx), (c_loc, rhs)) thy =
- let
- val _ = tracing c_loc;
val prfx = class_prefix class;
val thy' = thy |> Sign.add_path prfx;
+ val phi = morphism thy' class;
- val rhs' = export_fixes thy' class rhs;
- val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
- if w = Name.aT then TFree (w, [class]) else TFree var);
+ val c' = Sign.full_name thy' c;
+ val ((mx', _), _) = fork_mixfix true true mx;
+ val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs;
val ty' = Term.fastype_of rhs';
- val ty'' = subst_typ ty';
- val c' = Sign.full_name thy' c;
- val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
- val (mx', _) = fork_mixfix true true mx;
- fun interpret def thy =
- let
- val def' = symmetric def;
- val def_eq = (map_types Logic.unvarifyT o Thm.prop_of) def';
- in
- thy
- |> class_interpretation class [def'] [def_eq]
- |> Sign.add_const_constraint (c', SOME ty'')
- |> `(fn thy => mk_operation_entry thy (c', rhs))
- |-> (fn entry => register_operation class (entry, SOME def'))
- end;
+ val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
in
thy'
|> Sign.hide_consts_i false [c'']
|> Sign.declare_const [] (c, ty', mx') |> snd
|> Sign.parent_path
|> Sign.sticky_prefix prfx
- |> PureThy.add_defs_i false [(def, [])]
- |-> (fn [def] => interpret def)
+ |> yield_singleton (PureThy.add_defs_i false) (def, [])
+ |>> Thm.symmetric
+ |-> (fn def => class_interpretation class [def]
+ [(map_types Logic.unvarifyT o Thm.prop_of) def]
+ #> register_operation class ((c', rhs), SOME def))
|> Sign.restore_naming thy
|> pair c'
end;
@@ -814,20 +812,20 @@
(* abbreviation in class target *)
-fun add_abbrev_in_class class prmode ((c, mx), (c_loc, rhs)) thy =
+fun add_abbrev_in_class class prmode ((c, mx), rhs) thy =
let
- val _ = tracing c_loc;
val prfx = class_prefix class;
+ val phi = morphism thy class;
+
val naming = Sign.naming_of thy |> NameSpace.add_path prfx |> NameSpace.add_path prfx;
(*FIXME*)
val c' = NameSpace.full naming c;
- val rhs' = export_fixes thy class rhs;
+ val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs;
val ty' = Term.fastype_of rhs';
- val entry = mk_operation_entry thy (c', rhs);
in
thy
|> Sign.notation true prmode [(Const (c', ty'), mx)]
- |> register_operation class (entry, NONE)
+ |> register_operation class ((c', rhs), NONE)
|> pair c'
end;