src/HOL/Induct/Com.thy
 author oheimb Fri Nov 21 11:57:58 1997 +0100 (1997-11-21) changeset 4264 5e21f41ccd21 parent 3146 922a60451382 child 5102 8c782c25a11e permissions -rw-r--r--
minor improvements of formulation and proofs
```     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] 60)
```
```    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 syntax  eval'   :: "[exp*state,nat*state] =>
```
```    38 		    ((exp*state) * (nat*state)) set => bool"
```
```    39 						   ("_/ -|[_]-> _" [50,0,50] 50)
```
```    40 translations
```
```    41     "esig -|[eval]-> ns" => "(esig,ns) : eval"
```
```    42
```
```    43 constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
```
```    44   "s[m/x] ==  (%y. if y=x then m else s y)"
```
```    45
```
```    46
```
```    47 (*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
```
```    48 inductive "exec eval"
```
```    49   intrs
```
```    50     Skip    "(SKIP,s) -[eval]-> s"
```
```    51
```
```    52     Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'[v/x]"
```
```    53
```
```    54     Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
```
```    55             ==> (c0 ;; c1, s) -[eval]-> s1"
```
```    56
```
```    57     IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]
```
```    58             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
```
```    59
```
```    60     IfFalse "[| (e,s) -|[eval]->  (1,s');  (c1,s') -[eval]-> s1 |]
```
```    61              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
```
```    62
```
```    63     WhileFalse "(e,s) -|[eval]-> (1,s1) ==> (WHILE e DO c, s) -[eval]-> s1"
```
```    64
```
```    65     WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
```
```    66                 (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |]
```
```    67                 ==> (WHILE e DO c, s) -[eval]-> s3"
```
```    68
```
```    69 constdefs
```
```    70     Unique   :: "['a, 'b, ('a*'b) set] => bool"
```
```    71     "Unique x y r == ALL y'. (x,y'): r --> y = y'"
```
```    72
```
```    73     Function :: "('a*'b) set => bool"
```
```    74     "Function r == ALL x y. (x,y): r --> Unique x y r"
```
```    75 end
```