src/ZF/IMP/Equiv.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 19796 d86e7b1fc472
child 35762 af3ff2ba4c54
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
     1 (*  Title:      ZF/IMP/Equiv.thy
     2     ID:         $Id$
     3     Author:     Heiko Loetzbeyer and Robert Sandner, TU München
     4 *)
     5 
     6 header {* Equivalence *}
     7 
     8 theory Equiv imports Denotation Com begin
     9 
    10 lemma aexp_iff [rule_format]:
    11   "[| a \<in> aexp; sigma: loc -> nat |] 
    12     ==> ALL n. <a,sigma> -a-> n <-> A(a,sigma) = n"
    13   apply (erule aexp.induct)
    14      apply (force intro!: evala.intros)+
    15   done
    16 
    17 declare aexp_iff [THEN iffD1, simp]
    18         aexp_iff [THEN iffD2, intro!]
    19 
    20 inductive_cases [elim!]:
    21   "<true,sigma> -b-> x"
    22   "<false,sigma> -b-> x"
    23   "<ROp(f,a0,a1),sigma> -b-> x"
    24   "<noti(b),sigma> -b-> x"
    25   "<b0 andi b1,sigma> -b-> x"
    26   "<b0 ori b1,sigma> -b-> x"
    27 
    28 
    29 lemma bexp_iff [rule_format]:
    30   "[| b \<in> bexp; sigma: loc -> nat |] 
    31     ==> ALL w. <b,sigma> -b-> w <-> B(b,sigma) = w"
    32   apply (erule bexp.induct) 
    33   apply (auto intro!: evalb.intros)
    34   done
    35 
    36 declare bexp_iff [THEN iffD1, simp]
    37         bexp_iff [THEN iffD2, intro!]
    38 
    39 lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)"
    40   apply (erule evalc.induct)
    41         apply (simp_all (no_asm_simp))
    42      txt {* @{text assign} *}
    43      apply (simp add: update_type)
    44     txt {* @{text comp} *}
    45     apply fast
    46    txt {* @{text while} *}
    47    apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
    48    apply (simp add: Gamma_def)
    49   txt {* recursive case of @{text while} *}
    50   apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
    51   apply (auto simp add: Gamma_def)
    52   done
    53 
    54 declare B_type [intro!] A_type [intro!]
    55 declare evalc.intros [intro]
    56 
    57 
    58 lemma com2 [rule_format]: "c \<in> com ==> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)"
    59   apply (erule com.induct)
    60       txt {* @{text skip} *}
    61       apply force
    62      txt {* @{text assign} *}
    63      apply force
    64     txt {* @{text comp} *}
    65     apply force
    66    txt {* @{text while} *}
    67    apply safe
    68    apply simp_all
    69    apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
    70    apply (unfold Gamma_def)
    71    apply force
    72   txt {* @{text "if"} *}
    73   apply auto
    74   done
    75 
    76 
    77 subsection {* Main theorem *}
    78 
    79 theorem com_equivalence:
    80     "c \<in> com ==> C(c) = {io \<in> (loc->nat) \<times> (loc->nat). <c,fst(io)> -c-> snd(io)}"
    81   by (force intro: C_subset [THEN subsetD] elim: com2 dest: com1)
    82 
    83 end
    84