Quelle Collecting1.thy Sprache: Isabelle

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
to show 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 ?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}"] \<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

quality98%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.