added this stuff;
authorwenzelm
Mon Jan 15 15:49:21 1996 +0100 (1996-01-15)
changeset 1440de6f18da81bb
parent 1439 1f5949a43e82
child 1441 7fbe815c18ad
added this stuff;
src/HOL/AxClasses/Lattice/CLattice.ML
src/HOL/AxClasses/Lattice/CLattice.thy
src/HOL/AxClasses/Lattice/LatInsts.ML
src/HOL/AxClasses/Lattice/LatInsts.thy
src/HOL/AxClasses/Lattice/LatMorph.ML
src/HOL/AxClasses/Lattice/LatMorph.thy
src/HOL/AxClasses/Lattice/LatPreInsts.ML
src/HOL/AxClasses/Lattice/LatPreInsts.thy
src/HOL/AxClasses/Lattice/Lattice.ML
src/HOL/AxClasses/Lattice/Lattice.thy
src/HOL/AxClasses/Lattice/OrdDefs.ML
src/HOL/AxClasses/Lattice/OrdDefs.thy
src/HOL/AxClasses/Lattice/OrdInsts.thy
src/HOL/AxClasses/Lattice/Order.ML
src/HOL/AxClasses/Lattice/Order.thy
src/HOL/AxClasses/Lattice/ROOT.ML
src/HOL/AxClasses/Lattice/tools.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Mon Jan 15 15:49:21 1996 +0100
     1.3 @@ -0,0 +1,183 @@
     1.4 +
     1.5 +open CLattice;
     1.6 +
     1.7 +
     1.8 +(** basic properties of "Inf" and "Sup" **)
     1.9 +
    1.10 +(* unique existence *)
    1.11 +
    1.12 +goalw thy [Inf_def] "is_Inf A (Inf A)";
    1.13 +  br (ex_Inf RS spec RS selectI1) 1;
    1.14 +qed "Inf_is_Inf";
    1.15 +
    1.16 +goal thy "is_Inf A inf --> Inf A = inf";
    1.17 +  br impI 1;
    1.18 +  br (is_Inf_uniq RS mp) 1;
    1.19 +  br conjI 1;
    1.20 +  br Inf_is_Inf 1;
    1.21 +  ba 1;
    1.22 +qed "Inf_uniq";
    1.23 +
    1.24 +goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
    1.25 +  by (safe_tac HOL_cs);
    1.26 +  by (step_tac HOL_cs 1);
    1.27 +  by (step_tac HOL_cs 1);
    1.28 +  br Inf_is_Inf 1;
    1.29 +  br (Inf_uniq RS mp RS sym) 1;
    1.30 +  ba 1;
    1.31 +qed "ex1_Inf";
    1.32 +
    1.33 +
    1.34 +goalw thy [Sup_def] "is_Sup A (Sup A)";
    1.35 +  br (ex_Sup RS spec RS selectI1) 1;
    1.36 +qed "Sup_is_Sup";
    1.37 +
    1.38 +goal thy "is_Sup A sup --> Sup A = sup";
    1.39 +  br impI 1;
    1.40 +  br (is_Sup_uniq RS mp) 1;
    1.41 +  br conjI 1;
    1.42 +  br Sup_is_Sup 1;
    1.43 +  ba 1;
    1.44 +qed "Sup_uniq";
    1.45 +
    1.46 +goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
    1.47 +  by (safe_tac HOL_cs);
    1.48 +  by (step_tac HOL_cs 1);
    1.49 +  by (step_tac HOL_cs 1);
    1.50 +  br Sup_is_Sup 1;
    1.51 +  br (Sup_uniq RS mp RS sym) 1;
    1.52 +  ba 1;
    1.53 +qed "ex1_Sup";
    1.54 +
    1.55 +
    1.56 +(* "Inf" yields g.l.bs, "Sup" yields l.u.bs. --- in pieces *)
    1.57 +
    1.58 +val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
    1.59 +  by (cut_facts_tac prems 1);
    1.60 +  br selectI2 1;
    1.61 +  br Inf_is_Inf 1;
    1.62 +  by (rewrite_goals_tac [is_Inf_def]);
    1.63 +  by (fast_tac set_cs 1);
    1.64 +qed "Inf_lb";
    1.65 +
    1.66 +val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
    1.67 +  br selectI2 1;
    1.68 +  br Inf_is_Inf 1;
    1.69 +  by (rewrite_goals_tac [is_Inf_def]);
    1.70 +  by (step_tac HOL_cs 1);
    1.71 +  by (step_tac HOL_cs 1);
    1.72 +  be mp 1;
    1.73 +  br ballI 1;
    1.74 +  be prem 1;
    1.75 +qed "Inf_ub_lbs";
    1.76 +
    1.77 +
    1.78 +val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
    1.79 +  by (cut_facts_tac prems 1);
    1.80 +  br selectI2 1;
    1.81 +  br Sup_is_Sup 1;
    1.82 +  by (rewrite_goals_tac [is_Sup_def]);
    1.83 +  by (fast_tac set_cs 1);
    1.84 +qed "Sup_ub";
    1.85 +
    1.86 +val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
    1.87 +  br selectI2 1;
    1.88 +  br Sup_is_Sup 1;
    1.89 +  by (rewrite_goals_tac [is_Sup_def]);
    1.90 +  by (step_tac HOL_cs 1);
    1.91 +  by (step_tac HOL_cs 1);
    1.92 +  be mp 1;
    1.93 +  br ballI 1;
    1.94 +  be prem 1;
    1.95 +qed "Sup_lb_ubs";
    1.96 +
    1.97 +
    1.98 +(** minorized Infs / majorized Sups **)
    1.99 +
   1.100 +goal thy "(x [= Inf A) = (ALL y:A. x [= y)";
   1.101 +  br iffI 1;
   1.102 +  (*==>*)
   1.103 +    br ballI 1;
   1.104 +    br (le_trans RS mp) 1;
   1.105 +    be conjI 1;
   1.106 +    be Inf_lb 1;
   1.107 +  (*<==*)
   1.108 +    br Inf_ub_lbs 1;
   1.109 +    by (fast_tac set_cs 1);
   1.110 +qed "le_Inf_eq";
   1.111 +
   1.112 +goal thy "(Sup A [= x) = (ALL y:A. y [= x)";
   1.113 +  br iffI 1;
   1.114 +  (*==>*)
   1.115 +    br ballI 1;
   1.116 +    br (le_trans RS mp) 1;
   1.117 +    br conjI 1;
   1.118 +    be Sup_ub 1;
   1.119 +    ba 1;
   1.120 +  (*<==*)
   1.121 +    br Sup_lb_ubs 1;
   1.122 +    by (fast_tac set_cs 1);
   1.123 +qed "ge_Sup_eq";
   1.124 +
   1.125 +
   1.126 +
   1.127 +(** Subsets and limits **)
   1.128 +
   1.129 +goal thy "A <= B --> Inf B [= Inf A";
   1.130 +  br impI 1;
   1.131 +  by (stac le_Inf_eq 1);
   1.132 +  by (rewrite_goals_tac [Ball_def]);
   1.133 +  by (safe_tac set_cs);
   1.134 +  bd subsetD 1;
   1.135 +  ba 1;
   1.136 +  be Inf_lb 1;
   1.137 +qed "Inf_subset_antimon";
   1.138 +
   1.139 +goal thy "A <= B --> Sup A [= Sup B";
   1.140 +  br impI 1;
   1.141 +  by (stac ge_Sup_eq 1);
   1.142 +  by (rewrite_goals_tac [Ball_def]);
   1.143 +  by (safe_tac set_cs);
   1.144 +  bd subsetD 1;
   1.145 +  ba 1;
   1.146 +  be Sup_ub 1;
   1.147 +qed "Sup_subset_mon";
   1.148 +
   1.149 +
   1.150 +(** singleton / empty limits **)
   1.151 +
   1.152 +goal thy "Inf {x} = x";
   1.153 +  br (Inf_uniq RS mp) 1;
   1.154 +  by (rewrite_goals_tac [is_Inf_def]);
   1.155 +  by (safe_tac set_cs);
   1.156 +  br le_refl 1;
   1.157 +  by (fast_tac set_cs 1);
   1.158 +qed "sing_Inf_eq";
   1.159 +
   1.160 +goal thy "Sup {x} = x";
   1.161 +  br (Sup_uniq RS mp) 1;
   1.162 +  by (rewrite_goals_tac [is_Sup_def]);
   1.163 +  by (safe_tac set_cs);
   1.164 +  br le_refl 1;
   1.165 +  by (fast_tac set_cs 1);
   1.166 +qed "sing_Sup_eq";
   1.167 +
   1.168 +
   1.169 +goal thy "Inf {} = Sup {x. True}";
   1.170 +  br (Inf_uniq RS mp) 1;
   1.171 +  by (rewrite_goals_tac [is_Inf_def]);
   1.172 +  by (safe_tac set_cs);
   1.173 +  br (sing_Sup_eq RS subst) 1;
   1.174 +  back();
   1.175 +  br (Sup_subset_mon RS mp) 1;
   1.176 +  by (fast_tac set_cs 1);
   1.177 +qed "empty_Inf_eq";
   1.178 +
   1.179 +goal thy "Sup {} = Inf {x. True}";
   1.180 +  br (Sup_uniq RS mp) 1;
   1.181 +  by (rewrite_goals_tac [is_Sup_def]);
   1.182 +  by (safe_tac set_cs);
   1.183 +  br (sing_Inf_eq RS subst) 1;
   1.184 +  br (Inf_subset_antimon RS mp) 1;
   1.185 +  by (fast_tac set_cs 1);
   1.186 +qed "empty_Sup_eq";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/AxClasses/Lattice/CLattice.thy	Mon Jan 15 15:49:21 1996 +0100
     2.3 @@ -0,0 +1,27 @@
     2.4 +(*  Title:      CLattice.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Markus Wenzel, TU Muenchen
     2.7 +
     2.8 +Complete lattices are orders with infima and suprema of arbitrary
     2.9 +subsets.
    2.10 +
    2.11 +TODO:
    2.12 +  derive some more well-known theorems (e.g. ex_Inf == ex_Sup)
    2.13 +*)
    2.14 +
    2.15 +CLattice = Order +
    2.16 +
    2.17 +axclass
    2.18 +  clattice < order
    2.19 +  ex_Inf       "ALL A. EX inf. is_Inf A inf"
    2.20 +  ex_Sup       "ALL A. EX sup. is_Sup A sup"
    2.21 +
    2.22 +consts
    2.23 +  Inf           :: "'a::clattice set => 'a"
    2.24 +  Sup           :: "'a::clattice set => 'a"
    2.25 +
    2.26 +defs
    2.27 +  Inf_def       "Inf A == @inf. is_Inf A inf"
    2.28 +  Sup_def       "Sup A == @sup. is_Sup A sup"
    2.29 +
    2.30 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/AxClasses/Lattice/LatInsts.ML	Mon Jan 15 15:49:21 1996 +0100
     3.3 @@ -0,0 +1,98 @@
     3.4 +
     3.5 +open LatInsts;
     3.6 +
     3.7 +
     3.8 +goal thy "Inf {x, y} = x && y";
     3.9 +  br (Inf_uniq RS mp) 1;
    3.10 +  by (stac bin_is_Inf_eq 1);
    3.11 +  br inf_is_inf 1;
    3.12 +qed "bin_Inf_eq";
    3.13 +
    3.14 +goal thy "Sup {x, y} = x || y";
    3.15 +  br (Sup_uniq RS mp) 1;
    3.16 +  by (stac bin_is_Sup_eq 1);
    3.17 +  br sup_is_sup 1;
    3.18 +qed "bin_Sup_eq";
    3.19 +
    3.20 +
    3.21 +
    3.22 +(* Unions and limits *)
    3.23 +
    3.24 +goal thy "Inf (A Un B) = Inf A && Inf B";
    3.25 +  br (Inf_uniq RS mp) 1;
    3.26 +  by (rewrite_goals_tac [is_Inf_def]);
    3.27 +  by (safe_tac set_cs);
    3.28 +
    3.29 +  br (conjI RS (le_trans RS mp)) 1;
    3.30 +  br inf_lb1 1;
    3.31 +  be Inf_lb 1;
    3.32 +
    3.33 +  br (conjI RS (le_trans RS mp)) 1;
    3.34 +  br inf_lb2 1;
    3.35 +  be Inf_lb 1;
    3.36 +
    3.37 +  by (stac le_inf_eq 1);
    3.38 +  br conjI 1;
    3.39 +  br Inf_ub_lbs 1;
    3.40 +  by (fast_tac set_cs 1);
    3.41 +  br Inf_ub_lbs 1;
    3.42 +  by (fast_tac set_cs 1);
    3.43 +qed "Inf_Un_eq";
    3.44 +
    3.45 +goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
    3.46 +  br (Inf_uniq RS mp) 1;
    3.47 +  by (rewrite_goals_tac [is_Inf_def]);
    3.48 +  by (safe_tac set_cs);
    3.49 +  (*level 3*)
    3.50 +  br (conjI RS (le_trans RS mp)) 1;
    3.51 +  be Inf_lb 2;
    3.52 +  br (sing_Inf_eq RS subst) 1;
    3.53 +  br (Inf_subset_antimon RS mp) 1;
    3.54 +  by (fast_tac set_cs 1);
    3.55 +  (*level 8*)
    3.56 +  by (stac le_Inf_eq 1);
    3.57 +  by (safe_tac set_cs);
    3.58 +  by (stac le_Inf_eq 1);
    3.59 +  by (fast_tac set_cs 1);
    3.60 +qed "Inf_UN_eq";
    3.61 +
    3.62 +
    3.63 +
    3.64 +goal thy "Sup (A Un B) = Sup A || Sup B";
    3.65 +  br (Sup_uniq RS mp) 1;
    3.66 +  by (rewrite_goals_tac [is_Sup_def]);
    3.67 +  by (safe_tac set_cs);
    3.68 +
    3.69 +  br (conjI RS (le_trans RS mp)) 1;
    3.70 +  be Sup_ub 1;
    3.71 +  br sup_ub1 1;
    3.72 +
    3.73 +  br (conjI RS (le_trans RS mp)) 1;
    3.74 +  be Sup_ub 1;
    3.75 +  br sup_ub2 1;
    3.76 +
    3.77 +  by (stac ge_sup_eq 1);
    3.78 +  br conjI 1;
    3.79 +  br Sup_lb_ubs 1;
    3.80 +  by (fast_tac set_cs 1);
    3.81 +  br Sup_lb_ubs 1;
    3.82 +  by (fast_tac set_cs 1);
    3.83 +qed "Sup_Un_eq";
    3.84 +
    3.85 +goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
    3.86 +  br (Sup_uniq RS mp) 1;
    3.87 +  by (rewrite_goals_tac [is_Sup_def]);
    3.88 +  by (safe_tac set_cs);
    3.89 +  (*level 3*)
    3.90 +  br (conjI RS (le_trans RS mp)) 1;
    3.91 +  be Sup_ub 1;
    3.92 +  br (sing_Sup_eq RS subst) 1;
    3.93 +  back();
    3.94 +  br (Sup_subset_mon RS mp) 1;
    3.95 +  by (fast_tac set_cs 1);
    3.96 +  (*level 8*)
    3.97 +  by (stac ge_Sup_eq 1);
    3.98 +  by (safe_tac set_cs);
    3.99 +  by (stac ge_Sup_eq 1);
   3.100 +  by (fast_tac set_cs 1);
   3.101 +qed "Sup_UN_eq";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/AxClasses/Lattice/LatInsts.thy	Mon Jan 15 15:49:21 1996 +0100
     4.3 @@ -0,0 +1,41 @@
     4.4 +(*  Title:      LatInsts.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Markus Wenzel, TU Muenchen
     4.7 +
     4.8 +Some lattice instantiations.
     4.9 +*)
    4.10 +
    4.11 +LatInsts = LatPreInsts +
    4.12 +
    4.13 +
    4.14 +(* linear orders are lattices *)
    4.15 +
    4.16 +instance
    4.17 +  lin_order < lattice                   (allI, exI, min_is_inf, max_is_sup)
    4.18 +
    4.19 +
    4.20 +(* complete lattices are lattices *)
    4.21 +
    4.22 +instance
    4.23 +  clattice < lattice                    (allI, exI, Inf_is_inf, Sup_is_sup)
    4.24 +
    4.25 +
    4.26 +(* products of lattices are lattices *)
    4.27 +
    4.28 +instance
    4.29 +  "*" :: (lattice, lattice) lattice     (allI, exI, prod_is_inf, prod_is_sup)
    4.30 +
    4.31 +instance
    4.32 +  fun :: (term, lattice) lattice        (allI, exI, fun_is_inf, fun_is_sup)
    4.33 +
    4.34 +
    4.35 +(* duals of lattices are lattices *)
    4.36 +
    4.37 +instance
    4.38 +  dual :: (lattice) lattice             (allI, exI, dual_is_inf, dual_is_sup)
    4.39 +
    4.40 +(*FIXME bug workaround (see also OrdInsts.thy)*)
    4.41 +instance
    4.42 +  dual :: (lin_order) lin_order         (le_dual_lin)
    4.43 +
    4.44 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/AxClasses/Lattice/LatMorph.ML	Mon Jan 15 15:49:21 1996 +0100
     5.3 @@ -0,0 +1,53 @@
     5.4 +
     5.5 +open LatMorph;
     5.6 +
     5.7 +
     5.8 +(** monotone functions vs. "&&"- / "||"-semi-morphisms **)
     5.9 +
    5.10 +goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
    5.11 +  by (safe_tac set_cs);
    5.12 +  (*==> (level 1)*)
    5.13 +    by (stac le_inf_eq 1);
    5.14 +    br conjI 1;
    5.15 +    by (step_tac set_cs 1);
    5.16 +    by (step_tac set_cs 1);
    5.17 +    be mp 1;
    5.18 +    br inf_lb1 1;
    5.19 +    by (step_tac set_cs 1);
    5.20 +    by (step_tac set_cs 1);
    5.21 +    be mp 1;
    5.22 +    br inf_lb2 1;
    5.23 +  (*==> (level 11)*)
    5.24 +    br (conjI RS (le_trans RS mp)) 1;
    5.25 +    br inf_lb2 2;
    5.26 +    by (subgoal_tac "x && y = x" 1);
    5.27 +    be subst 1;
    5.28 +    by (fast_tac set_cs 1);
    5.29 +    by (stac inf_connect 1);
    5.30 +    ba 1;
    5.31 +qed "mono_inf_eq";
    5.32 +
    5.33 +goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
    5.34 +  by (safe_tac set_cs);
    5.35 +  (*==> (level 1)*)
    5.36 +    by (stac ge_sup_eq 1);
    5.37 +    br conjI 1;
    5.38 +    by (step_tac set_cs 1);
    5.39 +    by (step_tac set_cs 1);
    5.40 +    be mp 1;
    5.41 +    br sup_ub1 1;
    5.42 +    by (step_tac set_cs 1);
    5.43 +    by (step_tac set_cs 1);
    5.44 +    be mp 1;
    5.45 +    br sup_ub2 1;
    5.46 +  (*==> (level 11)*)
    5.47 +    br (conjI RS (le_trans RS mp)) 1;
    5.48 +    br sup_ub1 1;
    5.49 +    by (subgoal_tac "x || y = y" 1);
    5.50 +    be subst 1;
    5.51 +    by (fast_tac set_cs 1);
    5.52 +    by (stac sup_connect 1);
    5.53 +    ba 1;
    5.54 +qed "mono_sup_eq";
    5.55 +
    5.56 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/AxClasses/Lattice/LatMorph.thy	Mon Jan 15 15:49:21 1996 +0100
     6.3 @@ -0,0 +1,28 @@
     6.4 +(*  Title:      LatMorph.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Markus Wenzel, TU Muenchen
     6.7 +
     6.8 +Some lattice morphisms.
     6.9 +
    6.10 +TODO:
    6.11 +  more morphisms (?)
    6.12 +  more theorems
    6.13 +*)
    6.14 +
    6.15 +LatMorph = LatInsts +
    6.16 +
    6.17 +consts
    6.18 +  is_mono       :: "('a::le => 'b::le) => bool"
    6.19 +  is_inf_morph  :: "('a::lattice => 'b::lattice) => bool"
    6.20 +  is_sup_morph  :: "('a::lattice => 'b::lattice) => bool"
    6.21 +  is_Inf_morph  :: "('a::clattice => 'b::clattice) => bool"
    6.22 +  is_Sup_morph  :: "('a::clattice => 'b::clattice) => bool"
    6.23 +
    6.24 +defs
    6.25 +  is_mono_def       "is_mono f == ALL x y. x [= y --> f x [= f y"
    6.26 +  is_inf_morph_def  "is_inf_morph f == ALL x y. f (x && y) = f x && f y"
    6.27 +  is_sup_morph_def  "is_sup_morph f == ALL x y. f (x || y) = f x || f y"
    6.28 +  is_Inf_morph_def  "is_Inf_morph f == ALL A. f (Inf A) = Inf {f x |x. x:A}"
    6.29 +  is_Sup_morph_def  "is_Sup_morph f == ALL A. f (Sup A) = Sup {f x |x. x:A}"
    6.30 +
    6.31 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Mon Jan 15 15:49:21 1996 +0100
     7.3 @@ -0,0 +1,76 @@
     7.4 +
     7.5 +open LatPreInsts;
     7.6 +
     7.7 +
     7.8 +(** complete lattices **)
     7.9 +
    7.10 +goal thy "is_inf x y (Inf {x, y})";
    7.11 +  br (bin_is_Inf_eq RS subst) 1;
    7.12 +  br Inf_is_Inf 1;
    7.13 +qed "Inf_is_inf";
    7.14 +
    7.15 +goal thy "is_sup x y (Sup {x, y})";
    7.16 +  br (bin_is_Sup_eq RS subst) 1;
    7.17 +  br Sup_is_Sup 1;
    7.18 +qed "Sup_is_sup";
    7.19 +
    7.20 +
    7.21 +
    7.22 +(** product lattices **)
    7.23 +
    7.24 +(* pairs *)
    7.25 +
    7.26 +goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
    7.27 +  by (simp_tac prod_ss 1);
    7.28 +  by (safe_tac HOL_cs);
    7.29 +  by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
    7.30 +qed "prod_is_inf";
    7.31 +
    7.32 +goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
    7.33 +  by (simp_tac prod_ss 1);
    7.34 +  by (safe_tac HOL_cs);
    7.35 +  by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
    7.36 +qed "prod_is_sup";
    7.37 +
    7.38 +
    7.39 +(* functions *)
    7.40 +
    7.41 +goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
    7.42 +  by (safe_tac HOL_cs);
    7.43 +  br inf_lb1 1;
    7.44 +  br inf_lb2 1;
    7.45 +  br inf_ub_lbs 1;
    7.46 +  by (REPEAT_FIRST (fast_tac HOL_cs));
    7.47 +qed "fun_is_inf";
    7.48 +
    7.49 +goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
    7.50 +  by (safe_tac HOL_cs);
    7.51 +  br sup_ub1 1;
    7.52 +  br sup_ub2 1;
    7.53 +  br sup_lb_ubs 1;
    7.54 +  by (REPEAT_FIRST (fast_tac HOL_cs));
    7.55 +qed "fun_is_sup";
    7.56 +
    7.57 +
    7.58 +
    7.59 +(** dual lattices **)
    7.60 +
    7.61 +goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
    7.62 +  by (stac Abs_dual_inverse' 1);
    7.63 +  by (safe_tac HOL_cs);
    7.64 +  br sup_ub1 1;
    7.65 +  br sup_ub2 1;
    7.66 +  br sup_lb_ubs 1;
    7.67 +  ba 1;
    7.68 +  ba 1;
    7.69 +qed "dual_is_inf";
    7.70 +
    7.71 +goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
    7.72 +  by (stac Abs_dual_inverse' 1);
    7.73 +  by (safe_tac HOL_cs);
    7.74 +  br inf_lb1 1;
    7.75 +  br inf_lb2 1;
    7.76 +  br inf_ub_lbs 1;
    7.77 +  ba 1;
    7.78 +  ba 1;
    7.79 +qed "dual_is_sup";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/AxClasses/Lattice/LatPreInsts.thy	Mon Jan 15 15:49:21 1996 +0100
     8.3 @@ -0,0 +1,6 @@
     8.4 +(*  Title:      LatPreInsts.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     Markus Wenzel, TU Muenchen
     8.7 +*)
     8.8 +
     8.9 +LatPreInsts = OrdInsts + Lattice + CLattice
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/AxClasses/Lattice/Lattice.ML	Mon Jan 15 15:49:21 1996 +0100
     9.3 @@ -0,0 +1,269 @@
     9.4 +
     9.5 +open Lattice;
     9.6 +
     9.7 +
     9.8 +(** basic properties of "&&" and "||" **)
     9.9 +
    9.10 +(* unique existence *)
    9.11 +
    9.12 +goalw thy [inf_def] "is_inf x y (x && y)";
    9.13 +  br (ex_inf RS spec RS spec RS selectI1) 1;
    9.14 +qed "inf_is_inf";
    9.15 +
    9.16 +goal thy "is_inf x y inf --> x && y = inf";
    9.17 +  br impI 1;
    9.18 +  br (is_inf_uniq RS mp) 1;
    9.19 +  br conjI 1;
    9.20 +  br inf_is_inf 1;
    9.21 +  ba 1;
    9.22 +qed "inf_uniq";
    9.23 +
    9.24 +goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf";
    9.25 +  by (safe_tac HOL_cs);
    9.26 +  by (step_tac HOL_cs 1);
    9.27 +  by (step_tac HOL_cs 1);
    9.28 +  br inf_is_inf 1;
    9.29 +  br (inf_uniq RS mp RS sym) 1;
    9.30 +  ba 1;
    9.31 +qed "ex1_inf";
    9.32 +
    9.33 +
    9.34 +goalw thy [sup_def] "is_sup x y (x || y)";
    9.35 +  br (ex_sup RS spec RS spec RS selectI1) 1;
    9.36 +qed "sup_is_sup";
    9.37 +
    9.38 +goal thy "is_sup x y sup --> x || y = sup";
    9.39 +  br impI 1;
    9.40 +  br (is_sup_uniq RS mp) 1;
    9.41 +  br conjI 1;
    9.42 +  br sup_is_sup 1;
    9.43 +  ba 1;
    9.44 +qed "sup_uniq";
    9.45 +
    9.46 +goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup";
    9.47 +  by (safe_tac HOL_cs);
    9.48 +  by (step_tac HOL_cs 1);
    9.49 +  by (step_tac HOL_cs 1);
    9.50 +  br sup_is_sup 1;
    9.51 +  br (sup_uniq RS mp RS sym) 1;
    9.52 +  ba 1;
    9.53 +qed "ex1_sup";
    9.54 +
    9.55 +
    9.56 +(* "&&" yields g.l.bs, "||" yields l.u.bs. --- in pieces *)
    9.57 +
    9.58 +val tac =
    9.59 +  cut_facts_tac [inf_is_inf] 1 THEN
    9.60 +  rewrite_goals_tac [inf_def, is_inf_def] THEN
    9.61 +  fast_tac HOL_cs 1;
    9.62 +
    9.63 +goal thy "x && y [= x";
    9.64 +  by tac;
    9.65 +qed "inf_lb1";
    9.66 +
    9.67 +goal thy "x && y [= y";
    9.68 +  by tac;
    9.69 +qed "inf_lb2";
    9.70 +
    9.71 +val prems = goal thy "[| z [= x; z [= y |] ==> z [= x && y";
    9.72 +  by (cut_facts_tac prems 1);
    9.73 +  by tac;
    9.74 +qed "inf_ub_lbs";
    9.75 +
    9.76 +
    9.77 +val tac =
    9.78 +  cut_facts_tac [sup_is_sup] 1 THEN
    9.79 +  rewrite_goals_tac [sup_def, is_sup_def] THEN
    9.80 +  fast_tac HOL_cs 1;
    9.81 +
    9.82 +goal thy "x [= x || y";
    9.83 +  by tac;
    9.84 +qed "sup_ub1";
    9.85 +
    9.86 +goal thy "y [= x || y";
    9.87 +  by tac;
    9.88 +qed "sup_ub2";
    9.89 +
    9.90 +val prems = goal thy "[| x [= z; y [= z |] ==> x || y [= z";
    9.91 +  by (cut_facts_tac prems 1);
    9.92 +  by tac;
    9.93 +qed "sup_lb_ubs";
    9.94 +
    9.95 +
    9.96 +
    9.97 +(** some equations concerning "&&" and "||" vs. "[=" **)
    9.98 +
    9.99 +(* the Connection Theorems: "[=" expressed via "&&" or "||" *)
   9.100 +
   9.101 +goal thy "(x && y = x) = (x [= y)";
   9.102 +  br iffI 1;
   9.103 +  (*==>*)
   9.104 +    be subst 1;
   9.105 +    br inf_lb2 1;
   9.106 +  (*<==*)
   9.107 +    br (inf_uniq RS mp) 1;
   9.108 +    by (rewrite_goals_tac [is_inf_def]);
   9.109 +    by (REPEAT_FIRST (rtac conjI));
   9.110 +    br le_refl 1;
   9.111 +    ba 1;
   9.112 +    by (fast_tac HOL_cs 1);
   9.113 +qed "inf_connect";
   9.114 +
   9.115 +goal thy "(x || y = y) = (x [= y)";
   9.116 +  br iffI 1;
   9.117 +  (*==>*)
   9.118 +    be subst 1;
   9.119 +    br sup_ub1 1;
   9.120 +  (*<==*)
   9.121 +    br (sup_uniq RS mp) 1;
   9.122 +    by (rewrite_goals_tac [is_sup_def]);
   9.123 +    by (REPEAT_FIRST (rtac conjI));
   9.124 +    ba 1;
   9.125 +    br le_refl 1;
   9.126 +    by (fast_tac HOL_cs 1);
   9.127 +qed "sup_connect";
   9.128 +
   9.129 +
   9.130 +(* minorized infs / majorized sups *)
   9.131 +
   9.132 +goal thy "(x [= y && z) = (x [= y & x [= z)";
   9.133 +  br iffI 1;
   9.134 +  (*==> (level 1)*)
   9.135 +    by (cut_facts_tac [inf_lb1, inf_lb2] 1);
   9.136 +    br conjI 1;
   9.137 +    br (le_trans RS mp) 1;
   9.138 +    be conjI 1;
   9.139 +    ba 1;
   9.140 +    br (le_trans RS mp) 1;
   9.141 +    be conjI 1;
   9.142 +    ba 1;
   9.143 +  (*<== (level 9)*)
   9.144 +    be conjE 1;
   9.145 +    be inf_ub_lbs 1;
   9.146 +    ba 1;
   9.147 +qed "le_inf_eq";
   9.148 +
   9.149 +goal thy "(x || y [= z) = (x [= z & y [= z)";
   9.150 +  br iffI 1;
   9.151 +  (*==> (level 1)*)
   9.152 +    by (cut_facts_tac [sup_ub1, sup_ub2] 1);
   9.153 +    br conjI 1;
   9.154 +    br (le_trans RS mp) 1;
   9.155 +    be conjI 1;
   9.156 +    ba 1;
   9.157 +    br (le_trans RS mp) 1;
   9.158 +    be conjI 1;
   9.159 +    ba 1;
   9.160 +  (*<== (level 9)*)
   9.161 +    be conjE 1;
   9.162 +    be sup_lb_ubs 1;
   9.163 +    ba 1;
   9.164 +qed "ge_sup_eq";
   9.165 +
   9.166 +
   9.167 +(** algebraic properties of "&&" and "||": A, C, I, AB **)
   9.168 +
   9.169 +(* associativity *)
   9.170 +
   9.171 +goal thy "(x && y) && z = x && (y && z)";
   9.172 +  by (stac (inf_uniq RS mp RS sym) 1);
   9.173 +  back();
   9.174 +  back();
   9.175 +  back();
   9.176 +  back();
   9.177 +  back();
   9.178 +  back();
   9.179 +  back();
   9.180 +  back();
   9.181 +  br refl 2;
   9.182 +  br (is_inf_assoc RS mp) 1;
   9.183 +  by (REPEAT_FIRST (rtac conjI));
   9.184 +  by (REPEAT_FIRST (rtac inf_is_inf));
   9.185 +qed "inf_assoc";
   9.186 +
   9.187 +goal thy "(x || y) || z = x || (y || z)";
   9.188 +  by (stac (sup_uniq RS mp RS sym) 1);
   9.189 +  back();
   9.190 +  back();
   9.191 +  back();
   9.192 +  back();
   9.193 +  back();
   9.194 +  back();
   9.195 +  back();
   9.196 +  back();
   9.197 +  br refl 2;
   9.198 +  br (is_sup_assoc RS mp) 1;
   9.199 +  by (REPEAT_FIRST (rtac conjI));
   9.200 +  by (REPEAT_FIRST (rtac sup_is_sup));
   9.201 +qed "sup_assoc";
   9.202 +
   9.203 +
   9.204 +(* commutativity *)
   9.205 +
   9.206 +goalw thy [inf_def] "x && y = y && x";
   9.207 +  by (stac (is_inf_commut RS ext) 1);
   9.208 +  br refl 1;
   9.209 +qed "inf_commut";
   9.210 +
   9.211 +goalw thy [sup_def] "x || y = y || x";
   9.212 +  by (stac (is_sup_commut RS ext) 1);
   9.213 +  br refl 1;
   9.214 +qed "sup_commut";
   9.215 +
   9.216 +
   9.217 +(* idempotency *)
   9.218 +
   9.219 +goal thy "x && x = x";
   9.220 +  by (stac inf_connect 1);
   9.221 +  br le_refl 1;
   9.222 +qed "inf_idemp";
   9.223 +
   9.224 +goal thy "x || x = x";
   9.225 +  by (stac sup_connect 1);
   9.226 +  br le_refl 1;
   9.227 +qed "sup_idemp";
   9.228 +
   9.229 +
   9.230 +(* absorption *)
   9.231 +
   9.232 +goal thy "x || (x && y) = x";
   9.233 +  by (stac sup_commut 1);
   9.234 +  by (stac sup_connect 1);
   9.235 +  br inf_lb1 1;
   9.236 +qed "sup_inf_absorb";
   9.237 +
   9.238 +goal thy "x && (x || y) = x";
   9.239 +  by (stac inf_connect 1);
   9.240 +  br sup_ub1 1;
   9.241 +qed "inf_sup_absorb";
   9.242 +
   9.243 +
   9.244 +(* monotonicity *)
   9.245 +
   9.246 +val prems = goal thy "[| a [= b; x [= y |] ==> a && x [= b && y";
   9.247 +  by (cut_facts_tac prems 1);
   9.248 +  by (stac le_inf_eq 1);
   9.249 +  br conjI 1;
   9.250 +  br (le_trans RS mp) 1;
   9.251 +  br conjI 1;
   9.252 +  br inf_lb1 1;
   9.253 +  ba 1;
   9.254 +  br (le_trans RS mp) 1;
   9.255 +  br conjI 1;
   9.256 +  br inf_lb2 1;
   9.257 +  ba 1;
   9.258 +qed "inf_mon";
   9.259 +
   9.260 +val prems = goal thy "[| a [= b; x [= y |] ==> a || x [= b || y";
   9.261 +  by (cut_facts_tac prems 1);
   9.262 +  by (stac ge_sup_eq 1);
   9.263 +  br conjI 1;
   9.264 +  br (le_trans RS mp) 1;
   9.265 +  br conjI 1;
   9.266 +  ba 1;
   9.267 +  br sup_ub1 1;
   9.268 +  br (le_trans RS mp) 1;
   9.269 +  br conjI 1;
   9.270 +  ba 1;
   9.271 +  br sup_ub2 1;
   9.272 +qed "sup_mon";
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/AxClasses/Lattice/Lattice.thy	Mon Jan 15 15:49:21 1996 +0100
    10.3 @@ -0,0 +1,23 @@
    10.4 +(*  Title:      Lattice.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Markus Wenzel, TU Muenchen
    10.7 +
    10.8 +Lattices are orders with binary (finitary) infima and suprema.
    10.9 +*)
   10.10 +
   10.11 +Lattice = Order +
   10.12 +
   10.13 +axclass
   10.14 +  lattice < order
   10.15 +  ex_inf       "ALL x y. EX inf. is_inf x y inf"
   10.16 +  ex_sup       "ALL x y. EX sup. is_sup x y sup"
   10.17 +
   10.18 +consts
   10.19 +  "&&"          :: "['a::lattice, 'a] => 'a"       (infixl 70)
   10.20 +  "||"          :: "['a::lattice, 'a] => 'a"       (infixl 65)
   10.21 +
   10.22 +defs
   10.23 +  inf_def       "x && y == @inf. is_inf x y inf"
   10.24 +  sup_def       "x || y == @sup. is_sup x y sup"
   10.25 +
   10.26 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Mon Jan 15 15:49:21 1996 +0100
    11.3 @@ -0,0 +1,88 @@
    11.4 +
    11.5 +open OrdDefs;
    11.6 +
    11.7 +
    11.8 +(** lifting of quasi / partial orders **)
    11.9 +
   11.10 +(* pairs *)
   11.11 +
   11.12 +goalw thy [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)";
   11.13 +  br conjI 1;
   11.14 +  br le_refl 1;
   11.15 +  br le_refl 1;
   11.16 +qed "le_prod_refl";
   11.17 +
   11.18 +goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
   11.19 +  by (safe_tac HOL_cs);
   11.20 +  be (conjI RS (le_trans RS mp)) 1;
   11.21 +  ba 1;
   11.22 +  be (conjI RS (le_trans RS mp)) 1;
   11.23 +  ba 1;
   11.24 +qed "le_prod_trans";
   11.25 +
   11.26 +goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)";
   11.27 +  by (safe_tac HOL_cs);
   11.28 +  by (stac Pair_fst_snd_eq 1);
   11.29 +  br conjI 1;
   11.30 +  be (conjI RS (le_antisym RS mp)) 1;
   11.31 +  ba 1;
   11.32 +  be (conjI RS (le_antisym RS mp)) 1;
   11.33 +  ba 1;
   11.34 +qed "le_prod_antisym";
   11.35 +
   11.36 +
   11.37 +(* functions *)
   11.38 +
   11.39 +goalw thy [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
   11.40 +  br allI 1;
   11.41 +  br le_refl 1;
   11.42 +qed "le_fun_refl";
   11.43 +
   11.44 +goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
   11.45 +  by (safe_tac HOL_cs);
   11.46 +  br (le_trans RS mp) 1;
   11.47 +  by (fast_tac HOL_cs 1);
   11.48 +qed "le_fun_trans";
   11.49 +
   11.50 +goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)";
   11.51 +  by (safe_tac HOL_cs);
   11.52 +  br ext 1;
   11.53 +  br (le_antisym RS mp) 1;
   11.54 +  by (fast_tac HOL_cs 1);
   11.55 +qed "le_fun_antisym";
   11.56 +
   11.57 +
   11.58 +
   11.59 +(** duals **)
   11.60 +
   11.61 +(*"'a dual" is even an isotype*)
   11.62 +goal thy "Rep_dual (Abs_dual y) = y";
   11.63 +  br Abs_dual_inverse 1;
   11.64 +  by (rewrite_goals_tac [dual_def]);
   11.65 +  by (fast_tac set_cs 1);
   11.66 +qed "Abs_dual_inverse'";
   11.67 +
   11.68 +
   11.69 +goalw thy [le_dual_def] "x [= (x::'a::quasi_order dual)";
   11.70 +  br le_refl 1;
   11.71 +qed "le_dual_refl";
   11.72 +
   11.73 +goalw thy [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
   11.74 +  by (stac conj_commut 1);
   11.75 +  br le_trans 1;
   11.76 +qed "le_dual_trans";
   11.77 +
   11.78 +goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)";
   11.79 +  by (safe_tac prop_cs);
   11.80 +  br (Rep_dual_inverse RS subst) 1;
   11.81 +  br sym 1;
   11.82 +  br (Rep_dual_inverse RS subst) 1;
   11.83 +  br arg_cong 1;
   11.84 +  back();
   11.85 +  be (conjI RS (le_antisym RS mp)) 1;
   11.86 +  ba 1;
   11.87 +qed "le_dual_antisym";
   11.88 +
   11.89 +goalw thy [le_dual_def] "x [= y | y [= (x::'a::lin_order dual)";
   11.90 +  br le_lin 1;
   11.91 +qed "le_dual_lin";
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.thy	Mon Jan 15 15:49:21 1996 +0100
    12.3 @@ -0,0 +1,35 @@
    12.4 +(*  Title:      OrdDefs.thy
    12.5 +    ID:         $Id$
    12.6 +    Author:     Markus Wenzel, TU Muenchen
    12.7 +
    12.8 +Some overloaded definitions.
    12.9 +*)
   12.10 +
   12.11 +OrdDefs = Order + Prod +
   12.12 +
   12.13 +
   12.14 +(* binary / general products *)
   12.15 +
   12.16 +instance
   12.17 +  "*" :: (le, le) le
   12.18 +
   12.19 +instance
   12.20 +  fun :: (term, le) le
   12.21 +
   12.22 +defs
   12.23 +  le_prod_def   "p [= q == fst p [= fst q & snd p [= snd q"
   12.24 +  le_fun_def    "f [= g == ALL x. f x [= g x"
   12.25 +
   12.26 +
   12.27 +(* duals *)
   12.28 +
   12.29 +subtype
   12.30 +  'a dual = "{x::'a. True}"
   12.31 +
   12.32 +instance
   12.33 +  dual :: (le) le
   12.34 +
   12.35 +defs
   12.36 +  le_dual_def   "x [= y == Rep_dual y [= Rep_dual x"
   12.37 +
   12.38 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/AxClasses/Lattice/OrdInsts.thy	Mon Jan 15 15:49:21 1996 +0100
    13.3 @@ -0,0 +1,43 @@
    13.4 +(*  Title:      OrdInsts.thy
    13.5 +    ID:         $Id$
    13.6 +    Author:     Markus Wenzel, TU Muenchen
    13.7 +
    13.8 +Some order instantiations.
    13.9 +*)
   13.10 +
   13.11 +OrdInsts = OrdDefs +
   13.12 +
   13.13 +
   13.14 +(* binary / general products of quasi_orders / orders *)
   13.15 +
   13.16 +instance
   13.17 +  "*" :: (quasi_order, quasi_order) quasi_order         (le_prod_refl, le_prod_trans)
   13.18 +
   13.19 +instance
   13.20 +  "*" :: (order, order) order                           (le_prod_antisym)
   13.21 +  
   13.22 +
   13.23 +instance
   13.24 +  fun :: (term, quasi_order) quasi_order                (le_fun_refl, le_fun_trans)
   13.25 +
   13.26 +instance
   13.27 +  fun :: (term, order) order                            (le_fun_antisym)
   13.28 +
   13.29 +
   13.30 +(* duals of quasi_orders / orders / lin_orders *)
   13.31 +
   13.32 +instance
   13.33 +  dual :: (quasi_order) quasi_order                     (le_dual_refl, le_dual_trans)
   13.34 +
   13.35 +instance
   13.36 +  dual :: (order) order                                 (le_dual_antisym)
   13.37 +
   13.38 +
   13.39 +(*FIXME: had to be moved to LatInsts.thy due to some unpleasant
   13.40 +  'feature' in Pure/type.ML
   13.41 +
   13.42 +instance
   13.43 +  dual :: (lin_order) lin_order                         (le_dual_lin)
   13.44 +*)
   13.45 +
   13.46 +end
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/AxClasses/Lattice/Order.ML	Mon Jan 15 15:49:21 1996 +0100
    14.3 @@ -0,0 +1,173 @@
    14.4 +
    14.5 +open Order;
    14.6 +
    14.7 +
    14.8 +(** basic properties of limits **)
    14.9 +
   14.10 +(* uniqueness *)
   14.11 +
   14.12 +val tac =
   14.13 +  rtac impI 1 THEN
   14.14 +  rtac (le_antisym RS mp) 1 THEN
   14.15 +  fast_tac HOL_cs 1;
   14.16 +
   14.17 +
   14.18 +goalw thy [is_inf_def] "is_inf x y inf & is_inf x y inf' --> inf = inf'";
   14.19 +  by tac;
   14.20 +qed "is_inf_uniq";
   14.21 +
   14.22 +goalw thy [is_sup_def] "is_sup x y sup & is_sup x y sup' --> sup = sup'";
   14.23 +  by tac;
   14.24 +qed "is_sup_uniq";
   14.25 +
   14.26 +
   14.27 +goalw thy [is_Inf_def] "is_Inf A inf & is_Inf A inf' --> inf = inf'";
   14.28 +  by tac;
   14.29 +qed "is_Inf_uniq";
   14.30 +
   14.31 +goalw thy [is_Sup_def] "is_Sup A sup & is_Sup A sup' --> sup = sup'";
   14.32 +  by tac;
   14.33 +qed "is_Sup_uniq";
   14.34 +
   14.35 +
   14.36 +
   14.37 +(* commutativity *)
   14.38 +
   14.39 +goalw thy [is_inf_def] "is_inf x y inf = is_inf y x inf";
   14.40 +  by (fast_tac HOL_cs 1);
   14.41 +qed "is_inf_commut";
   14.42 +
   14.43 +goalw thy [is_sup_def] "is_sup x y sup = is_sup y x sup";
   14.44 +  by (fast_tac HOL_cs 1);
   14.45 +qed "is_sup_commut";
   14.46 +
   14.47 +
   14.48 +(* associativity *)
   14.49 +
   14.50 +goalw thy [is_inf_def] "is_inf x y xy & is_inf y z yz & is_inf xy z xyz --> is_inf x yz xyz";
   14.51 +  by (safe_tac HOL_cs);
   14.52 +  (*level 1*)
   14.53 +    br (le_trans RS mp) 1;
   14.54 +    be conjI 1;
   14.55 +    ba 1;
   14.56 +  (*level 4*)
   14.57 +    by (step_tac HOL_cs 1);
   14.58 +    back();
   14.59 +    be mp 1;
   14.60 +    br conjI 1;
   14.61 +    br (le_trans RS mp) 1;
   14.62 +    be conjI 1;
   14.63 +    ba 1;
   14.64 +    ba 1;
   14.65 +  (*level 11*)
   14.66 +    by (step_tac HOL_cs 1);
   14.67 +    back();
   14.68 +    back();
   14.69 +    be mp 1;
   14.70 +    br conjI 1;
   14.71 +    by (step_tac HOL_cs 1);
   14.72 +    be mp 1;
   14.73 +    be conjI 1;
   14.74 +    br (le_trans RS mp) 1;
   14.75 +    be conjI 1;
   14.76 +    ba 1;
   14.77 +    br (le_trans RS mp) 1;
   14.78 +    be conjI 1;
   14.79 +    back();     (* !! *)
   14.80 +    ba 1;
   14.81 +qed "is_inf_assoc";
   14.82 +
   14.83 +
   14.84 +goalw thy [is_sup_def] "is_sup x y xy & is_sup y z yz & is_sup xy z xyz --> is_sup x yz xyz";
   14.85 +  by (safe_tac HOL_cs);
   14.86 +  (*level 1*)
   14.87 +    br (le_trans RS mp) 1;
   14.88 +    be conjI 1;
   14.89 +    ba 1;
   14.90 +  (*level 4*)
   14.91 +    by (step_tac HOL_cs 1);
   14.92 +    back();
   14.93 +    be mp 1;
   14.94 +    br conjI 1;
   14.95 +    br (le_trans RS mp) 1;
   14.96 +    be conjI 1;
   14.97 +    ba 1;
   14.98 +    ba 1;
   14.99 +  (*level 11*)
  14.100 +    by (step_tac HOL_cs 1);
  14.101 +    back();
  14.102 +    back();
  14.103 +    be mp 1;
  14.104 +    br conjI 1;
  14.105 +    by (step_tac HOL_cs 1);
  14.106 +    be mp 1;
  14.107 +    be conjI 1;
  14.108 +    br (le_trans RS mp) 1;
  14.109 +    be conjI 1;
  14.110 +    back();     (* !! *)
  14.111 +    ba 1;
  14.112 +    br (le_trans RS mp) 1;
  14.113 +    be conjI 1;
  14.114 +    ba 1;
  14.115 +qed "is_sup_assoc";
  14.116 +
  14.117 +
  14.118 +(** limits in linear orders **)
  14.119 +
  14.120 +goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::lin_order) y (minimum x y)";
  14.121 +  by (stac expand_if 1);
  14.122 +  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
  14.123 +  (*case "x [= y"*)
  14.124 +    br le_refl 1;
  14.125 +    ba 1;
  14.126 +    by (fast_tac HOL_cs 1);
  14.127 +  (*case "~ x [= y"*)
  14.128 +    br (le_lin RS disjE) 1;
  14.129 +    ba 1;
  14.130 +    be notE 1;
  14.131 +    ba 1;
  14.132 +    br le_refl 1;
  14.133 +    by (fast_tac HOL_cs 1);
  14.134 +qed "min_is_inf";
  14.135 +
  14.136 +goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::lin_order) y (maximum x y)";
  14.137 +  by (stac expand_if 1);
  14.138 +  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
  14.139 +  (*case "x [= y"*)
  14.140 +    ba 1;
  14.141 +    br le_refl 1;
  14.142 +    by (fast_tac HOL_cs 1);
  14.143 +  (*case "~ x [= y"*)
  14.144 +    br le_refl 1;
  14.145 +    br (le_lin RS disjE) 1;
  14.146 +    ba 1;
  14.147 +    be notE 1;
  14.148 +    ba 1;
  14.149 +    by (fast_tac HOL_cs 1);
  14.150 +qed "max_is_sup";
  14.151 +
  14.152 +
  14.153 +
  14.154 +(** general vs. binary limits **)
  14.155 +
  14.156 +goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
  14.157 +  br iffI 1;
  14.158 +  (*==>*)
  14.159 +    by (fast_tac set_cs 1);
  14.160 +  (*<==*)
  14.161 +    by (safe_tac set_cs);
  14.162 +    by (step_tac set_cs 1);
  14.163 +    be mp 1;
  14.164 +    by (fast_tac set_cs 1);
  14.165 +qed "bin_is_Inf_eq";
  14.166 +
  14.167 +goalw thy [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
  14.168 +  br iffI 1;
  14.169 +  (*==>*)
  14.170 +    by (fast_tac set_cs 1);
  14.171 +  (*<==*)
  14.172 +    by (safe_tac set_cs);
  14.173 +    by (step_tac set_cs 1);
  14.174 +    be mp 1;
  14.175 +    by (fast_tac set_cs 1);
  14.176 +qed "bin_is_Sup_eq";
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/AxClasses/Lattice/Order.thy	Mon Jan 15 15:49:21 1996 +0100
    15.3 @@ -0,0 +1,83 @@
    15.4 +(*  Title:      Order.thy
    15.5 +    ID:         $Id$
    15.6 +    Author:     Markus Wenzel, TU Muenchen
    15.7 +
    15.8 +Basic theory of orders (quasi orders, partial orders, linear orders)
    15.9 +and limits (inf, sup, min, max).
   15.10 +*)
   15.11 +
   15.12 +Order = HOL + Set +
   15.13 +
   15.14 +
   15.15 +(** class definitions **)
   15.16 +
   15.17 +(* syntax for orders *)
   15.18 +
   15.19 +axclass
   15.20 +  le < term
   15.21 +
   15.22 +consts
   15.23 +  "[="          :: "['a::le, 'a] => bool"             (infixl 50)
   15.24 +
   15.25 +
   15.26 +(* quasi orders *)
   15.27 +
   15.28 +axclass
   15.29 +  quasi_order < le
   15.30 +  le_refl       "x [= x"
   15.31 +  le_trans      "x [= y & y [= z --> x [= z"
   15.32 +
   15.33 +
   15.34 +(* partial orders *)
   15.35 +
   15.36 +axclass
   15.37 +  order < quasi_order
   15.38 +  le_antisym    "x [= y & y [= x --> x = y"
   15.39 +
   15.40 +
   15.41 +(* linear orders *)
   15.42 +
   15.43 +axclass
   15.44 +  lin_order < order
   15.45 +  le_lin        "x [= y | y [= x"
   15.46 +
   15.47 +
   15.48 +
   15.49 +(** limits **)
   15.50 +
   15.51 +(* infima and suprema (on orders) *)
   15.52 +
   15.53 +consts
   15.54 +  (*binary*)
   15.55 +  is_inf        :: "['a::order, 'a, 'a] => bool"
   15.56 +  is_sup        :: "['a::order, 'a, 'a] => bool"
   15.57 +  (*general*)
   15.58 +  is_Inf        :: "['a::order set, 'a] => bool"
   15.59 +  is_Sup        :: "['a::order set, 'a] => bool"
   15.60 +
   15.61 +defs
   15.62 +  is_inf_def    "is_inf x y inf ==
   15.63 +                   inf [= x & inf [= y &
   15.64 +                   (ALL lb. lb [= x & lb [= y --> lb [= inf)"
   15.65 +  is_sup_def    "is_sup x y sup ==
   15.66 +                   x [= sup & y [= sup &
   15.67 +                   (ALL ub. x [= ub & y [= ub --> sup [= ub)"
   15.68 +  is_Inf_def    "is_Inf A inf ==
   15.69 +                   (ALL x:A. inf [= x) &
   15.70 +                   (ALL lb. (ALL x:A. lb [= x) --> lb [= inf)"
   15.71 +  is_Sup_def    "is_Sup A sup ==
   15.72 +                   (ALL x:A. x [= sup) &
   15.73 +                   (ALL ub. (ALL x:A. x [= ub) --> sup [= ub)"
   15.74 +
   15.75 +
   15.76 +(* binary minima and maxima (on lin_orders) *)
   15.77 +
   15.78 +consts
   15.79 +  minimum      :: "['a::lin_order, 'a] => 'a"
   15.80 +  maximum      :: "['a::lin_order, 'a] => 'a"
   15.81 +
   15.82 +defs
   15.83 +  minimum_def  "minimum x y == (if x [= y then x else y)"
   15.84 +  maximum_def  "maximum x y == (if x [= y then y else x)"
   15.85 +
   15.86 +end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/AxClasses/Lattice/ROOT.ML	Mon Jan 15 15:49:21 1996 +0100
    16.3 @@ -0,0 +1,29 @@
    16.4 +(*  Title:      HOL/AxClasses/Lattice/ROOT.ML
    16.5 +    ID:         $Id$
    16.6 +    Author:     Markus Wenzel, TU Muenchen
    16.7 +
    16.8 +Basic theory of lattices and orders via axiomatic type classes.
    16.9 +*)
   16.10 +
   16.11 +open AxClass;
   16.12 +
   16.13 +reset HOL_quantifiers;
   16.14 +reset eta_contract;
   16.15 +set show_types;
   16.16 +set show_sorts;
   16.17 +
   16.18 +use "tools.ML";
   16.19 +
   16.20 +use_thy "Order";
   16.21 +use_thy "OrdDefs";
   16.22 +use_thy "OrdInsts";
   16.23 +
   16.24 +use_thy "Lattice";
   16.25 +use_thy "CLattice";
   16.26 +
   16.27 +use_thy "LatPreInsts";
   16.28 +use_thy "LatInsts";
   16.29 +
   16.30 +use_thy "LatMorph";
   16.31 +
   16.32 +make_chart ();   (*make HTML chart*)
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/AxClasses/Lattice/tools.ML	Mon Jan 15 15:49:21 1996 +0100
    17.3 @@ -0,0 +1,10 @@
    17.4 +
    17.5 +(** generic tools **)
    17.6 +
    17.7 +val prems = goalw HOL.thy [Ex_def] "EX x. P x ==> P (@x. P x)";
    17.8 +  by (resolve_tac prems 1);
    17.9 +qed "selectI1";
   17.10 +
   17.11 +goal HOL.thy "(P & Q) = (Q & P)";
   17.12 +  by (fast_tac prop_cs 1);
   17.13 +qed "conj_commut";