src/HOL/IMP/Com.thy
author clasohm
Mon, 20 Mar 1995 15:35:28 +0100
changeset 965 24eef3860714
parent 924 806721cfbf46
child 972 e61b058d58d2
permissions -rw-r--r--
changed syntax of "if"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     1
(*  Title: 	HOL/IMP/Com.thy
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     3
    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994 TUM
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     5
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     6
Arithmetic expressions, Boolean expressions, Commands
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     7
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     8
And their Operational semantics
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     9
*)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    10
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    11
Com = Arith +
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    12
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    13
(** Arithmetic expressions **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    14
types loc
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    15
      state = "loc => nat"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    16
      n2n = "nat => nat"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    17
      n2n2n = "nat => nat => nat"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    18
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    19
arities loc :: term
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    20
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    21
datatype
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    22
  aexp = N (nat)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    23
       | X (loc)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    24
       | Op1 (n2n, aexp)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    25
       | Op2 (n2n2n, aexp, aexp)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    26
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    27
(** Evaluation of arithmetic expressions **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    28
consts  evala    :: "(aexp*state*nat)set"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    29
       "@evala"  :: "[aexp,state,nat] => bool"	("<_,_>/ -a-> _"  [0,0,50] 50)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    30
translations
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    31
    "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    32
inductive "evala"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    33
  intrs 
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    34
    N   "<N(n),s> -a-> n"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    35
    X  	"<X(x),s> -a-> s(x)"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    36
    Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    37
    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] \
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    38
\           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    39
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    40
types n2n2b = "[nat,nat] => bool"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    41
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    42
(** Boolean expressions **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    43
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    44
datatype
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    45
  bexp = true
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    46
       | false
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    47
       | ROp  (n2n2b, aexp, aexp)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    48
       | noti (bexp)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    49
       | andi (bexp,bexp)	(infixl 60)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    50
       | ori  (bexp,bexp)	(infixl 60)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    51
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    52
(** Evaluation of boolean expressions **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    53
consts evalb	:: "(bexp*state*bool)set"	
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    54
       "@evalb" :: "[bexp,state,bool] => bool"	("<_,_>/ -b-> _"  [0,0,50] 50)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    55
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    56
translations
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    57
    "<be,sig> -b-> b" == "<be,sig,b> : evalb"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    58
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    59
inductive "evalb"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    60
 intrs (*avoid clash with ML constructors true, false*)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    61
    tru   "<true,s> -b-> True"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    62
    fls   "<false,s> -b-> False"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    63
    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] \
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    64
\	   ==> <ROp f a0 a1,s> -b-> f n0 n1"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    65
    noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    66
    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    67
\          ==> <b0 andi b1,s> -b-> (w0 & w1)"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    68
    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    69
\	    ==> <b0 ori b1,s> -b-> (w0 | w1)"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    70
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    71
(** Commands **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    72
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    73
datatype
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    74
  com = skip
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    75
      | ":="   (loc,aexp)	 (infixl  60)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    76
      | semic  (com,com)	 ("_; _"  [60, 60] 10)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    77
      | whileC (bexp,com)	 ("while _ do _"  60)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    78
      | ifC    (bexp, com, com)	 ("ifc _ then _ else _"  60)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    79
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    80
(** Execution of commands **)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    81
consts  evalc    :: "(com*state*state)set"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    82
        "@evalc" :: "[com,state,state] => bool"  ("<_,_>/ -c-> _" [0,0,50] 50)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    83
	"assign" :: "[state,nat,loc] => state"   ("_[_'/_]"       [95,0,0] 95)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    84
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    85
translations
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    86
       "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    87
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    88
rules 
965
24eef3860714 changed syntax of "if"
clasohm
parents: 924
diff changeset
    89
	assign_def	"s[m/x] == (%y. if y=x then m else s y)"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    90
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    91
inductive "evalc"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    92
  intrs
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    93
    skip    "<skip,s> -c-> s"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    94
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    95
    assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    96
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    97
    semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] \
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    98
\            ==> <c0 ; c1, s> -c-> s1"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    99
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   100
    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] \
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   101
\            ==> <ifc b then c0 else c1, s> -c-> s1"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   102
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   103
    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] \
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   104
\             ==> <ifc b then c0 else c1, s> -c-> s1"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   105
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   106
    whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   107
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   108
    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; \
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   109
\                  <while b do c, s2> -c-> s1 |] \
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   110
\               ==> <while b do c, s> -c-> s1 "
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   111
 
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   112
end