src/HOL/Induct/Com.thy
changeset 3120 c58423c20740
child 3146 922a60451382
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Induct/Com.thy	Wed May 07 12:50:26 1997 +0200
     1.3 @@ -0,0 +1,69 @@
     1.4 +(*  Title:      HOL/Induct/Com
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1997  University of Cambridge
     1.8 +
     1.9 +Example of Mutual Induction via Iteratived Inductive Definitions: Commands
    1.10 +*)
    1.11 +
    1.12 +Com = Arith +
    1.13 +
    1.14 +types loc
    1.15 +      state = "loc => nat"
    1.16 +      n2n2n = "nat => nat => nat"
    1.17 +
    1.18 +arities loc :: term
    1.19 +
    1.20 +(*To avoid a mutually recursive datatype declaration, expressions and commands
    1.21 +  are combined to form a single datatype.*)
    1.22 +datatype
    1.23 +  exp = N nat
    1.24 +      | X loc
    1.25 +      | Op n2n2n exp exp
    1.26 +      | valOf exp exp          ("VALOF _ RESULTIS _"  60)
    1.27 +      | SKIP
    1.28 +      | ":="  loc exp          (infixl  60)
    1.29 +      | Semi  exp exp          ("_;;_"  [60, 60] 10)
    1.30 +      | Cond  exp exp exp      ("IF _ THEN _ ELSE _"  60)
    1.31 +      | While exp exp          ("WHILE _ DO _"  60)
    1.32 +
    1.33 +(** Execution of commands **)
    1.34 +consts  exec    :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
    1.35 +       "@exec"  :: "((exp*state) * (nat*state)) set => 
    1.36 +                    [exp*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    1.37 +
    1.38 +translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
    1.39 +
    1.40 +constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
    1.41 +  "s[m/x] ==  (%y. if y=x then m else s y)"
    1.42 +
    1.43 +
    1.44 +(*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
    1.45 +inductive "exec eval"
    1.46 +  intrs
    1.47 +    Skip    "(SKIP,s) -[eval]-> s"
    1.48 +
    1.49 +    Assign  "((e,s), (v,s')) : eval ==> (x := e, s) -[eval]-> s'[v/x]"
    1.50 +
    1.51 +    Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
    1.52 +            ==> (c0 ;; c1, s) -[eval]-> s1"
    1.53 +
    1.54 +    IfTrue "[| ((e,s), (0,s')) : eval;  (c0,s') -[eval]-> s1 |] 
    1.55 +            ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    1.56 +
    1.57 +    IfFalse "[| ((e,s), (1,s')) : eval;  (c1,s') -[eval]-> s1 |] 
    1.58 +             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    1.59 +
    1.60 +    WhileFalse "((e,s), (1,s1)) : eval ==> (WHILE e DO c, s) -[eval]-> s1"
    1.61 +
    1.62 +    WhileTrue  "[| ((e,s), (0,s1)) : eval;
    1.63 +                (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
    1.64 +                ==> (WHILE e DO c, s) -[eval]-> s3"
    1.65 +
    1.66 +constdefs
    1.67 +    Unique   :: "['a, 'b, ('a*'b) set] => bool"
    1.68 +    "Unique x y r == ALL y'. (x,y'): r --> y = y'"
    1.69 +
    1.70 +    Function :: "('a*'b) set => bool"
    1.71 +    "Function r == ALL x y. (x,y): r --> Unique x y r"
    1.72 +end