# HG changeset patch
# User chaieb
# Date 1202140801 -3600
# Node ID 08d52e2dba07ad44046bf562de827688c66f0943
# Parent  a27710a07d10bc8d757ac9d32fa5a64e2f42b7ef
replaced class by locale

diff -r a27710a07d10 -r 08d52e2dba07 src/HOL/Dense_Linear_Order.thy
--- a/src/HOL/Dense_Linear_Order.thy	Mon Feb 04 12:13:08 2008 +0100
+++ b/src/HOL/Dense_Linear_Order.thy	Mon Feb 04 17:00:01 2008 +0100
@@ -303,23 +303,32 @@
 
 text {* Linear order without upper bounds *}
 
-class linorder_no_ub = linorder +
-  assumes gt_ex: "\<exists>y. x < y"
+locale linorder_stupid_syntax = linorder
 begin
+notation
+  less_eq  ("op \<sqsubseteq>") and
+  less_eq  ("(_/ \<sqsubseteq> _)" [51, 51] 50) and
+  less  ("op \<sqsubset>") and
+  less  ("(_/ \<sqsubset> _)"  [51, 51] 50)
 
-lemma ge_ex: "\<exists>y. x \<le> y" using gt_ex by auto
+end
 
-text {* Theorems for @{text "\<exists>z. \<forall>x. z < x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
+locale linorder_no_ub = linorder_stupid_syntax +
+  assumes gt_ex: "\<exists>y. less x y"
+begin
+lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
+
+text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
 lemma pinf_conj:
-  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'))"
+  assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
 proof-
-  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 ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+     and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast
+  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
+  {fix x assume H: "z \<sqsubset> 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
   }
@@ -327,25 +336,25 @@
 qed
 
 lemma pinf_disj:
-  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'))"
+  assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
 proof-
-  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 ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+     and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast
+  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
+  {fix x assume H: "z \<sqsubset> 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 < x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
+lemma pinf_ex: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
 proof-
-  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 ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
+  from gt_ex obtain x where x: "z \<sqsubset> x" by blast
   from z x p1 show ?thesis by blast
 qed
 
@@ -353,23 +362,22 @@
 
 text {* Linear order without upper bounds *}
 
-class linorder_no_lb = linorder +
-  assumes lt_ex: "\<exists>y. y < x"
+locale linorder_no_lb = linorder_stupid_syntax +
+  assumes lt_ex: "\<exists>y. less y x"
 begin
-
-lemma le_ex: "\<exists>y. y \<le> x" using lt_ex by auto
+lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
 
 
-text {* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
+text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
 lemma minf_conj:
-  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'))"
+  assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
 proof-
-  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 ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast
+  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
+  {fix x assume H: "x \<sqsubset> 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
   }
@@ -377,78 +385,81 @@
 qed
 
 lemma minf_disj:
-  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'))"
+  assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
 proof-
-  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 ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast
+  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
+  {fix x assume H: "x \<sqsubset> 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 < z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
+lemma minf_ex: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
 proof-
-  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 ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
+  from lt_ex obtain x where x: "x \<sqsubset> z" by blast
   from z x p1 show ?thesis by blast
 qed
 
 end
 
 
-class constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
+locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   fixes between
-  assumes between_less: "x < y \<Longrightarrow> x < between x y \<and> between x y < y"
+  assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
      and  between_same: "between x x = x"
-begin
 
-subclass dense_linear_order
+interpretation  constr_dense_linear_order < dense_linear_order 
   apply unfold_locales
   using gt_ex lt_ex between_less
     by (auto, rule_tac x="between x y" in exI, simp)
 
+context  constr_dense_linear_order
+begin
+
 lemma rinf_U:
   assumes fU: "finite 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 lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
+  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> 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 \<sqsubseteq> x \<and> x \<sqsubseteq> 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 \<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 px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" by auto
+  then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<sqsubseteq> x" and xu':"x \<sqsubseteq> u'" by auto
   from uU have Une: "U \<noteq> {}" by auto
-  let ?l = "Min U"
-  let ?u = "Max U"
+  term "linorder.Min less_eq"
+  let ?l = "linorder.Min less_eq U"
+  let ?u = "linorder.Max less_eq 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 \<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" .
+  have lM: "\<forall> t\<in> U. ?l \<sqsubseteq> t" using Une fU by auto
+  have Mu: "\<forall> t\<in> U. t \<sqsubseteq> ?u" using Une fU by auto
+  have th:"?l \<sqsubseteq> u" using uU Une lM by auto
+  from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" .
+  have th: "u' \<sqsubseteq> ?u" using uU' Une Mu by simp
+  from order_trans[OF xu' th] have xu: "x \<sqsubseteq> ?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 < y \<and> y < t2 \<longrightarrow> y \<notin> U) \<and> t1 < x \<and> x < t2 \<and> P x)" .
+      (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> 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 < y \<and> y < t2 \<longrightarrow> y \<notin> U) \<and> t1 < x \<and> x < t2 \<and> P x"
+    assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x"
       then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U"
-        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"
+        and noM: "\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U" and t1x: "t1 \<sqsubset> x" and xt2: "x \<sqsubset> t2" and px: "P x"
         by blast
-      from less_trans[OF t1x xt2] have t1t2: "t1 < t2" .
+      from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" .
       let ?u = "between t1 t2"
-      from between_less t1t2 have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto
+      from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto
       from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast
       with t1M t2M have ?thesis by blast}
     ultimately show ?thesis by blast
@@ -456,11 +467,11 @@
 
 theorem fr_eq:
   assumes fU: "finite 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 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)"
+  and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
+   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
+  and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)"
+  and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)"
+  and mi: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x = MP)"  and pi: "\<exists>z. \<forall>x. z \<sqsubset> 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-
@@ -470,7 +481,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 \<le> x \<and> x \<le> u')" .
+     have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')" .
      from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast}
    ultimately have "?D" by blast}
  moreover
@@ -505,7 +516,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 <"}, @{term "op \<le>"}]
+  val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
   fun h x t =
    case term_of t of
      Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq