1(* Title: HOL/Library/FSet.thy 2 Author: Ondrej Kuncar, TU Muenchen 3 Author: Cezary Kaliszyk and Christian Urban 4 Author: Andrei Popescu, TU Muenchen 5*) 6 7section \<open>Type of finite sets defined as a subtype of sets\<close> 8 9theory FSet 10imports Main Countable 11begin 12 13subsection \<open>Definition of the type\<close> 14 15typedef 'a fset = "{A :: 'a set. finite A}" morphisms fset Abs_fset 16by auto 17 18setup_lifting type_definition_fset 19 20 21subsection \<open>Basic operations and type class instantiations\<close> 22 23(* FIXME transfer and right_total vs. bi_total *) 24instantiation fset :: (finite) finite 25begin 26instance by (standard; transfer; simp) 27end 28 29instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" 30begin 31 32lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp 33 34lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer 35 . 36 37definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)" 38 39lemma less_fset_transfer[transfer_rule]: 40 includes lifting_syntax 41 assumes [transfer_rule]: "bi_unique A" 42 shows "((pcr_fset A) ===> (pcr_fset A) ===> (=)) (\<subset>) (<)" 43 unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover 44 45 46lift_definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is union parametric union_transfer 47 by simp 48 49lift_definition inf_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is inter parametric inter_transfer 50 by simp 51 52lift_definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is minus parametric Diff_transfer 53 by simp 54 55instance 56 by (standard; transfer; auto)+ 57 58end 59 60abbreviation fempty :: "'a fset" ("{||}") where "{||} \<equiv> bot" 61abbreviation fsubset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50) where "xs |\<subseteq>| ys \<equiv> xs \<le> ys" 62abbreviation fsubset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50) where "xs |\<subset>| ys \<equiv> xs < ys" 63abbreviation funion :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65) where "xs |\<union>| ys \<equiv> sup xs ys" 64abbreviation finter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<inter>|" 65) where "xs |\<inter>| ys \<equiv> inf xs ys" 65abbreviation fminus :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|-|" 65) where "xs |-| ys \<equiv> minus xs ys" 66 67instantiation fset :: (equal) equal 68begin 69definition "HOL.equal A B \<longleftrightarrow> A |\<subseteq>| B \<and> B |\<subseteq>| A" 70instance by intro_classes (auto simp add: equal_fset_def) 71end 72 73instantiation fset :: (type) conditionally_complete_lattice 74begin 75 76context includes lifting_syntax 77begin 78 79lemma right_total_Inf_fset_transfer: 80 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" 81 shows "(rel_set (rel_set A) ===> rel_set A) 82 (\<lambda>S. if finite (\<Inter>S \<inter> Collect (Domainp A)) then \<Inter>S \<inter> Collect (Domainp A) else {}) 83 (\<lambda>S. if finite (Inf S) then Inf S else {})" 84 by transfer_prover 85 86lemma Inf_fset_transfer: 87 assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" 88 shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Inf A) then Inf A else {}) 89 (\<lambda>A. if finite (Inf A) then Inf A else {})" 90 by transfer_prover 91 92lift_definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Inf A) then Inf A else {}" 93parametric right_total_Inf_fset_transfer Inf_fset_transfer by simp 94 95lemma Sup_fset_transfer: 96 assumes [transfer_rule]: "bi_unique A" 97 shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Sup A) then Sup A else {}) 98 (\<lambda>A. if finite (Sup A) then Sup A else {})" by transfer_prover 99 100lift_definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Sup A) then Sup A else {}" 101parametric Sup_fset_transfer by simp 102 103lemma finite_Sup: "\<exists>z. finite z \<and> (\<forall>a. a \<in> X \<longrightarrow> a \<le> z) \<Longrightarrow> finite (Sup X)" 104by (auto intro: finite_subset) 105 106lemma transfer_bdd_below[transfer_rule]: "(rel_set (pcr_fset (=)) ===> (=)) bdd_below bdd_below" 107 by auto 108 109end 110 111instance 112proof 113 fix x z :: "'a fset" 114 fix X :: "'a fset set" 115 { 116 assume "x \<in> X" "bdd_below X" 117 then show "Inf X |\<subseteq>| x" by transfer auto 118 next 119 assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> z |\<subseteq>| x)" 120 then show "z |\<subseteq>| Inf X" by transfer (clarsimp, blast) 121 next 122 assume "x \<in> X" "bdd_above X" 123 then obtain z where "x \<in> X" "(\<And>x. x \<in> X \<Longrightarrow> x |\<subseteq>| z)" 124 by (auto simp: bdd_above_def) 125 then show "x |\<subseteq>| Sup X" 126 by transfer (auto intro!: finite_Sup) 127 next 128 assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> x |\<subseteq>| z)" 129 then show "Sup X |\<subseteq>| z" by transfer (clarsimp, blast) 130 } 131qed 132end 133 134instantiation fset :: (finite) complete_lattice 135begin 136 137lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer 138 by simp 139 140instance 141 by (standard; transfer; auto) 142 143end 144 145instantiation fset :: (finite) complete_boolean_algebra 146begin 147 148lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus 149 parametric right_total_Compl_transfer Compl_transfer by simp 150 151instance 152 by (standard; transfer) (simp_all add: Inf_Sup Diff_eq) 153end 154 155abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top" 156abbreviation fuminus :: "'a::finite fset \<Rightarrow> 'a fset" ("|-| _" [81] 80) where "|-| x \<equiv> uminus x" 157 158declare top_fset.rep_eq[simp] 159 160 161subsection \<open>Other operations\<close> 162 163lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer 164 by simp 165 166syntax 167 "_insert_fset" :: "args => 'a fset" ("{|(_)|}") 168 169translations 170 "{|x, xs|}" == "CONST finsert x {|xs|}" 171 "{|x|}" == "CONST finsert x {||}" 172 173lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member 174 parametric member_transfer . 175 176abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" 177 178context includes lifting_syntax 179begin 180 181lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter 182 parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp 183 184lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer 185by (simp add: finite_subset) 186 187lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer . 188 189lift_definition fimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" (infixr "|`|" 90) is image 190 parametric image_transfer by simp 191 192lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem . 193 194lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer 195by (simp add: Set.bind_def) 196 197lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp 198 199lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer . 200lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer . 201 202lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold . 203 204lift_definition fset_of_list :: "'a list \<Rightarrow> 'a fset" is set by (rule finite_set) 205 206lift_definition sorted_list_of_fset :: "'a::linorder fset \<Rightarrow> 'a list" is sorted_list_of_set . 207 208subsection \<open>Transferred lemmas from Set.thy\<close> 209 210lemmas fset_eqI = set_eqI[Transfer.transferred] 211lemmas fset_eq_iff[no_atp] = set_eq_iff[Transfer.transferred] 212lemmas fBallI[intro!] = ballI[Transfer.transferred] 213lemmas fbspec[dest?] = bspec[Transfer.transferred] 214lemmas fBallE[elim] = ballE[Transfer.transferred] 215lemmas fBexI[intro] = bexI[Transfer.transferred] 216lemmas rev_fBexI[intro?] = rev_bexI[Transfer.transferred] 217lemmas fBexCI = bexCI[Transfer.transferred] 218lemmas fBexE[elim!] = bexE[Transfer.transferred] 219lemmas fBall_triv[simp] = ball_triv[Transfer.transferred] 220lemmas fBex_triv[simp] = bex_triv[Transfer.transferred] 221lemmas fBex_triv_one_point1[simp] = bex_triv_one_point1[Transfer.transferred] 222lemmas fBex_triv_one_point2[simp] = bex_triv_one_point2[Transfer.transferred] 223lemmas fBex_one_point1[simp] = bex_one_point1[Transfer.transferred] 224lemmas fBex_one_point2[simp] = bex_one_point2[Transfer.transferred] 225lemmas fBall_one_point1[simp] = ball_one_point1[Transfer.transferred] 226lemmas fBall_one_point2[simp] = ball_one_point2[Transfer.transferred] 227lemmas fBall_conj_distrib = ball_conj_distrib[Transfer.transferred] 228lemmas fBex_disj_distrib = bex_disj_distrib[Transfer.transferred] 229lemmas fBall_cong[fundef_cong] = ball_cong[Transfer.transferred] 230lemmas fBex_cong[fundef_cong] = bex_cong[Transfer.transferred] 231lemmas fsubsetI[intro!] = subsetI[Transfer.transferred] 232lemmas fsubsetD[elim, intro?] = subsetD[Transfer.transferred] 233lemmas rev_fsubsetD[no_atp,intro?] = rev_subsetD[Transfer.transferred] 234lemmas fsubsetCE[no_atp,elim] = subsetCE[Transfer.transferred] 235lemmas fsubset_eq[no_atp] = subset_eq[Transfer.transferred] 236lemmas contra_fsubsetD[no_atp] = contra_subsetD[Transfer.transferred] 237lemmas fsubset_refl = subset_refl[Transfer.transferred] 238lemmas fsubset_trans = subset_trans[Transfer.transferred] 239lemmas fset_rev_mp = set_rev_mp[Transfer.transferred] 240lemmas fset_mp = set_mp[Transfer.transferred] 241lemmas fsubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred] 242lemmas eq_fmem_trans = eq_mem_trans[Transfer.transferred] 243lemmas fsubset_antisym[intro!] = subset_antisym[Transfer.transferred] 244lemmas fequalityD1 = equalityD1[Transfer.transferred] 245lemmas fequalityD2 = equalityD2[Transfer.transferred] 246lemmas fequalityE = equalityE[Transfer.transferred] 247lemmas fequalityCE[elim] = equalityCE[Transfer.transferred] 248lemmas eqfset_imp_iff = eqset_imp_iff[Transfer.transferred] 249lemmas eqfelem_imp_iff = eqelem_imp_iff[Transfer.transferred] 250lemmas fempty_iff[simp] = empty_iff[Transfer.transferred] 251lemmas fempty_fsubsetI[iff] = empty_subsetI[Transfer.transferred] 252lemmas equalsffemptyI = equals0I[Transfer.transferred] 253lemmas equalsffemptyD = equals0D[Transfer.transferred] 254lemmas fBall_fempty[simp] = ball_empty[Transfer.transferred] 255lemmas fBex_fempty[simp] = bex_empty[Transfer.transferred] 256lemmas fPow_iff[iff] = Pow_iff[Transfer.transferred] 257lemmas fPowI = PowI[Transfer.transferred] 258lemmas fPowD = PowD[Transfer.transferred] 259lemmas fPow_bottom = Pow_bottom[Transfer.transferred] 260lemmas fPow_top = Pow_top[Transfer.transferred] 261lemmas fPow_not_fempty = Pow_not_empty[Transfer.transferred] 262lemmas finter_iff[simp] = Int_iff[Transfer.transferred] 263lemmas finterI[intro!] = IntI[Transfer.transferred] 264lemmas finterD1 = IntD1[Transfer.transferred] 265lemmas finterD2 = IntD2[Transfer.transferred] 266lemmas finterE[elim!] = IntE[Transfer.transferred] 267lemmas funion_iff[simp] = Un_iff[Transfer.transferred] 268lemmas funionI1[elim?] = UnI1[Transfer.transferred] 269lemmas funionI2[elim?] = UnI2[Transfer.transferred] 270lemmas funionCI[intro!] = UnCI[Transfer.transferred] 271lemmas funionE[elim!] = UnE[Transfer.transferred] 272lemmas fminus_iff[simp] = Diff_iff[Transfer.transferred] 273lemmas fminusI[intro!] = DiffI[Transfer.transferred] 274lemmas fminusD1 = DiffD1[Transfer.transferred] 275lemmas fminusD2 = DiffD2[Transfer.transferred] 276lemmas fminusE[elim!] = DiffE[Transfer.transferred] 277lemmas finsert_iff[simp] = insert_iff[Transfer.transferred] 278lemmas finsertI1 = insertI1[Transfer.transferred] 279lemmas finsertI2 = insertI2[Transfer.transferred] 280lemmas finsertE[elim!] = insertE[Transfer.transferred] 281lemmas finsertCI[intro!] = insertCI[Transfer.transferred] 282lemmas fsubset_finsert_iff = subset_insert_iff[Transfer.transferred] 283lemmas finsert_ident = insert_ident[Transfer.transferred] 284lemmas fsingletonI[intro!,no_atp] = singletonI[Transfer.transferred] 285lemmas fsingletonD[dest!,no_atp] = singletonD[Transfer.transferred] 286lemmas fsingleton_iff = singleton_iff[Transfer.transferred] 287lemmas fsingleton_inject[dest!] = singleton_inject[Transfer.transferred] 288lemmas fsingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred] 289lemmas fsingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred] 290lemmas fsubset_fsingletonD = subset_singletonD[Transfer.transferred] 291lemmas fminus_single_finsert = Diff_single_insert[Transfer.transferred] 292lemmas fdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred] 293lemmas funion_fsingleton_iff = Un_singleton_iff[Transfer.transferred] 294lemmas fsingleton_funion_iff = singleton_Un_iff[Transfer.transferred] 295lemmas fimage_eqI[simp, intro] = image_eqI[Transfer.transferred] 296lemmas fimageI = imageI[Transfer.transferred] 297lemmas rev_fimage_eqI = rev_image_eqI[Transfer.transferred] 298lemmas fimageE[elim!] = imageE[Transfer.transferred] 299lemmas Compr_fimage_eq = Compr_image_eq[Transfer.transferred] 300lemmas fimage_funion = image_Un[Transfer.transferred] 301lemmas fimage_iff = image_iff[Transfer.transferred] 302lemmas fimage_fsubset_iff[no_atp] = image_subset_iff[Transfer.transferred] 303lemmas fimage_fsubsetI = image_subsetI[Transfer.transferred] 304lemmas fimage_ident[simp] = image_ident[Transfer.transferred] 305lemmas if_split_fmem1 = if_split_mem1[Transfer.transferred] 306lemmas if_split_fmem2 = if_split_mem2[Transfer.transferred] 307lemmas pfsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred] 308lemmas pfsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred] 309lemmas pfsubset_finsert_iff = psubset_insert_iff[Transfer.transferred] 310lemmas pfsubset_eq = psubset_eq[Transfer.transferred] 311lemmas pfsubset_imp_fsubset = psubset_imp_subset[Transfer.transferred] 312lemmas pfsubset_trans = psubset_trans[Transfer.transferred] 313lemmas pfsubsetD = psubsetD[Transfer.transferred] 314lemmas pfsubset_fsubset_trans = psubset_subset_trans[Transfer.transferred] 315lemmas fsubset_pfsubset_trans = subset_psubset_trans[Transfer.transferred] 316lemmas pfsubset_imp_ex_fmem = psubset_imp_ex_mem[Transfer.transferred] 317lemmas fimage_fPow_mono = image_Pow_mono[Transfer.transferred] 318lemmas fimage_fPow_surj = image_Pow_surj[Transfer.transferred] 319lemmas fsubset_finsertI = subset_insertI[Transfer.transferred] 320lemmas fsubset_finsertI2 = subset_insertI2[Transfer.transferred] 321lemmas fsubset_finsert = subset_insert[Transfer.transferred] 322lemmas funion_upper1 = Un_upper1[Transfer.transferred] 323lemmas funion_upper2 = Un_upper2[Transfer.transferred] 324lemmas funion_least = Un_least[Transfer.transferred] 325lemmas finter_lower1 = Int_lower1[Transfer.transferred] 326lemmas finter_lower2 = Int_lower2[Transfer.transferred] 327lemmas finter_greatest = Int_greatest[Transfer.transferred] 328lemmas fminus_fsubset = Diff_subset[Transfer.transferred] 329lemmas fminus_fsubset_conv = Diff_subset_conv[Transfer.transferred] 330lemmas fsubset_fempty[simp] = subset_empty[Transfer.transferred] 331lemmas not_pfsubset_fempty[iff] = not_psubset_empty[Transfer.transferred] 332lemmas finsert_is_funion = insert_is_Un[Transfer.transferred] 333lemmas finsert_not_fempty[simp] = insert_not_empty[Transfer.transferred] 334lemmas fempty_not_finsert = empty_not_insert[Transfer.transferred] 335lemmas finsert_absorb = insert_absorb[Transfer.transferred] 336lemmas finsert_absorb2[simp] = insert_absorb2[Transfer.transferred] 337lemmas finsert_commute = insert_commute[Transfer.transferred] 338lemmas finsert_fsubset[simp] = insert_subset[Transfer.transferred] 339lemmas finsert_inter_finsert[simp] = insert_inter_insert[Transfer.transferred] 340lemmas finsert_disjoint[simp,no_atp] = insert_disjoint[Transfer.transferred] 341lemmas disjoint_finsert[simp,no_atp] = disjoint_insert[Transfer.transferred] 342lemmas fimage_fempty[simp] = image_empty[Transfer.transferred] 343lemmas fimage_finsert[simp] = image_insert[Transfer.transferred] 344lemmas fimage_constant = image_constant[Transfer.transferred] 345lemmas fimage_constant_conv = image_constant_conv[Transfer.transferred] 346lemmas fimage_fimage = image_image[Transfer.transferred] 347lemmas finsert_fimage[simp] = insert_image[Transfer.transferred] 348lemmas fimage_is_fempty[iff] = image_is_empty[Transfer.transferred] 349lemmas fempty_is_fimage[iff] = empty_is_image[Transfer.transferred] 350lemmas fimage_cong = image_cong[Transfer.transferred] 351lemmas fimage_finter_fsubset = image_Int_subset[Transfer.transferred] 352lemmas fimage_fminus_fsubset = image_diff_subset[Transfer.transferred] 353lemmas finter_absorb = Int_absorb[Transfer.transferred] 354lemmas finter_left_absorb = Int_left_absorb[Transfer.transferred] 355lemmas finter_commute = Int_commute[Transfer.transferred] 356lemmas finter_left_commute = Int_left_commute[Transfer.transferred] 357lemmas finter_assoc = Int_assoc[Transfer.transferred] 358lemmas finter_ac = Int_ac[Transfer.transferred] 359lemmas finter_absorb1 = Int_absorb1[Transfer.transferred] 360lemmas finter_absorb2 = Int_absorb2[Transfer.transferred] 361lemmas finter_fempty_left = Int_empty_left[Transfer.transferred] 362lemmas finter_fempty_right = Int_empty_right[Transfer.transferred] 363lemmas disjoint_iff_fnot_equal = disjoint_iff_not_equal[Transfer.transferred] 364lemmas finter_funion_distrib = Int_Un_distrib[Transfer.transferred] 365lemmas finter_funion_distrib2 = Int_Un_distrib2[Transfer.transferred] 366lemmas finter_fsubset_iff[no_atp, simp] = Int_subset_iff[Transfer.transferred] 367lemmas funion_absorb = Un_absorb[Transfer.transferred] 368lemmas funion_left_absorb = Un_left_absorb[Transfer.transferred] 369lemmas funion_commute = Un_commute[Transfer.transferred] 370lemmas funion_left_commute = Un_left_commute[Transfer.transferred] 371lemmas funion_assoc = Un_assoc[Transfer.transferred] 372lemmas funion_ac = Un_ac[Transfer.transferred] 373lemmas funion_absorb1 = Un_absorb1[Transfer.transferred] 374lemmas funion_absorb2 = Un_absorb2[Transfer.transferred] 375lemmas funion_fempty_left = Un_empty_left[Transfer.transferred] 376lemmas funion_fempty_right = Un_empty_right[Transfer.transferred] 377lemmas funion_finsert_left[simp] = Un_insert_left[Transfer.transferred] 378lemmas funion_finsert_right[simp] = Un_insert_right[Transfer.transferred] 379lemmas finter_finsert_left = Int_insert_left[Transfer.transferred] 380lemmas finter_finsert_left_ifffempty[simp] = Int_insert_left_if0[Transfer.transferred] 381lemmas finter_finsert_left_if1[simp] = Int_insert_left_if1[Transfer.transferred] 382lemmas finter_finsert_right = Int_insert_right[Transfer.transferred] 383lemmas finter_finsert_right_ifffempty[simp] = Int_insert_right_if0[Transfer.transferred] 384lemmas finter_finsert_right_if1[simp] = Int_insert_right_if1[Transfer.transferred] 385lemmas funion_finter_distrib = Un_Int_distrib[Transfer.transferred] 386lemmas funion_finter_distrib2 = Un_Int_distrib2[Transfer.transferred] 387lemmas funion_finter_crazy = Un_Int_crazy[Transfer.transferred] 388lemmas fsubset_funion_eq = subset_Un_eq[Transfer.transferred] 389lemmas funion_fempty[iff] = Un_empty[Transfer.transferred] 390lemmas funion_fsubset_iff[no_atp, simp] = Un_subset_iff[Transfer.transferred] 391lemmas funion_fminus_finter = Un_Diff_Int[Transfer.transferred] 392lemmas ffunion_empty[simp] = Union_empty[Transfer.transferred] 393lemmas ffunion_mono = Union_mono[Transfer.transferred] 394lemmas ffunion_insert[simp] = Union_insert[Transfer.transferred] 395lemmas fminus_finter2 = Diff_Int2[Transfer.transferred] 396lemmas funion_finter_assoc_eq = Un_Int_assoc_eq[Transfer.transferred] 397lemmas fBall_funion = ball_Un[Transfer.transferred] 398lemmas fBex_funion = bex_Un[Transfer.transferred] 399lemmas fminus_eq_fempty_iff[simp,no_atp] = Diff_eq_empty_iff[Transfer.transferred] 400lemmas fminus_cancel[simp] = Diff_cancel[Transfer.transferred] 401lemmas fminus_idemp[simp] = Diff_idemp[Transfer.transferred] 402lemmas fminus_triv = Diff_triv[Transfer.transferred] 403lemmas fempty_fminus[simp] = empty_Diff[Transfer.transferred] 404lemmas fminus_fempty[simp] = Diff_empty[Transfer.transferred] 405lemmas fminus_finsertffempty[simp,no_atp] = Diff_insert0[Transfer.transferred] 406lemmas fminus_finsert = Diff_insert[Transfer.transferred] 407lemmas fminus_finsert2 = Diff_insert2[Transfer.transferred] 408lemmas finsert_fminus_if = insert_Diff_if[Transfer.transferred] 409lemmas finsert_fminus1[simp] = insert_Diff1[Transfer.transferred] 410lemmas finsert_fminus_single[simp] = insert_Diff_single[Transfer.transferred] 411lemmas finsert_fminus = insert_Diff[Transfer.transferred] 412lemmas fminus_finsert_absorb = Diff_insert_absorb[Transfer.transferred] 413lemmas fminus_disjoint[simp] = Diff_disjoint[Transfer.transferred] 414lemmas fminus_partition = Diff_partition[Transfer.transferred] 415lemmas double_fminus = double_diff[Transfer.transferred] 416lemmas funion_fminus_cancel[simp] = Un_Diff_cancel[Transfer.transferred] 417lemmas funion_fminus_cancel2[simp] = Un_Diff_cancel2[Transfer.transferred] 418lemmas fminus_funion = Diff_Un[Transfer.transferred] 419lemmas fminus_finter = Diff_Int[Transfer.transferred] 420lemmas funion_fminus = Un_Diff[Transfer.transferred] 421lemmas finter_fminus = Int_Diff[Transfer.transferred] 422lemmas fminus_finter_distrib = Diff_Int_distrib[Transfer.transferred] 423lemmas fminus_finter_distrib2 = Diff_Int_distrib2[Transfer.transferred] 424lemmas fUNIV_bool[no_atp] = UNIV_bool[Transfer.transferred] 425lemmas fPow_fempty[simp] = Pow_empty[Transfer.transferred] 426lemmas fPow_finsert = Pow_insert[Transfer.transferred] 427lemmas funion_fPow_fsubset = Un_Pow_subset[Transfer.transferred] 428lemmas fPow_finter_eq[simp] = Pow_Int_eq[Transfer.transferred] 429lemmas fset_eq_fsubset = set_eq_subset[Transfer.transferred] 430lemmas fsubset_iff[no_atp] = subset_iff[Transfer.transferred] 431lemmas fsubset_iff_pfsubset_eq = subset_iff_psubset_eq[Transfer.transferred] 432lemmas all_not_fin_conv[simp] = all_not_in_conv[Transfer.transferred] 433lemmas ex_fin_conv = ex_in_conv[Transfer.transferred] 434lemmas fimage_mono = image_mono[Transfer.transferred] 435lemmas fPow_mono = Pow_mono[Transfer.transferred] 436lemmas finsert_mono = insert_mono[Transfer.transferred] 437lemmas funion_mono = Un_mono[Transfer.transferred] 438lemmas finter_mono = Int_mono[Transfer.transferred] 439lemmas fminus_mono = Diff_mono[Transfer.transferred] 440lemmas fin_mono = in_mono[Transfer.transferred] 441lemmas fthe_felem_eq[simp] = the_elem_eq[Transfer.transferred] 442lemmas fLeast_mono = Least_mono[Transfer.transferred] 443lemmas fbind_fbind = bind_bind[Transfer.transferred] 444lemmas fempty_fbind[simp] = empty_bind[Transfer.transferred] 445lemmas nonfempty_fbind_const = nonempty_bind_const[Transfer.transferred] 446lemmas fbind_const = bind_const[Transfer.transferred] 447lemmas ffmember_filter[simp] = member_filter[Transfer.transferred] 448lemmas fequalityI = equalityI[Transfer.transferred] 449lemmas fset_of_list_simps[simp] = set_simps[Transfer.transferred] 450lemmas fset_of_list_append[simp] = set_append[Transfer.transferred] 451lemmas fset_of_list_rev[simp] = set_rev[Transfer.transferred] 452lemmas fset_of_list_map[simp] = set_map[Transfer.transferred] 453 454 455subsection \<open>Additional lemmas\<close> 456 457subsubsection \<open>\<open>ffUnion\<close>\<close> 458 459lemmas ffUnion_funion_distrib[simp] = Union_Un_distrib[Transfer.transferred] 460 461 462subsubsection \<open>\<open>fbind\<close>\<close> 463 464lemma fbind_cong[fundef_cong]: "A = B \<Longrightarrow> (\<And>x. x |\<in>| B \<Longrightarrow> f x = g x) \<Longrightarrow> fbind A f = fbind B g" 465by transfer force 466 467 468subsubsection \<open>\<open>fsingleton\<close>\<close> 469 470lemmas fsingletonE = fsingletonD [elim_format] 471 472 473subsubsection \<open>\<open>femepty\<close>\<close> 474 475lemma fempty_ffilter[simp]: "ffilter (\<lambda>_. False) A = {||}" 476by transfer auto 477 478(* FIXME, transferred doesn't work here *) 479lemma femptyE [elim!]: "a |\<in>| {||} \<Longrightarrow> P" 480 by simp 481 482 483subsubsection \<open>\<open>fset\<close>\<close> 484 485lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq 486 487lemma finite_fset [simp]: 488 shows "finite (fset S)" 489 by transfer simp 490 491lemmas fset_cong = fset_inject 492 493lemma filter_fset [simp]: 494 shows "fset (ffilter P xs) = Collect P \<inter> fset xs" 495 by transfer auto 496 497lemma notin_fset: "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S" by (simp add: fmember.rep_eq) 498 499lemmas inter_fset[simp] = inf_fset.rep_eq 500 501lemmas union_fset[simp] = sup_fset.rep_eq 502 503lemmas minus_fset[simp] = minus_fset.rep_eq 504 505 506subsubsection \<open>\<open>ffilter\<close>\<close> 507 508lemma subset_ffilter: 509 "ffilter P A |\<subseteq>| ffilter Q A = (\<forall> x. x |\<in>| A \<longrightarrow> P x \<longrightarrow> Q x)" 510 by transfer auto 511 512lemma eq_ffilter: 513 "(ffilter P A = ffilter Q A) = (\<forall>x. x |\<in>| A \<longrightarrow> P x = Q x)" 514 by transfer auto 515 516lemma pfsubset_ffilter: 517 "(\<And>x. x |\<in>| A \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| A \<and> \<not> P x \<and> Q x) \<Longrightarrow> 518 ffilter P A |\<subset>| ffilter Q A" 519 unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter) 520 521 522subsubsection \<open>\<open>fset_of_list\<close>\<close> 523 524lemma fset_of_list_filter[simp]: 525 "fset_of_list (filter P xs) = ffilter P (fset_of_list xs)" 526 by transfer (auto simp: Set.filter_def) 527 528lemma fset_of_list_subset[intro]: 529 "set xs \<subseteq> set ys \<Longrightarrow> fset_of_list xs |\<subseteq>| fset_of_list ys" 530 by transfer simp 531 532lemma fset_of_list_elem: "(x |\<in>| fset_of_list xs) \<longleftrightarrow> (x \<in> set xs)" 533 by transfer simp 534 535 536subsubsection \<open>\<open>finsert\<close>\<close> 537 538(* FIXME, transferred doesn't work here *) 539lemma set_finsert: 540 assumes "x |\<in>| A" 541 obtains B where "A = finsert x B" and "x |\<notin>| B" 542using assms by transfer (metis Set.set_insert finite_insert) 543 544lemma mk_disjoint_finsert: "a |\<in>| A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a |\<notin>| B" 545 by (rule exI [where x = "A |-| {|a|}"]) blast 546 547lemma finsert_eq_iff: 548 assumes "a |\<notin>| A" and "b |\<notin>| B" 549 shows "(finsert a A = finsert b B) = 550 (if a = b then A = B else \<exists>C. A = finsert b C \<and> b |\<notin>| C \<and> B = finsert a C \<and> a |\<notin>| C)" 551 using assms by transfer (force simp: insert_eq_iff) 552 553 554subsubsection \<open>\<open>fimage\<close>\<close> 555 556lemma subset_fimage_iff: "(B |\<subseteq>| f|`|A) = (\<exists> AA. AA |\<subseteq>| A \<and> B = f|`|AA)" 557by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff) 558 559 560subsubsection \<open>bounded quantification\<close> 561 562lemma bex_simps [simp, no_atp]: 563 "\<And>A P Q. fBex A (\<lambda>x. P x \<and> Q) = (fBex A P \<and> Q)" 564 "\<And>A P Q. fBex A (\<lambda>x. P \<and> Q x) = (P \<and> fBex A Q)" 565 "\<And>P. fBex {||} P = False" 566 "\<And>a B P. fBex (finsert a B) P = (P a \<or> fBex B P)" 567 "\<And>A P f. fBex (f |`| A) P = fBex A (\<lambda>x. P (f x))" 568 "\<And>A P. (\<not> fBex A P) = fBall A (\<lambda>x. \<not> P x)" 569by auto 570 571lemma ball_simps [simp, no_atp]: 572 "\<And>A P Q. fBall A (\<lambda>x. P x \<or> Q) = (fBall A P \<or> Q)" 573 "\<And>A P Q. fBall A (\<lambda>x. P \<or> Q x) = (P \<or> fBall A Q)" 574 "\<And>A P Q. fBall A (\<lambda>x. P \<longrightarrow> Q x) = (P \<longrightarrow> fBall A Q)" 575 "\<And>A P Q. fBall A (\<lambda>x. P x \<longrightarrow> Q) = (fBex A P \<longrightarrow> Q)" 576 "\<And>P. fBall {||} P = True" 577 "\<And>a B P. fBall (finsert a B) P = (P a \<and> fBall B P)" 578 "\<And>A P f. fBall (f |`| A) P = fBall A (\<lambda>x. P (f x))" 579 "\<And>A P. (\<not> fBall A P) = fBex A (\<lambda>x. \<not> P x)" 580by auto 581 582lemma atomize_fBall: 583 "(\<And>x. x |\<in>| A ==> P x) == Trueprop (fBall A (\<lambda>x. P x))" 584apply (simp only: atomize_all atomize_imp) 585apply (rule equal_intr_rule) 586 by (transfer, simp)+ 587 588lemma fBall_mono[mono]: "P \<le> Q \<Longrightarrow> fBall S P \<le> fBall S Q" 589by auto 590 591lemma fBex_mono[mono]: "P \<le> Q \<Longrightarrow> fBex S P \<le> fBex S Q" 592by auto 593 594end 595 596 597subsubsection \<open>\<open>fcard\<close>\<close> 598 599(* FIXME: improve transferred to handle bounded meta quantification *) 600 601lemma fcard_fempty: 602 "fcard {||} = 0" 603 by transfer (rule card_empty) 604 605lemma fcard_finsert_disjoint: 606 "x |\<notin>| A \<Longrightarrow> fcard (finsert x A) = Suc (fcard A)" 607 by transfer (rule card_insert_disjoint) 608 609lemma fcard_finsert_if: 610 "fcard (finsert x A) = (if x |\<in>| A then fcard A else Suc (fcard A))" 611 by transfer (rule card_insert_if) 612 613lemma fcard_0_eq [simp, no_atp]: 614 "fcard A = 0 \<longleftrightarrow> A = {||}" 615 by transfer (rule card_0_eq) 616 617lemma fcard_Suc_fminus1: 618 "x |\<in>| A \<Longrightarrow> Suc (fcard (A |-| {|x|})) = fcard A" 619 by transfer (rule card_Suc_Diff1) 620 621lemma fcard_fminus_fsingleton: 622 "x |\<in>| A \<Longrightarrow> fcard (A |-| {|x|}) = fcard A - 1" 623 by transfer (rule card_Diff_singleton) 624 625lemma fcard_fminus_fsingleton_if: 626 "fcard (A |-| {|x|}) = (if x |\<in>| A then fcard A - 1 else fcard A)" 627 by transfer (rule card_Diff_singleton_if) 628 629lemma fcard_fminus_finsert[simp]: 630 assumes "a |\<in>| A" and "a |\<notin>| B" 631 shows "fcard (A |-| finsert a B) = fcard (A |-| B) - 1" 632using assms by transfer (rule card_Diff_insert) 633 634lemma fcard_finsert: "fcard (finsert x A) = Suc (fcard (A |-| {|x|}))" 635by transfer (rule card_insert) 636 637lemma fcard_finsert_le: "fcard A \<le> fcard (finsert x A)" 638by transfer (rule card_insert_le) 639 640lemma fcard_mono: 641 "A |\<subseteq>| B \<Longrightarrow> fcard A \<le> fcard B" 642by transfer (rule card_mono) 643 644lemma fcard_seteq: "A |\<subseteq>| B \<Longrightarrow> fcard B \<le> fcard A \<Longrightarrow> A = B" 645by transfer (rule card_seteq) 646 647lemma pfsubset_fcard_mono: "A |\<subset>| B \<Longrightarrow> fcard A < fcard B" 648by transfer (rule psubset_card_mono) 649 650lemma fcard_funion_finter: 651 "fcard A + fcard B = fcard (A |\<union>| B) + fcard (A |\<inter>| B)" 652by transfer (rule card_Un_Int) 653 654lemma fcard_funion_disjoint: 655 "A |\<inter>| B = {||} \<Longrightarrow> fcard (A |\<union>| B) = fcard A + fcard B" 656by transfer (rule card_Un_disjoint) 657 658lemma fcard_funion_fsubset: 659 "B |\<subseteq>| A \<Longrightarrow> fcard (A |-| B) = fcard A - fcard B" 660by transfer (rule card_Diff_subset) 661 662lemma diff_fcard_le_fcard_fminus: 663 "fcard A - fcard B \<le> fcard(A |-| B)" 664by transfer (rule diff_card_le_card_Diff) 665 666lemma fcard_fminus1_less: "x |\<in>| A \<Longrightarrow> fcard (A |-| {|x|}) < fcard A" 667by transfer (rule card_Diff1_less) 668 669lemma fcard_fminus2_less: 670 "x |\<in>| A \<Longrightarrow> y |\<in>| A \<Longrightarrow> fcard (A |-| {|x|} |-| {|y|}) < fcard A" 671by transfer (rule card_Diff2_less) 672 673lemma fcard_fminus1_le: "fcard (A |-| {|x|}) \<le> fcard A" 674by transfer (rule card_Diff1_le) 675 676lemma fcard_pfsubset: "A |\<subseteq>| B \<Longrightarrow> fcard A < fcard B \<Longrightarrow> A < B" 677by transfer (rule card_psubset) 678 679 680subsubsection \<open>\<open>sorted_list_of_fset\<close>\<close> 681 682lemma sorted_list_of_fset_simps[simp]: 683 "set (sorted_list_of_fset S) = fset S" 684 "fset_of_list (sorted_list_of_fset S) = S" 685by (transfer, simp)+ 686 687 688subsubsection \<open>\<open>ffold\<close>\<close> 689 690(* FIXME: improve transferred to handle bounded meta quantification *) 691 692context comp_fun_commute 693begin 694 lemmas ffold_empty[simp] = fold_empty[Transfer.transferred] 695 696 lemma ffold_finsert [simp]: 697 assumes "x |\<notin>| A" 698 shows "ffold f z (finsert x A) = f x (ffold f z A)" 699 using assms by (transfer fixing: f) (rule fold_insert) 700 701 lemma ffold_fun_left_comm: 702 "f x (ffold f z A) = ffold f (f x z) A" 703 by (transfer fixing: f) (rule fold_fun_left_comm) 704 705 lemma ffold_finsert2: 706 "x |\<notin>| A \<Longrightarrow> ffold f z (finsert x A) = ffold f (f x z) A" 707 by (transfer fixing: f) (rule fold_insert2) 708 709 lemma ffold_rec: 710 assumes "x |\<in>| A" 711 shows "ffold f z A = f x (ffold f z (A |-| {|x|}))" 712 using assms by (transfer fixing: f) (rule fold_rec) 713 714 lemma ffold_finsert_fremove: 715 "ffold f z (finsert x A) = f x (ffold f z (A |-| {|x|}))" 716 by (transfer fixing: f) (rule fold_insert_remove) 717end 718 719lemma ffold_fimage: 720 assumes "inj_on g (fset A)" 721 shows "ffold f z (g |`| A) = ffold (f \<circ> g) z A" 722using assms by transfer' (rule fold_image) 723 724lemma ffold_cong: 725 assumes "comp_fun_commute f" "comp_fun_commute g" 726 "\<And>x. x |\<in>| A \<Longrightarrow> f x = g x" 727 and "s = t" and "A = B" 728 shows "ffold f s A = ffold g t B" 729using assms by transfer (metis Finite_Set.fold_cong) 730 731context comp_fun_idem 732begin 733 734 lemma ffold_finsert_idem: 735 "ffold f z (finsert x A) = f x (ffold f z A)" 736 by (transfer fixing: f) (rule fold_insert_idem) 737 738 declare ffold_finsert [simp del] ffold_finsert_idem [simp] 739 740 lemma ffold_finsert_idem2: 741 "ffold f z (finsert x A) = ffold f (f x z) A" 742 by (transfer fixing: f) (rule fold_insert_idem2) 743 744end 745 746 747subsubsection \<open>Group operations\<close> 748 749locale comm_monoid_fset = comm_monoid 750begin 751 752sublocale set: comm_monoid_set .. 753 754lift_definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" is set.F . 755 756lemmas cong[fundef_cong] = set.cong[Transfer.transferred] 757 758lemma strong_cong[cong]: 759 assumes "A = B" "\<And>x. x |\<in>| B =simp=> g x = h x" 760 shows "F g A = F h B" 761using assms unfolding simp_implies_def by (auto cong: cong) 762 763end 764 765context comm_monoid_add begin 766 767sublocale fsum: comm_monoid_fset plus 0 768 rewrites "comm_monoid_set.F plus 0 = sum" 769 defines fsum = fsum.F 770proof - 771 show "comm_monoid_fset (+) 0" by standard 772 773 show "comm_monoid_set.F (+) 0 = sum" unfolding sum_def .. 774qed 775 776end 777 778 779subsubsection \<open>Semilattice operations\<close> 780 781locale semilattice_fset = semilattice 782begin 783 784sublocale set: semilattice_set .. 785 786lift_definition F :: "'a fset \<Rightarrow> 'a" is set.F . 787 788lemma eq_fold: "F (finsert x A) = ffold f x A" 789 by transfer (rule set.eq_fold) 790 791lemma singleton [simp]: "F {|x|} = x" 792 by transfer (rule set.singleton) 793 794lemma insert_not_elem: "x |\<notin>| A \<Longrightarrow> A \<noteq> {||} \<Longrightarrow> F (finsert x A) = x \<^bold>* F A" 795 by transfer (rule set.insert_not_elem) 796 797lemma in_idem: "x |\<in>| A \<Longrightarrow> x \<^bold>* F A = F A" 798 by transfer (rule set.in_idem) 799 800lemma insert [simp]: "A \<noteq> {||} \<Longrightarrow> F (finsert x A) = x \<^bold>* F A" 801 by transfer (rule set.insert) 802 803end 804 805locale semilattice_order_fset = binary?: semilattice_order + semilattice_fset 806begin 807 808end 809 810 811context linorder begin 812 813sublocale fMin: semilattice_order_fset min less_eq less 814 rewrites "semilattice_set.F min = Min" 815 defines fMin = fMin.F 816proof - 817 show "semilattice_order_fset min (\<le>) (<)" by standard 818 819 show "semilattice_set.F min = Min" unfolding Min_def .. 820qed 821 822sublocale fMax: semilattice_order_fset max greater_eq greater 823 rewrites "semilattice_set.F max = Max" 824 defines fMax = fMax.F 825proof - 826 show "semilattice_order_fset max (\<ge>) (>)" 827 by standard 828 829 show "semilattice_set.F max = Max" 830 unfolding Max_def .. 831qed 832 833end 834 835lemma mono_fMax_commute: "mono f \<Longrightarrow> A \<noteq> {||} \<Longrightarrow> f (fMax A) = fMax (f |`| A)" 836 by transfer (rule mono_Max_commute) 837 838lemma mono_fMin_commute: "mono f \<Longrightarrow> A \<noteq> {||} \<Longrightarrow> f (fMin A) = fMin (f |`| A)" 839 by transfer (rule mono_Min_commute) 840 841lemma fMax_in[simp]: "A \<noteq> {||} \<Longrightarrow> fMax A |\<in>| A" 842 by transfer (rule Max_in) 843 844lemma fMin_in[simp]: "A \<noteq> {||} \<Longrightarrow> fMin A |\<in>| A" 845 by transfer (rule Min_in) 846 847lemma fMax_ge[simp]: "x |\<in>| A \<Longrightarrow> x \<le> fMax A" 848 by transfer (rule Max_ge) 849 850lemma fMin_le[simp]: "x |\<in>| A \<Longrightarrow> fMin A \<le> x" 851 by transfer (rule Min_le) 852 853lemma fMax_eqI: "(\<And>y. y |\<in>| A \<Longrightarrow> y \<le> x) \<Longrightarrow> x |\<in>| A \<Longrightarrow> fMax A = x" 854 by transfer (rule Max_eqI) 855 856lemma fMin_eqI: "(\<And>y. y |\<in>| A \<Longrightarrow> x \<le> y) \<Longrightarrow> x |\<in>| A \<Longrightarrow> fMin A = x" 857 by transfer (rule Min_eqI) 858 859lemma fMax_finsert[simp]: "fMax (finsert x A) = (if A = {||} then x else max x (fMax A))" 860 by transfer simp 861 862lemma fMin_finsert[simp]: "fMin (finsert x A) = (if A = {||} then x else min x (fMin A))" 863 by transfer simp 864 865context linorder begin 866 867lemma fset_linorder_max_induct[case_names fempty finsert]: 868 assumes "P {||}" 869 and "\<And>x S. \<lbrakk>\<forall>y. y |\<in>| S \<longrightarrow> y < x; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" 870 shows "P S" 871proof - 872 (* FIXME transfer and right_total vs. bi_total *) 873 note Domainp_forall_transfer[transfer_rule] 874 show ?thesis 875 using assms by (transfer fixing: less) (auto intro: finite_linorder_max_induct) 876qed 877 878lemma fset_linorder_min_induct[case_names fempty finsert]: 879 assumes "P {||}" 880 and "\<And>x S. \<lbrakk>\<forall>y. y |\<in>| S \<longrightarrow> y > x; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" 881 shows "P S" 882proof - 883 (* FIXME transfer and right_total vs. bi_total *) 884 note Domainp_forall_transfer[transfer_rule] 885 show ?thesis 886 using assms by (transfer fixing: less) (auto intro: finite_linorder_min_induct) 887qed 888 889end 890 891 892subsection \<open>Choice in fsets\<close> 893 894lemma fset_choice: 895 assumes "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)" 896 shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)" 897 using assms by transfer metis 898 899 900subsection \<open>Induction and Cases rules for fsets\<close> 901 902lemma fset_exhaust [case_names empty insert, cases type: fset]: 903 assumes fempty_case: "S = {||} \<Longrightarrow> P" 904 and finsert_case: "\<And>x S'. S = finsert x S' \<Longrightarrow> P" 905 shows "P" 906 using assms by transfer blast 907 908lemma fset_induct [case_names empty insert]: 909 assumes fempty_case: "P {||}" 910 and finsert_case: "\<And>x S. P S \<Longrightarrow> P (finsert x S)" 911 shows "P S" 912proof - 913 (* FIXME transfer and right_total vs. bi_total *) 914 note Domainp_forall_transfer[transfer_rule] 915 show ?thesis 916 using assms by transfer (auto intro: finite_induct) 917qed 918 919lemma fset_induct_stronger [case_names empty insert, induct type: fset]: 920 assumes empty_fset_case: "P {||}" 921 and insert_fset_case: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" 922 shows "P S" 923proof - 924 (* FIXME transfer and right_total vs. bi_total *) 925 note Domainp_forall_transfer[transfer_rule] 926 show ?thesis 927 using assms by transfer (auto intro: finite_induct) 928qed 929 930lemma fset_card_induct: 931 assumes empty_fset_case: "P {||}" 932 and card_fset_Suc_case: "\<And>S T. Suc (fcard S) = (fcard T) \<Longrightarrow> P S \<Longrightarrow> P T" 933 shows "P S" 934proof (induct S) 935 case empty 936 show "P {||}" by (rule empty_fset_case) 937next 938 case (insert x S) 939 have h: "P S" by fact 940 have "x |\<notin>| S" by fact 941 then have "Suc (fcard S) = fcard (finsert x S)" 942 by transfer auto 943 then show "P (finsert x S)" 944 using h card_fset_Suc_case by simp 945qed 946 947lemma fset_strong_cases: 948 obtains "xs = {||}" 949 | ys x where "x |\<notin>| ys" and "xs = finsert x ys" 950by transfer blast 951 952lemma fset_induct2: 953 "P {||} {||} \<Longrightarrow> 954 (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow> 955 (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow> 956 (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow> 957 P xsa ysa" 958 apply (induct xsa arbitrary: ysa) 959 apply (induct_tac x rule: fset_induct_stronger) 960 apply simp_all 961 apply (induct_tac xa rule: fset_induct_stronger) 962 apply simp_all 963 done 964 965 966subsection \<open>Setup for Lifting/Transfer\<close> 967 968subsubsection \<open>Relator and predicator properties\<close> 969 970lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is rel_set 971parametric rel_set_transfer . 972 973lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y) 974 \<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))" 975apply (rule ext)+ 976apply transfer' 977apply (subst rel_set_def[unfolded fun_eq_iff]) 978by blast 979 980lemma finite_rel_set: 981 assumes fin: "finite X" "finite Z" 982 assumes R_S: "rel_set (R OO S) X Z" 983 shows "\<exists>Y. finite Y \<and> rel_set R X Y \<and> rel_set S Y Z" 984proof - 985 obtain f where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)" 986 apply atomize_elim 987 apply (subst bchoice_iff[symmetric]) 988 using R_S[unfolded rel_set_def OO_def] by blast 989 990 obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))" 991 apply atomize_elim 992 apply (subst bchoice_iff[symmetric]) 993 using R_S[unfolded rel_set_def OO_def] by blast 994 995 let ?Y = "f ` X \<union> g ` Z" 996 have "finite ?Y" by (simp add: fin) 997 moreover have "rel_set R X ?Y" 998 unfolding rel_set_def 999 using f g by clarsimp blast 1000 moreover have "rel_set S ?Y Z" 1001 unfolding rel_set_def 1002 using f g by clarsimp blast 1003 ultimately show ?thesis by metis 1004qed 1005 1006subsubsection \<open>Transfer rules for the Transfer package\<close> 1007 1008text \<open>Unconditional transfer rules\<close> 1009 1010context includes lifting_syntax 1011begin 1012 1013lemmas fempty_transfer [transfer_rule] = empty_transfer[Transfer.transferred] 1014 1015lemma finsert_transfer [transfer_rule]: 1016 "(A ===> rel_fset A ===> rel_fset A) finsert finsert" 1017 unfolding rel_fun_def rel_fset_alt_def by blast 1018 1019lemma funion_transfer [transfer_rule]: 1020 "(rel_fset A ===> rel_fset A ===> rel_fset A) funion funion" 1021 unfolding rel_fun_def rel_fset_alt_def by blast 1022 1023lemma ffUnion_transfer [transfer_rule]: 1024 "(rel_fset (rel_fset A) ===> rel_fset A) ffUnion ffUnion" 1025 unfolding rel_fun_def rel_fset_alt_def by transfer (simp, fast) 1026 1027lemma fimage_transfer [transfer_rule]: 1028 "((A ===> B) ===> rel_fset A ===> rel_fset B) fimage fimage" 1029 unfolding rel_fun_def rel_fset_alt_def by simp blast 1030 1031lemma fBall_transfer [transfer_rule]: 1032 "(rel_fset A ===> (A ===> (=)) ===> (=)) fBall fBall" 1033 unfolding rel_fset_alt_def rel_fun_def by blast 1034 1035lemma fBex_transfer [transfer_rule]: 1036 "(rel_fset A ===> (A ===> (=)) ===> (=)) fBex fBex" 1037 unfolding rel_fset_alt_def rel_fun_def by blast 1038 1039(* FIXME transfer doesn't work here *) 1040lemma fPow_transfer [transfer_rule]: 1041 "(rel_fset A ===> rel_fset (rel_fset A)) fPow fPow" 1042 unfolding rel_fun_def 1043 using Pow_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] 1044 by blast 1045 1046lemma rel_fset_transfer [transfer_rule]: 1047 "((A ===> B ===> (=)) ===> rel_fset A ===> rel_fset B ===> (=)) 1048 rel_fset rel_fset" 1049 unfolding rel_fun_def 1050 using rel_set_transfer[unfolded rel_fun_def,rule_format, Transfer.transferred, where A = A and B = B] 1051 by simp 1052 1053lemma bind_transfer [transfer_rule]: 1054 "(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind" 1055 unfolding rel_fun_def 1056 using bind_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 1057 1058text \<open>Rules requiring bi-unique, bi-total or right-total relations\<close> 1059 1060lemma fmember_transfer [transfer_rule]: 1061 assumes "bi_unique A" 1062 shows "(A ===> rel_fset A ===> (=)) (|\<in>|) (|\<in>|)" 1063 using assms unfolding rel_fun_def rel_fset_alt_def bi_unique_def by metis 1064 1065lemma finter_transfer [transfer_rule]: 1066 assumes "bi_unique A" 1067 shows "(rel_fset A ===> rel_fset A ===> rel_fset A) finter finter" 1068 using assms unfolding rel_fun_def 1069 using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 1070 1071lemma fminus_transfer [transfer_rule]: 1072 assumes "bi_unique A" 1073 shows "(rel_fset A ===> rel_fset A ===> rel_fset A) (|-|) (|-|)" 1074 using assms unfolding rel_fun_def 1075 using Diff_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 1076 1077lemma fsubset_transfer [transfer_rule]: 1078 assumes "bi_unique A" 1079 shows "(rel_fset A ===> rel_fset A ===> (=)) (|\<subseteq>|) (|\<subseteq>|)" 1080 using assms unfolding rel_fun_def 1081 using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 1082 1083lemma fSup_transfer [transfer_rule]: 1084 "bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup" 1085 unfolding rel_fun_def 1086 apply clarify 1087 apply transfer' 1088 using Sup_fset_transfer[unfolded rel_fun_def] by blast 1089 1090(* FIXME: add right_total_fInf_transfer *) 1091 1092lemma fInf_transfer [transfer_rule]: 1093 assumes "bi_unique A" and "bi_total A" 1094 shows "(rel_set (rel_fset A) ===> rel_fset A) Inf Inf" 1095 using assms unfolding rel_fun_def 1096 apply clarify 1097 apply transfer' 1098 using Inf_fset_transfer[unfolded rel_fun_def] by blast 1099 1100lemma ffilter_transfer [transfer_rule]: 1101 assumes "bi_unique A" 1102 shows "((A ===> (=)) ===> rel_fset A ===> rel_fset A) ffilter ffilter" 1103 using assms unfolding rel_fun_def 1104 using Lifting_Set.filter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 1105 1106lemma card_transfer [transfer_rule]: 1107 "bi_unique A \<Longrightarrow> (rel_fset A ===> (=)) fcard fcard" 1108 unfolding rel_fun_def 1109 using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 1110 1111end 1112 1113lifting_update fset.lifting 1114lifting_forget fset.lifting 1115 1116 1117subsection \<open>BNF setup\<close> 1118 1119context 1120includes fset.lifting 1121begin 1122 1123lemma rel_fset_alt: 1124 "rel_fset R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)" 1125by transfer (simp add: rel_set_def) 1126 1127lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A" 1128apply (rule f_the_inv_into_f[unfolded inj_on_def]) 1129apply (simp add: fset_inject) 1130apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+ 1131. 1132 1133lemma rel_fset_aux: 1134"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow> 1135 ((BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO 1136 BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R") 1137proof 1138 assume ?L 1139 define R' where "R' = 1140 the_inv fset (Collect (case_prod R) \<inter> (fset a \<times> fset b))" (is "_ = the_inv fset ?L'") 1141 have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+ 1142 hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset) 1143 show ?R unfolding Grp_def relcompp.simps conversep.simps 1144 proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) 1145 from * show "a = fimage fst R'" using conjunct1[OF \<open>?L\<close>] 1146 by (transfer, auto simp add: image_def Int_def split: prod.splits) 1147 from * show "b = fimage snd R'" using conjunct2[OF \<open>?L\<close>] 1148 by (transfer, auto simp add: image_def Int_def split: prod.splits) 1149 qed (auto simp add: *) 1150next 1151 assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps 1152 apply (simp add: subset_eq Ball_def) 1153 apply (rule conjI) 1154 apply (transfer, clarsimp, metis snd_conv) 1155 by (transfer, clarsimp, metis fst_conv) 1156qed 1157 1158bnf "'a fset" 1159 map: fimage 1160 sets: fset 1161 bd: natLeq 1162 wits: "{||}" 1163 rel: rel_fset 1164apply - 1165 apply transfer' apply simp 1166 apply transfer' apply force 1167 apply transfer apply force 1168 apply transfer' apply force 1169 apply (rule natLeq_card_order) 1170 apply (rule natLeq_cinfinite) 1171 apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq) 1172 apply (fastforce simp: rel_fset_alt) 1173 apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt 1174 rel_fset_aux[unfolded OO_Grp_alt]) 1175apply transfer apply simp 1176done 1177 1178lemma rel_fset_fset: "rel_set \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2" 1179 by transfer (rule refl) 1180 1181end 1182 1183lemmas [simp] = fset.map_comp fset.map_id fset.set_map 1184 1185 1186subsection \<open>Size setup\<close> 1187 1188context includes fset.lifting begin 1189lift_definition size_fset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a fset \<Rightarrow> nat" is "\<lambda>f. sum (Suc \<circ> f)" . 1190end 1191 1192instantiation fset :: (type) size begin 1193definition size_fset where 1194 size_fset_overloaded_def: "size_fset = FSet.size_fset (\<lambda>_. 0)" 1195instance .. 1196end 1197 1198lemmas size_fset_simps[simp] = 1199 size_fset_def[THEN meta_eq_to_obj_eq, THEN fun_cong, THEN fun_cong, 1200 unfolded map_fun_def comp_def id_apply] 1201 1202lemmas size_fset_overloaded_simps[simp] = 1203 size_fset_simps[of "\<lambda>_. 0", unfolded add_0_left add_0_right, 1204 folded size_fset_overloaded_def] 1205 1206lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)" 1207 apply (subst fun_eq_iff) 1208 including fset.lifting by transfer (auto intro: sum.reindex_cong subset_inj_on) 1209 1210setup \<open> 1211BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset} 1212 @{thm size_fset_overloaded_def} @{thms size_fset_simps size_fset_overloaded_simps} 1213 @{thms fset_size_o_map} 1214\<close> 1215 1216lifting_update fset.lifting 1217lifting_forget fset.lifting 1218 1219subsection \<open>Advanced relator customization\<close> 1220 1221text \<open>Set vs. sum relators:\<close> 1222 1223lemma rel_set_rel_sum[simp]: 1224"rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow> 1225 rel_set \<chi> (Inl -` A1) (Inl -` A2) \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)" 1226(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr") 1227proof safe 1228 assume L: "?L" 1229 show ?Rl unfolding rel_set_def Bex_def vimage_eq proof safe 1230 fix l1 assume "Inl l1 \<in> A1" 1231 then obtain a2 where a2: "a2 \<in> A2" and "rel_sum \<chi> \<phi> (Inl l1) a2" 1232 using L unfolding rel_set_def by auto 1233 then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto) 1234 thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto 1235 next 1236 fix l2 assume "Inl l2 \<in> A2" 1237 then obtain a1 where a1: "a1 \<in> A1" and "rel_sum \<chi> \<phi> a1 (Inl l2)" 1238 using L unfolding rel_set_def by auto 1239 then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto) 1240 thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto 1241 qed 1242 show ?Rr unfolding rel_set_def Bex_def vimage_eq proof safe 1243 fix r1 assume "Inr r1 \<in> A1" 1244 then obtain a2 where a2: "a2 \<in> A2" and "rel_sum \<chi> \<phi> (Inr r1) a2" 1245 using L unfolding rel_set_def by auto 1246 then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto) 1247 thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto 1248 next 1249 fix r2 assume "Inr r2 \<in> A2" 1250 then obtain a1 where a1: "a1 \<in> A1" and "rel_sum \<chi> \<phi> a1 (Inr r2)" 1251 using L unfolding rel_set_def by auto 1252 then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto) 1253 thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto 1254 qed 1255next 1256 assume Rl: "?Rl" and Rr: "?Rr" 1257 show ?L unfolding rel_set_def Bex_def vimage_eq proof safe 1258 fix a1 assume a1: "a1 \<in> A1" 1259 show "\<exists> a2. a2 \<in> A2 \<and> rel_sum \<chi> \<phi> a1 a2" 1260 proof(cases a1) 1261 case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2" 1262 using Rl a1 unfolding rel_set_def by blast 1263 thus ?thesis unfolding Inl by auto 1264 next 1265 case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2" 1266 using Rr a1 unfolding rel_set_def by blast 1267 thus ?thesis unfolding Inr by auto 1268 qed 1269 next 1270 fix a2 assume a2: "a2 \<in> A2" 1271 show "\<exists> a1. a1 \<in> A1 \<and> rel_sum \<chi> \<phi> a1 a2" 1272 proof(cases a2) 1273 case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2" 1274 using Rl a2 unfolding rel_set_def by blast 1275 thus ?thesis unfolding Inl by auto 1276 next 1277 case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2" 1278 using Rr a2 unfolding rel_set_def by blast 1279 thus ?thesis unfolding Inr by auto 1280 qed 1281 qed 1282qed 1283 1284 1285subsubsection \<open>Countability\<close> 1286 1287lemma exists_fset_of_list: "\<exists>xs. fset_of_list xs = S" 1288including fset.lifting 1289by transfer (rule finite_list) 1290 1291lemma fset_of_list_surj[simp, intro]: "surj fset_of_list" 1292proof - 1293 have "x \<in> range fset_of_list" for x :: "'a fset" 1294 unfolding image_iff 1295 using exists_fset_of_list by fastforce 1296 thus ?thesis by auto 1297qed 1298 1299instance fset :: (countable) countable 1300proof 1301 obtain to_nat :: "'a list \<Rightarrow> nat" where "inj to_nat" 1302 by (metis ex_inj) 1303 moreover have "inj (inv fset_of_list)" 1304 using fset_of_list_surj by (rule surj_imp_inj_inv) 1305 ultimately have "inj (to_nat \<circ> inv fset_of_list)" 1306 by (rule inj_comp) 1307 thus "\<exists>to_nat::'a fset \<Rightarrow> nat. inj to_nat" 1308 by auto 1309qed 1310 1311 1312subsection \<open>Quickcheck setup\<close> 1313 1314text \<open>Setup adapted from sets.\<close> 1315 1316notation Quickcheck_Exhaustive.orelse (infixr "orelse" 55) 1317 1318definition (in term_syntax) [code_unfold]: 1319"valterm_femptyset = Code_Evaluation.valtermify ({||} :: ('a :: typerep) fset)" 1320 1321definition (in term_syntax) [code_unfold]: 1322"valtermify_finsert x s = Code_Evaluation.valtermify finsert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s" 1323 1324instantiation fset :: (exhaustive) exhaustive 1325begin 1326 1327fun exhaustive_fset where 1328"exhaustive_fset f i = (if i = 0 then None else (f {||} orelse exhaustive_fset (\<lambda>A. f A orelse Quickcheck_Exhaustive.exhaustive (\<lambda>x. if x |\<in>| A then None else f (finsert x A)) (i - 1)) (i - 1)))" 1329 1330instance .. 1331 1332end 1333 1334instantiation fset :: (full_exhaustive) full_exhaustive 1335begin 1336 1337fun full_exhaustive_fset where 1338"full_exhaustive_fset f i = (if i = 0 then None else (f valterm_femptyset orelse full_exhaustive_fset (\<lambda>A. f A orelse Quickcheck_Exhaustive.full_exhaustive (\<lambda>x. if fst x |\<in>| fst A then None else f (valtermify_finsert x A)) (i - 1)) (i - 1)))" 1339 1340instance .. 1341 1342end 1343 1344no_notation Quickcheck_Exhaustive.orelse (infixr "orelse" 55) 1345 1346notation scomp (infixl "\<circ>\<rightarrow>" 60) 1347 1348instantiation fset :: (random) random 1349begin 1350 1351fun random_aux_fset :: "natural \<Rightarrow> natural \<Rightarrow> natural \<times> natural \<Rightarrow> ('a fset \<times> (unit \<Rightarrow> term)) \<times> natural \<times> natural" where 1352"random_aux_fset 0 j = Quickcheck_Random.collapse (Random.select_weight [(1, Pair valterm_femptyset)])" | 1353"random_aux_fset (Code_Numeral.Suc i) j = 1354 Quickcheck_Random.collapse (Random.select_weight 1355 [(1, Pair valterm_femptyset), 1356 (Code_Numeral.Suc i, 1357 Quickcheck_Random.random j \<circ>\<rightarrow> (\<lambda>x. random_aux_fset i j \<circ>\<rightarrow> (\<lambda>s. Pair (valtermify_finsert x s))))])" 1358 1359lemma [code]: 1360 "random_aux_fset i j = 1361 Quickcheck_Random.collapse (Random.select_weight [(1, Pair valterm_femptyset), 1362 (i, Quickcheck_Random.random j \<circ>\<rightarrow> (\<lambda>x. random_aux_fset (i - 1) j \<circ>\<rightarrow> (\<lambda>s. Pair (valtermify_finsert x s))))])" 1363proof (induct i rule: natural.induct) 1364 case zero 1365 show ?case by (subst select_weight_drop_zero[symmetric]) (simp add: less_natural_def) 1366next 1367 case (Suc i) 1368 show ?case by (simp only: random_aux_fset.simps Suc_natural_minus_one) 1369qed 1370 1371definition "random_fset i = random_aux_fset i i" 1372 1373instance .. 1374 1375end 1376 1377no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 1378 1379end 1380