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