theory Collecting1

imports Collecting

begin

subsection "A small step semantics on annotated commands"

text{* The idea: the state is propagated through the annotated command as an

annotation @{term "{s}"}, all other annotations are @{term "{}"}. It is easy

to show that this semantics approximates the collecting semantics. *}

lemma step_preserves_le:

"[| step S cs = cs; S' ⊆ S; cs' ≤ cs |] ==>

step S' cs' ≤ cs"

by (metis mono2_step)

lemma steps_empty_preserves_le: assumes "step S cs = cs"

shows "cs' ≤ cs ==> (step {} ^^ n) cs' ≤ cs"

proof(induction n arbitrary: cs')

case 0 thus ?case by simp

next

case (Suc n) thus ?case

using Suc.IH[OF step_preserves_le[OF assms empty_subsetI Suc.prems]]

by(simp add:funpow_swap1)

qed

definition steps :: "state => com => nat => state set acom" where

"steps s c n = ((step {})^^n) (step {s} (annotate (λp. {}) c))"

lemma steps_approx_fix_step: assumes "step S cs = cs" and "s:S"

shows "steps s (strip cs) n ≤ cs"

proof-

let ?bot = "annotate (λp. {}) (strip cs)"

have "?bot ≤ cs" by(induction cs) auto

from step_preserves_le[OF assms(1)_ this, of "{s}"] `s:S`

have 1: "step {s} ?bot ≤ cs" by simp

from steps_empty_preserves_le[OF assms(1) 1]

show ?thesis by(simp add: steps_def)

qed

theorem steps_approx_CS: "steps s c n ≤ CS c"

by (metis CS_unfold UNIV_I steps_approx_fix_step strip_CS)

end