src/HOL/Orderings.thy
changeset 15837 7a567dcd4cda
parent 15822 916b9df2ce9f
child 15950 5c067c956a20
equal deleted inserted replaced
15836:b805d85909c7 15837:7a567dcd4cda
    91   order_antisym: "x <= y ==> y <= x ==> x = y"
    91   order_antisym: "x <= y ==> y <= x ==> x = y"
    92   order_less_le: "(x < y) = (x <= y & x ~= y)"
    92   order_less_le: "(x < y) = (x <= y & x ~= y)"
    93 
    93 
    94 text{* Connection to locale: *}
    94 text{* Connection to locale: *}
    95 
    95 
    96 interpretation order[rule del]:
    96 interpretation order:
    97   partial_order["op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool"]
    97   partial_order["op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool"]
    98 apply(rule partial_order.intro)
    98 apply(rule partial_order.intro)
    99 apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
    99 apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
   100 done
   100 done
   101 
   101 
   223 
   223 
   224 subsection "Linear / total orders"
   224 subsection "Linear / total orders"
   225 
   225 
   226 axclass linorder < order
   226 axclass linorder < order
   227   linorder_linear: "x <= y | y <= x"
   227   linorder_linear: "x <= y | y <= x"
   228 
       
   229 (* Could (should?) follow automatically from the interpretation of
       
   230    partial_order by class order. rule del is needed because two copies
       
   231    of refl with classes order and linorder confuse blast (and are pointless)*)
       
   232 interpretation order[rule del]:
       
   233   partial_order["op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool"]
       
   234 apply(rule partial_order.intro)
       
   235 apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
       
   236 done
       
   237 
       
   238 
   228 
   239 lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
   229 lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
   240   apply (simp add: order_less_le)
   230   apply (simp add: order_less_le)
   241   apply (insert linorder_linear, blast)
   231   apply (insert linorder_linear, blast)
   242   done
   232   done
   390 
   380 
   391 subsection "Min and max on (linear) orders"
   381 subsection "Min and max on (linear) orders"
   392 
   382 
   393 text{* Instantiate locales: *}
   383 text{* Instantiate locales: *}
   394 
   384 
   395 interpretation min_max [rule del]:
   385 interpretation min_max:
   396   lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   386   lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   397 apply -
   387 apply -
   398 apply(rule lower_semilattice_axioms.intro)
   388 apply(rule lower_semilattice_axioms.intro)
   399 apply(simp add:min_def linorder_not_le order_less_imp_le)
   389 apply(simp add:min_def linorder_not_le order_less_imp_le)
   400 apply(simp add:min_def linorder_not_le order_less_imp_le)
   390 apply(simp add:min_def linorder_not_le order_less_imp_le)
   401 apply(simp add:min_def linorder_not_le order_less_imp_le)
   391 apply(simp add:min_def linorder_not_le order_less_imp_le)
   402 done
   392 done
   403 
   393 
   404 interpretation min_max [rule del]:
   394 interpretation min_max:
   405   upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   395   upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   406 apply -
   396 apply -
   407 apply(rule upper_semilattice_axioms.intro)
   397 apply(rule upper_semilattice_axioms.intro)
   408 apply(simp add: max_def linorder_not_le order_less_imp_le)
   398 apply(simp add: max_def linorder_not_le order_less_imp_le)
   409 apply(simp add: max_def linorder_not_le order_less_imp_le)
   399 apply(simp add: max_def linorder_not_le order_less_imp_le)
   410 apply(simp add: max_def linorder_not_le order_less_imp_le)
   400 apply(simp add: max_def linorder_not_le order_less_imp_le)
   411 done
   401 done
   412 
   402 
   413 interpretation min_max [rule del]:
   403 interpretation min_max:
   414   lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   404   lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   415 .
   405 .
   416 
   406 
   417 interpretation min_max [rule del]:
   407 interpretation min_max:
   418   distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   408   distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   419 apply(rule distrib_lattice_axioms.intro)
   409 apply(rule distrib_lattice_axioms.intro)
   420 apply(rule_tac x=x and y=y in linorder_le_cases)
   410 apply(rule_tac x=x and y=y in linorder_le_cases)
   421 apply(rule_tac x=x and y=z in linorder_le_cases)
   411 apply(rule_tac x=x and y=z in linorder_le_cases)
   422 apply(rule_tac x=y and y=z in linorder_le_cases)
   412 apply(rule_tac x=y and y=z in linorder_le_cases)