lib: add foldl lemma to LemmaBucket

2018-04-18 07:11:03 +10:00 · 2018-04-18 07:11:03 +10:00 · 4dcd4df2b6
parent 02e5096534
commit 4dcd4df2b6
1 changed files with 7 additions and 0 deletions
--- a/lib/LemmaBucket.thy
+++ b/lib/LemmaBucket.thy
@ -464,4 +464,11 @@ lemma strenghten_False_imp:
  "\<not>P \<Longrightarrow> P \<longrightarrow> Q"
  by blast

+lemma foldl_fun_or_alt:
+  "foldl (\<lambda>x y. x \<or> f y) b ls = foldl (op \<or>) b (map f ls)"
+  apply (induct ls)
+   apply clarsimp
+  apply clarsimp
+  by (simp add: foldl_map)
+
 end