--- a/src/HOL/IMP/Fold.thy Mon Jul 29 22:17:32 2013 +0200
+++ b/src/HOL/IMP/Fold.thy Thu Aug 01 16:52:28 2013 +0200
@@ -7,7 +7,6 @@
type_synonym
tab = "vname \<Rightarrow> val option"
-(* maybe better as the composition of substitution and the existing simp_const(0) *)
fun afold :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
"afold (N n) _ = N n" |
"afold (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |
@@ -198,14 +197,11 @@
"approx empty = (\<lambda>_. True)"
by (auto simp: approx_def)
-lemma equiv_sym:
- "c \<sim> c' \<longleftrightarrow> c' \<sim> c"
- by (auto simp add: equiv_def)
theorem constant_folding_equiv:
"fold c empty \<sim> c"
using approx_eq [of empty c]
- by (simp add: equiv_up_to_True equiv_sym)
+ by (simp add: equiv_up_to_True sim_sym)
@@ -386,7 +382,7 @@
theorem constant_folding_equiv':
"fold' c empty \<sim> c"
using fold'_equiv [of empty c]
- by (simp add: equiv_up_to_True equiv_sym)
+ by (simp add: equiv_up_to_True sim_sym)
end