dropped "brown" syntax
authorhaftmann
Fri Oct 26 21:22:16 2007 +0200 (2007-10-26)
changeset 25205b408ceba4627
parent 25204 36cf92f63a44
child 25206 9c84ec7217a9
dropped "brown" syntax
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Oct 26 19:58:32 2007 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Oct 26 21:22:16 2007 +0200
     1.3 @@ -2043,32 +2043,27 @@
     1.4  begin
     1.5  
     1.6  notation
     1.7 -  less_eq  ("op \<^loc><=") and
     1.8 -  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50) and
     1.9 -  less  ("op \<^loc><") and
    1.10 -  less  ("(_/ \<^loc>< _)"  [51, 51] 50)
    1.11 -  
    1.12 +  less     ("(_/ \<prec> _)"  [51, 51] 50)
    1.13 +
    1.14  notation (xsymbols)
    1.15 -  less_eq  ("op \<^loc>\<le>") and
    1.16 -  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
    1.17 +  less_eq  ("(_/ \<preceq> _)"  [51, 51] 50)
    1.18  
    1.19  notation (HTML output)
    1.20 -  less_eq  ("op \<^loc>\<le>") and
    1.21 -  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
    1.22 -
    1.23 -lemma below_refl [simp]: "x \<^loc>\<le> x"
    1.24 +  less_eq  ("(_/ \<preceq> _)"  [51, 51] 50)
    1.25 +
    1.26 +lemma below_refl [simp]: "x \<preceq> x"
    1.27    by (simp add: below_def idem)
    1.28  
    1.29  lemma below_antisym:
    1.30 -  assumes xy: "x \<^loc>\<le> y" and yx: "y \<^loc>\<le> x"
    1.31 +  assumes xy: "x \<preceq> y" and yx: "y \<preceq> x"
    1.32    shows "x = y"
    1.33    using xy [unfolded below_def, symmetric]
    1.34      yx [unfolded below_def commute]
    1.35    by (rule trans)
    1.36  
    1.37  lemma below_trans:
    1.38 -  assumes xy: "x \<^loc>\<le> y" and yz: "y \<^loc>\<le> z"
    1.39 -  shows "x \<^loc>\<le> z"
    1.40 +  assumes xy: "x \<preceq> y" and yz: "y \<preceq> z"
    1.41 +  shows "x \<preceq> z"
    1.42  proof -
    1.43    from xy have x_xy: "x \<cdot> y = x" by (simp add: below_def)
    1.44    from yz have y_yz: "y \<cdot> z = y" by (simp add: below_def)
    1.45 @@ -2079,9 +2074,9 @@
    1.46    then show ?thesis by (simp add: below_def)
    1.47  qed
    1.48  
    1.49 -lemma below_f_conv [simp,noatp]: "x \<^loc>\<le> y \<cdot> z = (x \<^loc>\<le> y \<and> x \<^loc>\<le> z)"
    1.50 +lemma below_f_conv [simp,noatp]: "x \<preceq> y \<cdot> z = (x \<preceq> y \<and> x \<preceq> z)"
    1.51  proof
    1.52 -  assume "x \<^loc>\<le> y \<cdot> z"
    1.53 +  assume "x \<preceq> y \<cdot> z"
    1.54    hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
    1.55    have "x \<cdot> y = x"
    1.56    proof -
    1.57 @@ -2097,14 +2092,14 @@
    1.58      also have "\<dots> = x" by(rule xyzx)
    1.59      finally show ?thesis .
    1.60    qed
    1.61 -  ultimately show "x \<^loc>\<le> y \<and> x \<^loc>\<le> z" by(simp add: below_def)
    1.62 +  ultimately show "x \<preceq> y \<and> x \<preceq> z" by(simp add: below_def)
    1.63  next
    1.64 -  assume a: "x \<^loc>\<le> y \<and> x \<^loc>\<le> z"
    1.65 +  assume a: "x \<preceq> y \<and> x \<preceq> z"
    1.66    hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
    1.67    have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
    1.68    also have "x \<cdot> y = x" using a by(simp_all add: below_def)
    1.69    also have "x \<cdot> z = x" using a by(simp_all add: below_def)
    1.70 -  finally show "x \<^loc>\<le> y \<cdot> z" by(simp_all add: below_def)
    1.71 +  finally show "x \<preceq> y \<cdot> z" by(simp_all add: below_def)
    1.72  qed
    1.73  
    1.74  end
    1.75 @@ -2118,38 +2113,38 @@
    1.76  begin
    1.77  
    1.78  lemma above_f_conv:
    1.79 - "x \<cdot> y \<^loc>\<le> z = (x \<^loc>\<le> z \<or> y \<^loc>\<le> z)"
    1.80 + "x \<cdot> y \<preceq> z = (x \<preceq> z \<or> y \<preceq> z)"
    1.81  proof
    1.82 -  assume a: "x \<cdot> y \<^loc>\<le> z"
    1.83 +  assume a: "x \<cdot> y \<preceq> z"
    1.84    have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
    1.85 -  thus "x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
    1.86 +  thus "x \<preceq> z \<or> y \<preceq> z"
    1.87    proof
    1.88 -    assume "x \<cdot> y = x" hence "x \<^loc>\<le> z" by(rule subst)(rule a) thus ?thesis ..
    1.89 +    assume "x \<cdot> y = x" hence "x \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
    1.90    next
    1.91 -    assume "x \<cdot> y = y" hence "y \<^loc>\<le> z" by(rule subst)(rule a) thus ?thesis ..
    1.92 +    assume "x \<cdot> y = y" hence "y \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
    1.93    qed
    1.94  next
    1.95 -  assume "x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
    1.96 -  thus "x \<cdot> y \<^loc>\<le> z"
    1.97 +  assume "x \<preceq> z \<or> y \<preceq> z"
    1.98 +  thus "x \<cdot> y \<preceq> z"
    1.99    proof
   1.100 -    assume a: "x \<^loc>\<le> z"
   1.101 +    assume a: "x \<preceq> z"
   1.102      have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
   1.103      also have "x \<cdot> z = x" using a by(simp add:below_def)
   1.104 -    finally show "x \<cdot> y \<^loc>\<le> z" by(simp add:below_def)
   1.105 +    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
   1.106    next
   1.107 -    assume a: "y \<^loc>\<le> z"
   1.108 +    assume a: "y \<preceq> z"
   1.109      have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
   1.110      also have "y \<cdot> z = y" using a by(simp add:below_def)
   1.111 -    finally show "x \<cdot> y \<^loc>\<le> z" by(simp add:below_def)
   1.112 +    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
   1.113    qed
   1.114  qed
   1.115  
   1.116 -lemma strict_below_f_conv[simp,noatp]: "x \<^loc>< y \<cdot> z = (x \<^loc>< y \<and> x \<^loc>< z)"
   1.117 +lemma strict_below_f_conv[simp,noatp]: "x \<prec> y \<cdot> z = (x \<prec> y \<and> x \<prec> z)"
   1.118  apply(simp add: strict_below_def)
   1.119  using lin[of y z] by (auto simp:below_def ACI)
   1.120  
   1.121  lemma strict_above_f_conv:
   1.122 -  "x \<cdot> y \<^loc>< z = (x \<^loc>< z \<or> y \<^loc>< z)"
   1.123 +  "x \<cdot> y \<prec> z = (x \<prec> z \<or> y \<prec> z)"
   1.124  apply(simp add: strict_below_def above_f_conv)
   1.125  using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
   1.126  
   1.127 @@ -2196,18 +2191,18 @@
   1.128  
   1.129  lemma (in ACIfSL) below_fold1_iff:
   1.130  assumes A: "finite A" "A \<noteq> {}"
   1.131 -shows "x \<^loc>\<le> fold1 f A = (\<forall>a\<in>A. x \<^loc>\<le> a)"
   1.132 +shows "x \<preceq> fold1 f A = (\<forall>a\<in>A. x \<preceq> a)"
   1.133  using A
   1.134  by(induct rule:finite_ne_induct) simp_all
   1.135  
   1.136  lemma (in ACIfSLlin) strict_below_fold1_iff:
   1.137 -  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<^loc>< fold1 f A = (\<forall>a\<in>A. x \<^loc>< a)"
   1.138 +  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<prec> fold1 f A = (\<forall>a\<in>A. x \<prec> a)"
   1.139  by(induct rule:finite_ne_induct) simp_all
   1.140  
   1.141  
   1.142  lemma (in ACIfSL) fold1_belowI:
   1.143  assumes A: "finite A" "A \<noteq> {}"
   1.144 -shows "a \<in> A \<Longrightarrow> fold1 f A \<^loc>\<le> a"
   1.145 +shows "a \<in> A \<Longrightarrow> fold1 f A \<preceq> a"
   1.146  using A
   1.147  proof (induct rule:finite_ne_induct)
   1.148    case singleton thus ?case by simp
   1.149 @@ -2219,7 +2214,7 @@
   1.150      assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
   1.151    next
   1.152      assume "a \<in> F"
   1.153 -    hence bel: "fold1 f F \<^loc>\<le> a" by(rule insert)
   1.154 +    hence bel: "fold1 f F \<preceq> a" by(rule insert)
   1.155      have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
   1.156        using insert by(simp add:below_def ACI)
   1.157      also have "fold1 f F \<cdot> a = fold1 f F"
   1.158 @@ -2232,19 +2227,19 @@
   1.159  
   1.160  lemma (in ACIfSLlin) fold1_below_iff:
   1.161  assumes A: "finite A" "A \<noteq> {}"
   1.162 -shows "fold1 f A \<^loc>\<le> x = (\<exists>a\<in>A. a \<^loc>\<le> x)"
   1.163 +shows "fold1 f A \<preceq> x = (\<exists>a\<in>A. a \<preceq> x)"
   1.164  using A
   1.165  by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
   1.166  
   1.167  lemma (in ACIfSLlin) fold1_strict_below_iff:
   1.168  assumes A: "finite A" "A \<noteq> {}"
   1.169 -shows "fold1 f A \<^loc>< x = (\<exists>a\<in>A. a \<^loc>< x)"
   1.170 +shows "fold1 f A \<prec> x = (\<exists>a\<in>A. a \<prec> x)"
   1.171  using A
   1.172  by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv)
   1.173  
   1.174  lemma (in ACIfSLlin) fold1_antimono:
   1.175  assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
   1.176 -shows "fold1 f B \<^loc>\<le> fold1 f A"
   1.177 +shows "fold1 f B \<preceq> fold1 f A"
   1.178  proof(cases)
   1.179    assume "A = B" thus ?thesis by simp
   1.180  next
   1.181 @@ -2259,7 +2254,7 @@
   1.182      moreover have "A Int (B-A) = {}" using prems by blast
   1.183      ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
   1.184    qed
   1.185 -  also have "\<dots> \<^loc>\<le> fold1 f A" by(simp add: above_f_conv)
   1.186 +  also have "\<dots> \<preceq> fold1 f A" by(simp add: above_f_conv)
   1.187    finally show ?thesis .
   1.188  qed
   1.189