# HG changeset patch
# User wenzelm
# Date 1722808244 -7200
# Node ID 3cde955e4e47ea079d8f71b22f2cda90c77fb5c6
# Parent  3322b6ae6b191a7ceb72b25578b45d6b9ceffae3
tuned;

diff -r 3322b6ae6b19 -r 3cde955e4e47 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Aug 04 23:17:35 2024 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Aug 04 23:50:44 2024 +0200
@@ -62,7 +62,7 @@
     val T as Type (\<^type_name>\<open>fun\<close>, [T1, T2]) = fastype_of f
   in
     Const (\<^const_name>\<open>vimage\<close>, T --> HOLogic.mk_setT T2 --> HOLogic.mk_setT T1) $ f $ s
-  end; 
+  end;
 
 fun dest_Collect (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (x, T, t)) = ((x, T), t)
   | dest_Collect t = raise TERM ("dest_Collect", [t])
@@ -164,7 +164,7 @@
       SOME pat => (Pattern pat, Atom (Pattern pat, s))
     | NONE =>
         let
-          val (tuple, (vs', x')) = mk_term vs x 
+          val (tuple, (vs', x')) = mk_term vs x
           val rT = HOLogic.dest_setT (fastype_of s)
           val s = mk_vimage (snd (mk_case_prod rT vs' x')) s
         in (tuple, Atom (tuple, s)) end)
@@ -204,7 +204,7 @@
       else error "restricted merge: two patterns require relational join"
     | _ => error "restricted merge: multiple patterns overlap"
   end;
-  
+
 fun map_atoms f (Atom a) = Atom (f a)
   | map_atoms f (Un (fm1, fm2)) = Un (apply2 (map_atoms f) (fm1, fm2))
   | map_atoms f (Int (fm1, fm2)) = Int (apply2 (map_atoms f) (fm1, fm2))
@@ -236,13 +236,13 @@
 
 fun merge_inter vs (pats1, fm1) (pats2, fm2) =
   let
-    val pats = restricted_merge (map dest_Pattern pats1, map dest_Pattern pats2) 
+    val pats = restricted_merge (map dest_Pattern pats1, map dest_Pattern pats2)
     val (fm1', fm2') = apply2 (adjust_atoms vs pats) (fm1, fm2)
   in
     (map Pattern pats, Int (fm1', fm2'))
   end;
 
-fun merge_union vs (pats1, fm1) (pats2, fm2) = 
+fun merge_union vs (pats1, fm1) (pats2, fm2) =
   let
     val pats = merge (map dest_Pattern pats1, map dest_Pattern pats2)
     val (fm1', fm2') = apply2 (adjust_atoms vs pats) (fm1, fm2)
@@ -254,7 +254,7 @@
   | mk_formula vs \<^Const_>\<open>disj for t1 t2\<close> = merge_union vs (mk_formula vs t1) (mk_formula vs t2)
   | mk_formula vs t = apfst single (mk_atom vs t)
 
-fun strip_Int (Int (fm1, fm2)) = fm1 :: (strip_Int fm2) 
+fun strip_Int (Int (fm1, fm2)) = fm1 :: (strip_Int fm2)
   | strip_Int fm = [fm]
 
 (* term construction *)
@@ -296,7 +296,7 @@
     val t = mk_split_abs (rev ((x, T) :: vs)) pat (reorder_bounds pats f)
   in
     if the_default false (try is_reordering t) andalso is_collect_atom fm then
-      error "mk_pointfree_expr: trivial case" 
+      error "mk_pointfree_expr: trivial case"
     else (fm, mk_image t (mk_set fm))
   end;
 
@@ -305,14 +305,14 @@
 
 (* proof tactic *)
 
-val case_prod_beta = @{lemma "case_prod g x z = case_prod (\<lambda>x y. (g x y) z) x" by (simp add: case_prod_beta)}
+val case_prod_beta =
+  @{lemma "case_prod g x z = case_prod (\<lambda>x y. (g x y) z) x" by (simp add: case_prod_beta)}
 
-val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
-val vimageE' =
-  @{lemma "a \<notin> f -` B ==> (\<And> x. f a = x ==> x \<notin> B ==> P) ==> P" by simp}
+val vimageI2' = @{lemma "f a \<notin> A \<Longrightarrow> a \<notin> f -` A" by simp}
+val vimageE' = @{lemma "a \<notin> f -` B \<Longrightarrow> (\<And> x. f a = x ==> x \<notin> B \<Longrightarrow> P) \<Longrightarrow> P" by simp}
 
-val collectI' = @{lemma "\<not> P a ==> a \<notin> {x. P x}" by auto}
-val collectE' = @{lemma "a \<notin> {x. P x} ==> (\<not> P a ==> Q) ==> Q" by auto}
+val collectI' = @{lemma "\<not> P a \<Longrightarrow> a \<notin> {x. P x}" by auto}
+val collectE' = @{lemma "a \<notin> {x. P x} \<Longrightarrow> (\<not> P a \<Longrightarrow> Q) \<Longrightarrow> Q" by auto}
 
 fun elim_Collect_tac ctxt =
   dresolve_tac ctxt @{thms iffD1 [OF mem_Collect_eq]}
@@ -432,7 +432,7 @@
       end;
     fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (Thm.prop_of th))
     val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case}
-    fun tac ctxt = 
+    fun tac ctxt =
       resolve_tac ctxt @{thms set_eqI}
       THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms)
       THEN' resolve_tac ctxt @{thms iffI}