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