# HG changeset patch # User Andreas Lochbihler # Date 1428497949 -7200 # Node ID 0145010f3f83ef99129fba7955dd7f2b46d441ff # Parent 3d207f8f40dd49b1255b9272e0369e48c7de9d5f# Parent 5ee7e9721eacfd6c890232a4bcab76a599254816 merged diff -r 3d207f8f40dd -r 0145010f3f83 src/HOL/Library/Countable_Set_Type.thy --- a/src/HOL/Library/Countable_Set_Type.thy Wed Apr 08 11:52:53 2015 +0200 +++ b/src/HOL/Library/Countable_Set_Type.thy Wed Apr 08 14:59:09 2015 +0200 @@ -1,5 +1,6 @@ (* Title: HOL/Library/Countable_Set_Type.thy Author: Andrei Popescu, TU Muenchen + Author: Andreas Lochbihler, ETH Zurich Copyright 2012 Type of (at most) countable sets. @@ -8,11 +9,9 @@ section {* Type of (at Most) Countable Sets *} theory Countable_Set_Type -imports Countable_Set Cardinal_Notations +imports Countable_Set Cardinal_Notations Conditionally_Complete_Lattices begin -abbreviation "Grp \ BNF_Def.Grp" - subsection{* Cardinal stuff *} @@ -68,22 +67,418 @@ acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp] rcset[Transfer.transferred, unfolded mem_Collect_eq, simp] +instantiation cset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" +begin + +interpretation lifting_syntax . + +lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp + +lift_definition less_eq_cset :: "'a cset \ 'a cset \ bool" + is subset_eq parametric subset_transfer . + +definition less_cset :: "'a cset \ 'a cset \ bool" +where "xs < ys \ xs \ ys \ xs \ (ys::'a cset)" + +lemma less_cset_transfer[transfer_rule]: + assumes [transfer_rule]: "bi_unique A" + shows "((pcr_cset A) ===> (pcr_cset A) ===> op =) op \ op <" +unfolding less_cset_def[abs_def] psubset_eq[abs_def] by transfer_prover + +lift_definition sup_cset :: "'a cset \ 'a cset \ 'a cset" +is union parametric union_transfer by simp + +lift_definition inf_cset :: "'a cset \ 'a cset \ 'a cset" +is inter parametric inter_transfer by simp + +lift_definition minus_cset :: "'a cset \ 'a cset \ 'a cset" +is minus parametric Diff_transfer by simp + +instance by default(transfer, fastforce)+ +end + +abbreviation cempty :: "'a cset" where "cempty \ bot" +abbreviation csubset_eq :: "'a cset \ 'a cset \ bool" where "csubset_eq xs ys \ xs \ ys" +abbreviation csubset :: "'a cset \ 'a cset \ bool" where "csubset xs ys \ xs < ys" +abbreviation cUn :: "'a cset \ 'a cset \ 'a cset" where "cUn xs ys \ sup xs ys" +abbreviation cInt :: "'a cset \ 'a cset \ 'a cset" where "cInt xs ys \ inf xs ys" +abbreviation cDiff :: "'a cset \ 'a cset \ 'a cset" where "cDiff xs ys \ minus xs ys" + lift_definition cin :: "'a \ 'a cset \ bool" is "op \" parametric member_transfer . -lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer - by (rule countable_empty) lift_definition cinsert :: "'a \ 'a cset \ 'a cset" is insert parametric Lifting_Set.insert_transfer by (rule countable_insert) -lift_definition csingle :: "'a \ 'a cset" is "\x. {x}" - by (rule countable_insert[OF countable_empty]) -lift_definition cUn :: "'a cset \ 'a cset \ 'a cset" is "op \" parametric union_transfer - by (rule countable_Un) -lift_definition cInt :: "'a cset \ 'a cset \ 'a cset" is "op \" parametric inter_transfer - by (rule countable_Int1) -lift_definition cDiff :: "'a cset \ 'a cset \ 'a cset" is "op -" parametric Diff_transfer - by (rule countable_Diff) +abbreviation csingle :: "'a \ 'a cset" where "csingle x \ cinsert x cempty" lift_definition cimage :: "('a \ 'b) \ 'a cset \ 'b cset" is "op `" parametric image_transfer by (rule countable_image) +lift_definition cBall :: "'a cset \ ('a \ bool) \ bool" is Ball parametric Ball_transfer . +lift_definition cBex :: "'a cset \ ('a \ bool) \ bool" is Bex parametric Bex_transfer . +lift_definition cUNION :: "'a cset \ ('a \ 'b cset) \ 'b cset" + is "UNION" parametric UNION_transfer by simp +definition cUnion :: "'a cset cset \ 'a cset" where "cUnion A = cUNION A id" + +lemma Union_conv_UNION: "Union A = UNION A id" +by auto + +lemma cUnion_transfer [transfer_rule]: + "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) Union cUnion" +unfolding cUnion_def[abs_def] Union_conv_UNION[abs_def] by transfer_prover + +lemmas cset_eqI = set_eqI[Transfer.transferred] +lemmas cset_eq_iff[no_atp] = set_eq_iff[Transfer.transferred] +lemmas cBallI[intro!] = ballI[Transfer.transferred] +lemmas cbspec[dest?] = bspec[Transfer.transferred] +lemmas cBallE[elim] = ballE[Transfer.transferred] +lemmas cBexI[intro] = bexI[Transfer.transferred] +lemmas rev_cBexI[intro?] = rev_bexI[Transfer.transferred] +lemmas cBexCI = bexCI[Transfer.transferred] +lemmas cBexE[elim!] = bexE[Transfer.transferred] +lemmas cBall_triv[simp] = ball_triv[Transfer.transferred] +lemmas cBex_triv[simp] = bex_triv[Transfer.transferred] +lemmas cBex_triv_one_point1[simp] = bex_triv_one_point1[Transfer.transferred] +lemmas cBex_triv_one_point2[simp] = bex_triv_one_point2[Transfer.transferred] +lemmas cBex_one_point1[simp] = bex_one_point1[Transfer.transferred] +lemmas cBex_one_point2[simp] = bex_one_point2[Transfer.transferred] +lemmas cBall_one_point1[simp] = ball_one_point1[Transfer.transferred] +lemmas cBall_one_point2[simp] = ball_one_point2[Transfer.transferred] +lemmas cBall_conj_distrib = ball_conj_distrib[Transfer.transferred] +lemmas cBex_disj_distrib = bex_disj_distrib[Transfer.transferred] +lemmas cBall_cong = ball_cong[Transfer.transferred] +lemmas cBex_cong = bex_cong[Transfer.transferred] +lemmas csubsetI[intro!] = subsetI[Transfer.transferred] +lemmas csubsetD[elim, intro?] = subsetD[Transfer.transferred] +lemmas rev_csubsetD[no_atp,intro?] = rev_subsetD[Transfer.transferred] +lemmas csubsetCE[no_atp,elim] = subsetCE[Transfer.transferred] +lemmas csubset_eq[no_atp] = subset_eq[Transfer.transferred] +lemmas contra_csubsetD[no_atp] = contra_subsetD[Transfer.transferred] +lemmas csubset_refl = subset_refl[Transfer.transferred] +lemmas csubset_trans = subset_trans[Transfer.transferred] +lemmas cset_rev_mp = set_rev_mp[Transfer.transferred] +lemmas cset_mp = set_mp[Transfer.transferred] +lemmas csubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred] +lemmas eq_cmem_trans = eq_mem_trans[Transfer.transferred] +lemmas csubset_antisym[intro!] = subset_antisym[Transfer.transferred] +lemmas cequalityD1 = equalityD1[Transfer.transferred] +lemmas cequalityD2 = equalityD2[Transfer.transferred] +lemmas cequalityE = equalityE[Transfer.transferred] +lemmas cequalityCE[elim] = equalityCE[Transfer.transferred] +lemmas eqcset_imp_iff = eqset_imp_iff[Transfer.transferred] +lemmas eqcelem_imp_iff = eqelem_imp_iff[Transfer.transferred] +lemmas cempty_iff[simp] = empty_iff[Transfer.transferred] +lemmas cempty_fsubsetI[iff] = empty_subsetI[Transfer.transferred] +lemmas equals_cemptyI = equals0I[Transfer.transferred] +lemmas equals_cemptyD = equals0D[Transfer.transferred] +lemmas cBall_cempty[simp] = ball_empty[Transfer.transferred] +lemmas cBex_cempty[simp] = bex_empty[Transfer.transferred] +lemmas cInt_iff[simp] = Int_iff[Transfer.transferred] +lemmas cIntI[intro!] = IntI[Transfer.transferred] +lemmas cIntD1 = IntD1[Transfer.transferred] +lemmas cIntD2 = IntD2[Transfer.transferred] +lemmas cIntE[elim!] = IntE[Transfer.transferred] +lemmas cUn_iff[simp] = Un_iff[Transfer.transferred] +lemmas cUnI1[elim?] = UnI1[Transfer.transferred] +lemmas cUnI2[elim?] = UnI2[Transfer.transferred] +lemmas cUnCI[intro!] = UnCI[Transfer.transferred] +lemmas cuUnE[elim!] = UnE[Transfer.transferred] +lemmas cDiff_iff[simp] = Diff_iff[Transfer.transferred] +lemmas cDiffI[intro!] = DiffI[Transfer.transferred] +lemmas cDiffD1 = DiffD1[Transfer.transferred] +lemmas cDiffD2 = DiffD2[Transfer.transferred] +lemmas cDiffE[elim!] = DiffE[Transfer.transferred] +lemmas cinsert_iff[simp] = insert_iff[Transfer.transferred] +lemmas cinsertI1 = insertI1[Transfer.transferred] +lemmas cinsertI2 = insertI2[Transfer.transferred] +lemmas cinsertE[elim!] = insertE[Transfer.transferred] +lemmas cinsertCI[intro!] = insertCI[Transfer.transferred] +lemmas csubset_cinsert_iff = subset_insert_iff[Transfer.transferred] +lemmas cinsert_ident = insert_ident[Transfer.transferred] +lemmas csingletonI[intro!,no_atp] = singletonI[Transfer.transferred] +lemmas csingletonD[dest!,no_atp] = singletonD[Transfer.transferred] +lemmas fsingletonE = csingletonD [elim_format] +lemmas csingleton_iff = singleton_iff[Transfer.transferred] +lemmas csingleton_inject[dest!] = singleton_inject[Transfer.transferred] +lemmas csingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred] +lemmas csingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred] +lemmas csubset_csingletonD = subset_singletonD[Transfer.transferred] +lemmas cDiff_single_cinsert = diff_single_insert[Transfer.transferred] +lemmas cdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred] +lemmas cUn_csingleton_iff = Un_singleton_iff[Transfer.transferred] +lemmas csingleton_cUn_iff = singleton_Un_iff[Transfer.transferred] +lemmas cimage_eqI[simp, intro] = image_eqI[Transfer.transferred] +lemmas cimageI = imageI[Transfer.transferred] +lemmas rev_cimage_eqI = rev_image_eqI[Transfer.transferred] +lemmas cimageE[elim!] = imageE[Transfer.transferred] +lemmas Compr_cimage_eq = Compr_image_eq[Transfer.transferred] +lemmas cimage_cUn = image_Un[Transfer.transferred] +lemmas cimage_iff = image_iff[Transfer.transferred] +lemmas cimage_csubset_iff[no_atp] = image_subset_iff[Transfer.transferred] +lemmas cimage_csubsetI = image_subsetI[Transfer.transferred] +lemmas cimage_ident[simp] = image_ident[Transfer.transferred] +lemmas split_if_cin1 = split_if_mem1[Transfer.transferred] +lemmas split_if_cin2 = split_if_mem2[Transfer.transferred] +lemmas cpsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred] +lemmas cpsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred] +lemmas cpsubset_finsert_iff = psubset_insert_iff[Transfer.transferred] +lemmas cpsubset_eq = psubset_eq[Transfer.transferred] +lemmas cpsubset_imp_fsubset = psubset_imp_subset[Transfer.transferred] +lemmas cpsubset_trans = psubset_trans[Transfer.transferred] +lemmas cpsubsetD = psubsetD[Transfer.transferred] +lemmas cpsubset_csubset_trans = psubset_subset_trans[Transfer.transferred] +lemmas csubset_cpsubset_trans = subset_psubset_trans[Transfer.transferred] +lemmas cpsubset_imp_ex_fmem = psubset_imp_ex_mem[Transfer.transferred] +lemmas csubset_cinsertI = subset_insertI[Transfer.transferred] +lemmas csubset_cinsertI2 = subset_insertI2[Transfer.transferred] +lemmas csubset_cinsert = subset_insert[Transfer.transferred] +lemmas cUn_upper1 = Un_upper1[Transfer.transferred] +lemmas cUn_upper2 = Un_upper2[Transfer.transferred] +lemmas cUn_least = Un_least[Transfer.transferred] +lemmas cInt_lower1 = Int_lower1[Transfer.transferred] +lemmas cInt_lower2 = Int_lower2[Transfer.transferred] +lemmas cInt_greatest = Int_greatest[Transfer.transferred] +lemmas cDiff_csubset = Diff_subset[Transfer.transferred] +lemmas cDiff_csubset_conv = Diff_subset_conv[Transfer.transferred] +lemmas csubset_cempty[simp] = subset_empty[Transfer.transferred] +lemmas not_cpsubset_cempty[iff] = not_psubset_empty[Transfer.transferred] +lemmas cinsert_is_cUn = insert_is_Un[Transfer.transferred] +lemmas cinsert_not_cempty[simp] = insert_not_empty[Transfer.transferred] +lemmas cempty_not_cinsert = empty_not_insert[Transfer.transferred] +lemmas cinsert_absorb = insert_absorb[Transfer.transferred] +lemmas cinsert_absorb2[simp] = insert_absorb2[Transfer.transferred] +lemmas cinsert_commute = insert_commute[Transfer.transferred] +lemmas cinsert_csubset[simp] = insert_subset[Transfer.transferred] +lemmas cinsert_cinter_cinsert[simp] = insert_inter_insert[Transfer.transferred] +lemmas cinsert_disjoint[simp,no_atp] = insert_disjoint[Transfer.transferred] +lemmas disjoint_cinsert[simp,no_atp] = disjoint_insert[Transfer.transferred] +lemmas cimage_cempty[simp] = image_empty[Transfer.transferred] +lemmas cimage_cinsert[simp] = image_insert[Transfer.transferred] +lemmas cimage_constant = image_constant[Transfer.transferred] +lemmas cimage_constant_conv = image_constant_conv[Transfer.transferred] +lemmas cimage_cimage = image_image[Transfer.transferred] +lemmas cinsert_cimage[simp] = insert_image[Transfer.transferred] +lemmas cimage_is_cempty[iff] = image_is_empty[Transfer.transferred] +lemmas cempty_is_cimage[iff] = empty_is_image[Transfer.transferred] +lemmas cimage_cong = image_cong[Transfer.transferred] +lemmas cimage_cInt_csubset = image_Int_subset[Transfer.transferred] +lemmas cimage_cDiff_csubset = image_diff_subset[Transfer.transferred] +lemmas cInt_absorb = Int_absorb[Transfer.transferred] +lemmas cInt_left_absorb = Int_left_absorb[Transfer.transferred] +lemmas cInt_commute = Int_commute[Transfer.transferred] +lemmas cInt_left_commute = Int_left_commute[Transfer.transferred] +lemmas cInt_assoc = Int_assoc[Transfer.transferred] +lemmas cInt_ac = Int_ac[Transfer.transferred] +lemmas cInt_absorb1 = Int_absorb1[Transfer.transferred] +lemmas cInt_absorb2 = Int_absorb2[Transfer.transferred] +lemmas cInt_cempty_left = Int_empty_left[Transfer.transferred] +lemmas cInt_cempty_right = Int_empty_right[Transfer.transferred] +lemmas disjoint_iff_cnot_equal = disjoint_iff_not_equal[Transfer.transferred] +lemmas cInt_cUn_distrib = Int_Un_distrib[Transfer.transferred] +lemmas cInt_cUn_distrib2 = Int_Un_distrib2[Transfer.transferred] +lemmas cInt_csubset_iff[no_atp, simp] = Int_subset_iff[Transfer.transferred] +lemmas cUn_absorb = Un_absorb[Transfer.transferred] +lemmas cUn_left_absorb = Un_left_absorb[Transfer.transferred] +lemmas cUn_commute = Un_commute[Transfer.transferred] +lemmas cUn_left_commute = Un_left_commute[Transfer.transferred] +lemmas cUn_assoc = Un_assoc[Transfer.transferred] +lemmas cUn_ac = Un_ac[Transfer.transferred] +lemmas cUn_absorb1 = Un_absorb1[Transfer.transferred] +lemmas cUn_absorb2 = Un_absorb2[Transfer.transferred] +lemmas cUn_cempty_left = Un_empty_left[Transfer.transferred] +lemmas cUn_cempty_right = Un_empty_right[Transfer.transferred] +lemmas cUn_cinsert_left[simp] = Un_insert_left[Transfer.transferred] +lemmas cUn_cinsert_right[simp] = Un_insert_right[Transfer.transferred] +lemmas cInt_cinsert_left = Int_insert_left[Transfer.transferred] +lemmas cInt_cinsert_left_ifffempty[simp] = Int_insert_left_if0[Transfer.transferred] +lemmas cInt_cinsert_left_if1[simp] = Int_insert_left_if1[Transfer.transferred] +lemmas cInt_cinsert_right = Int_insert_right[Transfer.transferred] +lemmas cInt_cinsert_right_ifffempty[simp] = Int_insert_right_if0[Transfer.transferred] +lemmas cInt_cinsert_right_if1[simp] = Int_insert_right_if1[Transfer.transferred] +lemmas cUn_cInt_distrib = Un_Int_distrib[Transfer.transferred] +lemmas cUn_cInt_distrib2 = Un_Int_distrib2[Transfer.transferred] +lemmas cUn_cInt_crazy = Un_Int_crazy[Transfer.transferred] +lemmas csubset_cUn_eq = subset_Un_eq[Transfer.transferred] +lemmas cUn_cempty[iff] = Un_empty[Transfer.transferred] +lemmas cUn_csubset_iff[no_atp, simp] = Un_subset_iff[Transfer.transferred] +lemmas cUn_cDiff_cInt = Un_Diff_Int[Transfer.transferred] +lemmas cDiff_cInt2 = Diff_Int2[Transfer.transferred] +lemmas cUn_cInt_assoc_eq = Un_Int_assoc_eq[Transfer.transferred] +lemmas cBall_cUn = ball_Un[Transfer.transferred] +lemmas cBex_cUn = bex_Un[Transfer.transferred] +lemmas cDiff_eq_cempty_iff[simp,no_atp] = Diff_eq_empty_iff[Transfer.transferred] +lemmas cDiff_cancel[simp] = Diff_cancel[Transfer.transferred] +lemmas cDiff_idemp[simp] = Diff_idemp[Transfer.transferred] +lemmas cDiff_triv = Diff_triv[Transfer.transferred] +lemmas cempty_cDiff[simp] = empty_Diff[Transfer.transferred] +lemmas cDiff_cempty[simp] = Diff_empty[Transfer.transferred] +lemmas cDiff_cinsert0[simp,no_atp] = Diff_insert0[Transfer.transferred] +lemmas cDiff_cinsert = Diff_insert[Transfer.transferred] +lemmas cDiff_cinsert2 = Diff_insert2[Transfer.transferred] +lemmas cinsert_cDiff_if = insert_Diff_if[Transfer.transferred] +lemmas cinsert_cDiff1[simp] = insert_Diff1[Transfer.transferred] +lemmas cinsert_cDiff_single[simp] = insert_Diff_single[Transfer.transferred] +lemmas cinsert_cDiff = insert_Diff[Transfer.transferred] +lemmas cDiff_cinsert_absorb = Diff_insert_absorb[Transfer.transferred] +lemmas cDiff_disjoint[simp] = Diff_disjoint[Transfer.transferred] +lemmas cDiff_partition = Diff_partition[Transfer.transferred] +lemmas double_cDiff = double_diff[Transfer.transferred] +lemmas cUn_cDiff_cancel[simp] = Un_Diff_cancel[Transfer.transferred] +lemmas cUn_cDiff_cancel2[simp] = Un_Diff_cancel2[Transfer.transferred] +lemmas cDiff_cUn = Diff_Un[Transfer.transferred] +lemmas cDiff_cInt = Diff_Int[Transfer.transferred] +lemmas cUn_cDiff = Un_Diff[Transfer.transferred] +lemmas cInt_cDiff = Int_Diff[Transfer.transferred] +lemmas cDiff_cInt_distrib = Diff_Int_distrib[Transfer.transferred] +lemmas cDiff_cInt_distrib2 = Diff_Int_distrib2[Transfer.transferred] +lemmas cset_eq_csubset = set_eq_subset[Transfer.transferred] +lemmas csubset_iff[no_atp] = subset_iff[Transfer.transferred] +lemmas csubset_iff_pfsubset_eq = subset_iff_psubset_eq[Transfer.transferred] +lemmas all_not_cin_conv[simp] = all_not_in_conv[Transfer.transferred] +lemmas ex_cin_conv = ex_in_conv[Transfer.transferred] +lemmas cimage_mono = image_mono[Transfer.transferred] +lemmas cinsert_mono = insert_mono[Transfer.transferred] +lemmas cunion_mono = Un_mono[Transfer.transferred] +lemmas cinter_mono = Int_mono[Transfer.transferred] +lemmas cminus_mono = Diff_mono[Transfer.transferred] +lemmas cin_mono = in_mono[Transfer.transferred] +lemmas cLeast_mono = Least_mono[Transfer.transferred] +lemmas cequalityI = equalityI[Transfer.transferred] + + +subsection {* Additional lemmas*} + +subsubsection {* @{text femepty} *} + +lemma cemptyE [elim!]: "cin a cempty \ P" by simp + +subsubsection {* @{text finsert} *} + +lemma countable_insert_iff: "countable (insert x A) \ countable A" +by (metis Diff_eq_empty_iff countable_empty countable_insert subset_insertI uncountable_minus_countable) + +lemma set_cinsert: + assumes "cin x A" + obtains B where "A = cinsert x B" and "\ cin x B" +using assms by transfer(erule Set.set_insert, simp add: countable_insert_iff) + +lemma mk_disjoint_cinsert: "cin a A \ \B. A = cinsert a B \ \ cin a B" + by (rule exI[where x = "cDiff A (csingle a)"]) blast + +subsubsection {* @{text cimage} *} + +lemma subset_cimage_iff: "csubset_eq B (cimage f A) \ (\AA. csubset_eq AA A \ B = cimage f AA)" +by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE) + +subsubsection {* bounded quantification *} + +lemma cBex_simps [simp, no_atp]: + "\A P Q. cBex A (\x. P x \ Q) = (cBex A P \ Q)" + "\A P Q. cBex A (\x. P \ Q x) = (P \ cBex A Q)" + "\P. cBex cempty P = False" + "\a B P. cBex (cinsert a B) P = (P a \ cBex B P)" + "\A P f. cBex (cimage f A) P = cBex A (\x. P (f x))" + "\A P. (\ cBex A P) = cBall A (\x. \ P x)" +by auto + +lemma cBall_simps [simp, no_atp]: + "\A P Q. cBall A (\x. P x \ Q) = (cBall A P \ Q)" + "\A P Q. cBall A (\x. P \ Q x) = (P \ cBall A Q)" + "\A P Q. cBall A (\x. P \ Q x) = (P \ cBall A Q)" + "\A P Q. cBall A (\x. P x \ Q) = (cBex A P \ Q)" + "\P. cBall cempty P = True" + "\a B P. cBall (cinsert a B) P = (P a \ cBall B P)" + "\A P f. cBall (cimage f A) P = cBall A (\x. P (f x))" + "\A P. (\ cBall A P) = cBex A (\x. \ P x)" +by auto + +lemma atomize_cBall: + "(\x. cin x A ==> P x) == Trueprop (cBall A (\x. P x))" +apply (simp only: atomize_all atomize_imp) +apply (rule equal_intr_rule) +by (transfer, simp)+ + + +subsection {* Setup for Lifting/Transfer *} + +subsubsection {* Relator and predicator properties *} + +lift_definition rel_cset :: "('a \ 'b \ bool) \ 'a cset \ 'b cset \ bool" + is rel_set parametric rel_set_transfer . + +lemma rel_cset_alt_def: + "rel_cset R a b \ + (\t \ rcset a. \u \ rcset b. R t u) \ + (\t \ rcset b. \u \ rcset a. R u t)" +by(simp add: rel_cset_def rel_set_def) + +lemma rel_cset_iff: + "rel_cset R a b \ + (\t. cin t a \ (\u. cin u b \ R t u)) \ + (\t. cin t b \ (\u. cin u a \ R u t))" +by transfer(auto simp add: rel_set_def) + +subsubsection {* Transfer rules for the Transfer package *} + +text {* Unconditional transfer rules *} + +context begin interpretation lifting_syntax . + +lemmas cempty_parametric [transfer_rule] = empty_transfer[Transfer.transferred] + +lemma cinsert_parametric [transfer_rule]: + "(A ===> rel_cset A ===> rel_cset A) cinsert cinsert" + unfolding rel_fun_def rel_cset_iff by blast + +lemma cUn_parametric [transfer_rule]: + "(rel_cset A ===> rel_cset A ===> rel_cset A) cUn cUn" + unfolding rel_fun_def rel_cset_iff by blast + +lemma cUnion_parametric [transfer_rule]: + "(rel_cset (rel_cset A) ===> rel_cset A) cUnion cUnion" + unfolding rel_fun_def by transfer(simp, fast dest: rel_setD1 rel_setD2 intro!: rel_setI) + +lemma cimage_parametric [transfer_rule]: + "((A ===> B) ===> rel_cset A ===> rel_cset B) cimage cimage" + unfolding rel_fun_def rel_cset_iff by blast + +lemma cBall_parametric [transfer_rule]: + "(rel_cset A ===> (A ===> op =) ===> op =) cBall cBall" + unfolding rel_cset_iff rel_fun_def by blast + +lemma cBex_parametric [transfer_rule]: + "(rel_cset A ===> (A ===> op =) ===> op =) cBex cBex" + unfolding rel_cset_iff rel_fun_def by blast + +lemma rel_cset_parametric [transfer_rule]: + "((A ===> B ===> op =) ===> rel_cset A ===> rel_cset B ===> op =) rel_cset rel_cset" + unfolding rel_fun_def + using rel_set_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred, where A = A and B = B] + by simp + +text {* Rules requiring bi-unique, bi-total or right-total relations *} + +lemma cin_parametric [transfer_rule]: + "bi_unique A \ (A ===> rel_cset A ===> op =) cin cin" +unfolding rel_fun_def rel_cset_iff bi_unique_def by metis + +lemma cInt_parametric [transfer_rule]: + "bi_unique A \ (rel_cset A ===> rel_cset A ===> rel_cset A) cInt cInt" +unfolding rel_fun_def +using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] +by blast + +lemma cDiff_parametric [transfer_rule]: + "bi_unique A \ (rel_cset A ===> rel_cset A ===> rel_cset A) cDiff cDiff" +unfolding rel_fun_def +using Diff_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast + +lemma csubset_parametric [transfer_rule]: + "bi_unique A \ (rel_cset A ===> rel_cset A ===> op =) csubset_eq csubset_eq" +unfolding rel_fun_def +using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast + +end + +lifting_update cset.lifting +lifting_forget cset.lifting subsection {* Registration as BNF *} @@ -115,39 +510,34 @@ by (erule finite_Collect_subsets) lemma rcset_to_rcset: "countable A \ rcset (the_inv rcset A) = A" + including cset.lifting apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff]) apply transfer' apply simp apply transfer' apply simp done -lemma Collect_Int_Times: -"{(x, y). R x y} \ A \ B = {(x, y). R x y \ x \ A \ y \ B}" +lemma Collect_Int_Times: "{(x, y). R x y} \ A \ B = {(x, y). R x y \ x \ A \ y \ B}" by auto -definition rel_cset :: "('a \ 'b \ bool) \ 'a cset \ 'b cset \ bool" where -"rel_cset R a b \ - (\t \ rcset a. \u \ rcset b. R t u) \ - (\t \ rcset b. \u \ rcset a. R u t)" lemma rel_cset_aux: "(\t \ rcset a. \u \ rcset b. R t u) \ (\t \ rcset b. \u \ rcset a. R u t) \ - ((Grp {x. rcset x \ {(a, b). R a b}} (cimage fst))\\ OO - Grp {x. rcset x \ {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R") + ((BNF_Def.Grp {x. rcset x \ {(a, b). R a b}} (cimage fst))\\ OO + BNF_Def.Grp {x. rcset x \ {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R") proof assume ?L def R' \ "the_inv rcset (Collect (split R) \ (rcset a \ rcset b))" (is "the_inv rcset ?L'") have L: "countable ?L'" by auto hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset) - thus ?R unfolding Grp_def relcompp.simps conversep.simps + thus ?R unfolding Grp_def relcompp.simps conversep.simps including cset.lifting proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times) - next from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times) qed simp_all next assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps - by transfer force + by (simp add: subset_eq Ball_def)(transfer, auto simp add: cimage.rep_eq, metis snd_conv, metis fst_conv) qed bnf "'a cset" @@ -157,30 +547,31 @@ wits: "cempty" rel: rel_cset proof - - show "cimage id = id" by transfer' simp + show "cimage id = id" by auto next - fix f g show "cimage (g \ f) = cimage g \ cimage f" by transfer' fastforce + fix f g show "cimage (g \ f) = cimage g \ cimage f" by fastforce next fix C f g assume eq: "\a. a \ rcset C \ f a = g a" - thus "cimage f C = cimage g C" by transfer force + thus "cimage f C = cimage g C" including cset.lifting by transfer force next - fix f show "rcset \ cimage f = op ` f \ rcset" by transfer' fastforce + fix f show "rcset \ cimage f = op ` f \ rcset" including cset.lifting by transfer' fastforce next show "card_order natLeq" by (rule natLeq_card_order) next show "cinfinite natLeq" by (rule natLeq_cinfinite) next - fix C show "|rcset C| \o natLeq" by transfer (unfold countable_card_le_natLeq) + fix C show "|rcset C| \o natLeq" + including cset.lifting by transfer (unfold countable_card_le_natLeq) next fix R S show "rel_cset R OO rel_cset S \ rel_cset (R OO S)" - unfolding rel_cset_def[abs_def] by fast + unfolding rel_cset_alt_def[abs_def] by fast next fix R show "rel_cset R = - (Grp {x. rcset x \ Collect (split R)} (cimage fst))\\ OO - Grp {x. rcset x \ Collect (split R)} (cimage snd)" - unfolding rel_cset_def[abs_def] rel_cset_aux by simp -qed (transfer, simp) + (BNF_Def.Grp {x. rcset x \ Collect (split R)} (cimage fst))\\ OO + BNF_Def.Grp {x. rcset x \ Collect (split R)} (cimage snd)" + unfolding rel_cset_alt_def[abs_def] rel_cset_aux by simp +qed(simp add: bot_cset.rep_eq) end