Quelle  Equiv.thy

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

section ‹Equivalence›

theory Equiv imports Denotation Com begin

lemma aexp_iff [rule_format]:
  "[a ∈ aexp; sigma: loc -> nat]
    ==> ∀n. ⟨a,sigma⟩ -a-> n ⟷ 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]
    ==> ∀w. ⟨b,sigma⟩ -b-> w ⟷ 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 ‹‹assign›\›
     apply (simp add: update_type)
    txt ‹‹comp›\›
    apply fast
   txt ‹‹while›\›
   apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
   apply (simp add: Gamma_def)
  txt ‹recursive case of ‹while›\›
  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 ‹‹skip›\›
      apply force
     txt ‹‹assign›\›
     apply force
    txt ‹‹comp›\›
    apply force
   txt ‹‹while›\›
   apply safe
   apply simp_all
   apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
     unfolding Gamma_def
   apply force
  txt ‹‹if›\›
  apply auto
  done


subsection ‹Main theorem›

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