|
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 |