# HG changeset patch # User haftmann # Date 1163428991 -3600 # Node ID eb291029d6cd5a0374d6d77899f241cc6d486a67 # Parent 2605e1ccd9f2102ec0bc7f585e37aab47f992cde dropped LOrder dependency diff -r 2605e1ccd9f2 -r eb291029d6cd src/HOL/Set.thy --- a/src/HOL/Set.thy Mon Nov 13 15:43:09 2006 +0100 +++ b/src/HOL/Set.thy Mon Nov 13 15:43:11 2006 +0100 @@ -6,7 +6,7 @@ header {* Set theory for higher-order logic *} theory Set -imports LOrder +imports Lattices begin text {* A set in HOL is simply a predicate. *} @@ -43,8 +43,6 @@ local -instance set :: (type) "{ord, minus}" .. - subsection {* Additional concrete syntax *} @@ -77,36 +75,6 @@ not_mem ("op \") not_mem ("(_/ \ _)" [50, 51] 50) -abbreviation - subset :: "'a set \ 'a set \ bool" - "subset == less" - subset_eq :: "'a set \ 'a set \ bool" - "subset_eq == less_eq" - -notation (output) - subset ("op <") - subset ("(_/ < _)" [50, 51] 50) - subset_eq ("op <=") - subset_eq ("(_/ <= _)" [50, 51] 50) - -notation (xsymbols) - subset ("op \") - subset ("(_/ \ _)" [50, 51] 50) - subset_eq ("op \") - subset_eq ("(_/ \ _)" [50, 51] 50) - -notation (HTML output) - subset ("op \") - subset ("(_/ \ _)" [50, 51] 50) - subset_eq ("op \") - subset_eq ("(_/ \ _)" [50, 51] 50) - -abbreviation (input) - supset :: "'a set \ 'a set \ bool" (infixl "\" 50) - "supset == greater" - supset_eq :: "'a set \ 'a set \ bool" (infixl "\" 50) - "supset_eq == greater_eq" - syntax "@Finset" :: "args => 'a set" ("{(_)}") "@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})") @@ -176,6 +144,40 @@ union/intersection symbol because this leads to problems with nested subscripts in Proof General. *} +instance set :: (type) ord + subset_def: "A <= B == \x\A. x \ B" + psubset_def: "A < B == (A::'a set) <= B & ~ A=B" .. + +abbreviation + subset :: "'a set \ 'a set \ bool" + "subset == less" + subset_eq :: "'a set \ 'a set \ bool" + "subset_eq == less_eq" + +notation (output) + subset ("op <") + subset ("(_/ < _)" [50, 51] 50) + subset_eq ("op <=") + subset_eq ("(_/ <= _)" [50, 51] 50) + +notation (xsymbols) + subset ("op \") + subset ("(_/ \ _)" [50, 51] 50) + subset_eq ("op \") + subset_eq ("(_/ \ _)" [50, 51] 50) + +notation (HTML output) + subset ("op \") + subset ("(_/ \ _)" [50, 51] 50) + subset_eq ("op \") + subset_eq ("(_/ \ _)" [50, 51] 50) + +abbreviation (input) + supset :: "'a set \ 'a set \ bool" (infixl "\" 50) + "supset == greater" + supset_eq :: "'a set \ 'a set \ bool" (infixl "\" 50) + "supset_eq == greater_eq" + subsubsection "Bounded quantifiers" @@ -329,11 +331,9 @@ Bex_def: "Bex A P == EX x. x:A & P(x)" Bex1_def: "Bex1 A P == EX! x. x:A & P(x)" -defs (overloaded) - subset_def: "A <= B == ALL x:A. x:B" - psubset_def: "A < B == (A::'a set) <= B & ~ A=B" +instance set :: (type) minus Compl_def: "- A == {x. ~x:A}" - set_diff_def: "A - B == {x. x:A & ~x:B}" + set_diff_def: "A - B == {x. x:A & ~x:B}" .. defs Un_def: "A Un B == {x. x:A | x:B}" @@ -2224,6 +2224,10 @@ finally (ord_eq_less_trans) show ?thesis . qed +instance set :: (type) order + by (intro_classes, + (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+) + text {* Note that this list of rules is in reverse order of priorities. *}