# HG changeset patch # User desharna # Date 1685108699 -7200 # Node ID 7735645667f02287c97db3e8a1dfc7c893a1bbf5 # Parent a6989a7d192af9b018a13bc49ed6fee68359bdb7 redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set.Bex diff -r a6989a7d192a -r 7735645667f0 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Fri May 26 10:34:39 2023 +0200 +++ b/src/HOL/Library/FSet.thy Fri May 26 15:44:59 2023 +0200 @@ -177,6 +177,21 @@ abbreviation not_fmember :: "'a \ 'a fset \ bool" (infix "|\|" 50) where "x |\| X \ x \ fset X" +context +begin + +qualified abbreviation Ball :: "'a fset \ ('a \ bool) \ bool" where + "Ball X \ Set.Ball (fset X)" + +alias fBall = FSet.Ball + +qualified abbreviation Bex :: "'a fset \ ('a \ bool) \ bool" where + "Bex X \ Set.Bex (fset X)" + +alias fBex = FSet.Bex + +end + context includes lifting_syntax begin @@ -185,6 +200,16 @@ shows "(A ===> pcr_fset A ===> (=)) (\) (|\|)" 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 \ bool) \ 'a fset \ '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 \ 'a fset" is Union parametric Union_transfer by simp -lift_definition fBall :: "'a fset \ ('a \ bool) \ bool" is Ball parametric Ball_transfer . -lift_definition fBex :: "'a fset \ ('a \ bool) \ bool" is Bex parametric Bex_transfer . - lift_definition ffold :: "('a \ 'b \ 'b) \ 'b \ 'a fset \ 'b" is Finite_Set.fold . lift_definition fset_of_list :: "'a list \ 'a fset" is set by (rule finite_set) diff -r a6989a7d192a -r 7735645667f0 src/HOL/Library/Finite_Map.thy --- a/src/HOL/Library/Finite_Map.thy Fri May 26 10:34:39 2023 +0200 +++ b/src/HOL/Library/Finite_Map.thy Fri May 26 15:44:59 2023 +0200 @@ -1438,7 +1438,7 @@ \ \Code generation\ 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?