equal
deleted
inserted
replaced
1 (* Title: HOL/Induct/Exp |
|
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: Expressions |
|
7 *) |
|
8 |
|
9 Exp = Com + |
|
10 |
|
11 (** Evaluation of arithmetic expressions **) |
|
12 consts eval :: "((exp*state) * (nat*state)) set" |
|
13 "-|->" :: "[exp*state,nat*state] => bool" (infixl 50) |
|
14 translations |
|
15 "esig -|-> (n,s)" <= "(esig,n,s) : eval" |
|
16 "esig -|-> ns" == "(esig,ns ) : eval" |
|
17 |
|
18 inductive eval |
|
19 intrs |
|
20 N "(N(n),s) -|-> (n,s)" |
|
21 |
|
22 X "(X(x),s) -|-> (s(x),s)" |
|
23 |
|
24 Op "[| (e0,s) -|-> (n0,s0); (e1,s0) -|-> (n1,s1) |] |
|
25 ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)" |
|
26 |
|
27 valOf "[| (c,s) -[eval]-> s0; (e,s0) -|-> (n,s1) |] |
|
28 ==> (VALOF c RESULTIS e, s) -|-> (n, s1)" |
|
29 |
|
30 monos exec_mono |
|
31 |
|
32 end |
|
33 |
|