products/sources/formale Sprachen/Isabelle/HOL/IMP image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Sem_Equiv.thy   Sprache: Isabelle

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

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


Bot Zugriff