[isabelle] Iteration until saturation
Hi list,
I want to formalize a saturation algorithm.
That is, I start with some initial set v_0:: 's set and have a function
f:: 's set => 's set that maps sets to additional elements that should
be added.
Imperatively, I have the following algorithm:
input: v0
precondition: v0 \subseteq U & P v0
v:=v_0
while there is some x with x \in f v and not x \in v do v:=v \cup {x}; od
output: v
Function f is monotonous.
Termination is because I have a finite set U such that v_0 \subseteq U
and v\subseteq U ==> f v \subseteq U.
To prove something about the result, I have an invariant P, such that P
v_0 and [P v; x\in f v  v ] ==> P (v \cup {x}).
What approach should I use to formalize this algorithm in isabelle, i.e.
define some Isabelle function algo: 's set => 's set that describes the
algorithm above, and
how to prove
v0 \subseteq U & P v0 ==> P algo v0
and
v0 \subseteq U & P v0 ==> f(algo v0) \subseteq algo v0
My main problem with using inductive definition, i.e. somthing like
inductive "algo v0"
intros
"x\in v0 ==> x \in algo v0"
"x\in f (algo v0) ==> x \in (algo v0)"
monos f_mono
is, that I cannot use the invariant P to reason about the correctness of
the result. Using algo.induct, I can only reason about single elements
of (algo v0), but not
about the set as whole (as this reasoning would not be correct in
general for infinite sets).
Thanks in advance for any hints or pointers to examples of formalization
of such algorithms.
 Peter
 Previous by Date: [isabelle] 2nd CFP: Workshop on Invariant Generation (WING 2007), RISC, Hagenberg, Austria, 2526 June, 2007
 Next by Date: Re: [isabelle] Iteration until saturation
 Previous by Thread: [isabelle] 2nd CFP: Workshop on Invariant Generation (WING 2007), RISC, Hagenberg, Austria, 2526 June, 2007
 Next by Thread: Re: [isabelle] Iteration until saturation

Clisabelleusers January 2007 archives indexes sorted by: [ thread ]
[ subject ]
[ author ]
[ date ]

Clisabelleusers list archive Table of Contents

More information about the Clisabelleusers mailing list
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.