Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Collecting1.thy Sprache: Isabelle

Original von: 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

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.