author  blanchet 
Tue, 09 Sep 2014 20:51:36 +0200  
changeset 58249  180f1b3508ed 
parent 46914  c2ca2c3d23a6 
child 58310  91ea607a34d8 
permissions  rwrr 
5737  1 
(* Title: HOL/Induct/ABexp.thy 
2 
Author: Stefan Berghofer, TU Muenchen 

3 
*) 

4 

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

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

6 

46914  7 
theory ABexp 
8 
imports Main 

9 
begin 

5737  10 

58249
180f1b3508ed
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
blanchet
parents:
46914
diff
changeset

11 
datatype_new 'a aexp = 
11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
5802
diff
changeset

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

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

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

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

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

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

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

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

20 
 Neg "'a bexp" 
5737  21 

22 

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

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

39246  25 
primrec evala :: "('a => nat) => 'a aexp => nat" 
46914  26 
and evalb :: "('a => nat) => 'a bexp => bool" 
27 
where 

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

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

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

32 
 "evala env (Num n) = n" 

5737  33 

39246  34 
 "evalb env (Less a1 a2) = (evala env a1 < evala env a2)" 
35 
 "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)" 

36 
 "evalb env (Neg b) = (\<not> evalb env b)" 

5737  37 

38 

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

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

39246  41 
primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp" 
46914  42 
and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp" 
43 
where 

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

44 
"substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)" 
39246  45 
 "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)" 
46 
 "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)" 

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

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

5737  49 

39246  50 
 "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)" 
51 
 "substb f (And b1 b2) = And (substb f b1) (substb f b2)" 

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

5737  53 

12171  54 
lemma subst1_aexp: 
55 
"evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a" 

56 
and subst1_bexp: 

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

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

60 

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

63 
and subst_all_bexp: 

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

65 
by (induct a and b) auto 

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

66 

5737  67 
end 