src/ZF/IMP/Com.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 19796 d86e7b1fc472
child 22808 a7daa74e2980
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
clasohm@1478
     1
(*  Title:      ZF/IMP/Com.thy
nipkow@482
     2
    ID:         $Id$
wenzelm@12610
     3
    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
wenzelm@12610
     4
*)
nipkow@482
     5
wenzelm@12610
     6
header {* Arithmetic expressions, boolean expressions, commands *}
nipkow@482
     7
haftmann@16417
     8
theory Com imports Main begin
lcp@511
     9
wenzelm@12610
    10
wenzelm@12610
    11
subsection {* Arithmetic expressions *}
lcp@511
    12
wenzelm@12610
    13
consts
wenzelm@12610
    14
  loc :: i
wenzelm@12610
    15
  aexp :: i
wenzelm@12610
    16
wenzelm@12610
    17
datatype \<subseteq> "univ(loc \<union> (nat -> nat) \<union> ((nat \<times> nat) -> nat))"
wenzelm@12610
    18
  aexp = N ("n \<in> nat")
wenzelm@12610
    19
       | X ("x \<in> loc")
wenzelm@12610
    20
       | Op1 ("f \<in> nat -> nat", "a \<in> aexp")
wenzelm@12610
    21
       | Op2 ("f \<in> (nat \<times> nat) -> nat", "a0 \<in> aexp", "a1 \<in> aexp")
lcp@511
    22
lcp@511
    23
wenzelm@12610
    24
consts evala :: i
wenzelm@12610
    25
syntax "_evala" :: "[i, i] => o"    (infixl "-a->" 50)
wenzelm@12610
    26
translations "p -a-> n" == "<p,n> \<in> evala"
wenzelm@12610
    27
lcp@511
    28
inductive
wenzelm@12610
    29
  domains "evala" \<subseteq> "(aexp \<times> (loc -> nat)) \<times> nat"
wenzelm@12610
    30
  intros
paulson@12606
    31
    N:   "[| n \<in> nat;  sigma \<in> loc->nat |] ==> <N(n),sigma> -a-> n"
paulson@12606
    32
    X:   "[| x \<in> loc;  sigma \<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
paulson@12606
    33
    Op1: "[| <e,sigma> -a-> n; f \<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
wenzelm@12610
    34
    Op2: "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f \<in> (nat\<times>nat) -> nat |]
paulson@12606
    35
          ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
paulson@12606
    36
  type_intros aexp.intros apply_funtype
lcp@511
    37
lcp@511
    38
wenzelm@12610
    39
subsection {* Boolean expressions *}
wenzelm@12610
    40
wenzelm@12610
    41
consts bexp :: i
lcp@511
    42
wenzelm@12610
    43
datatype \<subseteq> "univ(aexp \<union> ((nat \<times> nat)->bool))"
wenzelm@12610
    44
  bexp = true
wenzelm@12610
    45
       | false
wenzelm@12610
    46
       | ROp  ("f \<in> (nat \<times> nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
wenzelm@12610
    47
       | noti ("b \<in> bexp")
wenzelm@12610
    48
       | andi ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl 60)
wenzelm@12610
    49
       | ori  ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl 60)
lcp@511
    50
lcp@511
    51
wenzelm@12610
    52
consts evalb :: i
wenzelm@12610
    53
syntax "_evalb" :: "[i,i] => o"    (infixl "-b->" 50)
wenzelm@12610
    54
translations "p -b-> b" == "<p,b> \<in> evalb"
lcp@511
    55
lcp@511
    56
inductive
wenzelm@12610
    57
  domains "evalb" \<subseteq> "(bexp \<times> (loc -> nat)) \<times> bool"
wenzelm@12610
    58
  intros
wenzelm@12610
    59
    true:  "[| sigma \<in> loc -> nat |] ==> <true,sigma> -b-> 1"
wenzelm@12610
    60
    false: "[| sigma \<in> loc -> nat |] ==> <false,sigma> -b-> 0"
wenzelm@12610
    61
    ROp:   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \<in> (nat*nat)->bool |]
clasohm@1478
    62
           ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
paulson@12606
    63
    noti:  "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
wenzelm@12610
    64
    andi:  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
clasohm@1155
    65
          ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
wenzelm@12610
    66
    ori:   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
clasohm@1478
    67
            ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
wenzelm@12610
    68
  type_intros  bexp.intros
paulson@12606
    69
               apply_funtype and_type or_type bool_1I bool_0I not_type
paulson@12606
    70
  type_elims   evala.dom_subset [THEN subsetD, elim_format]
lcp@511
    71
lcp@511
    72
wenzelm@12610
    73
subsection {* Commands *}
lcp@511
    74
wenzelm@12610
    75
consts com :: i
wenzelm@12610
    76
datatype com =
wenzelm@12610
    77
    skip                                  ("\<SKIP>" [])
wenzelm@12610
    78
  | assignment ("x \<in> loc", "a \<in> aexp")       (infixl "\<ASSN>" 60)
wenzelm@12610
    79
  | semicolon ("c0 \<in> com", "c1 \<in> com")       ("_\<SEQ> _"  [60, 60] 10)
wenzelm@12610
    80
  | while ("b \<in> bexp", "c \<in> com")            ("\<WHILE> _ \<DO> _"  60)
wenzelm@19796
    81
  | "if" ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com")    ("\<IF> _ \<THEN> _ \<ELSE> _" 60)
lcp@511
    82
lcp@511
    83
wenzelm@12610
    84
consts evalc :: i
wenzelm@12610
    85
syntax "_evalc" :: "[i, i] => o"    (infixl "-c->" 50)
wenzelm@12610
    86
translations "p -c-> s" == "<p,s> \<in> evalc"
lcp@511
    87
lcp@511
    88
inductive
wenzelm@12610
    89
  domains "evalc" \<subseteq> "(com \<times> (loc -> nat)) \<times> (loc -> nat)"
paulson@12606
    90
  intros
wenzelm@12610
    91
    skip:    "[| sigma \<in> loc -> nat |] ==> <\<SKIP>,sigma> -c-> sigma"
paulson@12606
    92
wenzelm@12610
    93
    assign:  "[| m \<in> nat; x \<in> loc; <a,sigma> -a-> m |]
wenzelm@12610
    94
              ==> <x \<ASSN> a,sigma> -c-> sigma(x:=m)"
lcp@511
    95
wenzelm@12610
    96
    semi:    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |]
wenzelm@12610
    97
              ==> <c0\<SEQ> c1, sigma> -c-> sigma1"
paulson@12606
    98
wenzelm@12610
    99
    if1:     "[| b \<in> bexp; c1 \<in> com; sigma \<in> loc->nat;
wenzelm@12610
   100
                 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |]
wenzelm@12610
   101
              ==> <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1"
lcp@511
   102
wenzelm@12610
   103
    if0:     "[| b \<in> bexp; c0 \<in> com; sigma \<in> loc->nat;
wenzelm@12610
   104
                 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |]
wenzelm@12610
   105
               ==> <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1"
paulson@12606
   106
wenzelm@12610
   107
    while0:   "[| c \<in> com; <b, sigma> -b-> 0 |]
wenzelm@12610
   108
               ==> <\<WHILE> b \<DO> c,sigma> -c-> sigma"
lcp@511
   109
wenzelm@12610
   110
    while1:   "[| c \<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2;
wenzelm@12610
   111
                  <\<WHILE> b \<DO> c, sigma2> -c-> sigma1 |]
wenzelm@12610
   112
               ==> <\<WHILE> b \<DO> c, sigma> -c-> sigma1"
paulson@12606
   113
paulson@12606
   114
  type_intros  com.intros update_type
paulson@12606
   115
  type_elims   evala.dom_subset [THEN subsetD, elim_format]
paulson@12606
   116
               evalb.dom_subset [THEN subsetD, elim_format]
paulson@12606
   117
paulson@12606
   118
wenzelm@12610
   119
subsection {* Misc lemmas *}
lcp@511
   120
wenzelm@12610
   121
lemmas evala_1 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
wenzelm@12610
   122
  and evala_2 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
wenzelm@12610
   123
  and evala_3 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD2]
lcp@511
   124
wenzelm@12610
   125
lemmas evalb_1 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
wenzelm@12610
   126
  and evalb_2 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
wenzelm@12610
   127
  and evalb_3 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD2]
lcp@511
   128
wenzelm@12610
   129
lemmas evalc_1 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
wenzelm@12610
   130
  and evalc_2 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
wenzelm@12610
   131
  and evalc_3 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD2]
lcp@511
   132
wenzelm@12610
   133
inductive_cases
wenzelm@12610
   134
    evala_N_E [elim!]: "<N(n),sigma> -a-> i"
wenzelm@12610
   135
  and evala_X_E [elim!]: "<X(x),sigma> -a-> i"
wenzelm@12610
   136
  and evala_Op1_E [elim!]: "<Op1(f,e),sigma> -a-> i"
wenzelm@12610
   137
  and evala_Op2_E [elim!]: "<Op2(f,a1,a2),sigma>  -a-> i"
lcp@511
   138
lcp@511
   139
end