# HG changeset patch
# User haftmann
# Date 1193426536 -7200
# Node ID b408ceba462736e16ed6e67bbb457e52a28fb2b2
# Parent  36cf92f63a4435a6e1d4bbd582be09516c3f9e52
dropped "brown" syntax

diff -r 36cf92f63a44 -r b408ceba4627 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Oct 26 19:58:32 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Oct 26 21:22:16 2007 +0200
@@ -2043,32 +2043,27 @@
 begin
 
 notation
-  less_eq  ("op \<^loc><=") and
-  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50) and
-  less  ("op \<^loc><") and
-  less  ("(_/ \<^loc>< _)"  [51, 51] 50)
-  
+  less     ("(_/ \<prec> _)"  [51, 51] 50)
+
 notation (xsymbols)
-  less_eq  ("op \<^loc>\<le>") and
-  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
+  less_eq  ("(_/ \<preceq> _)"  [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"
+  less_eq  ("(_/ \<preceq> _)"  [51, 51] 50)
+
+lemma below_refl [simp]: "x \<preceq> x"
   by (simp add: below_def idem)
 
 lemma below_antisym:
-  assumes xy: "x \<^loc>\<le> y" and yx: "y \<^loc>\<le> x"
+  assumes xy: "x \<preceq> y" and yx: "y \<preceq> x"
   shows "x = y"
   using xy [unfolded below_def, symmetric]
     yx [unfolded below_def commute]
   by (rule trans)
 
 lemma below_trans:
-  assumes xy: "x \<^loc>\<le> y" and yz: "y \<^loc>\<le> z"
-  shows "x \<^loc>\<le> z"
+  assumes xy: "x \<preceq> y" and yz: "y \<preceq> z"
+  shows "x \<preceq> z"
 proof -
   from xy have x_xy: "x \<cdot> y = x" by (simp add: below_def)
   from yz have y_yz: "y \<cdot> z = y" by (simp add: below_def)
@@ -2079,9 +2074,9 @@
   then show ?thesis by (simp add: below_def)
 qed
 
-lemma below_f_conv [simp,noatp]: "x \<^loc>\<le> y \<cdot> z = (x \<^loc>\<le> y \<and> x \<^loc>\<le> z)"
+lemma below_f_conv [simp,noatp]: "x \<preceq> y \<cdot> z = (x \<preceq> y \<and> x \<preceq> z)"
 proof
-  assume "x \<^loc>\<le> y \<cdot> z"
+  assume "x \<preceq> y \<cdot> z"
   hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
   have "x \<cdot> y = x"
   proof -
@@ -2097,14 +2092,14 @@
     also have "\<dots> = x" by(rule xyzx)
     finally show ?thesis .
   qed
-  ultimately show "x \<^loc>\<le> y \<and> x \<^loc>\<le> z" by(simp add: below_def)
+  ultimately show "x \<preceq> y \<and> x \<preceq> z" by(simp add: below_def)
 next
-  assume a: "x \<^loc>\<le> y \<and> x \<^loc>\<le> z"
+  assume a: "x \<preceq> y \<and> x \<preceq> z"
   hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
   have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
   also have "x \<cdot> y = x" using a by(simp_all add: below_def)
   also have "x \<cdot> z = x" using a by(simp_all add: below_def)
-  finally show "x \<^loc>\<le> y \<cdot> z" by(simp_all add: below_def)
+  finally show "x \<preceq> y \<cdot> z" by(simp_all add: below_def)
 qed
 
 end
@@ -2118,38 +2113,38 @@
 begin
 
 lemma above_f_conv:
- "x \<cdot> y \<^loc>\<le> z = (x \<^loc>\<le> z \<or> y \<^loc>\<le> z)"
+ "x \<cdot> y \<preceq> z = (x \<preceq> z \<or> y \<preceq> z)"
 proof
-  assume a: "x \<cdot> y \<^loc>\<le> z"
+  assume a: "x \<cdot> y \<preceq> z"
   have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
-  thus "x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
+  thus "x \<preceq> z \<or> y \<preceq> z"
   proof
-    assume "x \<cdot> y = x" hence "x \<^loc>\<le> z" by(rule subst)(rule a) thus ?thesis ..
+    assume "x \<cdot> y = x" hence "x \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
   next
-    assume "x \<cdot> y = y" hence "y \<^loc>\<le> z" by(rule subst)(rule a) thus ?thesis ..
+    assume "x \<cdot> y = y" hence "y \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
   qed
 next
-  assume "x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
-  thus "x \<cdot> y \<^loc>\<le> z"
+  assume "x \<preceq> z \<or> y \<preceq> z"
+  thus "x \<cdot> y \<preceq> z"
   proof
-    assume a: "x \<^loc>\<le> z"
+    assume a: "x \<preceq> z"
     have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
     also have "x \<cdot> z = x" using a by(simp add:below_def)
-    finally show "x \<cdot> y \<^loc>\<le> z" by(simp add:below_def)
+    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
   next
-    assume a: "y \<^loc>\<le> z"
+    assume a: "y \<preceq> z"
     have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
     also have "y \<cdot> z = y" using a by(simp add:below_def)
-    finally show "x \<cdot> y \<^loc>\<le> z" by(simp add:below_def)
+    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
   qed
 qed
 
-lemma strict_below_f_conv[simp,noatp]: "x \<^loc>< y \<cdot> z = (x \<^loc>< y \<and> x \<^loc>< z)"
+lemma strict_below_f_conv[simp,noatp]: "x \<prec> y \<cdot> z = (x \<prec> y \<and> x \<prec> z)"
 apply(simp add: strict_below_def)
 using lin[of y z] by (auto simp:below_def ACI)
 
 lemma strict_above_f_conv:
-  "x \<cdot> y \<^loc>< z = (x \<^loc>< z \<or> y \<^loc>< z)"
+  "x \<cdot> y \<prec> z = (x \<prec> z \<or> y \<prec> z)"
 apply(simp add: strict_below_def above_f_conv)
 using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
 
@@ -2196,18 +2191,18 @@
 
 lemma (in ACIfSL) below_fold1_iff:
 assumes A: "finite A" "A \<noteq> {}"
-shows "x \<^loc>\<le> fold1 f A = (\<forall>a\<in>A. x \<^loc>\<le> a)"
+shows "x \<preceq> fold1 f A = (\<forall>a\<in>A. x \<preceq> a)"
 using A
 by(induct rule:finite_ne_induct) simp_all
 
 lemma (in ACIfSLlin) strict_below_fold1_iff:
-  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<^loc>< fold1 f A = (\<forall>a\<in>A. x \<^loc>< a)"
+  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<prec> fold1 f A = (\<forall>a\<in>A. x \<prec> a)"
 by(induct rule:finite_ne_induct) simp_all
 
 
 lemma (in ACIfSL) fold1_belowI:
 assumes A: "finite A" "A \<noteq> {}"
-shows "a \<in> A \<Longrightarrow> fold1 f A \<^loc>\<le> a"
+shows "a \<in> A \<Longrightarrow> fold1 f A \<preceq> a"
 using A
 proof (induct rule:finite_ne_induct)
   case singleton thus ?case by simp
@@ -2219,7 +2214,7 @@
     assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
   next
     assume "a \<in> F"
-    hence bel: "fold1 f F \<^loc>\<le> a" by(rule insert)
+    hence bel: "fold1 f F \<preceq> a" by(rule insert)
     have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
       using insert by(simp add:below_def ACI)
     also have "fold1 f F \<cdot> a = fold1 f F"
@@ -2232,19 +2227,19 @@
 
 lemma (in ACIfSLlin) fold1_below_iff:
 assumes A: "finite A" "A \<noteq> {}"
-shows "fold1 f A \<^loc>\<le> x = (\<exists>a\<in>A. a \<^loc>\<le> x)"
+shows "fold1 f A \<preceq> x = (\<exists>a\<in>A. a \<preceq> x)"
 using A
 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
 
 lemma (in ACIfSLlin) fold1_strict_below_iff:
 assumes A: "finite A" "A \<noteq> {}"
-shows "fold1 f A \<^loc>< x = (\<exists>a\<in>A. a \<^loc>< x)"
+shows "fold1 f A \<prec> x = (\<exists>a\<in>A. a \<prec> x)"
 using A
 by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv)
 
 lemma (in ACIfSLlin) fold1_antimono:
 assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
-shows "fold1 f B \<^loc>\<le> fold1 f A"
+shows "fold1 f B \<preceq> fold1 f A"
 proof(cases)
   assume "A = B" thus ?thesis by simp
 next
@@ -2259,7 +2254,7 @@
     moreover have "A Int (B-A) = {}" using prems by blast
     ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
   qed
-  also have "\<dots> \<^loc>\<le> fold1 f A" by(simp add: above_f_conv)
+  also have "\<dots> \<preceq> fold1 f A" by(simp add: above_f_conv)
   finally show ?thesis .
 qed