Theory Collecting1

subsection "A small step semantics on annotated commands"

theory Collecting1
imports Collecting

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
  case (Suc n) thus ?case
    using Suc.IH[OF step_preserves_le[OF assms empty_subsetI Suc.prems]]
    by(simp add:funpow_swap1)

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"
  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)

theorem steps_approx_CS: "steps s c n  CS c"
by (metis CS_unfold UNIV_I steps_approx_fix_step strip_CS)