--- 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"
--- 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
--- 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"
--- 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";
--- 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
--- 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;
--- 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