# HG changeset patch
# User paulson
# Date 1532172653 -7200
# Node ID c51ede74c0b2b5bcd3f02d709529771455c7cbf9
# Parent  c9570658e8f13cb31634a811f059fa4e0efce8d4# Parent  7ddf297cfcdef5e263e670f550a6076900a13421
merged

diff -r 7ddf297cfcde -r c51ede74c0b2 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Sat Jul 21 13:30:43 2018 +0200
+++ b/src/HOL/Filter.thy	Sat Jul 21 13:30:53 2018 +0200
@@ -1104,6 +1104,34 @@
 lemma prod_filter_INF2: "J \<noteq> {} \<Longrightarrow> A \<times>\<^sub>F (\<Sqinter>i\<in>J. B i) = (\<Sqinter>i\<in>J. A \<times>\<^sub>F B i)"
   using prod_filter_INF[of "{A}" J "\<lambda>x. x" B] by simp
 
+lemma prod_filtermap1: "prod_filter (filtermap f F) G = filtermap (apfst f) (prod_filter F G)"
+  apply(clarsimp simp add: filter_eq_iff eventually_filtermap eventually_prod_filter; safe)
+  subgoal by auto
+  subgoal for P Q R by(rule exI[where x="\<lambda>y. \<exists>x. y = f x \<and> Q x"])(auto intro: eventually_mono)
+  done
+
+lemma prod_filtermap2: "prod_filter F (filtermap g G) = filtermap (apsnd g) (prod_filter F G)"
+  apply(clarsimp simp add: filter_eq_iff eventually_filtermap eventually_prod_filter; safe)
+  subgoal by auto
+  subgoal for P Q R  by(auto intro: exI[where x="\<lambda>y. \<exists>x. y = g x \<and> R x"] eventually_mono)
+  done
+
+lemma prod_filter_assoc:
+  "prod_filter (prod_filter F G) H = filtermap (\<lambda>(x, y, z). ((x, y), z)) (prod_filter F (prod_filter G H))"
+  apply(clarsimp simp add: filter_eq_iff eventually_filtermap eventually_prod_filter; safe)
+  subgoal for P Q R S T by(auto 4 4 intro: exI[where x="\<lambda>(a, b). T a \<and> S b"])
+  subgoal for P Q R S T by(auto 4 3 intro: exI[where x="\<lambda>(a, b). Q a \<and> S b"])
+  done
+
+lemma prod_filter_principal_singleton: "prod_filter (principal {x}) F = filtermap (Pair x) F"
+  by(fastforce simp add: filter_eq_iff eventually_prod_filter eventually_principal eventually_filtermap elim: eventually_mono intro: exI[where x="\<lambda>a. a = x"])
+
+lemma prod_filter_principal_singleton2: "prod_filter F (principal {x}) = filtermap (\<lambda>a. (a, x)) F"
+  by(fastforce simp add: filter_eq_iff eventually_prod_filter eventually_principal eventually_filtermap elim: eventually_mono intro: exI[where x="\<lambda>a. a = x"])
+
+lemma prod_filter_commute: "prod_filter F G = filtermap prod.swap (prod_filter G F)"
+  by(auto simp add: filter_eq_iff eventually_prod_filter eventually_filtermap)
+
 subsection \<open>Limits\<close>
 
 definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
@@ -1699,6 +1727,50 @@
 
 end
 
+lemma prod_filter_parametric [transfer_rule]: includes lifting_syntax shows
+   "(rel_filter R ===> rel_filter S ===> rel_filter (rel_prod R S)) prod_filter prod_filter"
+proof(intro rel_funI; elim rel_filter.cases; hypsubst)
+  fix F G
+  assume F: "\<forall>\<^sub>F (x, y) in F. R x y" and G: "\<forall>\<^sub>F (x, y) in G. S x y"
+  show "rel_filter (rel_prod R S)
+    (map_filter_on {(x, y). R x y} fst F \<times>\<^sub>F map_filter_on {(x, y). S x y} fst G)
+    (map_filter_on {(x, y). R x y} snd F \<times>\<^sub>F map_filter_on {(x, y). S x y} snd G)"
+    (is "rel_filter ?RS ?F ?G")
+  proof
+    let ?Z = "filtermap (\<lambda>((a, b), (a', b')). ((a, a'), (b, b'))) (prod_filter F G)"
+    show *: "\<forall>\<^sub>F (x, y) in ?Z. rel_prod R S x y" using F G
+      by(auto simp add: eventually_filtermap split_beta eventually_prod_filter)
+    show "map_filter_on {(x, y). ?RS x y} fst ?Z = ?F"
+      using F G
+      apply(clarsimp simp add: filter_eq_iff eventually_map_filter_on *)
+      apply(simp add: eventually_filtermap split_beta eventually_prod_filter)
+      apply(subst eventually_map_filter_on; simp)+
+      apply(rule iffI; clarsimp)
+      subgoal for P P' P''
+        apply(rule exI[where x="\<lambda>a. \<exists>b. P' (a, b) \<and> R a b"]; rule conjI)
+        subgoal by(fastforce elim: eventually_rev_mp eventually_mono)
+        subgoal
+          by(rule exI[where x="\<lambda>a. \<exists>b. P'' (a, b) \<and> S a b"])(fastforce elim: eventually_rev_mp eventually_mono)
+        done
+      subgoal by fastforce
+      done
+    show "map_filter_on {(x, y). ?RS x y} snd ?Z = ?G"
+      using F G
+      apply(clarsimp simp add: filter_eq_iff eventually_map_filter_on *)
+      apply(simp add: eventually_filtermap split_beta eventually_prod_filter)
+      apply(subst eventually_map_filter_on; simp)+
+      apply(rule iffI; clarsimp)
+      subgoal for P P' P''
+        apply(rule exI[where x="\<lambda>b. \<exists>a. P' (a, b) \<and> R a b"]; rule conjI)
+        subgoal by(fastforce elim: eventually_rev_mp eventually_mono)
+        subgoal
+          by(rule exI[where x="\<lambda>b. \<exists>a. P'' (a, b) \<and> S a b"])(fastforce elim: eventually_rev_mp eventually_mono)
+        done
+      subgoal by fastforce
+      done
+  qed
+qed
+
 text \<open>Code generation for filters\<close>
 
 definition abstract_filter :: "(unit \<Rightarrow> 'a filter) \<Rightarrow> 'a filter"
diff -r 7ddf297cfcde -r c51ede74c0b2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jul 21 13:30:43 2018 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jul 21 13:30:53 2018 +0200
@@ -424,8 +424,13 @@
                    (case isar_proof of
                      Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
                      let
-                       val used_facts' = filter (fn (s, (sc, _)) =>
-                         member (op =) gfs s andalso sc <> Chained) used_facts
+                       val used_facts' =
+                         map_filter (fn s =>
+                            if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained)
+                                used_facts then
+                              NONE
+                            else
+                              SOME (s, (Global, General))) gfs
                      in
                        ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
                      end)