merged

--- a/src/HOL/Library/AList.thy	Tue Apr 14 08:42:16 2015 +0200
+++ b/src/HOL/Library/AList.thy	Tue Apr 14 15:54:17 2015 +0200
@@ -215,6 +215,87 @@
   by (simp add: delete_eq)
 
 
+subsection {* @{text update_with_aux} and @{text delete_aux}*}
+
+qualified primrec update_with_aux :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+where
+  "update_with_aux v k f [] = [(k, f v)]"
+| "update_with_aux v k f (p # ps) = (if (fst p = k) then (k, f (snd p)) # ps else p # update_with_aux v k f ps)"
+
+text {*
+  The above @{term "delete"} traverses all the list even if it has found the key.
+  This one does not have to keep going because is assumes the invariant that keys are distinct.
+*}
+qualified fun delete_aux :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+where
+  "delete_aux k [] = []"
+| "delete_aux k ((k', v) # xs) = (if k = k' then xs else (k', v) # delete_aux k xs)"
+
+lemma map_of_update_with_aux':
+  "map_of (update_with_aux v k f ps) k' = ((map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))) k'"
+by(induct ps) auto
+
+lemma map_of_update_with_aux:
+  "map_of (update_with_aux v k f ps) = (map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))"
+by(simp add: fun_eq_iff map_of_update_with_aux')
+
+lemma dom_update_with_aux: "fst ` set (update_with_aux v k f ps) = {k} \<union> fst ` set ps"
+  by (induct ps) auto
+
+lemma distinct_update_with_aux [simp]:
+  "distinct (map fst (update_with_aux v k f ps)) = distinct (map fst ps)"
+by(induct ps)(auto simp add: dom_update_with_aux)
+
+lemma set_update_with_aux:
+  "distinct (map fst xs) 
+  \<Longrightarrow> set (update_with_aux v k f xs) = (set xs - {k} \<times> UNIV \<union> {(k, f (case map_of xs k of None \<Rightarrow> v | Some v \<Rightarrow> v))})"
+by(induct xs)(auto intro: rev_image_eqI)
+
+lemma set_delete_aux: "distinct (map fst xs) \<Longrightarrow> set (delete_aux k xs) = set xs - {k} \<times> UNIV"
+apply(induct xs)
+apply simp_all
+apply clarsimp
+apply(fastforce intro: rev_image_eqI)
+done
+
+lemma dom_delete_aux: "distinct (map fst ps) \<Longrightarrow> fst ` set (delete_aux k ps) = fst ` set ps - {k}"
+by(auto simp add: set_delete_aux)
+
+lemma distinct_delete_aux [simp]:
+  "distinct (map fst ps) \<Longrightarrow> distinct (map fst (delete_aux k ps))"
+proof(induct ps)
+  case Nil thus ?case by simp
+next
+  case (Cons a ps)
+  obtain k' v where a: "a = (k', v)" by(cases a)
+  show ?case
+  proof(cases "k' = k")
+    case True with Cons a show ?thesis by simp
+  next
+    case False
+    with Cons a have "k' \<notin> fst ` set ps" "distinct (map fst ps)" by simp_all
+    with False a have "k' \<notin> fst ` set (delete_aux k ps)"
+      by(auto dest!: dom_delete_aux[where k=k])
+    with Cons a show ?thesis by simp
+  qed
+qed
+
+lemma map_of_delete_aux':
+  "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) = (map_of xs)(k := None)"
+  apply (induct xs)
+  apply (fastforce simp add: map_of_eq_None_iff fun_upd_twist)
+  apply (auto intro!: ext)
+  apply (simp add: map_of_eq_None_iff)
+  done
+
+lemma map_of_delete_aux:
+  "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) k' = ((map_of xs)(k := None)) k'"
+by(simp add: map_of_delete_aux')
+
+lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
+by(cases ts)(auto split: split_if_asm)
+
+
 subsection {* @{text restrict} *}
 
 qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"

--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Apr 14 08:42:16 2015 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Apr 14 15:54:17 2015 +0200
@@ -24,6 +24,11 @@
 
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}] *}
 
+section {* Filters *}
+
+(*TODO: shouldn't this be done by typedef? *)
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name Abs_filter}, @{const_name Rep_filter}] *}
+
 section {* Bounded quantifiers *}
 
 declare Ball_def[code_pred_inline]

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Tue Apr 14 08:42:16 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Tue Apr 14 15:54:17 2015 +0200
@@ -68,12 +68,18 @@
 
     fun prove goal =
       Goal.prove_sorry_global thy [] [] goal (fn {context = ctxt, ...} =>
+        HEADGOAL Goal.conjunction_tac THEN
         ALLGOALS (simp_tac
           (put_simpset HOL_basic_ss ctxt
-            addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))))
-      |> Simpdata.mk_eq;
+            addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))));
+
+    fun proves goals = goals
+      |> Logic.mk_conjunction_balanced
+      |> prove
+      |> Conjunction.elim_balanced (length goals)
+      |> map Simpdata.mk_eq;
   in
-    (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
+    (proves (triv_inject_goals @ inject_goals @ distinct_goals), Simpdata.mk_eq (prove refl_goal))
   end;
 
 fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =