# HG changeset patch
# User desharna
# Date 1685223282 -7200
# Node ID a8e5cefeb3ab91880d92c5ea62c825cc4d41e51b
# Parent  6f43068a71d158dec1aa5e6f9e7edb6f47be4338# Parent  cc17e2f0f1fcdb8fff39d86224629901527779c2
merged

diff -r cc17e2f0f1fc -r a8e5cefeb3ab NEWS
--- a/NEWS	Sat May 27 13:30:42 2023 +0200
+++ b/NEWS	Sat May 27 23:34:42 2023 +0200
@@ -223,6 +223,8 @@
     Minor INCOMPATIBILITY.
   - Redefined notin_fset as an abbreviation based on Set.not_member and
     renamed to not_fmember. Minor INCOMPATIBILITY.
+  - Redefined fBall and fBex as abbreviations based on Set.Ball and Set.Bex.
+    Minor INCOMPATIBILITY.
   - Removed lemmas. Minor INCOMPATIBILITIES.
       fmember_iff_member_fset
       notin_fset
diff -r cc17e2f0f1fc -r a8e5cefeb3ab src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Sat May 27 13:30:42 2023 +0200
+++ b/src/HOL/Library/FSet.thy	Sat May 27 23:34:42 2023 +0200
@@ -177,6 +177,21 @@
 abbreviation not_fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
   "x |\<notin>| X \<equiv> x \<notin> fset X"
 
+context
+begin
+
+qualified abbreviation Ball :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "Ball X \<equiv> Set.Ball (fset X)"
+
+alias fBall = FSet.Ball
+
+qualified abbreviation Bex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "Bex X \<equiv> Set.Bex (fset X)"
+
+alias fBex = FSet.Bex
+
+end
+
 context includes lifting_syntax
 begin
 
@@ -185,6 +200,16 @@
   shows "(A ===> pcr_fset A ===> (=)) (\<in>) (|\<in>|)"
   by transfer_prover
 
+lemma fBall_transfer0[transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(pcr_fset A ===> (A ===> (=)) ===> (=)) (Ball) (fBall)"
+  by transfer_prover
+
+lemma fBex_transfer0[transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(pcr_fset A ===> (A ===> (=)) ===> (=)) (Bex) (fBex)"
+  by transfer_prover
+
 lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
   parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
 
@@ -203,9 +228,6 @@
 
 lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp
 
-lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer .
-lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
-
 lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold .
 
 lift_definition fset_of_list :: "'a list \<Rightarrow> 'a fset" is set by (rule finite_set)
@@ -1948,4 +1970,22 @@
 
 end
 
+
+subsection \<open>Code Generation Setup\<close>
+
+text \<open>The following @{attribute code_unfold} lemmas are so the pre-processor of the code generator
+will perform conversions like, e.g.,
+@{lemma "x |\<in>| fimage f (fset_of_list xs) \<longleftrightarrow> x \<in> f ` set xs"
+  by (simp only: fimage.rep_eq fset_of_list.rep_eq)}.\<close>
+
+declare
+  ffilter.rep_eq[code_unfold]
+  fimage.rep_eq[code_unfold]
+  finsert.rep_eq[code_unfold]
+  fset_of_list.rep_eq[code_unfold]
+  inf_fset.rep_eq[code_unfold]
+  minus_fset.rep_eq[code_unfold]
+  sup_fset.rep_eq[code_unfold]
+  uminus_fset.rep_eq[code_unfold]
+
 end
diff -r cc17e2f0f1fc -r a8e5cefeb3ab src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Sat May 27 13:30:42 2023 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Sat May 27 23:34:42 2023 +0200
@@ -1438,7 +1438,7 @@
 \<comment> \<open>Code generation\<close>
 
 export_code
-  fBall fmrel fmran fmran' fmdom fmdom' fmpred pred_fmap fmsubset fmupd fmrel_on_fset
+  Ball fset fmrel fmran fmran' fmdom fmdom' fmpred pred_fmap fmsubset fmupd fmrel_on_fset
   fmdrop fmdrop_set fmdrop_fset fmrestrict_set fmrestrict_fset fmimage fmlookup fmempty
   fmfilter fmadd fmmap fmmap_keys fmcomp
   checking SML Scala Haskell? OCaml?