src/HOL/Orderings.thy
changeset 61076 bdc1e2f0a86a
parent 60758 d8d85a8172b5
child 61169 4de9ff3ea29a
     1.1 --- a/src/HOL/Orderings.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -1034,21 +1034,21 @@
     1.4  context order
     1.5  begin
     1.6  
     1.7 -definition mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
     1.8 +definition mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
     1.9    "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
    1.10  
    1.11  lemma monoI [intro?]:
    1.12 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    1.13 +  fixes f :: "'a \<Rightarrow> 'b::order"
    1.14    shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
    1.15    unfolding mono_def by iprover
    1.16  
    1.17  lemma monoD [dest?]:
    1.18 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    1.19 +  fixes f :: "'a \<Rightarrow> 'b::order"
    1.20    shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
    1.21    unfolding mono_def by iprover
    1.22  
    1.23  lemma monoE:
    1.24 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    1.25 +  fixes f :: "'a \<Rightarrow> 'b::order"
    1.26    assumes "mono f"
    1.27    assumes "x \<le> y"
    1.28    obtains "f x \<le> f y"
    1.29 @@ -1056,21 +1056,21 @@
    1.30    from assms show "f x \<le> f y" by (simp add: mono_def)
    1.31  qed
    1.32  
    1.33 -definition antimono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
    1.34 +definition antimono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
    1.35    "antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
    1.36  
    1.37  lemma antimonoI [intro?]:
    1.38 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    1.39 +  fixes f :: "'a \<Rightarrow> 'b::order"
    1.40    shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<ge> f y) \<Longrightarrow> antimono f"
    1.41    unfolding antimono_def by iprover
    1.42  
    1.43  lemma antimonoD [dest?]:
    1.44 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    1.45 +  fixes f :: "'a \<Rightarrow> 'b::order"
    1.46    shows "antimono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
    1.47    unfolding antimono_def by iprover
    1.48  
    1.49  lemma antimonoE:
    1.50 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    1.51 +  fixes f :: "'a \<Rightarrow> 'b::order"
    1.52    assumes "antimono f"
    1.53    assumes "x \<le> y"
    1.54    obtains "f x \<ge> f y"
    1.55 @@ -1078,7 +1078,7 @@
    1.56    from assms show "f x \<ge> f y" by (simp add: antimono_def)
    1.57  qed
    1.58  
    1.59 -definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
    1.60 +definition strict_mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
    1.61    "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
    1.62  
    1.63  lemma strict_monoI [intro?]:
    1.64 @@ -1112,7 +1112,7 @@
    1.65  begin
    1.66  
    1.67  lemma mono_invE:
    1.68 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    1.69 +  fixes f :: "'a \<Rightarrow> 'b::order"
    1.70    assumes "mono f"
    1.71    assumes "f x < f y"
    1.72    obtains "x \<le> y"
    1.73 @@ -1180,10 +1180,10 @@
    1.74  lemma max_absorb2: "x \<le> y \<Longrightarrow> max x y = y"
    1.75    by (simp add: max_def)
    1.76  
    1.77 -lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y"
    1.78 +lemma min_absorb2: "(y::'a::order) \<le> x \<Longrightarrow> min x y = y"
    1.79    by (simp add:min_def)
    1.80  
    1.81 -lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x"
    1.82 +lemma max_absorb1: "(y::'a::order) \<le> x \<Longrightarrow> max x y = x"
    1.83    by (simp add: max_def)
    1.84  
    1.85  
    1.86 @@ -1409,7 +1409,7 @@
    1.87    le_bool_def [simp]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
    1.88  
    1.89  definition
    1.90 -  [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    1.91 +  [simp]: "(P::bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    1.92  
    1.93  definition
    1.94    [simp]: "\<bottom> \<longleftrightarrow> False"
    1.95 @@ -1457,7 +1457,7 @@
    1.96    le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
    1.97  
    1.98  definition
    1.99 -  "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
   1.100 +  "(f::'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
   1.101  
   1.102  instance ..
   1.103  
   1.104 @@ -1620,4 +1620,3 @@
   1.105  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   1.106  
   1.107  end
   1.108 -