Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/IMP/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 6 kB

Quelle Sem_Equiv.thy Sprache: Isabelle

section "Constant Folding"

theory Sem_Equiv
imports Big_Step
begin

subsection "Semantic Equivalence up to a Condition"

type_synonym assn = "state \ bool"

definition
  equiv_up_to :: "assn \ com \ com \ bool" (\_ \ _ \ _\ [50,0,10] 50)
where
  "(P \ c \ c') = (\s s'. P s \ (c,s) \ s' \ (c',s) \ s')"

definition
  bequiv_up_to :: "assn \ bexp \ bexp \ bool" (\_ \ _ <\> _\ [50,0,10] 50)
where
  "(P \ b <\> b') = (\s. P s \ bval b s = bval b' s)"

lemma equiv_up_to_True:
  "((\_. True) \ c \ c') = (c \ c')"
  by (simp add: equiv_def equiv_up_to_def)

lemma equiv_up_to_weaken:
  "P \ c \ c' \ (\s. P' s \ P s) \ P' \ c \ c'"
  by (simp add: equiv_up_to_def)

lemma equiv_up_toI:
  "(\s s'. P s \ (c, s) \ s' = (c', s) \ s') \ P \ c \ c'"
  by (unfold equiv_up_to_def) blast

lemma equiv_up_toD1:
  "P \ c \ c' \ (c, s) \ s' \ P s \ (c', s) \ s'"
  by (unfold equiv_up_to_def) blast

lemma equiv_up_toD2:
  "P \ c \ c' \ (c', s) \ s' \ P s \ (c, s) \ s'"
  by (unfold equiv_up_to_def) blast

lemma equiv_up_to_refl [simp, intro!]:
  "P \ c \ c"
  by (auto simp: equiv_up_to_def)

lemma equiv_up_to_sym:
  "(P \ c \ c') = (P \ c' \ c)"
  by (auto simp: equiv_up_to_def)

lemma equiv_up_to_trans:
  "P \ c \ c' \ P \ c' \ c'' \ P \ c \ c''"
  by (auto simp: equiv_up_to_def)

lemma bequiv_up_to_refl [simp, intro!]:
  "P \ b <\> b"
  by (auto simp: bequiv_up_to_def)

lemma bequiv_up_to_sym:
  "(P \ b <\> b') = (P \ b' <\> b)"
  by (auto simp: bequiv_up_to_def)

lemma bequiv_up_to_trans:
  "P \ b <\> b' \ P \ b' <\> b'' \ P \ b <\> b''"
  by (auto simp: bequiv_up_to_def)

lemma bequiv_up_to_subst:
  "P \ b <\> b' \ P s \ bval b s = bval b' s"
  by (simp add: bequiv_up_to_def)

lemma equiv_up_to_seq:
  "P \ c \ c' \ Q \ d \ d' \
  (\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> Q s') \<Longrightarrow>
  P \<Turnstile> (c;; d) \<sim> (c';; d')"
  by (clarsimp simp: equiv_up_to_def) blast

lemma equiv_up_to_while_lemma_weak:
  shows "(d,s) \ s' \
         P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
         P \<Turnstile> c \<sim> c' \<Longrightarrow>
         (\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
         P s \<Longrightarrow>
         d = WHILE b DO c \<Longrightarrow>
         (WHILE b' DO c', s) \<Rightarrow> s'"
proof (induction rule: big_step_induct)
  case (WhileTrue b s1 c s2 s3)
  hence IH: "P s2 \ (WHILE b' DO c', s2) \ s3" by auto
  from WhileTrue.prems
  have "P \ b <\> b'" by simp
  with \<open>bval b s1\<close> \<open>P s1\<close>
  have "bval b' s1" by (simp add: bequiv_up_to_def)
  moreover
  from WhileTrue.prems
  have "P \ c \ c'" by simp
  with \<open>bval b s1\<close> \<open>P s1\<close> \<open>(c, s1) \<Rightarrow> s2\<close>
  have "(c', s1) \ s2" by (simp add: equiv_up_to_def)
  moreover
  from WhileTrue.prems
  have "\s s'. (c,s) \ s' \ P s \ bval b s \ P s'" by simp
  with \<open>P s1\<close> \<open>bval b s1\<close> \<open>(c, s1) \<Rightarrow> s2\<close>
  have "P s2" by simp
  hence "(WHILE b' DO c', s2) \ s3" by (rule IH)
  ultimately
  show ?case by blast
next
  case WhileFalse
  thus ?case by (auto simp: bequiv_up_to_def)
qed (fastforce simp: equiv_up_to_def bequiv_up_to_def)+

lemma equiv_up_to_while_weak:
  assumes b: "P \ b <\> b'"
  assumes c: "P \ c \ c'"
  assumes I: "\s s'. (c, s) \ s' \ P s \ bval b s \ P s'"
  shows "P \ WHILE b DO c \ WHILE b' DO c'"
proof -
  from b have b': "P \ b' <\> b" by (simp add: bequiv_up_to_sym)

  from c b have c': "P \ c' \ c" by (simp add: equiv_up_to_sym)

  from I
  have I': "\s s'. (c', s) \ s' \ P s \ bval b' s \ P s'"
    by (auto dest!: equiv_up_toD1 [OF c'] simp: bequiv_up_to_subst [OF b'])

  note equiv_up_to_while_lemma_weak [OF _ b c]
       equiv_up_to_while_lemma_weak [OF _ b' c']
  thus ?thesis using I I' by (auto intro!: equiv_up_toI)
qed

lemma equiv_up_to_if_weak:
  "P \ b <\> b' \ P \ c \ c' \ P \ d \ d' \
   P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
  by (auto simp: bequiv_up_to_def equiv_up_to_def)

lemma equiv_up_to_if_True [intro!]:
  "(\s. P s \ bval b s) \ P \ IF b THEN c1 ELSE c2 \ c1"
  by (auto simp: equiv_up_to_def)

lemma equiv_up_to_if_False [intro!]:
  "(\s. P s \ \ bval b s) \ P \ IF b THEN c1 ELSE c2 \ c2"
  by (auto simp: equiv_up_to_def)

lemma equiv_up_to_while_False [intro!]:
  "(\s. P s \ \ bval b s) \ P \ WHILE b DO c \ SKIP"
  by (auto simp: equiv_up_to_def)

lemma while_never: "(c, s) \ u \ c \ WHILE (Bc True) DO c'"
by (induct rule: big_step_induct) auto

lemma equiv_up_to_while_True [intro!,simp]:
  "P \ WHILE Bc True DO c \ WHILE Bc True DO SKIP"
  unfolding equiv_up_to_def
  by (blast dest: while_never)

end

quality98%

¤ Dauer der Verarbeitung: 0.12 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.