(*<*) theory tut08 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. \ lemma "Set.insert x s = {x} \ s" by auto 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)" unfolding union_def proof - define xs where "xs = to_list A" (*obtain xs where xs_def: "xs = to_list A" by auto*) from \invar B\ have "invar (fold ins xs B)" apply (induction xs arbitrary: B) apply (auto simp: ins_invar) done then show "invar (fold ins (to_list A) B)" unfolding xs_def by simp qed lemma assumes "invar A" assumes "invar B" shows "invar (union A B)" unfolding union_def proof - { fix xs from \invar B\ have "invar (fold ins xs B)" apply (induction xs arbitrary: B) apply (auto simp: ins_invar) done } note aux=this from \invar B\ have "invar (fold ins xs B)" for xs apply (induction xs arbitrary: B) apply (auto simp: ins_invar) done then show "invar (fold ins (to_list A) B)" by simp qed lemma union_\: assumes "invar A" assumes "invar B" shows "\ (union A B) = \ A \ \ B" unfolding union_def proof - from \invar B\ have "\ (fold ins xs B) = set xs \ \ B" for xs apply (induction xs arbitrary: B) apply (auto simp: ins_\ ins_invar) done from this[of "to_list A"] show "\ (fold ins (to_list A) B) = \ A \ \ B" thm to_list_\[OF \invar A\] by (simp add: to_list_\[OF \invar A\]) qed text \Define an intersection function and show its interface specification\ definition intersect :: "'s \ 's \ 's" where "intersect A B \ fold (\x res. if is_in B x then ins x res else res) (to_list A) empty" lemma intersect_invar: assumes "invar A" and "invar B" shows "invar (intersect A B)" proof - have "invar (fold (\x res. if is_in B x then ins x res else res) xs s)" if invs: "invar s" for xs s using invs apply (induction xs arbitrary: s) apply (auto simp: ins_invar) done from this[OF empty_invar] show ?thesis unfolding intersect_def . qed lemma intersect_\: assumes "invar A" assumes "invar B" shows "\ (intersect A B) = \ A \ \ B" proof - have "\ (fold (\x res. if is_in B x then ins x res else res) xs s) = \ s \ (set xs \ \ B)" if "invar s" for s xs using that apply (induction xs arbitrary: s) apply (auto simp: ins_\ ins_invar is_in_\ \invar B\) done from this[OF empty_invar] to_list_\[OF \invar A\] show ?thesis unfolding intersect_def by (auto simp: empty_\) 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 subgoal by (simp add: set_tree_isin) subgoal by (simp add: set_tree_isin) subgoal by (simp add: bst_ins) subgoal by (simp add: set_tree_ins) subgoal by (simp add: set_tree_ins) subgoal by (simp add: 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 \ term List.insert export_code List.insert in SML interpretation dl_set: set_interface distinct set "[]" "List.member" "List.insert" "\x. x" apply unfold_locales apply (auto simp: in_set_member) done term dl_set.union thm dl_set.union_\ (*<*) end (*>*)