tuned names: partial order, linear order;
authorwenzelm
Wed Feb 12 15:42:31 1997 +0100 (1997-02-12)
changeset 260627cdd600a3b1
parent 2605 1effe7413486
child 2607 a224a2865e05
tuned names: partial order, linear order;
src/HOL/AxClasses/Lattice/CLattice.thy
src/HOL/AxClasses/Lattice/LatInsts.thy
src/HOL/AxClasses/Lattice/Lattice.thy
src/HOL/AxClasses/Lattice/OrdDefs.ML
src/HOL/AxClasses/Lattice/OrdInsts.thy
src/HOL/AxClasses/Lattice/Order.ML
src/HOL/AxClasses/Lattice/Order.thy
     1.1 --- a/src/HOL/AxClasses/Lattice/CLattice.thy	Mon Feb 10 16:16:55 1997 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/CLattice.thy	Wed Feb 12 15:42:31 1997 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  CLattice = Order +
     1.5  
     1.6  axclass
     1.7 -  clattice < order
     1.8 +  clattice < partial_order
     1.9    ex_Inf       "ALL A. EX inf. is_Inf A inf"
    1.10    ex_Sup       "ALL A. EX sup. is_Sup A sup"
    1.11  
     2.1 --- a/src/HOL/AxClasses/Lattice/LatInsts.thy	Mon Feb 10 16:16:55 1997 +0100
     2.2 +++ b/src/HOL/AxClasses/Lattice/LatInsts.thy	Wed Feb 12 15:42:31 1997 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4  (* linear orders are lattices *)
     2.5  
     2.6  instance
     2.7 -  lin_order < lattice                   (allI, exI, min_is_inf, max_is_sup)
     2.8 +  linear_order < lattice                (allI, exI, min_is_inf, max_is_sup)
     2.9  
    2.10  
    2.11  (* complete lattices are lattices *)
    2.12 @@ -36,6 +36,6 @@
    2.13  
    2.14  (*FIXME bug workaround (see also OrdInsts.thy)*)
    2.15  instance
    2.16 -  dual :: (lin_order) lin_order         (le_dual_lin)
    2.17 +  dual :: (linear_order) linear_order   (le_dual_linear)
    2.18  
    2.19  end
     3.1 --- a/src/HOL/AxClasses/Lattice/Lattice.thy	Mon Feb 10 16:16:55 1997 +0100
     3.2 +++ b/src/HOL/AxClasses/Lattice/Lattice.thy	Wed Feb 12 15:42:31 1997 +0100
     3.3 @@ -8,7 +8,7 @@
     3.4  Lattice = Order +
     3.5  
     3.6  axclass
     3.7 -  lattice < order
     3.8 +  lattice < partial_order
     3.9    ex_inf       "ALL x y. EX inf. is_inf x y inf"
    3.10    ex_sup       "ALL x y. EX sup. is_sup x y sup"
    3.11  
     4.1 --- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Mon Feb 10 16:16:55 1997 +0100
     4.2 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Feb 12 15:42:31 1997 +0100
     4.3 @@ -20,7 +20,7 @@
     4.4    ba 1;
     4.5  qed "le_prod_trans";
     4.6  
     4.7 -goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)";
     4.8 +goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
     4.9    by (safe_tac (!claset));
    4.10    by (stac Pair_fst_snd_eq 1);
    4.11    br conjI 1;
    4.12 @@ -44,7 +44,7 @@
    4.13    by (Fast_tac 1);
    4.14  qed "le_fun_trans";
    4.15  
    4.16 -goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)";
    4.17 +goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
    4.18    by (safe_tac (!claset));
    4.19    br ext 1;
    4.20    br (le_antisym RS mp) 1;
    4.21 @@ -72,7 +72,7 @@
    4.22    br le_trans 1;
    4.23  qed "le_dual_trans";
    4.24  
    4.25 -goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)";
    4.26 +goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
    4.27    by (safe_tac (!claset));
    4.28    br (Rep_dual_inverse RS subst) 1;
    4.29    br sym 1;
    4.30 @@ -83,6 +83,6 @@
    4.31    ba 1;
    4.32  qed "le_dual_antisym";
    4.33  
    4.34 -goalw thy [le_dual_def] "x [= y | y [= (x::'a::lin_order dual)";
    4.35 -  br le_lin 1;
    4.36 -qed "le_dual_lin";
    4.37 +goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
    4.38 +  br le_linear 1;
    4.39 +qed "le_dual_linear";
     5.1 --- a/src/HOL/AxClasses/Lattice/OrdInsts.thy	Mon Feb 10 16:16:55 1997 +0100
     5.2 +++ b/src/HOL/AxClasses/Lattice/OrdInsts.thy	Wed Feb 12 15:42:31 1997 +0100
     5.3 @@ -14,30 +14,30 @@
     5.4    "*" :: (quasi_order, quasi_order) quasi_order         (le_prod_refl, le_prod_trans)
     5.5  
     5.6  instance
     5.7 -  "*" :: (order, order) order                           (le_prod_antisym)
     5.8 +  "*" :: (partial_order, partial_order) partial_order   (le_prod_antisym)
     5.9    
    5.10  
    5.11  instance
    5.12    fun :: (term, quasi_order) quasi_order                (le_fun_refl, le_fun_trans)
    5.13  
    5.14  instance
    5.15 -  fun :: (term, order) order                            (le_fun_antisym)
    5.16 +  fun :: (term, partial_order) partial_order            (le_fun_antisym)
    5.17  
    5.18  
    5.19 -(* duals of quasi_orders / orders / lin_orders *)
    5.20 +(* duals of quasi orders / partial orders / linear orders *)
    5.21  
    5.22  instance
    5.23    dual :: (quasi_order) quasi_order                     (le_dual_refl, le_dual_trans)
    5.24  
    5.25  instance
    5.26 -  dual :: (order) order                                 (le_dual_antisym)
    5.27 +  dual :: (partial_order) partial_order                 (le_dual_antisym)
    5.28  
    5.29  
    5.30  (*FIXME: had to be moved to LatInsts.thy due to some unpleasant
    5.31    'feature' in Pure/type.ML
    5.32  
    5.33  instance
    5.34 -  dual :: (lin_order) lin_order                         (le_dual_lin)
    5.35 +  dual :: (linear_order) linear_order                   (le_dual_lin)
    5.36  *)
    5.37  
    5.38  end
     6.1 --- a/src/HOL/AxClasses/Lattice/Order.ML	Mon Feb 10 16:16:55 1997 +0100
     6.2 +++ b/src/HOL/AxClasses/Lattice/Order.ML	Wed Feb 12 15:42:31 1997 +0100
     6.3 @@ -114,7 +114,7 @@
     6.4  
     6.5  (** limits in linear orders **)
     6.6  
     6.7 -goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::lin_order) y (minimum x y)";
     6.8 +goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::linear_order) y (minimum x y)";
     6.9    by (stac expand_if 1);
    6.10    by (REPEAT_FIRST (resolve_tac [conjI, impI]));
    6.11    (*case "x [= y"*)
    6.12 @@ -122,7 +122,7 @@
    6.13      ba 1;
    6.14      by (Fast_tac 1);
    6.15    (*case "~ x [= y"*)
    6.16 -    br (le_lin RS disjE) 1;
    6.17 +    br (le_linear RS disjE) 1;
    6.18      ba 1;
    6.19      be notE 1;
    6.20      ba 1;
    6.21 @@ -130,7 +130,7 @@
    6.22      by (Fast_tac 1);
    6.23  qed "min_is_inf";
    6.24  
    6.25 -goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::lin_order) y (maximum x y)";
    6.26 +goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::linear_order) y (maximum x y)";
    6.27    by (stac expand_if 1);
    6.28    by (REPEAT_FIRST (resolve_tac [conjI, impI]));
    6.29    (*case "x [= y"*)
    6.30 @@ -139,7 +139,7 @@
    6.31      by (Fast_tac 1);
    6.32    (*case "~ x [= y"*)
    6.33      br le_refl 1;
    6.34 -    br (le_lin RS disjE) 1;
    6.35 +    br (le_linear RS disjE) 1;
    6.36      ba 1;
    6.37      be notE 1;
    6.38      ba 1;
     7.1 --- a/src/HOL/AxClasses/Lattice/Order.thy	Mon Feb 10 16:16:55 1997 +0100
     7.2 +++ b/src/HOL/AxClasses/Lattice/Order.thy	Wed Feb 12 15:42:31 1997 +0100
     7.3 @@ -31,15 +31,15 @@
     7.4  (* partial orders *)
     7.5  
     7.6  axclass
     7.7 -  order < quasi_order
     7.8 +  partial_order < quasi_order
     7.9    le_antisym    "x [= y & y [= x --> x = y"
    7.10  
    7.11  
    7.12  (* linear orders *)
    7.13  
    7.14  axclass
    7.15 -  lin_order < order
    7.16 -  le_lin        "x [= y | y [= x"
    7.17 +  linear_order < partial_order
    7.18 +  le_linear     "x [= y | y [= x"
    7.19  
    7.20  
    7.21  
    7.22 @@ -49,11 +49,11 @@
    7.23  
    7.24  consts
    7.25    (*binary*)
    7.26 -  is_inf        :: "['a::order, 'a, 'a] => bool"
    7.27 -  is_sup        :: "['a::order, 'a, 'a] => bool"
    7.28 +  is_inf        :: "['a::partial_order, 'a, 'a] => bool"
    7.29 +  is_sup        :: "['a::partial_order, 'a, 'a] => bool"
    7.30    (*general*)
    7.31 -  is_Inf        :: "['a::order set, 'a] => bool"
    7.32 -  is_Sup        :: "['a::order set, 'a] => bool"
    7.33 +  is_Inf        :: "['a::partial_order set, 'a] => bool"
    7.34 +  is_Sup        :: "['a::partial_order set, 'a] => bool"
    7.35  
    7.36  defs
    7.37    is_inf_def    "is_inf x y inf ==
    7.38 @@ -71,13 +71,13 @@
    7.39  
    7.40  
    7.41  
    7.42 -(* binary minima and maxima (on lin_orders) *)
    7.43 +(* binary minima and maxima (on linear_orders) *)
    7.44  
    7.45  constdefs
    7.46 -  minimum      :: "['a::lin_order, 'a] => 'a"
    7.47 +  minimum      :: "['a::linear_order, 'a] => 'a"
    7.48    "minimum x y == (if x [= y then x else y)"
    7.49  
    7.50 -  maximum      :: "['a::lin_order, 'a] => 'a"
    7.51 +  maximum      :: "['a::linear_order, 'a] => 'a"
    7.52    "maximum x y == (if x [= y then y else x)"
    7.53  
    7.54  end