(*<*) theory tmpl08_ex imports Complex_Main "../../Material/Demos/BST_Demo" "~~/src/HOL/Library/Multiset" "~~/src/HOL/Data_Structures/Tree23_Set" begin (*>*) text {* \ExerciseSheet{8}{16.~6.~2017} *} text \\Exercise{Abstract Set Interface} In Isabelle/HOL we can use a so called \locale\ to model the abstract set interface. The locale fixes the operations as parameters, and makes assumptions on them. \ locale set_interface = fixes invar :: "'s \ bool" and \ :: "'s \ 'a set" fixes empty :: 's assumes empty_invar: "invar empty" and empty_\: "\ empty = {}" fixes is_in :: "'s \ 'a \ bool" assumes is_in_\: "invar s \ is_in s x \ x \ \ s" fixes ins :: "'a \ 's \ 's" assumes ins_invar: "invar s \ invar (ins x s)" and ins_\: "invar s \ \ (ins x s) = Set.insert x (\ s)" fixes to_list :: "'s \ 'a list" assumes to_list_\: "invar s \ set (to_list s) = \ s" begin text \ Inside the locale, all the assumptions are available \ thm empty_invar empty_\ is_in_\ ins_invar ins_\ to_list_\ text \ Note that you know nothing about the structure of the fixed parameters or the types @{typ 'a} and @{typ 's}! \ text \We can define a union function as follows:\ definition union :: "'s \ 's \ 's" where "union A B = fold ins (to_list A) B" text \Show the interface specification for union: \ lemma union_invar: assumes "invar A" assumes "invar B" shows "invar (union A B)" sorry lemma union_\: assumes "invar A" assumes "invar B" shows "\ (union A B) = \ A \ \ B" sorry text \Define an intersection function and show its interface specification\ definition intersect :: "'s \ 's \ 's" where "intersect A B \ undefined" lemma intersect_invar: "True" sorry lemma intersect_\: "True" sorry end text \Having defined the locale, we can instantiate it for implementations of the set interface. For example for BSTs:\ interpretation bst_set: set_interface bst set_tree Tree.Leaf "BST_Demo.isin" "BST_Demo.ins" Tree.inorder apply unfold_locales text \Show the goals\ sorry text \Now we also have instantiated versions of union and intersection\ term bst_set.union thm bst_set.union_\ bst_set.union_invar term bst_set.intersect thm bst_set.intersect_\ bst_set.intersect_invar text \ Instantiate the set interface also for: \<^item> Distinct lists \<^item> 2-3-Trees \ (*<*) end (*>*)