author kleing Thu, 01 Aug 2013 16:52:28 +0200 changeset 52825 71fef62c4213 parent 52783 084ac81e9871 child 52826 122416054a9c
removed duplicate lemma
 src/HOL/IMP/Fold.thy file | annotate | diff | comparison | revisions
```--- 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```