# HG changeset patch
# User wenzelm
# Date 821717361 -3600
# Node ID de6f18da81bb750b11b3dec486fda7b30938838a
# Parent  1f5949a43e8297b92bf1eb8ce74744d96b27dc00
added this stuff;

diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/CLattice.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,183 @@
+
+open CLattice;
+
+
+(** basic properties of "Inf" and "Sup" **)
+
+(* unique existence *)
+
+goalw thy [Inf_def] "is_Inf A (Inf A)";
+  br (ex_Inf RS spec RS selectI1) 1;
+qed "Inf_is_Inf";
+
+goal thy "is_Inf A inf --> Inf A = inf";
+  br impI 1;
+  br (is_Inf_uniq RS mp) 1;
+  br conjI 1;
+  br Inf_is_Inf 1;
+  ba 1;
+qed "Inf_uniq";
+
+goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
+  by (safe_tac HOL_cs);
+  by (step_tac HOL_cs 1);
+  by (step_tac HOL_cs 1);
+  br Inf_is_Inf 1;
+  br (Inf_uniq RS mp RS sym) 1;
+  ba 1;
+qed "ex1_Inf";
+
+
+goalw thy [Sup_def] "is_Sup A (Sup A)";
+  br (ex_Sup RS spec RS selectI1) 1;
+qed "Sup_is_Sup";
+
+goal thy "is_Sup A sup --> Sup A = sup";
+  br impI 1;
+  br (is_Sup_uniq RS mp) 1;
+  br conjI 1;
+  br Sup_is_Sup 1;
+  ba 1;
+qed "Sup_uniq";
+
+goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
+  by (safe_tac HOL_cs);
+  by (step_tac HOL_cs 1);
+  by (step_tac HOL_cs 1);
+  br Sup_is_Sup 1;
+  br (Sup_uniq RS mp RS sym) 1;
+  ba 1;
+qed "ex1_Sup";
+
+
+(* "Inf" yields g.l.bs, "Sup" yields l.u.bs. --- in pieces *)
+
+val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
+  by (cut_facts_tac prems 1);
+  br selectI2 1;
+  br Inf_is_Inf 1;
+  by (rewrite_goals_tac [is_Inf_def]);
+  by (fast_tac set_cs 1);
+qed "Inf_lb";
+
+val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
+  br selectI2 1;
+  br Inf_is_Inf 1;
+  by (rewrite_goals_tac [is_Inf_def]);
+  by (step_tac HOL_cs 1);
+  by (step_tac HOL_cs 1);
+  be mp 1;
+  br ballI 1;
+  be prem 1;
+qed "Inf_ub_lbs";
+
+
+val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
+  by (cut_facts_tac prems 1);
+  br selectI2 1;
+  br Sup_is_Sup 1;
+  by (rewrite_goals_tac [is_Sup_def]);
+  by (fast_tac set_cs 1);
+qed "Sup_ub";
+
+val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
+  br selectI2 1;
+  br Sup_is_Sup 1;
+  by (rewrite_goals_tac [is_Sup_def]);
+  by (step_tac HOL_cs 1);
+  by (step_tac HOL_cs 1);
+  be mp 1;
+  br ballI 1;
+  be prem 1;
+qed "Sup_lb_ubs";
+
+
+(** minorized Infs / majorized Sups **)
+
+goal thy "(x [= Inf A) = (ALL y:A. x [= y)";
+  br iffI 1;
+  (*==>*)
+    br ballI 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    be Inf_lb 1;
+  (*<==*)
+    br Inf_ub_lbs 1;
+    by (fast_tac set_cs 1);
+qed "le_Inf_eq";
+
+goal thy "(Sup A [= x) = (ALL y:A. y [= x)";
+  br iffI 1;
+  (*==>*)
+    br ballI 1;
+    br (le_trans RS mp) 1;
+    br conjI 1;
+    be Sup_ub 1;
+    ba 1;
+  (*<==*)
+    br Sup_lb_ubs 1;
+    by (fast_tac set_cs 1);
+qed "ge_Sup_eq";
+
+
+
+(** Subsets and limits **)
+
+goal thy "A <= B --> Inf B [= Inf A";
+  br impI 1;
+  by (stac le_Inf_eq 1);
+  by (rewrite_goals_tac [Ball_def]);
+  by (safe_tac set_cs);
+  bd subsetD 1;
+  ba 1;
+  be Inf_lb 1;
+qed "Inf_subset_antimon";
+
+goal thy "A <= B --> Sup A [= Sup B";
+  br impI 1;
+  by (stac ge_Sup_eq 1);
+  by (rewrite_goals_tac [Ball_def]);
+  by (safe_tac set_cs);
+  bd subsetD 1;
+  ba 1;
+  be Sup_ub 1;
+qed "Sup_subset_mon";
+
+
+(** singleton / empty limits **)
+
+goal thy "Inf {x} = x";
+  br (Inf_uniq RS mp) 1;
+  by (rewrite_goals_tac [is_Inf_def]);
+  by (safe_tac set_cs);
+  br le_refl 1;
+  by (fast_tac set_cs 1);
+qed "sing_Inf_eq";
+
+goal thy "Sup {x} = x";
+  br (Sup_uniq RS mp) 1;
+  by (rewrite_goals_tac [is_Sup_def]);
+  by (safe_tac set_cs);
+  br le_refl 1;
+  by (fast_tac set_cs 1);
+qed "sing_Sup_eq";
+
+
+goal thy "Inf {} = Sup {x. True}";
+  br (Inf_uniq RS mp) 1;
+  by (rewrite_goals_tac [is_Inf_def]);
+  by (safe_tac set_cs);
+  br (sing_Sup_eq RS subst) 1;
+  back();
+  br (Sup_subset_mon RS mp) 1;
+  by (fast_tac set_cs 1);
+qed "empty_Inf_eq";
+
+goal thy "Sup {} = Inf {x. True}";
+  br (Sup_uniq RS mp) 1;
+  by (rewrite_goals_tac [is_Sup_def]);
+  by (safe_tac set_cs);
+  br (sing_Inf_eq RS subst) 1;
+  br (Inf_subset_antimon RS mp) 1;
+  by (fast_tac set_cs 1);
+qed "empty_Sup_eq";
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/CLattice.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/CLattice.thy	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,27 @@
+(*  Title:      CLattice.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Complete lattices are orders with infima and suprema of arbitrary
+subsets.
+
+TODO:
+  derive some more well-known theorems (e.g. ex_Inf == ex_Sup)
+*)
+
+CLattice = Order +
+
+axclass
+  clattice < order
+  ex_Inf       "ALL A. EX inf. is_Inf A inf"
+  ex_Sup       "ALL A. EX sup. is_Sup A sup"
+
+consts
+  Inf           :: "'a::clattice set => 'a"
+  Sup           :: "'a::clattice set => 'a"
+
+defs
+  Inf_def       "Inf A == @inf. is_Inf A inf"
+  Sup_def       "Sup A == @sup. is_Sup A sup"
+
+end
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/LatInsts.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/LatInsts.ML	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,98 @@
+
+open LatInsts;
+
+
+goal thy "Inf {x, y} = x && y";
+  br (Inf_uniq RS mp) 1;
+  by (stac bin_is_Inf_eq 1);
+  br inf_is_inf 1;
+qed "bin_Inf_eq";
+
+goal thy "Sup {x, y} = x || y";
+  br (Sup_uniq RS mp) 1;
+  by (stac bin_is_Sup_eq 1);
+  br sup_is_sup 1;
+qed "bin_Sup_eq";
+
+
+
+(* Unions and limits *)
+
+goal thy "Inf (A Un B) = Inf A && Inf B";
+  br (Inf_uniq RS mp) 1;
+  by (rewrite_goals_tac [is_Inf_def]);
+  by (safe_tac set_cs);
+
+  br (conjI RS (le_trans RS mp)) 1;
+  br inf_lb1 1;
+  be Inf_lb 1;
+
+  br (conjI RS (le_trans RS mp)) 1;
+  br inf_lb2 1;
+  be Inf_lb 1;
+
+  by (stac le_inf_eq 1);
+  br conjI 1;
+  br Inf_ub_lbs 1;
+  by (fast_tac set_cs 1);
+  br Inf_ub_lbs 1;
+  by (fast_tac set_cs 1);
+qed "Inf_Un_eq";
+
+goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
+  br (Inf_uniq RS mp) 1;
+  by (rewrite_goals_tac [is_Inf_def]);
+  by (safe_tac set_cs);
+  (*level 3*)
+  br (conjI RS (le_trans RS mp)) 1;
+  be Inf_lb 2;
+  br (sing_Inf_eq RS subst) 1;
+  br (Inf_subset_antimon RS mp) 1;
+  by (fast_tac set_cs 1);
+  (*level 8*)
+  by (stac le_Inf_eq 1);
+  by (safe_tac set_cs);
+  by (stac le_Inf_eq 1);
+  by (fast_tac set_cs 1);
+qed "Inf_UN_eq";
+
+
+
+goal thy "Sup (A Un B) = Sup A || Sup B";
+  br (Sup_uniq RS mp) 1;
+  by (rewrite_goals_tac [is_Sup_def]);
+  by (safe_tac set_cs);
+
+  br (conjI RS (le_trans RS mp)) 1;
+  be Sup_ub 1;
+  br sup_ub1 1;
+
+  br (conjI RS (le_trans RS mp)) 1;
+  be Sup_ub 1;
+  br sup_ub2 1;
+
+  by (stac ge_sup_eq 1);
+  br conjI 1;
+  br Sup_lb_ubs 1;
+  by (fast_tac set_cs 1);
+  br Sup_lb_ubs 1;
+  by (fast_tac set_cs 1);
+qed "Sup_Un_eq";
+
+goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
+  br (Sup_uniq RS mp) 1;
+  by (rewrite_goals_tac [is_Sup_def]);
+  by (safe_tac set_cs);
+  (*level 3*)
+  br (conjI RS (le_trans RS mp)) 1;
+  be Sup_ub 1;
+  br (sing_Sup_eq RS subst) 1;
+  back();
+  br (Sup_subset_mon RS mp) 1;
+  by (fast_tac set_cs 1);
+  (*level 8*)
+  by (stac ge_Sup_eq 1);
+  by (safe_tac set_cs);
+  by (stac ge_Sup_eq 1);
+  by (fast_tac set_cs 1);
+qed "Sup_UN_eq";
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/LatInsts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/LatInsts.thy	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,41 @@
+(*  Title:      LatInsts.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Some lattice instantiations.
+*)
+
+LatInsts = LatPreInsts +
+
+
+(* linear orders are lattices *)
+
+instance
+  lin_order < lattice                   (allI, exI, min_is_inf, max_is_sup)
+
+
+(* complete lattices are lattices *)
+
+instance
+  clattice < lattice                    (allI, exI, Inf_is_inf, Sup_is_sup)
+
+
+(* products of lattices are lattices *)
+
+instance
+  "*" :: (lattice, lattice) lattice     (allI, exI, prod_is_inf, prod_is_sup)
+
+instance
+  fun :: (term, lattice) lattice        (allI, exI, fun_is_inf, fun_is_sup)
+
+
+(* duals of lattices are lattices *)
+
+instance
+  dual :: (lattice) lattice             (allI, exI, dual_is_inf, dual_is_sup)
+
+(*FIXME bug workaround (see also OrdInsts.thy)*)
+instance
+  dual :: (lin_order) lin_order         (le_dual_lin)
+
+end
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/LatMorph.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/LatMorph.ML	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,53 @@
+
+open LatMorph;
+
+
+(** monotone functions vs. "&&"- / "||"-semi-morphisms **)
+
+goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
+  by (safe_tac set_cs);
+  (*==> (level 1)*)
+    by (stac le_inf_eq 1);
+    br conjI 1;
+    by (step_tac set_cs 1);
+    by (step_tac set_cs 1);
+    be mp 1;
+    br inf_lb1 1;
+    by (step_tac set_cs 1);
+    by (step_tac set_cs 1);
+    be mp 1;
+    br inf_lb2 1;
+  (*==> (level 11)*)
+    br (conjI RS (le_trans RS mp)) 1;
+    br inf_lb2 2;
+    by (subgoal_tac "x && y = x" 1);
+    be subst 1;
+    by (fast_tac set_cs 1);
+    by (stac inf_connect 1);
+    ba 1;
+qed "mono_inf_eq";
+
+goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
+  by (safe_tac set_cs);
+  (*==> (level 1)*)
+    by (stac ge_sup_eq 1);
+    br conjI 1;
+    by (step_tac set_cs 1);
+    by (step_tac set_cs 1);
+    be mp 1;
+    br sup_ub1 1;
+    by (step_tac set_cs 1);
+    by (step_tac set_cs 1);
+    be mp 1;
+    br sup_ub2 1;
+  (*==> (level 11)*)
+    br (conjI RS (le_trans RS mp)) 1;
+    br sup_ub1 1;
+    by (subgoal_tac "x || y = y" 1);
+    be subst 1;
+    by (fast_tac set_cs 1);
+    by (stac sup_connect 1);
+    ba 1;
+qed "mono_sup_eq";
+
+
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/LatMorph.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/LatMorph.thy	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,28 @@
+(*  Title:      LatMorph.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Some lattice morphisms.
+
+TODO:
+  more morphisms (?)
+  more theorems
+*)
+
+LatMorph = LatInsts +
+
+consts
+  is_mono       :: "('a::le => 'b::le) => bool"
+  is_inf_morph  :: "('a::lattice => 'b::lattice) => bool"
+  is_sup_morph  :: "('a::lattice => 'b::lattice) => bool"
+  is_Inf_morph  :: "('a::clattice => 'b::clattice) => bool"
+  is_Sup_morph  :: "('a::clattice => 'b::clattice) => bool"
+
+defs
+  is_mono_def       "is_mono f == ALL x y. x [= y --> f x [= f y"
+  is_inf_morph_def  "is_inf_morph f == ALL x y. f (x && y) = f x && f y"
+  is_sup_morph_def  "is_sup_morph f == ALL x y. f (x || y) = f x || f y"
+  is_Inf_morph_def  "is_Inf_morph f == ALL A. f (Inf A) = Inf {f x |x. x:A}"
+  is_Sup_morph_def  "is_Sup_morph f == ALL A. f (Sup A) = Sup {f x |x. x:A}"
+
+end
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/LatPreInsts.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,76 @@
+
+open LatPreInsts;
+
+
+(** complete lattices **)
+
+goal thy "is_inf x y (Inf {x, y})";
+  br (bin_is_Inf_eq RS subst) 1;
+  br Inf_is_Inf 1;
+qed "Inf_is_inf";
+
+goal thy "is_sup x y (Sup {x, y})";
+  br (bin_is_Sup_eq RS subst) 1;
+  br Sup_is_Sup 1;
+qed "Sup_is_sup";
+
+
+
+(** product lattices **)
+
+(* pairs *)
+
+goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
+  by (simp_tac prod_ss 1);
+  by (safe_tac HOL_cs);
+  by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
+qed "prod_is_inf";
+
+goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
+  by (simp_tac prod_ss 1);
+  by (safe_tac HOL_cs);
+  by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
+qed "prod_is_sup";
+
+
+(* functions *)
+
+goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
+  by (safe_tac HOL_cs);
+  br inf_lb1 1;
+  br inf_lb2 1;
+  br inf_ub_lbs 1;
+  by (REPEAT_FIRST (fast_tac HOL_cs));
+qed "fun_is_inf";
+
+goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
+  by (safe_tac HOL_cs);
+  br sup_ub1 1;
+  br sup_ub2 1;
+  br sup_lb_ubs 1;
+  by (REPEAT_FIRST (fast_tac HOL_cs));
+qed "fun_is_sup";
+
+
+
+(** dual lattices **)
+
+goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
+  by (stac Abs_dual_inverse' 1);
+  by (safe_tac HOL_cs);
+  br sup_ub1 1;
+  br sup_ub2 1;
+  br sup_lb_ubs 1;
+  ba 1;
+  ba 1;
+qed "dual_is_inf";
+
+goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
+  by (stac Abs_dual_inverse' 1);
+  by (safe_tac HOL_cs);
+  br inf_lb1 1;
+  br inf_lb2 1;
+  br inf_ub_lbs 1;
+  ba 1;
+  ba 1;
+qed "dual_is_sup";
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/LatPreInsts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/LatPreInsts.thy	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,6 @@
+(*  Title:      LatPreInsts.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+*)
+
+LatPreInsts = OrdInsts + Lattice + CLattice
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/Lattice.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/Lattice.ML	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,269 @@
+
+open Lattice;
+
+
+(** basic properties of "&&" and "||" **)
+
+(* unique existence *)
+
+goalw thy [inf_def] "is_inf x y (x && y)";
+  br (ex_inf RS spec RS spec RS selectI1) 1;
+qed "inf_is_inf";
+
+goal thy "is_inf x y inf --> x && y = inf";
+  br impI 1;
+  br (is_inf_uniq RS mp) 1;
+  br conjI 1;
+  br inf_is_inf 1;
+  ba 1;
+qed "inf_uniq";
+
+goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf";
+  by (safe_tac HOL_cs);
+  by (step_tac HOL_cs 1);
+  by (step_tac HOL_cs 1);
+  br inf_is_inf 1;
+  br (inf_uniq RS mp RS sym) 1;
+  ba 1;
+qed "ex1_inf";
+
+
+goalw thy [sup_def] "is_sup x y (x || y)";
+  br (ex_sup RS spec RS spec RS selectI1) 1;
+qed "sup_is_sup";
+
+goal thy "is_sup x y sup --> x || y = sup";
+  br impI 1;
+  br (is_sup_uniq RS mp) 1;
+  br conjI 1;
+  br sup_is_sup 1;
+  ba 1;
+qed "sup_uniq";
+
+goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup";
+  by (safe_tac HOL_cs);
+  by (step_tac HOL_cs 1);
+  by (step_tac HOL_cs 1);
+  br sup_is_sup 1;
+  br (sup_uniq RS mp RS sym) 1;
+  ba 1;
+qed "ex1_sup";
+
+
+(* "&&" yields g.l.bs, "||" yields l.u.bs. --- in pieces *)
+
+val tac =
+  cut_facts_tac [inf_is_inf] 1 THEN
+  rewrite_goals_tac [inf_def, is_inf_def] THEN
+  fast_tac HOL_cs 1;
+
+goal thy "x && y [= x";
+  by tac;
+qed "inf_lb1";
+
+goal thy "x && y [= y";
+  by tac;
+qed "inf_lb2";
+
+val prems = goal thy "[| z [= x; z [= y |] ==> z [= x && y";
+  by (cut_facts_tac prems 1);
+  by tac;
+qed "inf_ub_lbs";
+
+
+val tac =
+  cut_facts_tac [sup_is_sup] 1 THEN
+  rewrite_goals_tac [sup_def, is_sup_def] THEN
+  fast_tac HOL_cs 1;
+
+goal thy "x [= x || y";
+  by tac;
+qed "sup_ub1";
+
+goal thy "y [= x || y";
+  by tac;
+qed "sup_ub2";
+
+val prems = goal thy "[| x [= z; y [= z |] ==> x || y [= z";
+  by (cut_facts_tac prems 1);
+  by tac;
+qed "sup_lb_ubs";
+
+
+
+(** some equations concerning "&&" and "||" vs. "[=" **)
+
+(* the Connection Theorems: "[=" expressed via "&&" or "||" *)
+
+goal thy "(x && y = x) = (x [= y)";
+  br iffI 1;
+  (*==>*)
+    be subst 1;
+    br inf_lb2 1;
+  (*<==*)
+    br (inf_uniq RS mp) 1;
+    by (rewrite_goals_tac [is_inf_def]);
+    by (REPEAT_FIRST (rtac conjI));
+    br le_refl 1;
+    ba 1;
+    by (fast_tac HOL_cs 1);
+qed "inf_connect";
+
+goal thy "(x || y = y) = (x [= y)";
+  br iffI 1;
+  (*==>*)
+    be subst 1;
+    br sup_ub1 1;
+  (*<==*)
+    br (sup_uniq RS mp) 1;
+    by (rewrite_goals_tac [is_sup_def]);
+    by (REPEAT_FIRST (rtac conjI));
+    ba 1;
+    br le_refl 1;
+    by (fast_tac HOL_cs 1);
+qed "sup_connect";
+
+
+(* minorized infs / majorized sups *)
+
+goal thy "(x [= y && z) = (x [= y & x [= z)";
+  br iffI 1;
+  (*==> (level 1)*)
+    by (cut_facts_tac [inf_lb1, inf_lb2] 1);
+    br conjI 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    ba 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    ba 1;
+  (*<== (level 9)*)
+    be conjE 1;
+    be inf_ub_lbs 1;
+    ba 1;
+qed "le_inf_eq";
+
+goal thy "(x || y [= z) = (x [= z & y [= z)";
+  br iffI 1;
+  (*==> (level 1)*)
+    by (cut_facts_tac [sup_ub1, sup_ub2] 1);
+    br conjI 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    ba 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    ba 1;
+  (*<== (level 9)*)
+    be conjE 1;
+    be sup_lb_ubs 1;
+    ba 1;
+qed "ge_sup_eq";
+
+
+(** algebraic properties of "&&" and "||": A, C, I, AB **)
+
+(* associativity *)
+
+goal thy "(x && y) && z = x && (y && z)";
+  by (stac (inf_uniq RS mp RS sym) 1);
+  back();
+  back();
+  back();
+  back();
+  back();
+  back();
+  back();
+  back();
+  br refl 2;
+  br (is_inf_assoc RS mp) 1;
+  by (REPEAT_FIRST (rtac conjI));
+  by (REPEAT_FIRST (rtac inf_is_inf));
+qed "inf_assoc";
+
+goal thy "(x || y) || z = x || (y || z)";
+  by (stac (sup_uniq RS mp RS sym) 1);
+  back();
+  back();
+  back();
+  back();
+  back();
+  back();
+  back();
+  back();
+  br refl 2;
+  br (is_sup_assoc RS mp) 1;
+  by (REPEAT_FIRST (rtac conjI));
+  by (REPEAT_FIRST (rtac sup_is_sup));
+qed "sup_assoc";
+
+
+(* commutativity *)
+
+goalw thy [inf_def] "x && y = y && x";
+  by (stac (is_inf_commut RS ext) 1);
+  br refl 1;
+qed "inf_commut";
+
+goalw thy [sup_def] "x || y = y || x";
+  by (stac (is_sup_commut RS ext) 1);
+  br refl 1;
+qed "sup_commut";
+
+
+(* idempotency *)
+
+goal thy "x && x = x";
+  by (stac inf_connect 1);
+  br le_refl 1;
+qed "inf_idemp";
+
+goal thy "x || x = x";
+  by (stac sup_connect 1);
+  br le_refl 1;
+qed "sup_idemp";
+
+
+(* absorption *)
+
+goal thy "x || (x && y) = x";
+  by (stac sup_commut 1);
+  by (stac sup_connect 1);
+  br inf_lb1 1;
+qed "sup_inf_absorb";
+
+goal thy "x && (x || y) = x";
+  by (stac inf_connect 1);
+  br sup_ub1 1;
+qed "inf_sup_absorb";
+
+
+(* monotonicity *)
+
+val prems = goal thy "[| a [= b; x [= y |] ==> a && x [= b && y";
+  by (cut_facts_tac prems 1);
+  by (stac le_inf_eq 1);
+  br conjI 1;
+  br (le_trans RS mp) 1;
+  br conjI 1;
+  br inf_lb1 1;
+  ba 1;
+  br (le_trans RS mp) 1;
+  br conjI 1;
+  br inf_lb2 1;
+  ba 1;
+qed "inf_mon";
+
+val prems = goal thy "[| a [= b; x [= y |] ==> a || x [= b || y";
+  by (cut_facts_tac prems 1);
+  by (stac ge_sup_eq 1);
+  br conjI 1;
+  br (le_trans RS mp) 1;
+  br conjI 1;
+  ba 1;
+  br sup_ub1 1;
+  br (le_trans RS mp) 1;
+  br conjI 1;
+  ba 1;
+  br sup_ub2 1;
+qed "sup_mon";
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/Lattice.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/Lattice.thy	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,23 @@
+(*  Title:      Lattice.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Lattices are orders with binary (finitary) infima and suprema.
+*)
+
+Lattice = Order +
+
+axclass
+  lattice < 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"
+
+consts
+  "&&"          :: "['a::lattice, 'a] => 'a"       (infixl 70)
+  "||"          :: "['a::lattice, 'a] => 'a"       (infixl 65)
+
+defs
+  inf_def       "x && y == @inf. is_inf x y inf"
+  sup_def       "x || y == @sup. is_sup x y sup"
+
+end
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/OrdDefs.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,88 @@
+
+open OrdDefs;
+
+
+(** lifting of quasi / partial orders **)
+
+(* pairs *)
+
+goalw thy [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)";
+  br conjI 1;
+  br le_refl 1;
+  br le_refl 1;
+qed "le_prod_refl";
+
+goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
+  by (safe_tac HOL_cs);
+  be (conjI RS (le_trans RS mp)) 1;
+  ba 1;
+  be (conjI RS (le_trans RS mp)) 1;
+  ba 1;
+qed "le_prod_trans";
+
+goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)";
+  by (safe_tac HOL_cs);
+  by (stac Pair_fst_snd_eq 1);
+  br conjI 1;
+  be (conjI RS (le_antisym RS mp)) 1;
+  ba 1;
+  be (conjI RS (le_antisym RS mp)) 1;
+  ba 1;
+qed "le_prod_antisym";
+
+
+(* functions *)
+
+goalw thy [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
+  br allI 1;
+  br le_refl 1;
+qed "le_fun_refl";
+
+goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
+  by (safe_tac HOL_cs);
+  br (le_trans RS mp) 1;
+  by (fast_tac HOL_cs 1);
+qed "le_fun_trans";
+
+goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)";
+  by (safe_tac HOL_cs);
+  br ext 1;
+  br (le_antisym RS mp) 1;
+  by (fast_tac HOL_cs 1);
+qed "le_fun_antisym";
+
+
+
+(** duals **)
+
+(*"'a dual" is even an isotype*)
+goal thy "Rep_dual (Abs_dual y) = y";
+  br Abs_dual_inverse 1;
+  by (rewrite_goals_tac [dual_def]);
+  by (fast_tac set_cs 1);
+qed "Abs_dual_inverse'";
+
+
+goalw thy [le_dual_def] "x [= (x::'a::quasi_order dual)";
+  br le_refl 1;
+qed "le_dual_refl";
+
+goalw thy [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
+  by (stac conj_commut 1);
+  br le_trans 1;
+qed "le_dual_trans";
+
+goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)";
+  by (safe_tac prop_cs);
+  br (Rep_dual_inverse RS subst) 1;
+  br sym 1;
+  br (Rep_dual_inverse RS subst) 1;
+  br arg_cong 1;
+  back();
+  be (conjI RS (le_antisym RS mp)) 1;
+  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";
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/OrdDefs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.thy	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,35 @@
+(*  Title:      OrdDefs.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Some overloaded definitions.
+*)
+
+OrdDefs = Order + Prod +
+
+
+(* binary / general products *)
+
+instance
+  "*" :: (le, le) le
+
+instance
+  fun :: (term, le) le
+
+defs
+  le_prod_def   "p [= q == fst p [= fst q & snd p [= snd q"
+  le_fun_def    "f [= g == ALL x. f x [= g x"
+
+
+(* duals *)
+
+subtype
+  'a dual = "{x::'a. True}"
+
+instance
+  dual :: (le) le
+
+defs
+  le_dual_def   "x [= y == Rep_dual y [= Rep_dual x"
+
+end
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/OrdInsts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/OrdInsts.thy	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,43 @@
+(*  Title:      OrdInsts.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Some order instantiations.
+*)
+
+OrdInsts = OrdDefs +
+
+
+(* binary / general products of quasi_orders / orders *)
+
+instance
+  "*" :: (quasi_order, quasi_order) quasi_order         (le_prod_refl, le_prod_trans)
+
+instance
+  "*" :: (order, order) 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)
+
+
+(* duals of quasi_orders / orders / lin_orders *)
+
+instance
+  dual :: (quasi_order) quasi_order                     (le_dual_refl, le_dual_trans)
+
+instance
+  dual :: (order) 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)
+*)
+
+end
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/Order.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/Order.ML	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,173 @@
+
+open Order;
+
+
+(** basic properties of limits **)
+
+(* uniqueness *)
+
+val tac =
+  rtac impI 1 THEN
+  rtac (le_antisym RS mp) 1 THEN
+  fast_tac HOL_cs 1;
+
+
+goalw thy [is_inf_def] "is_inf x y inf & is_inf x y inf' --> inf = inf'";
+  by tac;
+qed "is_inf_uniq";
+
+goalw thy [is_sup_def] "is_sup x y sup & is_sup x y sup' --> sup = sup'";
+  by tac;
+qed "is_sup_uniq";
+
+
+goalw thy [is_Inf_def] "is_Inf A inf & is_Inf A inf' --> inf = inf'";
+  by tac;
+qed "is_Inf_uniq";
+
+goalw thy [is_Sup_def] "is_Sup A sup & is_Sup A sup' --> sup = sup'";
+  by tac;
+qed "is_Sup_uniq";
+
+
+
+(* commutativity *)
+
+goalw thy [is_inf_def] "is_inf x y inf = is_inf y x inf";
+  by (fast_tac HOL_cs 1);
+qed "is_inf_commut";
+
+goalw thy [is_sup_def] "is_sup x y sup = is_sup y x sup";
+  by (fast_tac HOL_cs 1);
+qed "is_sup_commut";
+
+
+(* associativity *)
+
+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";
+  by (safe_tac HOL_cs);
+  (*level 1*)
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    ba 1;
+  (*level 4*)
+    by (step_tac HOL_cs 1);
+    back();
+    be mp 1;
+    br conjI 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    ba 1;
+    ba 1;
+  (*level 11*)
+    by (step_tac HOL_cs 1);
+    back();
+    back();
+    be mp 1;
+    br conjI 1;
+    by (step_tac HOL_cs 1);
+    be mp 1;
+    be conjI 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    ba 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    back();     (* !! *)
+    ba 1;
+qed "is_inf_assoc";
+
+
+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";
+  by (safe_tac HOL_cs);
+  (*level 1*)
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    ba 1;
+  (*level 4*)
+    by (step_tac HOL_cs 1);
+    back();
+    be mp 1;
+    br conjI 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    ba 1;
+    ba 1;
+  (*level 11*)
+    by (step_tac HOL_cs 1);
+    back();
+    back();
+    be mp 1;
+    br conjI 1;
+    by (step_tac HOL_cs 1);
+    be mp 1;
+    be conjI 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    back();     (* !! *)
+    ba 1;
+    br (le_trans RS mp) 1;
+    be conjI 1;
+    ba 1;
+qed "is_sup_assoc";
+
+
+(** limits in linear orders **)
+
+goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::lin_order) y (minimum x y)";
+  by (stac expand_if 1);
+  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
+  (*case "x [= y"*)
+    br le_refl 1;
+    ba 1;
+    by (fast_tac HOL_cs 1);
+  (*case "~ x [= y"*)
+    br (le_lin RS disjE) 1;
+    ba 1;
+    be notE 1;
+    ba 1;
+    br le_refl 1;
+    by (fast_tac HOL_cs 1);
+qed "min_is_inf";
+
+goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::lin_order) y (maximum x y)";
+  by (stac expand_if 1);
+  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
+  (*case "x [= y"*)
+    ba 1;
+    br le_refl 1;
+    by (fast_tac HOL_cs 1);
+  (*case "~ x [= y"*)
+    br le_refl 1;
+    br (le_lin RS disjE) 1;
+    ba 1;
+    be notE 1;
+    ba 1;
+    by (fast_tac HOL_cs 1);
+qed "max_is_sup";
+
+
+
+(** general vs. binary limits **)
+
+goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
+  br iffI 1;
+  (*==>*)
+    by (fast_tac set_cs 1);
+  (*<==*)
+    by (safe_tac set_cs);
+    by (step_tac set_cs 1);
+    be mp 1;
+    by (fast_tac set_cs 1);
+qed "bin_is_Inf_eq";
+
+goalw thy [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
+  br iffI 1;
+  (*==>*)
+    by (fast_tac set_cs 1);
+  (*<==*)
+    by (safe_tac set_cs);
+    by (step_tac set_cs 1);
+    be mp 1;
+    by (fast_tac set_cs 1);
+qed "bin_is_Sup_eq";
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/Order.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/Order.thy	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,83 @@
+(*  Title:      Order.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Basic theory of orders (quasi orders, partial orders, linear orders)
+and limits (inf, sup, min, max).
+*)
+
+Order = HOL + Set +
+
+
+(** class definitions **)
+
+(* syntax for orders *)
+
+axclass
+  le < term
+
+consts
+  "[="          :: "['a::le, 'a] => bool"             (infixl 50)
+
+
+(* quasi orders *)
+
+axclass
+  quasi_order < le
+  le_refl       "x [= x"
+  le_trans      "x [= y & y [= z --> x [= z"
+
+
+(* partial orders *)
+
+axclass
+  order < quasi_order
+  le_antisym    "x [= y & y [= x --> x = y"
+
+
+(* linear orders *)
+
+axclass
+  lin_order < order
+  le_lin        "x [= y | y [= x"
+
+
+
+(** limits **)
+
+(* infima and suprema (on orders) *)
+
+consts
+  (*binary*)
+  is_inf        :: "['a::order, 'a, 'a] => bool"
+  is_sup        :: "['a::order, 'a, 'a] => bool"
+  (*general*)
+  is_Inf        :: "['a::order set, 'a] => bool"
+  is_Sup        :: "['a::order set, 'a] => bool"
+
+defs
+  is_inf_def    "is_inf x y inf ==
+                   inf [= x & inf [= y &
+                   (ALL lb. lb [= x & lb [= y --> lb [= inf)"
+  is_sup_def    "is_sup x y sup ==
+                   x [= sup & y [= sup &
+                   (ALL ub. x [= ub & y [= ub --> sup [= ub)"
+  is_Inf_def    "is_Inf A inf ==
+                   (ALL x:A. inf [= x) &
+                   (ALL lb. (ALL x:A. lb [= x) --> lb [= inf)"
+  is_Sup_def    "is_Sup A sup ==
+                   (ALL x:A. x [= sup) &
+                   (ALL ub. (ALL x:A. x [= ub) --> sup [= ub)"
+
+
+(* binary minima and maxima (on lin_orders) *)
+
+consts
+  minimum      :: "['a::lin_order, 'a] => 'a"
+  maximum      :: "['a::lin_order, 'a] => 'a"
+
+defs
+  minimum_def  "minimum x y == (if x [= y then x else y)"
+  maximum_def  "maximum x y == (if x [= y then y else x)"
+
+end
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/ROOT.ML	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,29 @@
+(*  Title:      HOL/AxClasses/Lattice/ROOT.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Basic theory of lattices and orders via axiomatic type classes.
+*)
+
+open AxClass;
+
+reset HOL_quantifiers;
+reset eta_contract;
+set show_types;
+set show_sorts;
+
+use "tools.ML";
+
+use_thy "Order";
+use_thy "OrdDefs";
+use_thy "OrdInsts";
+
+use_thy "Lattice";
+use_thy "CLattice";
+
+use_thy "LatPreInsts";
+use_thy "LatInsts";
+
+use_thy "LatMorph";
+
+make_chart ();   (*make HTML chart*)
diff -r 1f5949a43e82 -r de6f18da81bb src/HOL/AxClasses/Lattice/tools.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Lattice/tools.ML	Mon Jan 15 15:49:21 1996 +0100
@@ -0,0 +1,10 @@
+
+(** generic tools **)
+
+val prems = goalw HOL.thy [Ex_def] "EX x. P x ==> P (@x. P x)";
+  by (resolve_tac prems 1);
+qed "selectI1";
+
+goal HOL.thy "(P & Q) = (Q & P)";
+  by (fast_tac prop_cs 1);
+qed "conj_commut";