(*<*) theory sol08 imports Complex_Main "../../Material/Demos/BST_Demo" "~~/src/HOL/Library/Multiset" (*"~~/src/HOL/Library/List_lexord"*) "~~/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)" (*<*) proof - have union_invar_aux: "invar (fold ins list B)" for list using \invar B\ by (induction list arbitrary: B) (auto simp: ins_invar) show ?thesis unfolding union_def using union_invar_aux by auto qed (*>*) lemma union_\: assumes "invar A" assumes "invar B" shows "\ (union A B) = \ A \ \ B" (*<*) proof - have "\ (fold ins list B) = \ B \ set list" for list using \invar B\ by (induction list arbitrary: B) (auto simp: ins_\ ins_invar) also have "set (to_list A) = \ A" using to_list_\[OF \invar A\] . finally show ?thesis unfolding union_def by auto qed (*>*) text \Define an intersection function and show its interface specification\ definition intersect :: "'s \ 's \ 's" (*<*) where "intersect A B \ fold (\x s. if is_in A x then ins x s else s) (to_list B) empty" (*>*) lemma intersect_invar: (*<*) assumes "invar A" assumes "invar B" shows "invar (intersect A B)" proof - have "invar (fold (\x s. if is_in A x then ins x s else s) list S)" if \invar S\ for list S using that by (induction list arbitrary: S) (auto simp: ins_invar) thus ?thesis unfolding intersect_def by (auto simp: empty_invar) qed (*>*) lemma intersect_\: (*<*) assumes "invar A" assumes "invar B" shows "\ (intersect A B) = \ A \ \ B" proof - have "\ (fold (\x s. if is_in A x then ins x s else s) list S) = \ S \ (set list \ \ A)" if \invar S\ for list S using that by (induction list arbitrary: S) (auto simp: is_in_\[OF \invar A\] ins_\ ins_invar) from this[OF empty_invar] show ?thesis unfolding intersect_def by (auto simp: empty_\ to_list_\[OF \invar B\]) qed (*>*) 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\ (*<*) apply (auto simp: set_tree_isin bst_ins set_tree_ins) done (*>*) 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 \ (*<*) definition "dlist_ins x l \ if x\set l then l else x#l" interpretation dlist_set: set_interface "distinct" set "[]" "\l x. x\set l" dlist_ins "\x. x" apply unfold_locales unfolding dlist_ins_def apply (auto) done term dlist_set.union thm dlist_set.union_\ dlist_set.union_invar term dlist_set.intersect thm dlist_set.intersect_\ dlist_set.intersect_invar interpretation set23: set_interface "\t. bal t \ sorted (inorder t)" "elems o inorder" "\\::_ tree23" "isin" "insert" "inorder" proof (unfold_locales; clarify?) show "bal \\ \ Sorted_Less.sorted (Tree23.inorder \\)" by simp next show "(elems \ Tree23.inorder) \\ = {}" by simp next fix t x assume "bal t" "Sorted_Less.sorted (Tree23.inorder t)" then show "Tree23_Set.isin t x = (x \ (elems \ Tree23.inorder) t)" by (auto simp: isin_set) next fix t x assume "bal t" "Sorted_Less.sorted (Tree23.inorder t)" then show "bal (Tree23_Set.insert x t) \ Sorted_Less.sorted (Tree23.inorder (Tree23_Set.insert x t))" apply (auto simp: bal_insert) by (simp add: invar_insert) next fix t x assume "bal t" "Sorted_Less.sorted (Tree23.inorder t)" then show "(elems \ Tree23.inorder) (Tree23_Set.insert x t) = Set.insert x ((elems \ Tree23.inorder) t)" by (auto simp: set_ins_list inorder_insert) next fix t x assume "bal t" "Sorted_Less.sorted (Tree23.inorder t)" then show "set (Tree23.inorder t) = (elems \ Tree23.inorder) t" by (auto simp: elems_eq_set) qed term set23.union thm set23.union_\ set23.union_invar term set23.intersect thm set23.intersect_\ set23.intersect_invar (*>*) (*<*) end (*>*)