diff options
Diffstat (limited to 'snapshots/isabelle/lib/lem/Lem_set.thy')
| -rw-r--r-- | snapshots/isabelle/lib/lem/Lem_set.thy | 325 |
1 files changed, 325 insertions, 0 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_set.thy b/snapshots/isabelle/lib/lem/Lem_set.thy new file mode 100644 index 00000000..f77d4d98 --- /dev/null +++ b/snapshots/isabelle/lib/lem/Lem_set.thy @@ -0,0 +1,325 @@ +chapter \<open>Generated by Lem from set.lem.\<close> + +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 \<Rightarrow> bool)\<Rightarrow> 'a set \<Rightarrow> 'a set*'a set " where + " partition P s = ( (set_filter P s, set_filter (\<lambda> e . \<not> (P e)) s))" + + + +(* ----------------------- *) +(* split *) +(* ----------------------- *) + +(*val split : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * set 'a*) +definition split :: " 'a Ord_class \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> '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 \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> '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 \<in> 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 \<Rightarrow> 'a set " where + " bigintersection bs = ( (let x2 = + ({}) in Finite_Set.fold + (\<lambda>x x2 . + if( \<forall> s \<in> bs. x \<in> s) then Set.insert x x2 else x2) + x2 (\<Union> 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 \<Rightarrow> 'b option)\<Rightarrow> 'a set \<Rightarrow> 'b set " where + " setMapMaybe f s = ( + \<Union> (Set.image (\<lambda> 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 \<Rightarrow> 'a set " where + " removeMaybe s = ( setMapMaybe (\<lambda> 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 \<Rightarrow>('a set \<Rightarrow> 'a set)\<Rightarrow> 'a set \<Rightarrow> 'a set " where + " leastFixedPoint 0 f x = ( x )" +|" leastFixedPoint ((Suc bound')) f x = ( (let fx = (f x) in + if fx \<subseteq> x then x + else leastFixedPoint bound' f (fx \<union> x)))" + +end |