Quelle Equiv.thy Sprache: Isabelle

(*  Title:      ZF/IMP/Equiv.thy
    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
*)

section \<open>Equivalence\<close>

theory Equiv imports Denotation Com begin

lemma aexp_iff [rule_format]:
  "\a \ aexp; sigma: loc -> nat\
    \<Longrightarrow> \<forall>n. \<langle>a,sigma\<rangle> -a-> n \<longleftrightarrow> A(a,sigma) = n"
  apply (erule aexp.induct)
     apply (force intro!: evala.intros)+
  done

declare aexp_iff [THEN iffD1, simp]
        aexp_iff [THEN iffD2, intro!]

inductive_cases [elim!]:
  "\true,sigma\ -b-> x"
  "\false,sigma\ -b-> x"
  " -b-> x"
  " -b-> x"
  " -b-> x"
  " -b-> x"

lemma bexp_iff [rule_format]:
  "\b \ bexp; sigma: loc -> nat\
    \<Longrightarrow> \<forall>w. \<langle>b,sigma\<rangle> -b-> w \<longleftrightarrow> B(b,sigma) = w"
  apply (erule bexp.induct)
  apply (auto intro!: evalb.intros)
  done

declare bexp_iff [THEN iffD1, simp]
        bexp_iff [THEN iffD2, intro!]

lemma com1: "\c,sigma\ -c-> sigma' \ \ C(c)"
  apply (erule evalc.induct)
        apply (simp_all (no_asm_simp))
     txt \<open>\<open>assign\<close>\<close>
     apply (simp add: update_type)
    txt \<open>\<open>comp\<close>\<close>
    apply fast
   txt \<open>\<open>while\<close>\<close>
   apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
   apply (simp add: Gamma_def)
  txt \<open>recursive case of \<open>while\<close>\<close>
  apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
  apply (auto simp add: Gamma_def)
  done

declare B_type [intro!] A_type [intro!]
declare evalc.intros [intro]

lemma com2 [rule_format]: "c \ com \ \x \ C(c). -c-> snd(x)"
  apply (erule com.induct)
      txt \<open>\<open>skip\<close>\<close>
      apply force
     txt \<open>\<open>assign\<close>\<close>
     apply force
    txt \<open>\<open>comp\<close>\<close>
    apply force
   txt \<open>\<open>while\<close>\<close>
   apply safe
   apply simp_all
   apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
     unfolding Gamma_def
   apply force
  txt \<open>\<open>if\<close>\<close>
  apply auto
  done

subsection \<open>Main theorem\<close>

theorem com_equivalence:
    "c \ com \ C(c) = {io \ (loc->nat) \ (loc->nat). -c-> snd(io)}"
  by (force intro: C_subset [THEN subsetD] elim: com2 dest: com1)

end

quality100%

¤ 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.