src/HOL/Induct/Com.thy
author nipkow
Mon Aug 06 13:43:24 2001 +0200 (2001-08-06)
changeset 11464 ddea204de5bc
parent 10759 994877ee68cb
child 11701 3d51fbf81c17
permissions -rw-r--r--
turned translation for 1::nat into def.
introduced 1' and replaced most occurrences of 1 by 1'.
     1 (*  Title:      HOL/Induct/Com
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     7 *)
     8 
     9 Com = Main +
    10 
    11 types loc
    12       state = "loc => nat"
    13       n2n2n = "nat => nat => nat"
    14 
    15 arities loc :: term
    16 
    17 datatype
    18   exp = N nat
    19       | X loc
    20       | Op n2n2n exp exp
    21       | valOf com exp          ("VALOF _ RESULTIS _"  60)
    22 and
    23   com = SKIP
    24       | ":="  loc exp          (infixl  60)
    25       | Semi  com com          ("_;;_"  [60, 60] 60)
    26       | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
    27       | While exp com          ("WHILE _ DO _"  60)
    28 
    29 (** Execution of commands **)
    30 consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
    31        "@exec"  :: "((exp*state) * (nat*state)) set => 
    32                     [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    33 
    34 translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
    35 
    36 syntax  eval'   :: "[exp*state,nat*state] => 
    37 		    ((exp*state) * (nat*state)) set => bool"
    38 						   ("_/ -|[_]-> _" [50,0,50] 50)
    39 translations
    40     "esig -|[eval]-> ns" => "(esig,ns) : eval"
    41 
    42 (*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
    43 inductive "exec eval"
    44   intrs
    45     Skip    "(SKIP,s) -[eval]-> s"
    46 
    47     Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
    48 
    49     Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
    50             ==> (c0 ;; c1, s) -[eval]-> s1"
    51 
    52     IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
    53             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    54 
    55     IfFalse "[| (e,s) -|[eval]->  (1',s');  (c1,s') -[eval]-> s1 |] 
    56              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    57 
    58     WhileFalse "(e,s) -|[eval]-> (1',s1) ==> (WHILE e DO c, s) -[eval]-> s1"
    59 
    60     WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
    61                 (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
    62                 ==> (WHILE e DO c, s) -[eval]-> s3"
    63 end