|
(* 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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
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.
|
