src/HOL/Induct/Com.thy
author paulson
Wed May 07 12:50:26 1997 +0200 (1997-05-07)
changeset 3120 c58423c20740
child 3146 922a60451382
permissions -rw-r--r--
New directory to contain examples of (co)inductive definitions
     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 = Arith +
    10 
    11 types loc
    12       state = "loc => nat"
    13       n2n2n = "nat => nat => nat"
    14 
    15 arities loc :: term
    16 
    17 (*To avoid a mutually recursive datatype declaration, expressions and commands
    18   are combined to form a single datatype.*)
    19 datatype
    20   exp = N nat
    21       | X loc
    22       | Op n2n2n exp exp
    23       | valOf exp exp          ("VALOF _ RESULTIS _"  60)
    24       | SKIP
    25       | ":="  loc exp          (infixl  60)
    26       | Semi  exp exp          ("_;;_"  [60, 60] 10)
    27       | Cond  exp exp exp      ("IF _ THEN _ ELSE _"  60)
    28       | While exp exp          ("WHILE _ DO _"  60)
    29 
    30 (** Execution of commands **)
    31 consts  exec    :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
    32        "@exec"  :: "((exp*state) * (nat*state)) set => 
    33                     [exp*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    34 
    35 translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
    36 
    37 constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
    38   "s[m/x] ==  (%y. if y=x then m else s y)"
    39 
    40 
    41 (*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
    42 inductive "exec eval"
    43   intrs
    44     Skip    "(SKIP,s) -[eval]-> s"
    45 
    46     Assign  "((e,s), (v,s')) : eval ==> (x := e, s) -[eval]-> s'[v/x]"
    47 
    48     Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
    49             ==> (c0 ;; c1, s) -[eval]-> s1"
    50 
    51     IfTrue "[| ((e,s), (0,s')) : eval;  (c0,s') -[eval]-> s1 |] 
    52             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    53 
    54     IfFalse "[| ((e,s), (1,s')) : eval;  (c1,s') -[eval]-> s1 |] 
    55              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    56 
    57     WhileFalse "((e,s), (1,s1)) : eval ==> (WHILE e DO c, s) -[eval]-> s1"
    58 
    59     WhileTrue  "[| ((e,s), (0,s1)) : eval;
    60                 (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
    61                 ==> (WHILE e DO c, s) -[eval]-> s3"
    62 
    63 constdefs
    64     Unique   :: "['a, 'b, ('a*'b) set] => bool"
    65     "Unique x y r == ALL y'. (x,y'): r --> y = y'"
    66 
    67     Function :: "('a*'b) set => bool"
    68     "Function r == ALL x y. (x,y): r --> Unique x y r"
    69 end