subsection "A small step semantics on annotated commands"
theory Collecting1 imports Collecting begin
text\<open>The idea: the state is propagated through the annotated command as an
annotation \<^term>\<open>{s}\<close>, all other annotations are \<^term>\<open>{}\<close>. It is easy toshow that this semantics approximates the collecting semantics.\<close>
lemma step_preserves_le: "\ step S cs = cs; S' \ S; cs' \ cs \ \
step S' cs'\<le> 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 ?caseby 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}"] \<open>s \<in> S\<close> 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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
