# [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



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