(* Title: ZF/IMP/Equiv.thy Author: Heiko Loetzbeyer and Robert Sandner, TU München \<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]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]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 fasttxt \<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 forcetxt \<open>\<open>assign\<close>\<close> apply forcetxt \<open>\<open>comp\<close>\<close> apply forcetxt \<open>\<open>while\<close>\<close> apply safeapply simp_allapply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)unfolding Gamma_defapply forcetxt \<open>\<open>if\<close>\<close> apply autodone \<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 quality 100%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
