header {* \isaheader{Examples from ITP-2010 slides} *}
theory itp_2010
imports "../Collections"
begin
text {*
Illustrates the various possibilities how to use the ICF in your own
algorithms by simple examples. The examples all use the data refinement scheme,
and either define a generic algorithm or fix the operations.
*}
-- "Example for slides"
subsection "List to Set"
text {*
In this simple example we do conversion from a list to a set.
We define an abstract algorithm.
This is then refined by a generic algorithm using a locale and by a generic
algorithm fixing its operations as parameters.
*}
subsubsection "Straightforward version"
-- "Abstract algorithm"
fun set_a where
"set_a [] s = s" |
"set_a (a#l) s = set_a l (insert a s)"
-- "Correctness of aa"
lemma set_a_correct: "set_a l s = set l ∪ s"
by (induct l arbitrary: s) auto
-- "Generic algorithm"
fun (in StdSetDefs) set_i where
"set_i [] s = s" |
"set_i (a#l) s = set_i l (ins a s)"
-- "Correct implementation of ca"
lemma (in StdSet) set_i_impl: "invar s ==> invar (set_i l s) ∧ α (set_i l s) = set_a l (α s)"
by (induct l arbitrary: s) (auto simp add: correct)
-- "Instantiation"
definition "hs_seti == hsr.set_i"
declare hsr.set_i.simps[folded hs_seti_def, code]
lemmas hs_set_i_impl = hsr.set_i_impl[folded hs_seti_def]
export_code hs_seti in SML file -
-- "Code generation"
ML_val {* @{code hs_seti} *}
subsubsection "Tail-Recursive version"
-- "Abstract algorithm"
fun set_a2 where
"set_a2 [] = {}" |
"set_a2 (a#l) = (insert a (set_a2 l))"
-- "Correctness of aa"
lemma set_a2_correct: "set_a2 l = set l"
by (induct l) auto
-- "Generic algorithm"
fun (in StdSetDefs) set_i2 where
"set_i2 [] = empty ()" |
"set_i2 (a#l) = (ins a (set_i2 l))"
-- "Correct implementation of ca"
lemma (in StdSet) set_i2_impl: "invar s ==> invar (set_i2 l) ∧ α (set_i2 l) = set_a2 l"
by (induct l) (auto simp add: correct)
-- "Instantiation"
definition "hs_seti2 == hsr.set_i2"
declare hsr.set_i2.simps[folded hs_seti2_def, code]
lemmas hs_set_i2_impl = hsr.set_i2_impl[folded hs_seti2_def]
-- "Code generation"
ML_val {* @{code hs_seti2} *}
subsubsection "With explicit operation parameters"
-- "Alternative for few operation parameters"
fun set_i' where
"!!ins. set_i' ins [] s = s" |
"!!ins. set_i' ins (a#l) s = set_i' ins l (ins a s)"
lemma (in StdSet) set_i'_impl:
"invar s ==> invar (set_i' ins l s) ∧ α (set_i' ins l s) = set_a l (α s)"
by (induct l arbitrary: s) (auto simp add: correct)
-- "Instantiation"
definition "hs_seti' == set_i' hs_ins"
lemmas hs_set_i'_impl = hsr.set_i'_impl[folded hs_seti'_def, unfolded hs_ops_unfold]
-- "Code generation"
ML_val {* @{code hs_seti'} *}
subsection "Complex Example: Filter Average"
text {*
In this more complex example, we develop a function that filters from a set all
numbers that are above the average of the set.
First, we formulate this as a generic algorithm using a locale.
This solution illustrates some technical problems with larger generic
algorithms:
\begin{itemize}
\item Operations that are used with different types within the generic
algorithm need to be specified multiple times, once for every type.
This is an inherent problem with Isabelle's type system, and there is
no obvious solution.
This effect occurs especially when one uses the same type of set/map
for different element types, or uses operations that have some
additional type parameters, like the iterators in our example.
\item The code generator has problems generating code for instantiated
algorithms. This is due to the resulting equations having the
instantiated part fixed on their lhs. This problem could probably be
solved within the code generator. The workaround we use here is to
define one new constant per function and instantiation and alter the
code equations using this definitions. This could probably be automated
and/or integrated into the code generator.
\end{itemize}
The second possibility avoids the above problems by fixing the used
implementaion beforehand. Changing the implementation is still easy by
changing the used operations. In this example, all used operations are
introduced by abbbreviations, localizing the required changes to a small part
of the theory.
*}
abbreviation "average S == ∑S div card S"
locale MyContextDefs =
StdSetDefs ops for ops :: "(nat,'s,'more) set_ops_scheme" +
fixes iterate :: "'s => (nat,nat×nat) set_iterator"
fixes iterate' :: "'s => (nat,'s) set_iterator"
begin
definition avg_aux :: "'s => nat×nat"
where
"avg_aux s == iterate s (λ_. True) (λx (c,s). (c+1, s+x)) (0,0)"
definition "avg s == case avg_aux s of (c,s) => s div c"
definition "filter_le_avg s == let a=avg s in
iterate' s (λ_. True) (λx s. if x≤a then ins x s else s) (empty ())"
end
locale MyContext = MyContextDefs ops iterate iterate' +
StdSet ops +
it!: set_iteratei α invar iterate +
it'!: set_iteratei α invar iterate'
for ops iterate iterate'
begin
lemma avg_aux_correct: "invar s ==> avg_aux s = (card (α s), ∑(α s) )"
apply (unfold avg_aux_def)
apply (rule_tac
I="λit (c,sum). c=card (α s - it) ∧ sum=∑(α s - it)"
in it.iterate_rule_P)
apply auto
apply (subgoal_tac "α s - (it - {x}) = insert x (α s - it)")
apply auto
apply (subgoal_tac "α s - (it - {x}) = insert x (α s - it)")
apply auto
done
lemma avg_correct: "invar s ==> avg s = average (α s)"
unfolding avg_def
using avg_aux_correct
by auto
lemma filter_le_avg_correct:
"invar s ==>
invar (filter_le_avg s) ∧
α (filter_le_avg s) = {x∈α s. x≤average (α s)}"
unfolding filter_le_avg_def Let_def
apply (rule_tac
I="λit r. invar r ∧ α r = {x∈α s - it. x≤average (α s)}"
in it'.iterate_rule_P)
apply (auto simp add: correct avg_correct)
done
end
interpretation hs_ctx: MyContext hs_ops hs_iteratei hs_iteratei
by unfold_locales
definition "test_hs == hs_ins (1::nat) (hs_ins 10 (hs_ins 11 (hs_empty ())))"
definition "testfun_hs == hs_ctx.filter_le_avg"
definition "hs_avg_aux == hs_ctx.avg_aux"
definition "hs_avg == hs_ctx.avg"
definition "hs_filter_le_avg == hs_ctx.filter_le_avg"
lemmas hs_ctx_defs = hs_avg_aux_def hs_avg_def hs_filter_le_avg_def
lemmas [code] = hs_ctx.avg_aux_def[folded hs_ctx_defs]
lemmas [code] = hs_ctx.avg_def[folded hs_ctx_defs]
lemmas [code] = hs_ctx.filter_le_avg_def[folded hs_ctx_defs]
interpretation rs_ctx: MyContext rs_ops rs_iteratei rs_iteratei
by unfold_locales
definition "test_rs == rs_ins (1::nat) (rs_ins 10 (rs_ins 11 (rs_empty ())))"
definition "testfun_rs == rs_ctx.filter_le_avg"
definition "rs_avg_aux == rs_ctx.avg_aux"
definition "rs_avg == rs_ctx.avg"
definition "rs_filter_le_avg == rs_ctx.filter_le_avg"
lemmas rs_ctx_defs = rs_avg_aux_def rs_avg_def rs_filter_le_avg_def
lemmas [code] = rs_ctx.avg_aux_def[folded rs_ctx_defs]
lemmas [code] = rs_ctx.avg_def[folded rs_ctx_defs]
lemmas [code] = rs_ctx.filter_le_avg_def[folded rs_ctx_defs]
-- "Code generation"
ML_val {* @{code hs_filter_le_avg} @{code test_hs} *}
-- "Using abbreviations"
type_synonym 'a my_set = "'a hs"
abbreviation "my_α == hs_α"
abbreviation "my_invar == hs_invar"
abbreviation "my_empty == hs_empty"
abbreviation "my_ins == hs_ins"
abbreviation "my_iterate == hs_iteratei"
lemmas my_correct = hs_correct
lemmas my_iterate_rule_P = hs.iterate_rule_P
definition avg_aux :: "nat my_set => nat×nat"
where
"avg_aux s == my_iterate s (λ_. True) (λx (c,s). (c+1, s+x)) (0,0)"
definition "avg s == case avg_aux s of (c,s) => s div c"
definition "filter_le_avg s == let a=avg s in
my_iterate s (λ_. True) (λx s. if x≤a then my_ins x s else s) (my_empty ())"
lemma avg_aux_correct: "my_invar s ==> avg_aux s = (card (my_α s), ∑(my_α s) )"
apply (unfold avg_aux_def)
apply (rule_tac
I="λit (c,sum). c=card (my_α s - it) ∧ sum=∑(my_α s - it)"
in my_iterate_rule_P)
apply auto
apply (subgoal_tac "my_α s - (it - {x}) = insert x (my_α s - it)")
apply auto
apply (subgoal_tac "my_α s - (it - {x}) = insert x (my_α s - it)")
apply auto
done
lemma avg_correct: "my_invar s ==> avg s = average (my_α s)"
unfolding avg_def
using avg_aux_correct
by auto
lemma filter_le_avg_correct:
"my_invar s ==>
my_invar (filter_le_avg s) ∧
my_α (filter_le_avg s) = {x∈my_α s. x≤average (my_α s)}"
unfolding filter_le_avg_def Let_def
apply (rule_tac
I="λit r. my_invar r ∧ my_α r = {x∈my_α s - it. x≤average (my_α s)}"
in my_iterate_rule_P)
apply (auto simp add: my_correct avg_correct)
done
definition "test_set == my_ins (1::nat) (my_ins 2 (my_ins 3 (my_empty ())))"
export_code avg_aux avg filter_le_avg test_set in SML module_name Test file -
end