--- /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";
--- /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
--- /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";
--- /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
--- /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";
+
+
--- /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
--- /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";
--- /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
--- /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";
--- /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
--- /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";
--- /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
--- /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
--- /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";
--- /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
--- /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*)
--- /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";