Re: [isabelle] Iteration until saturation


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

Alexander Krauss                   E-Mail: krauss at
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  

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