paulson@3120: (*  Title:      HOL/Induct/Com
paulson@3120:     ID:         $Id$
paulson@3120:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3120:     Copyright   1997  University of Cambridge
paulson@3120: 
paulson@3120: Example of Mutual Induction via Iteratived Inductive Definitions: Commands
paulson@3120: *)
paulson@3120: 
nipkow@10759: Com = Main +
paulson@3120: 
paulson@3120: types loc
paulson@3120:       state = "loc => nat"
paulson@3120:       n2n2n = "nat => nat => nat"
paulson@3120: 
paulson@3120: arities loc :: term
paulson@3120: 
paulson@3120: datatype
paulson@3120:   exp = N nat
paulson@3120:       | X loc
paulson@3120:       | Op n2n2n exp exp
nipkow@10759:       | valOf com exp          ("VALOF _ RESULTIS _"  60)
nipkow@10759: and
nipkow@10759:   com = SKIP
paulson@3120:       | ":="  loc exp          (infixl  60)
nipkow@10759:       | Semi  com com          ("_;;_"  [60, 60] 60)
nipkow@10759:       | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
nipkow@10759:       | While exp com          ("WHILE _ DO _"  60)
paulson@3120: 
paulson@3120: (** Execution of commands **)
nipkow@10759: consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
paulson@3120:        "@exec"  :: "((exp*state) * (nat*state)) set => 
nipkow@10759:                     [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
paulson@3120: 
paulson@3120: translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
paulson@3120: 
oheimb@4264: syntax  eval'   :: "[exp*state,nat*state] => 
oheimb@4264: 		    ((exp*state) * (nat*state)) set => bool"
oheimb@4264: 						   ("_/ -|[_]-> _" [50,0,50] 50)
oheimb@4264: translations
oheimb@4264:     "esig -|[eval]-> ns" => "(esig,ns) : eval"
oheimb@4264: 
paulson@3120: (*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
paulson@3120: inductive "exec eval"
paulson@3120:   intrs
paulson@3120:     Skip    "(SKIP,s) -[eval]-> s"
paulson@3120: 
nipkow@10759:     Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
paulson@3120: 
paulson@3120:     Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
paulson@3120:             ==> (c0 ;; c1, s) -[eval]-> s1"
paulson@3120: 
oheimb@4264:     IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
paulson@3120:             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
paulson@3120: 
nipkow@11464:     IfFalse "[| (e,s) -|[eval]->  (1',s');  (c1,s') -[eval]-> s1 |] 
paulson@3120:              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
paulson@3120: 
nipkow@11464:     WhileFalse "(e,s) -|[eval]-> (1',s1) ==> (WHILE e DO c, s) -[eval]-> s1"
paulson@3120: 
oheimb@4264:     WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
paulson@3120:                 (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
paulson@3120:                 ==> (WHILE e DO c, s) -[eval]-> s3"
paulson@3120: end