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