equal
deleted
inserted
replaced
3 Copyright 1995 University of Cambridge |
3 Copyright 1995 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 theory Language imports Main begin |
6 theory Language imports Main begin |
7 |
7 |
8 consts |
|
9 Const :: i (* Abstract type of constants *) |
|
10 c_app :: "[i,i] => i" (* Abstract constructor for fun application*) |
|
11 |
|
12 |
8 |
13 text{*these really can't be definitions without losing the abstraction*} |
9 text{*these really can't be definitions without losing the abstraction*} |
14 axioms |
10 |
15 constNEE: "c \<in> Const ==> c \<noteq> 0" |
11 axiomatization |
|
12 Const :: i and (* Abstract type of constants *) |
|
13 c_app :: "[i,i] => i" (* Abstract constructor for fun application*) |
|
14 where |
|
15 constNEE: "c \<in> Const ==> c \<noteq> 0" and |
16 c_appI: "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const" |
16 c_appI: "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const" |
17 |
17 |
18 |
18 |
19 consts |
19 consts |
20 Exp :: i (* Datatype of expressions *) |
20 Exp :: i (* Datatype of expressions *) |