author  nipkow 
Sat, 27 Apr 1996 18:49:21 +0200  
changeset 1697  687f0710c22d 
child 1729  e4f8682eea2e 
permissions  rwrr 
1697
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

1 
(* Title: HOL/IMP/Expr.thy 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

3 
Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

4 
Copyright 1994 TUM 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

5 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

6 
Arithmetic expressions and Boolean expressions. 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

7 
Not used in the rest of the language, but included for completeness. 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

8 
*) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

9 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

10 
Expr = Arith + 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

11 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

12 
(** Arithmetic expressions **) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

13 
types loc 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

14 
state = "loc => nat" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

15 
n2n = "nat => nat" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

16 
n2n2n = "nat => nat => nat" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

17 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

18 
arities loc :: term 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

19 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

20 
datatype 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

21 
aexp = N nat 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

22 
 X loc 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

23 
 Op1 n2n aexp 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

24 
 Op2 n2n2n aexp aexp 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

25 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

26 
(** Evaluation of arithmetic expressions **) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

27 
consts evala :: "(aexp*state*nat)set" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

28 
"@evala" :: [aexp,state,nat] => bool ("<_,_>/ a> _" [0,0,50] 50) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

29 
translations 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

30 
"<ae,sig> a> n" == "(ae,sig,n) : evala" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

31 
inductive "evala" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

32 
intrs 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

33 
N "<N(n),s> a> n" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

34 
X "<X(x),s> a> s(x)" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

35 
Op1 "<e,s> a> n ==> <Op1 f e,s> a> f(n)" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

36 
Op2 "[ <e0,s> a> n0; <e1,s> a> n1 ] 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

37 
==> <Op2 f e0 e1,s> a> f n0 n1" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

38 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

39 
types n2n2b = "[nat,nat] => bool" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

40 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

41 
(** Boolean expressions **) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

42 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

43 
datatype 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

44 
bexp = true 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

45 
 false 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

46 
 ROp n2n2b aexp aexp 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

47 
 noti bexp 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

48 
 andi bexp bexp (infixl 60) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

49 
 ori bexp bexp (infixl 60) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

50 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

51 
(** Evaluation of boolean expressions **) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

52 
consts evalb :: "(bexp*state*bool)set" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

53 
"@evalb" :: [bexp,state,bool] => bool ("<_,_>/ b> _" [0,0,50] 50) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

54 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

55 
translations 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

56 
"<be,sig> b> b" == "(be,sig,b) : evalb" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

57 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

58 
inductive "evalb" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

59 
intrs (*avoid clash with ML constructors true, false*) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

60 
tru "<true,s> b> True" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

61 
fls "<false,s> b> False" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

62 
ROp "[ <a0,s> a> n0; <a1,s> a> n1 ] 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

63 
==> <ROp f a0 a1,s> b> f n0 n1" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

64 
noti "<b,s> b> w ==> <noti(b),s> b> (~w)" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

65 
andi "[ <b0,s> b> w0; <b1,s> b> w1 ] 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

66 
==> <b0 andi b1,s> b> (w0 & w1)" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

67 
ori "[ <b0,s> b> w0; <b1,s> b> w1 ] 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

68 
==> <b0 ori b1,s> b> (w0  w1)" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

69 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

70 
(** Denotational semantics of arithemtic and boolean expressions **) 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

71 
consts 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

72 
A :: aexp => state => nat 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

73 
B :: bexp => state => bool 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

74 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

75 
primrec A aexp 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

76 
A_nat "A(N(n)) = (%s. n)" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

77 
A_loc "A(X(x)) = (%s. s(x))" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

78 
A_op1 "A(Op1 f a) = (%s. f(A a s))" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

79 
A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

80 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

81 
primrec B bexp 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

82 
B_true "B(true) = (%s. True)" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

83 
B_false "B(false) = (%s. False)" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

84 
B_op "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

85 
B_not "B(noti(b)) = (%s. ~(B b s))" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

86 
B_and "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

87 
B_or "B(b0 ori b1) = (%s. (B b0 s)  (B b1 s))" 
687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

88 

687f0710c22d
Arithemtic and boolean expressions are now in a separate theory.
nipkow
parents:
diff
changeset

89 
end 