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