--- a/src/HOL/AxClasses/Group/Group.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-(* Title: HOL/AxClasses/Group/Group.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Some basic theorems of group theory.
-*)
-
-fun sub r = standard (r RS subst);
-fun ssub r = standard (r RS ssubst);
-
-
-Goal "x * inverse x = (1::'a::group)";
-by (rtac (sub left_unit) 1);
-back();
-by (rtac (sub assoc) 1);
-by (rtac (sub left_inverse) 1);
-back();
-back();
-by (rtac (ssub assoc) 1);
-back();
-by (rtac (ssub left_inverse) 1);
-by (rtac (ssub assoc) 1);
-by (rtac (ssub left_unit) 1);
-by (rtac (ssub left_inverse) 1);
-by (rtac refl 1);
-qed "right_inverse";
-
-
-Goal "x * 1 = (x::'a::group)";
-by (rtac (sub left_inverse) 1);
-by (rtac (sub assoc) 1);
-by (rtac (ssub right_inverse) 1);
-by (rtac (ssub left_unit) 1);
-by (rtac refl 1);
-qed "right_unit";
-
-
-Goal "e * x = x --> e = (1::'a::group)";
-by (rtac impI 1);
-by (rtac (sub right_unit) 1);
-back();
-by (res_inst_tac [("x", "x")] (sub right_inverse) 1);
-by (rtac (sub assoc) 1);
-by (rtac arg_cong 1);
-back();
-by (assume_tac 1);
-qed "strong_one_unit";
-
-
-Goal "EX! e. ALL x. e * x = (x::'a::group)";
-by (rtac ex1I 1);
-by (rtac allI 1);
-by (rtac left_unit 1);
-by (rtac mp 1);
-by (rtac strong_one_unit 1);
-by (etac allE 1);
-by (assume_tac 1);
-qed "ex1_unit";
-
-
-Goal "ALL x. EX! e. e * x = (x::'a::group)";
-by (rtac allI 1);
-by (rtac ex1I 1);
-by (rtac left_unit 1);
-by (rtac (strong_one_unit RS mp) 1);
-by (assume_tac 1);
-qed "ex1_unit'";
-
-
-Goal "inj (op * (x::'a::group))";
-by (rtac injI 1);
-by (rtac (sub left_unit) 1);
-back();
-by (rtac (sub left_unit) 1);
-by (res_inst_tac [("x", "x")] (sub left_inverse) 1);
-by (rtac (ssub assoc) 1);
-back();
-by (rtac (ssub assoc) 1);
-by (rtac arg_cong 1);
-back();
-by (assume_tac 1);
-qed "inj_times";
-
-
-Goal "y * x = 1 --> y = inverse (x::'a::group)";
-by (rtac impI 1);
-by (rtac (sub right_unit) 1);
-back();
-back();
-by (rtac (sub right_unit) 1);
-by (res_inst_tac [("x", "x")] (sub right_inverse) 1);
-by (rtac (sub assoc) 1);
-by (rtac (sub assoc) 1);
-by (rtac arg_cong 1);
-back();
-by (rtac (ssub left_inverse) 1);
-by (assume_tac 1);
-qed "one_inverse";
-
-
-Goal "ALL x. EX! y. y * x = (1::'a::group)";
-by (rtac allI 1);
-by (rtac ex1I 1);
-by (rtac left_inverse 1);
-by (rtac mp 1);
-by (rtac one_inverse 1);
-by (assume_tac 1);
-qed "ex1_inverse";
-
-
-Goal "inverse (x * y) = inverse y * inverse (x::'a::group)";
-by (rtac sym 1);
-by (rtac mp 1);
-by (rtac one_inverse 1);
-by (rtac (ssub assoc) 1);
-by (rtac (sub assoc) 1);
-back();
-by (rtac (ssub left_inverse) 1);
-by (rtac (ssub left_unit) 1);
-by (rtac (ssub left_inverse) 1);
-by (rtac refl 1);
-qed "inverse_times";
-
-
-Goal "inverse (inverse x) = (x::'a::group)";
-by (rtac sym 1);
-by (rtac (one_inverse RS mp) 1);
-by (rtac (ssub right_inverse) 1);
-by (rtac refl 1);
-qed "inverse_inverse";
--- a/src/HOL/AxClasses/Group/Group.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Title: Group.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-*)
-
-Group = Sigs + Fun +
-
-(* semigroups *)
-
-axclass
- semigroup < times
- assoc "(x * y) * z = x * (y * z)"
-
-
-(* groups *)
-
-axclass
- group < one, inverse, semigroup
- left_unit "1 * x = x"
- left_inverse "inverse x * x = 1"
-
-
-(* abelian groups *)
-
-axclass
- agroup < group
- commut "x * y = y * x"
-
-end
--- a/src/HOL/AxClasses/Group/GroupDefs.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(* bool *)
-
-(*this is really overkill - should be rather proven 'inline'*)
-
-Goalw [times_bool_def] "(x * y) * z = x * (y * (z::bool))";
-by (Fast_tac 1);
-qed "bool_assoc";
-
-Goalw [times_bool_def, one_bool_def] "1 * x = (x::bool)";
-by (Fast_tac 1);
-qed "bool_left_unit";
-
-Goalw [times_bool_def, one_bool_def] "x * 1 = (x::bool)";
-by (Fast_tac 1);
-qed "bool_right_unit";
-
-Goalw [times_bool_def, inverse_bool_def, one_bool_def]
- "inverse(x) * x = (1::bool)";
-by (Fast_tac 1);
-qed "bool_left_inverse";
-
-Goalw [times_bool_def] "x * y = (y * (x::bool))";
-by (Fast_tac 1);
-qed "bool_commut";
-
-
-(* cartesian products *)
-
-val prod_ss = simpset_of Prod.thy;
-
-Goalw [times_prod_def]
- "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))";
-by (simp_tac (prod_ss addsimps [assoc]) 1);
-qed "prod_assoc";
-
-Goalw [times_prod_def, one_prod_def] "1 * x = (x::'a::monoid*'b::monoid)";
-by (simp_tac (prod_ss addsimps [Monoid.left_unit]) 1);
-qed "prod_left_unit";
-
-Goalw [times_prod_def, one_prod_def] "x * 1 = (x::'a::monoid*'b::monoid)";
-by (simp_tac (prod_ss addsimps [Monoid.right_unit]) 1);
-qed "prod_right_unit";
-
-Goalw [times_prod_def, inverse_prod_def, one_prod_def]
- "inverse x * x = (1::'a::group*'b::group)";
-by (simp_tac (prod_ss addsimps [left_inverse]) 1);
-qed "prod_left_inverse";
-
-Goalw [times_prod_def] "x * y = y * (x::'a::agroup*'b::agroup)";
-by (simp_tac (prod_ss addsimps [commut]) 1);
-qed "prod_commut";
-
-
-(* function spaces *)
-
-Goalw [times_fun_def] "(x * y) * z = x * (y * (z::'a => 'b::semigroup))";
-by (stac expand_fun_eq 1);
-by (rtac allI 1);
-by (rtac assoc 1);
-qed "fun_assoc";
-
-Goalw [times_fun_def, one_fun_def] "1 * x = (x::'a => 'b::monoid)";
-by (stac expand_fun_eq 1);
-by (rtac allI 1);
-by (rtac Monoid.left_unit 1);
-qed "fun_left_unit";
-
-Goalw [times_fun_def, one_fun_def] "x * 1 = (x::'a => 'b::monoid)";
-by (stac expand_fun_eq 1);
-by (rtac allI 1);
-by (rtac Monoid.right_unit 1);
-qed "fun_right_unit";
-
-Goalw [times_fun_def, inverse_fun_def, one_fun_def]
- "inverse x * x = (1::'a => 'b::group)";
-by (stac expand_fun_eq 1);
-by (rtac allI 1);
-by (rtac left_inverse 1);
-qed "fun_left_inverse";
-
-Goalw [times_fun_def] "x * y = y * (x::'a => 'b::agroup)";
-by (stac expand_fun_eq 1);
-by (rtac allI 1);
-by (rtac commut 1);
-qed "fun_commut";
--- a/src/HOL/AxClasses/Group/GroupDefs.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Title: GroupDefs.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-*)
-
-GroupDefs = MonoidGroupInsts + Prod + Fun +
-
-
-(* bool *)
-
-instance
- bool :: {times, inverse, one}
-
-defs
- times_bool_def "x * y == (x ~= y)"
- inverse_bool_def "inverse x == (x::bool)"
- one_bool_def "1 == False"
-
-
-(* cartesian products *)
-
-instance
- "*" :: (term, term) {times, inverse, one}
-
-defs
- times_prod_def "p * q == (fst p * fst q, snd p * snd q)"
- inverse_prod_def "inverse p == (inverse (fst p), inverse (snd p))"
- one_prod_def "1 == (1, 1)"
-
-
-(* function spaces *)
-
-instance
- fun :: (term, term) {times, inverse, one}
-
-defs
- times_fun_def "f * g == (%x. f x * g x)"
- inverse_fun_def "inverse f == (%x. inverse (f x))"
- one_fun_def "1 == (%x. 1)"
-
-end
--- a/src/HOL/AxClasses/Group/GroupInsts.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* Title: GroupInsts.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Some concrete instantiations: 'structures' and 'functors'.
-*)
-
-GroupInsts = GroupDefs +
-
-
-(* bool *)
-
-instance
- bool :: semigroup (bool_assoc)
-instance
- bool :: monoid (bool_assoc, bool_left_unit, bool_right_unit)
-instance
- bool :: group (bool_left_unit, bool_left_inverse)
-instance
- bool :: agroup (bool_commut)
-
-
-(* cartesian products *)
-
-instance
- "*" :: (semigroup, semigroup) semigroup (prod_assoc)
-instance
- "*" :: (monoid, monoid) monoid (prod_assoc, prod_left_unit, prod_right_unit)
-instance
- "*" :: (group, group) group (prod_left_unit, prod_left_inverse)
-instance
- "*" :: (agroup, agroup) agroup (prod_commut)
-
-
-(* function spaces *)
-
-instance
- fun :: (term, semigroup) semigroup (fun_assoc)
-instance
- fun :: (term, monoid) monoid (fun_assoc, fun_left_unit, fun_right_unit)
-instance
- fun :: (term, group) group (fun_left_unit, fun_left_inverse)
-instance
- fun :: (term, agroup) agroup (fun_commut)
-
-end
--- a/src/HOL/AxClasses/Group/Monoid.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Monoid.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-*)
-
-Monoid = Sigs +
-
-(* monoids *)
-
-axclass
- monoid < times, one
- assoc "(x * y) * z = x * (y * z)"
- left_unit "1 * x = x"
- right_unit "x * 1 = x"
-
-end
--- a/src/HOL/AxClasses/Group/MonoidGroupInsts.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: MonoidGroupInsts.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Some class inclusions or 'abstract instantiations'.
-*)
-
-MonoidGroupInsts = Group + Monoid +
-
-
-(* monoids are semigroups *)
-
-instance
- monoid < semigroup (Monoid.assoc)
-
-
-(* groups are monoids *)
-
-instance
- group < monoid ("Group.assoc", "Group.left_unit", "Group.right_unit")
-
-end
--- a/src/HOL/AxClasses/Group/ROOT.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Title: HOL/AxClasses/Group/ROOT.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Some bits of group theory via axiomatic type classes.
-*)
-
-set show_types;
-set show_sorts;
-
-time_use_thy "Monoid";
-time_use_thy "Group";
-time_use_thy "MonoidGroupInsts";
-time_use_thy "GroupInsts";
--- a/src/HOL/AxClasses/Group/Sigs.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(* Title: Sigs.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-*)
-
-Sigs = HOL +
-
-axclass
- inverse < term
-
-axclass
- one < term
-
-consts
- inverse :: 'a::inverse => 'a
- "1" :: 'a::one ("1")
-
-end
--- a/src/HOL/AxClasses/Lattice/CLattice.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,180 +0,0 @@
-
-(** basic properties of "Inf" and "Sup" **)
-
-(* unique existence *)
-
-Goalw [Inf_def] "is_Inf A (Inf A)";
- by (rtac (ex_Inf RS spec RS selectI1) 1);
-qed "Inf_is_Inf";
-
-Goal "is_Inf A inf --> Inf A = inf";
- by (rtac impI 1);
- by (rtac (is_Inf_uniq RS mp) 1);
- by (rtac conjI 1);
- by (rtac Inf_is_Inf 1);
- by (assume_tac 1);
-qed "Inf_uniq";
-
-Goalw [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
- by Safe_tac;
- by (Step_tac 1);
- by (Step_tac 1);
- by (rtac Inf_is_Inf 1);
- by (rtac (Inf_uniq RS mp RS sym) 1);
- by (assume_tac 1);
-qed "ex1_Inf";
-
-
-Goalw [Sup_def] "is_Sup A (Sup A)";
- by (rtac (ex_Sup RS spec RS selectI1) 1);
-qed "Sup_is_Sup";
-
-Goal "is_Sup A sup --> Sup A = sup";
- by (rtac impI 1);
- by (rtac (is_Sup_uniq RS mp) 1);
- by (rtac conjI 1);
- by (rtac Sup_is_Sup 1);
- by (assume_tac 1);
-qed "Sup_uniq";
-
-Goalw [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
- by Safe_tac;
- by (Step_tac 1);
- by (Step_tac 1);
- by (rtac Sup_is_Sup 1);
- by (rtac (Sup_uniq RS mp RS sym) 1);
- by (assume_tac 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);
- by (rtac someI2 1);
- by (rtac Inf_is_Inf 1);
- by (rewtac is_Inf_def);
- by (Fast_tac 1);
-qed "Inf_lb";
-
-val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
- by (rtac someI2 1);
- by (rtac Inf_is_Inf 1);
- by (rewtac is_Inf_def);
- by (Step_tac 1);
- by (Step_tac 1);
- by (etac mp 1);
- by (rtac ballI 1);
- by (etac prem 1);
-qed "Inf_ub_lbs";
-
-
-val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
- by (cut_facts_tac prems 1);
- by (rtac someI2 1);
- by (rtac Sup_is_Sup 1);
- by (rewtac is_Sup_def);
- by (Fast_tac 1);
-qed "Sup_ub";
-
-val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
- by (rtac someI2 1);
- by (rtac Sup_is_Sup 1);
- by (rewtac is_Sup_def);
- by (Step_tac 1);
- by (Step_tac 1);
- by (etac mp 1);
- by (rtac ballI 1);
- by (etac prem 1);
-qed "Sup_lb_ubs";
-
-
-(** minorized Infs / majorized Sups **)
-
-Goal "(x [= Inf A) = (ALL y:A. x [= y)";
- by (rtac iffI 1);
- (*==>*)
- by (rtac ballI 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (etac Inf_lb 1);
- (*<==*)
- by (rtac Inf_ub_lbs 1);
- by (Fast_tac 1);
-qed "le_Inf_eq";
-
-Goal "(Sup A [= x) = (ALL y:A. y [= x)";
- by (rtac iffI 1);
- (*==>*)
- by (rtac ballI 1);
- by (rtac (le_trans RS mp) 1);
- by (rtac conjI 1);
- by (etac Sup_ub 1);
- by (assume_tac 1);
- (*<==*)
- by (rtac Sup_lb_ubs 1);
- by (Fast_tac 1);
-qed "ge_Sup_eq";
-
-
-
-(** Subsets and limits **)
-
-Goal "A <= B --> Inf B [= Inf A";
- by (rtac impI 1);
- by (stac le_Inf_eq 1);
- by (rewtac Ball_def);
- by Safe_tac;
- by (dtac subsetD 1);
- by (assume_tac 1);
- by (etac Inf_lb 1);
-qed "Inf_subset_antimon";
-
-Goal "A <= B --> Sup A [= Sup B";
- by (rtac impI 1);
- by (stac ge_Sup_eq 1);
- by (rewtac Ball_def);
- by Safe_tac;
- by (dtac subsetD 1);
- by (assume_tac 1);
- by (etac Sup_ub 1);
-qed "Sup_subset_mon";
-
-
-(** singleton / empty limits **)
-
-Goal "Inf {x} = x";
- by (rtac (Inf_uniq RS mp) 1);
- by (rewtac is_Inf_def);
- by Safe_tac;
- by (rtac le_refl 1);
- by (Fast_tac 1);
-qed "sing_Inf_eq";
-
-Goal "Sup {x} = x";
- by (rtac (Sup_uniq RS mp) 1);
- by (rewtac is_Sup_def);
- by Safe_tac;
- by (rtac le_refl 1);
- by (Fast_tac 1);
-qed "sing_Sup_eq";
-
-
-Goal "Inf {} = Sup {x. True}";
- by (rtac (Inf_uniq RS mp) 1);
- by (rewtac is_Inf_def);
- by Safe_tac;
- by (rtac (sing_Sup_eq RS subst) 1);
- back();
- by (rtac (Sup_subset_mon RS mp) 1);
- by (Fast_tac 1);
-qed "empty_Inf_eq";
-
-Goal "Sup {} = Inf {x. True}";
- by (rtac (Sup_uniq RS mp) 1);
- by (rewtac is_Sup_def);
- by Safe_tac;
- by (rtac (sing_Inf_eq RS subst) 1);
- by (rtac (Inf_subset_antimon RS mp) 1);
- by (Fast_tac 1);
-qed "empty_Sup_eq";
--- a/src/HOL/AxClasses/Lattice/CLattice.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* 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 < partial_order
- ex_Inf "ALL A. EX inf. is_Inf A inf"
- ex_Sup "ALL A. EX sup. is_Sup A sup"
-
-constdefs
- Inf :: "'a::clattice set => 'a"
- "Inf A == @inf. is_Inf A inf"
-
- Sup :: "'a::clattice set => 'a"
- "Sup A == @sup. is_Sup A sup"
-
-end
--- a/src/HOL/AxClasses/Lattice/LatInsts.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-
-
-Goal "Inf {x, y} = x && y";
- by (rtac (Inf_uniq RS mp) 1);
- by (stac bin_is_Inf_eq 1);
- by (rtac inf_is_inf 1);
-qed "bin_Inf_eq";
-
-Goal "Sup {x, y} = x || y";
- by (rtac (Sup_uniq RS mp) 1);
- by (stac bin_is_Sup_eq 1);
- by (rtac sup_is_sup 1);
-qed "bin_Sup_eq";
-
-
-
-(* Unions and limits *)
-
-Goal "Inf (A Un B) = Inf A && Inf B";
- by (rtac (Inf_uniq RS mp) 1);
- by (rewtac is_Inf_def);
- by Safe_tac;
-
- by (rtac (conjI RS (le_trans RS mp)) 1);
- by (rtac inf_lb1 1);
- by (etac Inf_lb 1);
-
- by (rtac (conjI RS (le_trans RS mp)) 1);
- by (rtac inf_lb2 1);
- by (etac Inf_lb 1);
-
- by (stac le_inf_eq 1);
- by (rtac conjI 1);
- by (rtac Inf_ub_lbs 1);
- by (Fast_tac 1);
- by (rtac Inf_ub_lbs 1);
- by (Fast_tac 1);
-qed "Inf_Un_eq";
-
-Goal "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
- by (rtac (Inf_uniq RS mp) 1);
- by (rewtac is_Inf_def);
- by Safe_tac;
- (*level 3*)
- by (rtac (conjI RS (le_trans RS mp)) 1);
- by (etac Inf_lb 2);
- by (rtac (sing_Inf_eq RS subst) 1);
- by (rtac (Inf_subset_antimon RS mp) 1);
- by (Fast_tac 1);
- (*level 8*)
- by (stac le_Inf_eq 1);
- by Safe_tac;
- by (stac le_Inf_eq 1);
- by (Fast_tac 1);
-qed "Inf_UN_eq";
-
-
-
-Goal "Sup (A Un B) = Sup A || Sup B";
- by (rtac (Sup_uniq RS mp) 1);
- by (rewtac is_Sup_def);
- by Safe_tac;
-
- by (rtac (conjI RS (le_trans RS mp)) 1);
- by (etac Sup_ub 1);
- by (rtac sup_ub1 1);
-
- by (rtac (conjI RS (le_trans RS mp)) 1);
- by (etac Sup_ub 1);
- by (rtac sup_ub2 1);
-
- by (stac ge_sup_eq 1);
- by (rtac conjI 1);
- by (rtac Sup_lb_ubs 1);
- by (Fast_tac 1);
- by (rtac Sup_lb_ubs 1);
- by (Fast_tac 1);
-qed "Sup_Un_eq";
-
-Goal "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
- by (rtac (Sup_uniq RS mp) 1);
- by (rewtac is_Sup_def);
- by Safe_tac;
- (*level 3*)
- by (rtac (conjI RS (le_trans RS mp)) 1);
- by (etac Sup_ub 1);
- by (rtac (sing_Sup_eq RS subst) 1);
- back();
- by (rtac (Sup_subset_mon RS mp) 1);
- by (Fast_tac 1);
- (*level 8*)
- by (stac ge_Sup_eq 1);
- by Safe_tac;
- by (stac ge_Sup_eq 1);
- by (Fast_tac 1);
-qed "Sup_UN_eq";
--- a/src/HOL/AxClasses/Lattice/LatInsts.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Title: LatInsts.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Some lattice instantiations.
-*)
-
-LatInsts = LatPreInsts +
-
-
-(* linear orders are lattices *)
-
-instance
- linear_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 :: (linear_order) linear_order (le_dual_linear)
-
-end
--- a/src/HOL/AxClasses/Lattice/LatMorph.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-
-
-(** monotone functions vs. "&&"- / "||"-semi-morphisms **)
-
-Goalw [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
- by Safe_tac;
- (*==> (level 1)*)
- by (stac le_inf_eq 1);
- by (rtac conjI 1);
- by (Step_tac 1);
- by (Step_tac 1);
- by (etac mp 1);
- by (rtac inf_lb1 1);
- by (Step_tac 1);
- by (Step_tac 1);
- by (etac mp 1);
- by (rtac inf_lb2 1);
- (*==> (level 11)*)
- by (rtac (conjI RS (le_trans RS mp)) 1);
- by (rtac inf_lb2 2);
- by (subgoal_tac "x && y = x" 1);
- by (etac subst 1);
- by (Fast_tac 1);
- by (stac inf_connect 1);
- by (assume_tac 1);
-qed "mono_inf_eq";
-
-Goalw [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
- by Safe_tac;
- (*==> (level 1)*)
- by (stac ge_sup_eq 1);
- by (rtac conjI 1);
- by (Step_tac 1);
- by (Step_tac 1);
- by (etac mp 1);
- by (rtac sup_ub1 1);
- by (Step_tac 1);
- by (Step_tac 1);
- by (etac mp 1);
- by (rtac sup_ub2 1);
- (*==> (level 11)*)
- by (rtac (conjI RS (le_trans RS mp)) 1);
- by (rtac sup_ub1 1);
- by (subgoal_tac "x || y = y" 1);
- by (etac subst 1);
- by (Fast_tac 1);
- by (stac sup_connect 1);
- by (assume_tac 1);
-qed "mono_sup_eq";
-
-
--- a/src/HOL/AxClasses/Lattice/LatMorph.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: LatMorph.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Some lattice morphisms.
-
-TODO:
- more morphisms (?)
- more theorems
-*)
-
-LatMorph = LatInsts +
-
-constdefs
- is_mono :: "('a::le => 'b::le) => bool"
- "is_mono f == ALL x y. x [= y --> f x [= f y"
-
- is_inf_morph :: "('a::lattice => 'b::lattice) => bool"
- "is_inf_morph f == ALL x y. f (x && y) = f x && f y"
-
- is_sup_morph :: "('a::lattice => 'b::lattice) => bool"
- "is_sup_morph f == ALL x y. f (x || y) = f x || f y"
-
- is_Inf_morph :: "('a::clattice => 'b::clattice) => bool"
- "is_Inf_morph f == ALL A. f (Inf A) = Inf {f x |x. x:A}"
-
- is_Sup_morph :: "('a::clattice => 'b::clattice) => bool"
- "is_Sup_morph f == ALL A. f (Sup A) = Sup {f x |x. x:A}"
-
-end
--- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-
-
-(** complete lattices **)
-
-Goal "is_inf x y (Inf {x, y})";
- by (rtac (bin_is_Inf_eq RS subst) 1);
- by (rtac Inf_is_Inf 1);
-qed "Inf_is_inf";
-
-Goal "is_sup x y (Sup {x, y})";
- by (rtac (bin_is_Sup_eq RS subst) 1);
- by (rtac Sup_is_Sup 1);
-qed "Sup_is_sup";
-
-
-
-(** product lattices **)
-
-(* pairs *)
-
-Goalw [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
- by (Simp_tac 1);
- by Safe_tac;
- by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
-qed "prod_is_inf";
-
-Goalw [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
- by (Simp_tac 1);
- by Safe_tac;
- by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
-qed "prod_is_sup";
-
-
-(* functions *)
-
-Goalw [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
- by Safe_tac;
- by (rtac inf_lb1 1);
- by (rtac inf_lb2 1);
- by (rtac inf_ub_lbs 1);
- by (REPEAT_FIRST (Fast_tac));
-qed "fun_is_inf";
-
-Goalw [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
- by Safe_tac;
- by (rtac sup_ub1 1);
- by (rtac sup_ub2 1);
- by (rtac sup_lb_ubs 1);
- by (REPEAT_FIRST (Fast_tac));
-qed "fun_is_sup";
-
-
-
-(** dual lattices **)
-
-Goalw [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;
- by (rtac sup_ub1 1);
- by (rtac sup_ub2 1);
- by (rtac sup_lb_ubs 1);
- by (assume_tac 1);
- by (assume_tac 1);
-qed "dual_is_inf";
-
-Goalw [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;
- by (rtac inf_lb1 1);
- by (rtac inf_lb2 1);
- by (rtac inf_ub_lbs 1);
- by (assume_tac 1);
- by (assume_tac 1);
-qed "dual_is_sup";
--- a/src/HOL/AxClasses/Lattice/LatPreInsts.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(* Title: LatPreInsts.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-*)
-
-LatPreInsts = OrdInsts + Lattice + CLattice
--- a/src/HOL/AxClasses/Lattice/Lattice.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,276 +0,0 @@
-
-context HOL.thy;
-
-Goalw [Ex_def] "EX x. P x ==> P (@x. P x)";
- by (assume_tac 1);
-qed "selectI1";
-
-context thy;
-
-
-
-(** basic properties of "&&" and "||" **)
-
-(* unique existence *)
-
-Goalw [inf_def] "is_inf x y (x && y)";
- by (rtac (ex_inf RS spec RS spec RS selectI1) 1);
-qed "inf_is_inf";
-
-Goal "is_inf x y inf --> x && y = inf";
- by (rtac impI 1);
- by (rtac (is_inf_uniq RS mp) 1);
- by (rtac conjI 1);
- by (rtac inf_is_inf 1);
- by (assume_tac 1);
-qed "inf_uniq";
-
-Goalw [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf";
- by Safe_tac;
- by (Step_tac 1);
- by (Step_tac 1);
- by (rtac inf_is_inf 1);
- by (rtac (inf_uniq RS mp RS sym) 1);
- by (assume_tac 1);
-qed "ex1_inf";
-
-
-Goalw [sup_def] "is_sup x y (x || y)";
- by (rtac (ex_sup RS spec RS spec RS selectI1) 1);
-qed "sup_is_sup";
-
-Goal "is_sup x y sup --> x || y = sup";
- by (rtac impI 1);
- by (rtac (is_sup_uniq RS mp) 1);
- by (rtac conjI 1);
- by (rtac sup_is_sup 1);
- by (assume_tac 1);
-qed "sup_uniq";
-
-Goalw [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup";
- by Safe_tac;
- by (Step_tac 1);
- by (Step_tac 1);
- by (rtac sup_is_sup 1);
- by (rtac (sup_uniq RS mp RS sym) 1);
- by (assume_tac 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 1;
-
-Goal "x && y [= x";
- by tac;
-qed "inf_lb1";
-
-Goal "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 1;
-
-Goal "x [= x || y";
- by tac;
-qed "sup_ub1";
-
-Goal "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 "(x && y = x) = (x [= y)";
- by (rtac iffI 1);
- (*==>*)
- by (etac subst 1);
- by (rtac inf_lb2 1);
- (*<==*)
- by (rtac (inf_uniq RS mp) 1);
- by (rewtac is_inf_def);
- by (REPEAT_FIRST (rtac conjI));
- by (rtac le_refl 1);
- by (assume_tac 1);
- by (Fast_tac 1);
-qed "inf_connect";
-
-Goal "(x || y = y) = (x [= y)";
- by (rtac iffI 1);
- (*==>*)
- by (etac subst 1);
- by (rtac sup_ub1 1);
- (*<==*)
- by (rtac (sup_uniq RS mp) 1);
- by (rewtac is_sup_def);
- by (REPEAT_FIRST (rtac conjI));
- by (assume_tac 1);
- by (rtac le_refl 1);
- by (Fast_tac 1);
-qed "sup_connect";
-
-
-(* minorized infs / majorized sups *)
-
-Goal "(x [= y && z) = (x [= y & x [= z)";
- by (rtac iffI 1);
- (*==> (level 1)*)
- by (cut_facts_tac [inf_lb1, inf_lb2] 1);
- by (rtac conjI 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (assume_tac 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (assume_tac 1);
- (*<== (level 9)*)
- by (etac conjE 1);
- by (etac inf_ub_lbs 1);
- by (assume_tac 1);
-qed "le_inf_eq";
-
-Goal "(x || y [= z) = (x [= z & y [= z)";
- by (rtac iffI 1);
- (*==> (level 1)*)
- by (cut_facts_tac [sup_ub1, sup_ub2] 1);
- by (rtac conjI 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (assume_tac 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (assume_tac 1);
- (*<== (level 9)*)
- by (etac conjE 1);
- by (etac sup_lb_ubs 1);
- by (assume_tac 1);
-qed "ge_sup_eq";
-
-
-(** algebraic properties of "&&" and "||": A, C, I, AB **)
-
-(* associativity *)
-
-Goal "(x && y) && z = x && (y && z)";
- by (stac (inf_uniq RS mp RS sym) 1);
- back();
- back();
- back();
- back();
- back();
- back();
- back();
- back();
- by (rtac refl 2);
- by (rtac (is_inf_assoc RS mp) 1);
- by (REPEAT_FIRST (rtac conjI));
- by (REPEAT_FIRST (rtac inf_is_inf));
-qed "inf_assoc";
-
-Goal "(x || y) || z = x || (y || z)";
- by (stac (sup_uniq RS mp RS sym) 1);
- back();
- back();
- back();
- back();
- back();
- back();
- back();
- back();
- by (rtac refl 2);
- by (rtac (is_sup_assoc RS mp) 1);
- by (REPEAT_FIRST (rtac conjI));
- by (REPEAT_FIRST (rtac sup_is_sup));
-qed "sup_assoc";
-
-
-(* commutativity *)
-
-Goalw [inf_def] "x && y = y && x";
- by (stac (is_inf_commut RS ext) 1);
- by (rtac refl 1);
-qed "inf_commut";
-
-Goalw [sup_def] "x || y = y || x";
- by (stac (is_sup_commut RS ext) 1);
- by (rtac refl 1);
-qed "sup_commut";
-
-
-(* idempotency *)
-
-Goal "x && x = x";
- by (stac inf_connect 1);
- by (rtac le_refl 1);
-qed "inf_idemp";
-
-Goal "x || x = x";
- by (stac sup_connect 1);
- by (rtac le_refl 1);
-qed "sup_idemp";
-
-
-(* absorption *)
-
-Goal "x || (x && y) = x";
- by (stac sup_commut 1);
- by (stac sup_connect 1);
- by (rtac inf_lb1 1);
-qed "sup_inf_absorb";
-
-Goal "x && (x || y) = x";
- by (stac inf_connect 1);
- by (rtac 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);
- by (rtac conjI 1);
- by (rtac (le_trans RS mp) 1);
- by (rtac conjI 1);
- by (rtac inf_lb1 1);
- by (assume_tac 1);
- by (rtac (le_trans RS mp) 1);
- by (rtac conjI 1);
- by (rtac inf_lb2 1);
- by (assume_tac 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);
- by (rtac conjI 1);
- by (rtac (le_trans RS mp) 1);
- by (rtac conjI 1);
- by (assume_tac 1);
- by (rtac sup_ub1 1);
- by (rtac (le_trans RS mp) 1);
- by (rtac conjI 1);
- by (assume_tac 1);
- by (rtac sup_ub2 1);
-qed "sup_mon";
--- a/src/HOL/AxClasses/Lattice/Lattice.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Title: Lattice.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Lattices are orders with binary (finitary) infima and suprema.
-*)
-
-Lattice = Order +
-
-axclass
- lattice < partial_order
- ex_inf "ALL x y. EX inf. is_inf x y inf"
- ex_sup "ALL x y. EX sup. is_sup x y sup"
-
-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
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-
-
-(** lifting of quasi / partial orders **)
-
-(* pairs *)
-
-Goalw [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)";
- by (rtac conjI 1);
- by (rtac le_refl 1);
- by (rtac le_refl 1);
-qed "le_prod_refl";
-
-Goalw [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
- by Safe_tac;
- by (etac (conjI RS (le_trans RS mp)) 1);
- by (assume_tac 1);
- by (etac (conjI RS (le_trans RS mp)) 1);
- by (assume_tac 1);
-qed "le_prod_trans";
-
-Goalw [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
- by Safe_tac;
- by (stac Pair_fst_snd_eq 1);
- by (rtac conjI 1);
- by (etac (conjI RS (le_antisym RS mp)) 1);
- by (assume_tac 1);
- by (etac (conjI RS (le_antisym RS mp)) 1);
- by (assume_tac 1);
-qed "le_prod_antisym";
-
-
-(* functions *)
-
-Goalw [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
- by (rtac allI 1);
- by (rtac le_refl 1);
-qed "le_fun_refl";
-
-Goalw [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
- by Safe_tac;
- by (rtac (le_trans RS mp) 1);
- by (Fast_tac 1);
-qed "le_fun_trans";
-
-Goalw [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
- by Safe_tac;
- by (rtac ext 1);
- by (rtac (le_antisym RS mp) 1);
- by (Fast_tac 1);
-qed "le_fun_antisym";
-
-
-
-(** duals **)
-
-(*"'a dual" is even an isotype*)
-Goal "Rep_dual (Abs_dual y) = y";
- by (rtac Abs_dual_inverse 1);
- by (rewtac dual_def);
- by (Fast_tac 1);
-qed "Abs_dual_inverse'";
-
-
-Goalw [le_dual_def] "x [= (x::'a::quasi_order dual)";
- by (rtac le_refl 1);
-qed "le_dual_refl";
-
-Goalw [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
- by (rtac impI 1);
- by (rtac (le_trans RS mp) 1);
- by (Blast_tac 1);
-qed "le_dual_trans";
-
-Goalw [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
- by Safe_tac;
- by (rtac (Rep_dual_inverse RS subst) 1);
- by (rtac sym 1);
- by (rtac (Rep_dual_inverse RS subst) 1);
- by (rtac arg_cong 1);
- back();
- by (etac (conjI RS (le_antisym RS mp)) 1);
- by (assume_tac 1);
-qed "le_dual_antisym";
-
-Goalw [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
- by (rtac le_linear 1);
-qed "le_dual_linear";
--- a/src/HOL/AxClasses/Lattice/OrdDefs.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(* 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 *)
-
-typedef
- 'a dual = "{x::'a. True}"
-
-instance
- dual :: (le) le
-
-defs
- le_dual_def "x [= y == Rep_dual y [= Rep_dual x"
-
-end
--- a/src/HOL/AxClasses/Lattice/Order.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-
-
-(** basic properties of limits **)
-
-(* uniqueness *)
-
-val tac =
- rtac impI 1 THEN
- rtac (le_antisym RS mp) 1 THEN
- Fast_tac 1;
-
-
-Goalw [is_inf_def] "is_inf x y inf & is_inf x y inf' --> inf = inf'";
- by tac;
-qed "is_inf_uniq";
-
-Goalw [is_sup_def] "is_sup x y sup & is_sup x y sup' --> sup = sup'";
- by tac;
-qed "is_sup_uniq";
-
-
-Goalw [is_Inf_def] "is_Inf A inf & is_Inf A inf' --> inf = inf'";
- by tac;
-qed "is_Inf_uniq";
-
-Goalw [is_Sup_def] "is_Sup A sup & is_Sup A sup' --> sup = sup'";
- by tac;
-qed "is_Sup_uniq";
-
-
-
-(* commutativity *)
-
-Goalw [is_inf_def] "is_inf x y inf = is_inf y x inf";
- by (Fast_tac 1);
-qed "is_inf_commut";
-
-Goalw [is_sup_def] "is_sup x y sup = is_sup y x sup";
- by (Fast_tac 1);
-qed "is_sup_commut";
-
-
-(* associativity *)
-
-Goalw [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;
- (*level 1*)
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (assume_tac 1);
- (*level 4*)
- by (Step_tac 1);
- back();
- by (etac mp 1);
- by (rtac conjI 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (assume_tac 1);
- by (assume_tac 1);
- (*level 11*)
- by (Step_tac 1);
- back();
- back();
- by (etac mp 1);
- by (rtac conjI 1);
- by (Step_tac 1);
- by (etac mp 1);
- by (etac conjI 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (assume_tac 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- back(); (* !! *)
- by (assume_tac 1);
-qed "is_inf_assoc";
-
-
-Goalw [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;
- (*level 1*)
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (assume_tac 1);
- (*level 4*)
- by (Step_tac 1);
- back();
- by (etac mp 1);
- by (rtac conjI 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (assume_tac 1);
- by (assume_tac 1);
- (*level 11*)
- by (Step_tac 1);
- back();
- back();
- by (etac mp 1);
- by (rtac conjI 1);
- by (Step_tac 1);
- by (etac mp 1);
- by (etac conjI 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- back(); (* !! *)
- by (assume_tac 1);
- by (rtac (le_trans RS mp) 1);
- by (etac conjI 1);
- by (assume_tac 1);
-qed "is_sup_assoc";
-
-
-(** limits in linear orders **)
-
-Goalw [minimum_def, is_inf_def] "is_inf (x::'a::linear_order) y (minimum x y)";
- by (stac split_if 1);
- by (REPEAT_FIRST (resolve_tac [conjI, impI]));
- (*case "x [= y"*)
- by (rtac le_refl 1);
- by (assume_tac 1);
- by (Fast_tac 1);
- (*case "~ x [= y"*)
- by (rtac (le_linear RS disjE) 1);
- by (assume_tac 1);
- by (etac notE 1);
- by (assume_tac 1);
- by (rtac le_refl 1);
- by (Fast_tac 1);
-qed "min_is_inf";
-
-Goalw [maximum_def, is_sup_def] "is_sup (x::'a::linear_order) y (maximum x y)";
- by (stac split_if 1);
- by (REPEAT_FIRST (resolve_tac [conjI, impI]));
- (*case "x [= y"*)
- by (assume_tac 1);
- by (rtac le_refl 1);
- by (Fast_tac 1);
- (*case "~ x [= y"*)
- by (rtac le_refl 1);
- by (rtac (le_linear RS disjE) 1);
- by (assume_tac 1);
- by (etac notE 1);
- by (assume_tac 1);
- by (Fast_tac 1);
-qed "max_is_sup";
-
-
-
-(** general vs. binary limits **)
-
-Goalw [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
- by (rtac iffI 1);
- (*==>*)
- by (Fast_tac 1);
- (*<==*)
- by Safe_tac;
- by (Step_tac 1);
- by (etac mp 1);
- by (Fast_tac 1);
-qed "bin_is_Inf_eq";
-
-Goalw [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
- by (rtac iffI 1);
- (*==>*)
- by (Fast_tac 1);
- (*<==*)
- by Safe_tac;
- by (Step_tac 1);
- by (etac mp 1);
- by (Fast_tac 1);
-qed "bin_is_Sup_eq";
--- a/src/HOL/AxClasses/Lattice/Order.thy Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-(* 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
- partial_order < quasi_order
- le_antisym "x [= y & y [= x --> x = y"
-
-
-(* linear orders *)
-
-axclass
- linear_order < partial_order
- le_linear "x [= y | y [= x"
-
-
-
-(** limits **)
-
-(* infima and suprema (on orders) *)
-
-consts
- (*binary*)
- is_inf :: "['a::partial_order, 'a, 'a] => bool"
- is_sup :: "['a::partial_order, 'a, 'a] => bool"
- (*general*)
- is_Inf :: "['a::partial_order set, 'a] => bool"
- is_Sup :: "['a::partial_order set, 'a] => bool"
-
-defs
- is_inf_def "is_inf x y inf ==
- 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 linear_orders) *)
-
-constdefs
- minimum :: "['a::linear_order, 'a] => 'a"
- "minimum x y == (if x [= y then x else y)"
-
- maximum :: "['a::linear_order, 'a] => 'a"
- "maximum x y == (if x [= y then y else x)"
-
-end
--- a/src/HOL/AxClasses/Lattice/ROOT.ML Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(* 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 eta_contract;
-set show_types;
-set show_sorts;
-
-time_use_thy "Order";
-time_use_thy "OrdDefs";
-time_use_thy "OrdInsts";
-
-time_use_thy "Lattice";
-time_use_thy "CLattice";
-
-time_use_thy "LatPreInsts";
-time_use_thy "LatInsts";
-
-time_use_thy "LatMorph";
--- a/src/HOL/IsaMakefile Tue Oct 03 18:30:56 2000 +0200
+++ b/src/HOL/IsaMakefile Tue Oct 03 18:34:20 2000 +0200
@@ -8,13 +8,12 @@
default: HOL
images: HOL HOL-Real TLA
-test: HOL-Isar_examples HOL-Induct HOL-Lambda HOL-ex HOL-Subst HOL-IMP HOL-IMPP \
- HOL-NumberTheory HOL-Hoare HOL-Lex HOL-Algebra \
- HOL-Auth HOL-UNITY HOL-Modelcheck \
- HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \
- HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
- HOL-AxClasses-Tutorial HOL-Real-ex \
- HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
+
+test: HOL-Isar_examples HOL-Induct HOL-Lambda HOL-AxClasses HOL-ex HOL-Subst HOL-IMP \
+ HOL-IMPP HOL-NumberTheory HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth \
+ HOL-UNITY HOL-Modelcheck HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV \
+ HOL-MicroJava HOL-IOA HOL-Real-ex HOL-Real-HahnBanach \
+ TLA-Inc TLA-Buffer TLA-Memory
all: images test
@@ -398,42 +397,13 @@
@$(ISATOOL) usedir $(OUT)/HOL IOA
-## HOL-AxClasses-Group
-
-HOL-AxClasses-Group: HOL $(LOG)/HOL-AxClasses-Group.gz
+## HOL-AxClasses
-$(LOG)/HOL-AxClasses-Group.gz: $(OUT)/HOL AxClasses/Group/Group.ML \
- AxClasses/Group/Group.thy AxClasses/Group/GroupDefs.ML \
- AxClasses/Group/GroupDefs.thy AxClasses/Group/GroupInsts.thy \
- AxClasses/Group/Monoid.thy AxClasses/Group/MonoidGroupInsts.thy \
- AxClasses/Group/ROOT.ML AxClasses/Group/Sigs.thy
- @$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
-
-
-## HOL-AxClasses-Lattice
-
-HOL-AxClasses-Lattice: HOL $(LOG)/HOL-AxClasses-Lattice.gz
+HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
-$(LOG)/HOL-AxClasses-Lattice.gz: $(OUT)/HOL AxClasses/Lattice/CLattice.ML \
- AxClasses/Lattice/CLattice.thy AxClasses/Lattice/LatInsts.ML \
- AxClasses/Lattice/LatInsts.thy AxClasses/Lattice/LatMorph.ML \
- AxClasses/Lattice/LatMorph.thy AxClasses/Lattice/LatPreInsts.ML \
- AxClasses/Lattice/LatPreInsts.thy AxClasses/Lattice/Lattice.ML \
- AxClasses/Lattice/Lattice.thy AxClasses/Lattice/OrdDefs.ML \
- AxClasses/Lattice/OrdDefs.thy AxClasses/Lattice/OrdInsts.thy \
- AxClasses/Lattice/Order.ML AxClasses/Lattice/Order.thy \
- AxClasses/Lattice/ROOT.ML
- @$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
-
-
-## HOL-AxClasses-Tutorial
-
-HOL-AxClasses-Tutorial: HOL $(LOG)/HOL-AxClasses-Tutorial.gz
-
-$(LOG)/HOL-AxClasses-Tutorial.gz: $(OUT)/HOL \
- AxClasses/Tutorial/Group.thy AxClasses/Tutorial/Product.thy \
- AxClasses/Tutorial/ROOT.ML AxClasses/Tutorial/Semigroups.thy
- @$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
+$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy \
+ AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
+ @$(ISATOOL) usedir $(OUT)/HOL AxClasses
## HOL-ex
@@ -531,8 +501,7 @@
$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
$(LOG)/HOL-BCV.gz $(LOG)/HOL-MicroJava.gz \
- $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses-Group.gz \
- $(LOG)/HOL-AxClasses-Lattice.gz \
- $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Real-ex.gz \
+ $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
+ $(LOG)/HOL-Real-ex.gz \
$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz