src/HOL/Orderings.thy
 changeset 15837 7a567dcd4cda parent 15822 916b9df2ce9f child 15950 5c067c956a20
equal 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"`
`   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)`