products/sources/formale sprachen/Isabelle/ZF/IMP/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: reals.summary   Sprache: Isabelle

Untersuchung 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 |]
    ==> \<forall>n. <a,sigma> -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!]:
  " -b-> x"
  " -b-> x"
  " -b-> x"
  " -b-> x"
  " -b-> x"
  " -b-> x"


lemma bexp_iff [rule_format]:
  "[| b \ bexp; sigma: loc -> nat |]
    ==> \<forall>w. <b,sigma> -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(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)
   apply (unfold 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


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.27Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Kontakt
Drucken
Kontakt
Hier finden Sie eine Liste der Produkte des Unternehmens

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff