# Theory Equiv

Up to index of Isabelle/ZF/IMP

theory Equiv
imports Denotation Com
begin

    (*  Title:      ZF/IMP/Equiv.thy
        ID:         $Id: Equiv.thy,v 1.8 2005/06/17 14:15:11 haftmann Exp $
        Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    *)

    header {* Equivalence *}

    theory Equiv imports Denotation Com begin

    lemma aexp_iff [rule_format]:
      "[| a ∈ aexp; sigma: loc -> nat |]
        ==> ALL 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"
      "<ROp(f,a0,a1),sigma> -b-> x"
      "<noti(b),sigma> -b-> x"
      "<b0 andi b1,sigma> -b-> x"
      "<b0 ori b1,sigma> -b-> x"

    lemma bexp_iff [rule_format]:
      "[| b ∈ bexp; sigma: loc -> nat |]
        ==> ALL 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' ==> <sigma,sigma'> ∈ C(c)"
      apply (erule evalc.induct)
            apply (simp_all (no_asm_simp))
         txt {* @{text assign} *}
         apply (simp add: update_type)
        txt {* @{text comp} *}
        apply fast
       txt {* @{text while} *}
       apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
       apply (simp add: Gamma_def)
      txt {* recursive case of @{text 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,fst(x)> -c-> snd(x)"
      apply (erule com.induct)
          txt {* @{text skip} *}
          apply force
         txt {* @{text assign} *}
         apply force
        txt {* @{text comp} *}
        apply force
       txt {* @{text while} *}
       apply safe
       apply simp_all
       apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
       apply (unfold Gamma_def)
       apply force
      txt {* @{text if} *}
      apply auto
      done

    subsection {* Main theorem *}

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

    end

lemma aexp_iff:

      [| a ∈ aexp; sigma ∈ loc -> nat |] ==> ⟨a, sigma⟩ -a-> n <-> A(a, sigma) = n

lemmas

      [| ⟨true, sigma⟩ -b-> x; [| sigma ∈ loc -> nat; x = 1 |] ==> Q |] ==> Q

      [| ⟨false, sigma⟩ -b-> x; [| sigma ∈ loc -> nat; x = 0 |] ==> Q |] ==> Q

      [| ⟨ROp(f, a0.0, a1.0), sigma⟩ -b-> x;
         !!n0 n1.
            [| ⟨a0.0, sigma⟩ -a-> n0; ⟨a1.0, sigma⟩ -a-> n1; f ∈ nat × nat -> bool;
               x = f ` ⟨n0, n1⟩ |]
            ==> Q |]
      ==> Q

      [| ⟨noti(b), sigma⟩ -b-> x; !!w. [| ⟨b, sigma⟩ -b-> w; x = not(w) |] ==> Q |]
      ==> Q

      [| ⟨b0.0 andi b1.0, sigma⟩ -b-> x;
         !!w0 w1.
            [| ⟨b0.0, sigma⟩ -b-> w0; ⟨b1.0, sigma⟩ -b-> w1; x = w0 and w1 |] ==> Q |]
      ==> Q

      [| ⟨b0.0 ori b1.0, sigma⟩ -b-> x;
         !!w0 w1.
            [| ⟨b0.0, sigma⟩ -b-> w0; ⟨b1.0, sigma⟩ -b-> w1; x = w0 or w1 |] ==> Q |]
      ==> Q

lemma bexp_iff:

      [| b ∈ bexp; sigma ∈ loc -> nat |] ==> ⟨b, sigma⟩ -b-> w <-> B(b, sigma) = w

lemma com1:

      ⟨c, sigma⟩ -c-> sigma' ==> ⟨sigma, sigma'⟩ ∈ C(c)

lemma com2:

      [| c ∈ com; x ∈ C(c) |] ==> ⟨c, fst(x)⟩ -c-> snd(x)

### Main theorem

theorem com_equivalence:

      c ∈ com
      ==> C(c) = {io ∈ (loc -> nat) × (loc -> nat) . ⟨c, fst(io)⟩ -c-> snd(io)}