src/HOL/Orderings.thy
changeset 24422 c0b5ff9e9e4d
parent 24286 7619080e49f0
child 24641 448edc627ee4
     1.1 --- a/src/HOL/Orderings.thy	Fri Aug 24 14:14:17 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Aug 24 14:14:18 2007 +0200
     1.3 @@ -236,53 +236,6 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsection {* Name duplicates *}
     1.8 -
     1.9 -lemmas order_less_le = less_le
    1.10 -lemmas order_eq_refl = order_class.eq_refl
    1.11 -lemmas order_less_irrefl = order_class.less_irrefl
    1.12 -lemmas order_le_less = order_class.le_less
    1.13 -lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
    1.14 -lemmas order_less_imp_le = order_class.less_imp_le
    1.15 -lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
    1.16 -lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
    1.17 -lemmas order_neq_le_trans = order_class.neq_le_trans
    1.18 -lemmas order_le_neq_trans = order_class.le_neq_trans
    1.19 -
    1.20 -lemmas order_antisym = antisym
    1.21 -lemmas order_less_not_sym = order_class.less_not_sym
    1.22 -lemmas order_less_asym = order_class.less_asym
    1.23 -lemmas order_eq_iff = order_class.eq_iff
    1.24 -lemmas order_antisym_conv = order_class.antisym_conv
    1.25 -lemmas order_less_trans = order_class.less_trans
    1.26 -lemmas order_le_less_trans = order_class.le_less_trans
    1.27 -lemmas order_less_le_trans = order_class.less_le_trans
    1.28 -lemmas order_less_imp_not_less = order_class.less_imp_not_less
    1.29 -lemmas order_less_imp_triv = order_class.less_imp_triv
    1.30 -lemmas order_less_asym' = order_class.less_asym'
    1.31 -
    1.32 -lemmas linorder_linear = linear
    1.33 -lemmas linorder_less_linear = linorder_class.less_linear
    1.34 -lemmas linorder_le_less_linear = linorder_class.le_less_linear
    1.35 -lemmas linorder_le_cases = linorder_class.le_cases
    1.36 -lemmas linorder_not_less = linorder_class.not_less
    1.37 -lemmas linorder_not_le = linorder_class.not_le
    1.38 -lemmas linorder_neq_iff = linorder_class.neq_iff
    1.39 -lemmas linorder_neqE = linorder_class.neqE
    1.40 -lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
    1.41 -lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
    1.42 -lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
    1.43 -
    1.44 -lemmas min_le_iff_disj = linorder_class.min_le_iff_disj
    1.45 -lemmas le_max_iff_disj = linorder_class.le_max_iff_disj
    1.46 -lemmas min_less_iff_disj = linorder_class.min_less_iff_disj
    1.47 -lemmas less_max_iff_disj = linorder_class.less_max_iff_disj
    1.48 -lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj
    1.49 -lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj
    1.50 -lemmas split_min = linorder_class.split_min
    1.51 -lemmas split_max = linorder_class.split_max
    1.52 -
    1.53 -
    1.54  subsection {* Reasoning tools setup *}
    1.55  
    1.56  ML {*
    1.57 @@ -336,25 +289,25 @@
    1.58  
    1.59  structure Order_Tac = Order_Tac_Fun (
    1.60  struct
    1.61 -  val less_reflE = thm "order_less_irrefl" RS thm "notE";
    1.62 -  val le_refl = thm "order_refl";
    1.63 -  val less_imp_le = thm "order_less_imp_le";
    1.64 -  val not_lessI = thm "linorder_not_less" RS thm "iffD2";
    1.65 -  val not_leI = thm "linorder_not_le" RS thm "iffD2";
    1.66 -  val not_lessD = thm "linorder_not_less" RS thm "iffD1";
    1.67 -  val not_leD = thm "linorder_not_le" RS thm "iffD1";
    1.68 -  val eqI = thm "order_antisym";
    1.69 -  val eqD1 = thm "order_eq_refl";
    1.70 -  val eqD2 = thm "sym" RS thm "order_eq_refl";
    1.71 -  val less_trans = thm "order_less_trans";
    1.72 -  val less_le_trans = thm "order_less_le_trans";
    1.73 -  val le_less_trans = thm "order_le_less_trans";
    1.74 -  val le_trans = thm "order_trans";
    1.75 -  val le_neq_trans = thm "order_le_neq_trans";
    1.76 -  val neq_le_trans = thm "order_neq_le_trans";
    1.77 -  val less_imp_neq = thm "less_imp_neq";
    1.78 -  val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
    1.79 -  val not_sym = thm "not_sym";
    1.80 +  val less_reflE = @{thm less_irrefl} RS @{thm notE};
    1.81 +  val le_refl = @{thm order_refl};
    1.82 +  val less_imp_le = @{thm less_imp_le};
    1.83 +  val not_lessI = @{thm not_less} RS @{thm iffD2};
    1.84 +  val not_leI = @{thm not_le} RS @{thm iffD2};
    1.85 +  val not_lessD = @{thm not_less} RS @{thm iffD1};
    1.86 +  val not_leD = @{thm not_le} RS @{thm iffD1};
    1.87 +  val eqI = @{thm antisym};
    1.88 +  val eqD1 = @{thm eq_refl};
    1.89 +  val eqD2 = @{thm sym} RS @{thm eq_refl};
    1.90 +  val less_trans = @{thm less_trans};
    1.91 +  val less_le_trans = @{thm less_le_trans};
    1.92 +  val le_less_trans = @{thm le_less_trans};
    1.93 +  val le_trans = @{thm order_trans};
    1.94 +  val le_neq_trans = @{thm le_neq_trans};
    1.95 +  val neq_le_trans = @{thm neq_le_trans};
    1.96 +  val less_imp_neq = @{thm less_imp_neq};
    1.97 +  val eq_neq_eq_imp_neq = @{thm eq_neq_eq_imp_neq};
    1.98 +  val not_sym = @{thm not_sym};
    1.99    val decomp_part = decomp_gen ["Orderings.order"];
   1.100    val decomp_lin = decomp_gen ["Orderings.linorder"];
   1.101  end);
   1.102 @@ -376,9 +329,9 @@
   1.103           let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
   1.104           in case find_first (prp t) prems of
   1.105                NONE => NONE
   1.106 -            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv1}))
   1.107 +            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1}))
   1.108           end
   1.109 -     | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_antisym_conv}))
   1.110 +     | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv}))
   1.111    end
   1.112    handle THM _ => NONE;
   1.113  
   1.114 @@ -391,9 +344,9 @@
   1.115           let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
   1.116           in case find_first (prp t) prems of
   1.117                NONE => NONE
   1.118 -            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv3}))
   1.119 +            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3}))
   1.120           end
   1.121 -     | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv2}))
   1.122 +     | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2}))
   1.123    end
   1.124    handle THM _ => NONE;
   1.125  
   1.126 @@ -420,6 +373,66 @@
   1.127  *}
   1.128  
   1.129  
   1.130 +subsection {* Dense orders *}
   1.131 +
   1.132 +class dense_linear_order = linorder + 
   1.133 +  assumes gt_ex: "\<exists>y. x \<sqsubset> y" 
   1.134 +  and lt_ex: "\<exists>y. y \<sqsubset> x"
   1.135 +  and dense: "x \<sqsubset> y \<Longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
   1.136 +  (*see further theory Dense_Linear_Order*)
   1.137 +
   1.138 +lemma interval_empty_iff:
   1.139 +  fixes x y z :: "'a\<Colon>dense_linear_order"
   1.140 +  shows "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
   1.141 +  by (auto dest: dense)
   1.142 +
   1.143 +subsection {* Name duplicates *}
   1.144 +
   1.145 +lemmas order_less_le = less_le
   1.146 +lemmas order_eq_refl = order_class.eq_refl
   1.147 +lemmas order_less_irrefl = order_class.less_irrefl
   1.148 +lemmas order_le_less = order_class.le_less
   1.149 +lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
   1.150 +lemmas order_less_imp_le = order_class.less_imp_le
   1.151 +lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
   1.152 +lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
   1.153 +lemmas order_neq_le_trans = order_class.neq_le_trans
   1.154 +lemmas order_le_neq_trans = order_class.le_neq_trans
   1.155 +
   1.156 +lemmas order_antisym = antisym
   1.157 +lemmas order_less_not_sym = order_class.less_not_sym
   1.158 +lemmas order_less_asym = order_class.less_asym
   1.159 +lemmas order_eq_iff = order_class.eq_iff
   1.160 +lemmas order_antisym_conv = order_class.antisym_conv
   1.161 +lemmas order_less_trans = order_class.less_trans
   1.162 +lemmas order_le_less_trans = order_class.le_less_trans
   1.163 +lemmas order_less_le_trans = order_class.less_le_trans
   1.164 +lemmas order_less_imp_not_less = order_class.less_imp_not_less
   1.165 +lemmas order_less_imp_triv = order_class.less_imp_triv
   1.166 +lemmas order_less_asym' = order_class.less_asym'
   1.167 +
   1.168 +lemmas linorder_linear = linear
   1.169 +lemmas linorder_less_linear = linorder_class.less_linear
   1.170 +lemmas linorder_le_less_linear = linorder_class.le_less_linear
   1.171 +lemmas linorder_le_cases = linorder_class.le_cases
   1.172 +lemmas linorder_not_less = linorder_class.not_less
   1.173 +lemmas linorder_not_le = linorder_class.not_le
   1.174 +lemmas linorder_neq_iff = linorder_class.neq_iff
   1.175 +lemmas linorder_neqE = linorder_class.neqE
   1.176 +lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
   1.177 +lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
   1.178 +lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   1.179 +
   1.180 +lemmas min_le_iff_disj = linorder_class.min_le_iff_disj
   1.181 +lemmas le_max_iff_disj = linorder_class.le_max_iff_disj
   1.182 +lemmas min_less_iff_disj = linorder_class.min_less_iff_disj
   1.183 +lemmas less_max_iff_disj = linorder_class.less_max_iff_disj
   1.184 +lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj
   1.185 +lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj
   1.186 +lemmas split_min = linorder_class.split_min
   1.187 +lemmas split_max = linorder_class.split_max
   1.188 +
   1.189 +
   1.190  subsection {* Bounded quantifiers *}
   1.191  
   1.192  syntax
   1.193 @@ -754,6 +767,7 @@
   1.194    le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
   1.195    less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
   1.196    by intro_classes (auto simp add: le_bool_def less_bool_def)
   1.197 +lemmas [code func del] = le_bool_def less_bool_def
   1.198  
   1.199  lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
   1.200  by (simp add: le_bool_def)