# Re: [isabelle] Iteration until saturation

Peter,
> 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.

`It seems the best way to to this is using recdef (I assume you are using
``Isabelle 2005, otherwise the new "function" package for partial
``functions would be just what you need)
`

`The problem here is that the function might not terminate if called
``outside the finite set U you mention...? In this case, you might need to
``have an extra check for this:
`
recdef algo "???"
"algo v = (if v \subseteq U then
then if f v \subseteq v then v else algo (v \union f v)
else arbitrary)"

`for the termination relation, you should be able to construct something
``using the predefined wellfounded relation "finite_psubset".
`

`I replaced the "pointwise" addition by a union, which should be the same
``if f is monotone...
`
> 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}).
From this you should also be able to prove
"[| v \subseteq U; P v |] ==> P (v \union f v)"

`(using your finiteness assumptions and induction) which together with
``algo.induct gives you your result.
`
Hope this helps...
Alex
--
Alexander Krauss E-Mail: krauss at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17300
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3 Room: 01.11.060
85748 Garching, GERMANY http://www4.in.tum.de/~kraussPeter

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*