# HG changeset patch # User wenzelm # Date 855758551 -3600 # Node ID 27cdd600a3b13c6c2a7fca6420beb127bdadf26a # Parent 1effe74134860bb9ac15a7bcdf9161c9aa56274e tuned names: partial order, linear order; diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/CLattice.thy --- a/src/HOL/AxClasses/Lattice/CLattice.thy Mon Feb 10 16:16:55 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/CLattice.thy Wed Feb 12 15:42:31 1997 +0100 @@ -12,7 +12,7 @@ CLattice = Order + axclass - clattice < order + clattice < partial_order ex_Inf "ALL A. EX inf. is_Inf A inf" ex_Sup "ALL A. EX sup. is_Sup A sup" diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/LatInsts.thy --- a/src/HOL/AxClasses/Lattice/LatInsts.thy Mon Feb 10 16:16:55 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/LatInsts.thy Wed Feb 12 15:42:31 1997 +0100 @@ -11,7 +11,7 @@ (* linear orders are lattices *) instance - lin_order < lattice (allI, exI, min_is_inf, max_is_sup) + linear_order < lattice (allI, exI, min_is_inf, max_is_sup) (* complete lattices are lattices *) @@ -36,6 +36,6 @@ (*FIXME bug workaround (see also OrdInsts.thy)*) instance - dual :: (lin_order) lin_order (le_dual_lin) + dual :: (linear_order) linear_order (le_dual_linear) end diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/Lattice.thy --- a/src/HOL/AxClasses/Lattice/Lattice.thy Mon Feb 10 16:16:55 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/Lattice.thy Wed Feb 12 15:42:31 1997 +0100 @@ -8,7 +8,7 @@ Lattice = Order + axclass - lattice < order + lattice < partial_order ex_inf "ALL x y. EX inf. is_inf x y inf" ex_sup "ALL x y. EX sup. is_sup x y sup" diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/OrdDefs.ML --- a/src/HOL/AxClasses/Lattice/OrdDefs.ML Mon Feb 10 16:16:55 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML Wed Feb 12 15:42:31 1997 +0100 @@ -20,7 +20,7 @@ ba 1; qed "le_prod_trans"; -goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)"; +goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)"; by (safe_tac (!claset)); by (stac Pair_fst_snd_eq 1); br conjI 1; @@ -44,7 +44,7 @@ by (Fast_tac 1); qed "le_fun_trans"; -goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)"; +goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)"; by (safe_tac (!claset)); br ext 1; br (le_antisym RS mp) 1; @@ -72,7 +72,7 @@ br le_trans 1; qed "le_dual_trans"; -goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)"; +goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)"; by (safe_tac (!claset)); br (Rep_dual_inverse RS subst) 1; br sym 1; @@ -83,6 +83,6 @@ ba 1; qed "le_dual_antisym"; -goalw thy [le_dual_def] "x [= y | y [= (x::'a::lin_order dual)"; - br le_lin 1; -qed "le_dual_lin"; +goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)"; + br le_linear 1; +qed "le_dual_linear"; diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/OrdInsts.thy --- a/src/HOL/AxClasses/Lattice/OrdInsts.thy Mon Feb 10 16:16:55 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/OrdInsts.thy Wed Feb 12 15:42:31 1997 +0100 @@ -14,30 +14,30 @@ "*" :: (quasi_order, quasi_order) quasi_order (le_prod_refl, le_prod_trans) instance - "*" :: (order, order) order (le_prod_antisym) + "*" :: (partial_order, partial_order) partial_order (le_prod_antisym) instance fun :: (term, quasi_order) quasi_order (le_fun_refl, le_fun_trans) instance - fun :: (term, order) order (le_fun_antisym) + fun :: (term, partial_order) partial_order (le_fun_antisym) -(* duals of quasi_orders / orders / lin_orders *) +(* duals of quasi orders / partial orders / linear orders *) instance dual :: (quasi_order) quasi_order (le_dual_refl, le_dual_trans) instance - dual :: (order) order (le_dual_antisym) + dual :: (partial_order) partial_order (le_dual_antisym) (*FIXME: had to be moved to LatInsts.thy due to some unpleasant 'feature' in Pure/type.ML instance - dual :: (lin_order) lin_order (le_dual_lin) + dual :: (linear_order) linear_order (le_dual_lin) *) end diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/Order.ML --- a/src/HOL/AxClasses/Lattice/Order.ML Mon Feb 10 16:16:55 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/Order.ML Wed Feb 12 15:42:31 1997 +0100 @@ -114,7 +114,7 @@ (** limits in linear orders **) -goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::lin_order) y (minimum x y)"; +goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::linear_order) y (minimum x y)"; by (stac expand_if 1); by (REPEAT_FIRST (resolve_tac [conjI, impI])); (*case "x [= y"*) @@ -122,7 +122,7 @@ ba 1; by (Fast_tac 1); (*case "~ x [= y"*) - br (le_lin RS disjE) 1; + br (le_linear RS disjE) 1; ba 1; be notE 1; ba 1; @@ -130,7 +130,7 @@ by (Fast_tac 1); qed "min_is_inf"; -goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::lin_order) y (maximum x y)"; +goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::linear_order) y (maximum x y)"; by (stac expand_if 1); by (REPEAT_FIRST (resolve_tac [conjI, impI])); (*case "x [= y"*) @@ -139,7 +139,7 @@ by (Fast_tac 1); (*case "~ x [= y"*) br le_refl 1; - br (le_lin RS disjE) 1; + br (le_linear RS disjE) 1; ba 1; be notE 1; ba 1; diff -r 1effe7413486 -r 27cdd600a3b1 src/HOL/AxClasses/Lattice/Order.thy --- a/src/HOL/AxClasses/Lattice/Order.thy Mon Feb 10 16:16:55 1997 +0100 +++ b/src/HOL/AxClasses/Lattice/Order.thy Wed Feb 12 15:42:31 1997 +0100 @@ -31,15 +31,15 @@ (* partial orders *) axclass - order < quasi_order + partial_order < quasi_order le_antisym "x [= y & y [= x --> x = y" (* linear orders *) axclass - lin_order < order - le_lin "x [= y | y [= x" + linear_order < partial_order + le_linear "x [= y | y [= x" @@ -49,11 +49,11 @@ consts (*binary*) - is_inf :: "['a::order, 'a, 'a] => bool" - is_sup :: "['a::order, 'a, 'a] => bool" + is_inf :: "['a::partial_order, 'a, 'a] => bool" + is_sup :: "['a::partial_order, 'a, 'a] => bool" (*general*) - is_Inf :: "['a::order set, 'a] => bool" - is_Sup :: "['a::order set, 'a] => bool" + is_Inf :: "['a::partial_order set, 'a] => bool" + is_Sup :: "['a::partial_order set, 'a] => bool" defs is_inf_def "is_inf x y inf == @@ -71,13 +71,13 @@ -(* binary minima and maxima (on lin_orders) *) +(* binary minima and maxima (on linear_orders) *) constdefs - minimum :: "['a::lin_order, 'a] => 'a" + minimum :: "['a::linear_order, 'a] => 'a" "minimum x y == (if x [= y then x else y)" - maximum :: "['a::lin_order, 'a] => 'a" + maximum :: "['a::linear_order, 'a] => 'a" "maximum x y == (if x [= y then y else x)" end