author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 14981  e73f8140af78 
child 36862  952b2b102a0a 
permissions  rwrr 
5737  1 
(* Title: HOL/Induct/ABexp.thy 
2 
ID: $Id$ 

3 
Author: Stefan Berghofer, TU Muenchen 

4 
*) 

5 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

6 
header {* Arithmetic and boolean expressions *} 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

7 

16417  8 
theory ABexp imports Main begin 
5737  9 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

10 
datatype 'a aexp = 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

11 
IF "'a bexp" "'a aexp" "'a aexp" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

12 
 Sum "'a aexp" "'a aexp" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

13 
 Diff "'a aexp" "'a aexp" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

14 
 Var 'a 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

15 
 Num nat 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

16 
and 'a bexp = 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

17 
Less "'a aexp" "'a aexp" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

18 
 And "'a bexp" "'a bexp" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

19 
 Neg "'a bexp" 
5737  20 

21 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

22 
text {* \medskip Evaluation of arithmetic and boolean expressions *} 
5737  23 

24 
consts 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

25 
evala :: "('a => nat) => 'a aexp => nat" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

26 
evalb :: "('a => nat) => 'a bexp => bool" 
5737  27 

28 
primrec 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

29 
"evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)" 
5802  30 
"evala env (Sum a1 a2) = evala env a1 + evala env a2" 
31 
"evala env (Diff a1 a2) = evala env a1  evala env a2" 

32 
"evala env (Var v) = env v" 

33 
"evala env (Num n) = n" 

5737  34 

5802  35 
"evalb env (Less a1 a2) = (evala env a1 < evala env a2)" 
11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

36 
"evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

37 
"evalb env (Neg b) = (\<not> evalb env b)" 
5737  38 

39 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

40 
text {* \medskip Substitution on arithmetic and boolean expressions *} 
5737  41 

42 
consts 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

43 
substa :: "('a => 'b aexp) => 'a aexp => 'b aexp" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

44 
substb :: "('a => 'b aexp) => 'a bexp => 'b bexp" 
5737  45 

46 
primrec 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

47 
"substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)" 
5802  48 
"substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)" 
49 
"substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)" 

50 
"substa f (Var v) = f v" 

51 
"substa f (Num n) = Num n" 

5737  52 

5802  53 
"substb f (Less a1 a2) = Less (substa f a1) (substa f a2)" 
54 
"substb f (And b1 b2) = And (substb f b1) (substb f b2)" 

55 
"substb f (Neg b) = Neg (substb f b)" 

5737  56 

12171  57 
lemma subst1_aexp: 
58 
"evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a" 

59 
and subst1_bexp: 

60 
"evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b" 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

61 
 {* one variable *} 
12171  62 
by (induct a and b) simp_all 
11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

63 

12171  64 
lemma subst_all_aexp: 
65 
"evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a" 

66 
and subst_all_bexp: 

67 
"evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b" 

68 
by (induct a and b) auto 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

69 

5737  70 
end 