equal
deleted
inserted
replaced
2 |
2 |
3 theory Fold imports Sem_Equiv begin |
3 theory Fold imports Sem_Equiv begin |
4 |
4 |
5 subsection "Simple folding of arithmetic expressions" |
5 subsection "Simple folding of arithmetic expressions" |
6 |
6 |
7 types |
7 type_synonym |
8 tab = "name \<Rightarrow> val option" |
8 tab = "name \<Rightarrow> val option" |
9 |
9 |
10 (* maybe better as the composition of substitution and the existing simp_const(0) *) |
10 (* maybe better as the composition of substitution and the existing simp_const(0) *) |
11 fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where |
11 fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where |
12 "simp_const (N n) _ = N n" | |
12 "simp_const (N n) _ = N n" | |