(*<*)
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
(*>*)