chapter ‹Generated by Lem from ‹set.lem›.› theory "Lem_set" imports Main "Lem_bool" "Lem_basic_classes" "Lem_maybe" "Lem_function" "Lem_num" "Lem_list" "Lem_set_helpers" "Lem" begin ― ‹‹****************************************************************************›› ― ‹‹ A library for sets ›› ― ‹‹ ›› ― ‹‹ It mainly follows the Haskell Set-library ›› ― ‹‹****************************************************************************›› ― ‹‹ Sets in Lem are a bit tricky. On the one hand, we want efficiently executable sets. OCaml and Haskell both represent sets by some kind of balancing trees. This means that sets are finite and an order on the element type is required. Such sets are constructed by simple, executable operations like inserting or deleting elements, union, intersection, filtering etc. On the other hand, we want to use sets for specifications. This leads often infinite sets, which are specificied in complicated, perhaps even undecidable ways. The set library in this file, chooses the first approach. It describes *finite* sets with an underlying order. Infinite sets should in the medium run be represented by a separate type. Since this would require some significant changes to Lem, for the moment also infinite sets are represented using this class. However, a run-time exception might occour when using these sets. This problem needs adressing in the future. ›› ― ‹‹ ========================================================================== ›› ― ‹‹ Header ›› ― ‹‹ ========================================================================== ›› ― ‹‹open import Bool Basic_classes Maybe Function Num List Set_helpers›› ― ‹‹ DPM: sets currently implemented as lists due to mismatch between Coq type * class hierarchy and the hierarchy implemented in Lem. ›› ― ‹‹open import {coq} `Coq.Lists.List`›› ― ‹‹open import {hol} `lemTheory`›› ― ‹‹open import {isabelle} `$LIB_DIR/Lem`›› ― ‹‹ ----------------------- ›› ― ‹‹ Equality check ›› ― ‹‹ ----------------------- ›› ― ‹‹val setEqualBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool›› ― ‹‹val setEqual : forall 'a. SetType 'a => set 'a -> set 'a -> bool›› ― ‹‹ ----------------------- ›› ― ‹‹ Empty set ›› ― ‹‹ ----------------------- ›› ― ‹‹val empty : forall 'a. SetType 'a => set 'a›› ― ‹‹val emptyBy : forall 'a. ('a -> 'a -> ordering) -> set 'a›› ― ‹‹ ----------------------- ›› ― ‹‹ any / all ›› ― ‹‹ ----------------------- ›› ― ‹‹val any : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> bool›› ― ‹‹val all : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> bool›› ― ‹‹ ----------------------- ›› ― ‹‹ (IN) ›› ― ‹‹ ----------------------- ›› ― ‹‹val IN [member] : forall 'a. SetType 'a => 'a -> set 'a -> bool›› ― ‹‹val memberBy : forall 'a. ('a -> 'a -> ordering) -> 'a -> set 'a -> bool›› ― ‹‹ ----------------------- ›› ― ‹‹ not (IN) ›› ― ‹‹ ----------------------- ›› ― ‹‹val NIN [notMember] : forall 'a. SetType 'a => 'a -> set 'a -> bool›› ― ‹‹ ----------------------- ›› ― ‹‹ Emptyness check ›› ― ‹‹ ----------------------- ›› ― ‹‹val null : forall 'a. SetType 'a => set 'a -> bool›› ― ‹‹ ------------------------ ›› ― ‹‹ singleton ›› ― ‹‹ ------------------------ ›› ― ‹‹val singletonBy : forall 'a. ('a -> 'a -> ordering) -> 'a -> set 'a›› ― ‹‹val singleton : forall 'a. SetType 'a => 'a -> set 'a›› ― ‹‹ ----------------------- ›› ― ‹‹ size ›› ― ‹‹ ----------------------- ›› ― ‹‹val size : forall 'a. SetType 'a => set 'a -> nat›› ― ‹‹ ----------------------------›› ― ‹‹ setting up pattern matching ›› ― ‹‹ --------------------------- ›› ― ‹‹val set_case : forall 'a 'b. SetType 'a => set 'a -> 'b -> ('a -> 'b) -> 'b -> 'b›› ― ‹‹ ------------------------ ›› ― ‹‹ union ›› ― ‹‹ ------------------------ ›› ― ‹‹val unionBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a›› ― ‹‹val union : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a›› ― ‹‹ ----------------------- ›› ― ‹‹ insert ›› ― ‹‹ ----------------------- ›› ― ‹‹val insert : forall 'a. SetType 'a => 'a -> set 'a -> set 'a›› ― ‹‹ ----------------------- ›› ― ‹‹ filter ›› ― ‹‹ ----------------------- ›› ― ‹‹val filter : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> set 'a›› ― ‹‹let filter P s= {e | forall (e IN s) | P e}›› ― ‹‹ ----------------------- ›› ― ‹‹ partition ›› ― ‹‹ ----------------------- ›› ― ‹‹val partition : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> set 'a * set 'a›› definition partition :: "('a ⇒ bool)⇒ 'a set ⇒ 'a set*'a set " where " partition P s = ( (set_filter P s, set_filter (λ e . ¬ (P e)) s))" ― ‹‹ ----------------------- ›› ― ‹‹ split ›› ― ‹‹ ----------------------- ›› ― ‹‹val split : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * set 'a›› definition split :: " 'a Ord_class ⇒ 'a ⇒ 'a set ⇒ 'a set*'a set " where " split dict_Basic_classes_Ord_a p s = ( (set_filter ( (isGreater_method dict_Basic_classes_Ord_a) p) s, set_filter ((isLess_method dict_Basic_classes_Ord_a) p) s))" ― ‹‹val splitMember : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * bool * set 'a›› definition splitMember :: " 'a Ord_class ⇒ 'a ⇒ 'a set ⇒ 'a set*bool*'a set " where " splitMember dict_Basic_classes_Ord_a p s = ( (set_filter ( (isLess_method dict_Basic_classes_Ord_a) p) s, (p ∈ s), set_filter ( (isGreater_method dict_Basic_classes_Ord_a) p) s))" ― ‹‹ ------------------------ ›› ― ‹‹ subset and proper subset ›› ― ‹‹ ------------------------ ›› ― ‹‹val isSubsetOfBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool›› ― ‹‹val isProperSubsetOfBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool›› ― ‹‹val isSubsetOf : forall 'a. SetType 'a => set 'a -> set 'a -> bool›› ― ‹‹val isProperSubsetOf : forall 'a. SetType 'a => set 'a -> set 'a -> bool›› ― ‹‹ ------------------------ ›› ― ‹‹ delete ›› ― ‹‹ ------------------------ ›› ― ‹‹val delete : forall 'a. SetType 'a, Eq 'a => 'a -> set 'a -> set 'a›› ― ‹‹val deleteBy : forall 'a. SetType 'a => ('a -> 'a -> bool) -> 'a -> set 'a -> set 'a›› ― ‹‹ ------------------------ ›› ― ‹‹ bigunion ›› ― ‹‹ ------------------------ ›› ― ‹‹val bigunion : forall 'a. SetType 'a => set (set 'a) -> set 'a›› ― ‹‹val bigunionBy : forall 'a. ('a -> 'a -> ordering) -> set (set 'a) -> set 'a›› ― ‹‹let bigunion bs= {x | forall (s IN bs) (x IN s) | true}›› ― ‹‹ ------------------------ ›› ― ‹‹ big intersection ›› ― ‹‹ ------------------------ ›› ― ‹‹ Shaked's addition, for which he is now forever responsible as a de facto * Lem maintainer... ›› ― ‹‹val bigintersection : forall 'a. SetType 'a => set (set 'a) -> set 'a›› definition bigintersection :: "('a set)set ⇒ 'a set " where " bigintersection bs = ( (let x2 = ({}) in Finite_Set.fold (λx x2 . if( ∀ s ∈ bs. x ∈ s) then Set.insert x x2 else x2) x2 (⋃ bs)))" ― ‹‹ ------------------------ ›› ― ‹‹ difference ›› ― ‹‹ ------------------------ ›› ― ‹‹val differenceBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a›› ― ‹‹val difference : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a›› ― ‹‹ ------------------------ ›› ― ‹‹ intersection ›› ― ‹‹ ------------------------ ›› ― ‹‹val intersection : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a›› ― ‹‹val intersectionBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a›› ― ‹‹ ------------------------ ›› ― ‹‹ map ›› ― ‹‹ ------------------------ ›› ― ‹‹val map : forall 'a 'b. SetType 'a, SetType 'b => ('a -> 'b) -> set 'a -> set 'b›› ― ‹‹ before image ›› ― ‹‹let map f s= { f e | forall (e IN s) | true }›› ― ‹‹val mapBy : forall 'a 'b. ('b -> 'b -> ordering) -> ('a -> 'b) -> set 'a -> set 'b›› ― ‹‹ ------------------------ ›› ― ‹‹ bigunionMap ›› ― ‹‹ ------------------------ ›› ― ‹‹ In order to avoid providing an comparison function for sets of sets, it might be better to combine bigunion and map sometimes into a single operation. ›› ― ‹‹val bigunionMap : forall 'a 'b. SetType 'a, SetType 'b => ('a -> set 'b) -> set 'a -> set 'b›› ― ‹‹val bigunionMapBy : forall 'a 'b. ('b -> 'b -> ordering) -> ('a -> set 'b) -> set 'a -> set 'b›› ― ‹‹ ------------------------ ›› ― ‹‹ mapMaybe and fromMaybe ›› ― ‹‹ ------------------------ ›› ― ‹‹ If the mapping function returns Just x, x is added to the result set. If it returns Nothing, no element is added. ›› ― ‹‹val mapMaybe : forall 'a 'b. SetType 'a, SetType 'b => ('a -> maybe 'b) -> set 'a -> set 'b›› definition setMapMaybe :: "('a ⇒ 'b option)⇒ 'a set ⇒ 'b set " where " setMapMaybe f s = ( ⋃ (Set.image (λ x . (case f x of Some y => {y} | None => {} )) s))" ― ‹‹val removeMaybe : forall 'a. SetType 'a => set (maybe 'a) -> set 'a›› definition removeMaybe :: "('a option)set ⇒ 'a set " where " removeMaybe s = ( setMapMaybe (λ x . x) s )" ― ‹‹ ------------------------ ›› ― ‹‹ min and max ›› ― ‹‹ ------------------------ ›› ― ‹‹val findMin : forall 'a. SetType 'a, Eq 'a => set 'a -> maybe 'a›› ― ‹‹val findMax : forall 'a. SetType 'a, Eq 'a => set 'a -> maybe 'a›› ― ‹‹ ------------------------ ›› ― ‹‹ fromList ›› ― ‹‹ ------------------------ ›› ― ‹‹val fromList : forall 'a. SetType 'a => list 'a -> set 'a›› ― ‹‹ before from_list ›› ― ‹‹val fromListBy : forall 'a. ('a -> 'a -> ordering) -> list 'a -> set 'a›› ― ‹‹ ------------------------ ›› ― ‹‹ Sigma ›› ― ‹‹ ------------------------ ›› ― ‹‹val sigma : forall 'a 'b. SetType 'a, SetType 'b => set 'a -> ('a -> set 'b) -> set ('a * 'b)›› ― ‹‹val sigmaBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> ordering) -> set 'a -> ('a -> set 'b) -> set ('a * 'b)›› ― ‹‹let sigma sa sb= { (a, b) | forall (a IN sa) (b IN sb a) | true }›› ― ‹‹ ------------------------ ›› ― ‹‹ cross product ›› ― ‹‹ ------------------------ ›› ― ‹‹val cross : forall 'a 'b. SetType 'a, SetType 'b => set 'a -> set 'b -> set ('a * 'b)›› ― ‹‹val crossBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> ordering) -> set 'a -> set 'b -> set ('a * 'b)›› ― ‹‹let cross s1 s2= { (e1, e2) | forall (e1 IN s1) (e2 IN s2) | true }›› ― ‹‹ ------------------------ ›› ― ‹‹ finite ›› ― ‹‹ ------------------------ ›› ― ‹‹val finite : forall 'a. SetType 'a => set 'a -> bool›› ― ‹‹ ----------------------------›› ― ‹‹ fixed point ›› ― ‹‹ --------------------------- ›› ― ‹‹val leastFixedPoint : forall 'a. SetType 'a => nat -> (set 'a -> set 'a) -> set 'a -> set 'a›› fun leastFixedPoint :: " nat ⇒('a set ⇒ 'a set)⇒ 'a set ⇒ 'a set " where " leastFixedPoint 0 f x = ( x )" |" leastFixedPoint ((Suc bound')) f x = ( (let fx = (f x) in if fx ⊆ x then x else leastFixedPoint bound' f (fx ∪ x)))" end