renamed 'fset_rel' to 'rel_fset'
authorblanchet
Thu Mar 06 13:36:49 2014 +0100 (2014-03-06)
changeset 5593312ee2c407dad
parent 55932 68c5104d2204
child 55934 800e155d051a
renamed 'fset_rel' to 'rel_fset'
NEWS
src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
src/HOL/BNF_Examples/TreeFsetI.thy
src/HOL/Library/FSet.thy
     1.1 --- a/NEWS	Thu Mar 06 13:36:48 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 06 13:36:49 2014 +0100
     1.3 @@ -190,8 +190,10 @@
     1.4      the.simps ~> option.sel
     1.5    INCOMPATIBILITY.
     1.6  
     1.7 -* The following map function has been renamed:
     1.8 +* The following map functions and relators have been renamed:
     1.9      map_sum ~> sum_map
    1.10 +    map_pair ~> prod_map
    1.11 +    fset_rel ~> rel_fset
    1.12  
    1.13  * New theory:
    1.14      Cardinals/Ordinal_Arithmetic.thy
     2.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 13:36:48 2014 +0100
     2.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 13:36:49 2014 +0100
     2.3 @@ -61,8 +61,8 @@
     2.4  by (metis Node_root_cont assms)
     2.5  
     2.6  lemma set_rel_cont:
     2.7 -"set_rel \<chi> (cont tr1) (cont tr2) = fset_rel \<chi> (ccont tr1) (ccont tr2)"
     2.8 -unfolding cont_def comp_def fset_rel_fset ..
     2.9 +"set_rel \<chi> (cont tr1) (cont tr2) = rel_fset \<chi> (ccont tr1) (ccont tr2)"
    2.10 +unfolding cont_def comp_def rel_fset_fset ..
    2.11  
    2.12  lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]:
    2.13  assumes phi: "\<phi> tr1 tr2" and
     3.1 --- a/src/HOL/BNF_Examples/TreeFsetI.thy	Thu Mar 06 13:36:48 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/TreeFsetI.thy	Thu Mar 06 13:36:49 2014 +0100
     3.3 @@ -20,6 +20,6 @@
     3.4  "sub (tmap f t) = fimage (tmap f) (sub t)"
     3.5  
     3.6  lemma "tmap (f o g) x = tmap f (tmap g x)"
     3.7 -  by (coinduction arbitrary: x) (auto simp: fset_rel_alt)
     3.8 +  by (coinduction arbitrary: x) (auto simp: rel_fset_alt)
     3.9  
    3.10  end
     4.1 --- a/src/HOL/Library/FSet.thy	Thu Mar 06 13:36:48 2014 +0100
     4.2 +++ b/src/HOL/Library/FSet.thy	Thu Mar 06 13:36:49 2014 +0100
     4.3 @@ -762,23 +762,23 @@
     4.4  
     4.5  subsubsection {* Relator and predicator properties *}
     4.6  
     4.7 -lift_definition fset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is set_rel
     4.8 +lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is set_rel
     4.9  parametric set_rel_transfer .
    4.10  
    4.11 -lemma fset_rel_alt_def: "fset_rel R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y) 
    4.12 +lemma 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) 
    4.13    \<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
    4.14  apply (rule ext)+
    4.15  apply transfer'
    4.16  apply (subst set_rel_def[unfolded fun_eq_iff]) 
    4.17  by blast
    4.18  
    4.19 -lemma fset_rel_conversep: "fset_rel (conversep R) = conversep (fset_rel R)"
    4.20 -  unfolding fset_rel_alt_def by auto
    4.21 +lemma rel_fset_conversep: "rel_fset (conversep R) = conversep (rel_fset R)"
    4.22 +  unfolding rel_fset_alt_def by auto
    4.23  
    4.24 -lemmas fset_rel_eq [relator_eq] = set_rel_eq[Transfer.transferred]
    4.25 +lemmas rel_fset_eq [relator_eq] = set_rel_eq[Transfer.transferred]
    4.26  
    4.27 -lemma fset_rel_mono[relator_mono]: "A \<le> B \<Longrightarrow> fset_rel A \<le> fset_rel B"
    4.28 -unfolding fset_rel_alt_def by blast
    4.29 +lemma rel_fset_mono[relator_mono]: "A \<le> B \<Longrightarrow> rel_fset A \<le> rel_fset B"
    4.30 +unfolding rel_fset_alt_def by blast
    4.31  
    4.32  lemma finite_set_rel:
    4.33    assumes fin: "finite X" "finite Z"
    4.34 @@ -806,27 +806,27 @@
    4.35    ultimately show ?thesis by metis
    4.36  qed
    4.37  
    4.38 -lemma fset_rel_OO[relator_distr]: "fset_rel R OO fset_rel S = fset_rel (R OO S)"
    4.39 +lemma rel_fset_OO[relator_distr]: "rel_fset R OO rel_fset S = rel_fset (R OO S)"
    4.40  apply (rule ext)+
    4.41  by transfer (auto intro: finite_set_rel set_rel_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
    4.42  
    4.43  lemma Domainp_fset[relator_domain]:
    4.44    assumes "Domainp T = P"
    4.45 -  shows "Domainp (fset_rel T) = (\<lambda>A. fBall A P)"
    4.46 +  shows "Domainp (rel_fset T) = (\<lambda>A. fBall A P)"
    4.47  proof -
    4.48    from assms obtain f where f: "\<forall>x\<in>Collect P. T x (f x)"
    4.49      unfolding Domainp_iff[abs_def]
    4.50      apply atomize_elim
    4.51      by (subst bchoice_iff[symmetric]) auto
    4.52    from assms f show ?thesis
    4.53 -    unfolding fun_eq_iff fset_rel_alt_def Domainp_iff
    4.54 +    unfolding fun_eq_iff rel_fset_alt_def Domainp_iff
    4.55      apply clarify
    4.56      apply (rule iffI)
    4.57        apply blast
    4.58      by (rename_tac A, rule_tac x="f |`| A" in exI, blast)
    4.59  qed
    4.60  
    4.61 -lemma right_total_fset_rel[transfer_rule]: "right_total A \<Longrightarrow> right_total (fset_rel A)"
    4.62 +lemma right_total_rel_fset[transfer_rule]: "right_total A \<Longrightarrow> right_total (rel_fset A)"
    4.63  unfolding right_total_def 
    4.64  apply transfer
    4.65  apply (subst(asm) choice_iff)
    4.66 @@ -834,7 +834,7 @@
    4.67  apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
    4.68  by (auto simp add: set_rel_def)
    4.69  
    4.70 -lemma left_total_fset_rel[reflexivity_rule]: "left_total A \<Longrightarrow> left_total (fset_rel A)"
    4.71 +lemma left_total_rel_fset[reflexivity_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
    4.72  unfolding left_total_def 
    4.73  apply transfer
    4.74  apply (subst(asm) choice_iff)
    4.75 @@ -842,16 +842,16 @@
    4.76  apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
    4.77  by (auto simp add: set_rel_def)
    4.78  
    4.79 -lemmas right_unique_fset_rel[transfer_rule] = right_unique_set_rel[Transfer.transferred]
    4.80 -lemmas left_unique_fset_rel[reflexivity_rule] = left_unique_set_rel[Transfer.transferred]
    4.81 +lemmas right_unique_rel_fset[transfer_rule] = right_unique_set_rel[Transfer.transferred]
    4.82 +lemmas left_unique_rel_fset[reflexivity_rule] = left_unique_set_rel[Transfer.transferred]
    4.83  
    4.84 -thm right_unique_fset_rel left_unique_fset_rel
    4.85 +thm right_unique_rel_fset left_unique_rel_fset
    4.86  
    4.87 -lemma bi_unique_fset_rel[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (fset_rel A)"
    4.88 -by (auto intro: right_unique_fset_rel left_unique_fset_rel iff: bi_unique_iff)
    4.89 +lemma bi_unique_rel_fset[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_fset A)"
    4.90 +by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_iff)
    4.91  
    4.92 -lemma bi_total_fset_rel[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (fset_rel A)"
    4.93 -by (auto intro: right_total_fset_rel left_total_fset_rel iff: bi_total_iff)
    4.94 +lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
    4.95 +by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff)
    4.96  
    4.97  lemmas fset_invariant_commute [invariant_commute] = set_invariant_commute[Transfer.transferred]
    4.98  
    4.99 @@ -860,9 +860,9 @@
   4.100  
   4.101  lemma Quotient_fset_map[quot_map]:
   4.102    assumes "Quotient R Abs Rep T"
   4.103 -  shows "Quotient (fset_rel R) (fimage Abs) (fimage Rep) (fset_rel T)"
   4.104 +  shows "Quotient (rel_fset R) (fimage Abs) (fimage Rep) (rel_fset T)"
   4.105    using assms unfolding Quotient_alt_def4
   4.106 -  by (simp add: fset_rel_OO[symmetric] fset_rel_conversep) (simp add: fset_rel_alt_def, blast)
   4.107 +  by (simp add: rel_fset_OO[symmetric] rel_fset_conversep) (simp add: rel_fset_alt_def, blast)
   4.108  
   4.109  
   4.110  subsubsection {* Transfer rules for the Transfer package *}
   4.111 @@ -877,45 +877,45 @@
   4.112  lemmas fempty_transfer [transfer_rule] = empty_transfer[Transfer.transferred]
   4.113  
   4.114  lemma finsert_transfer [transfer_rule]:
   4.115 -  "(A ===> fset_rel A ===> fset_rel A) finsert finsert"
   4.116 -  unfolding fun_rel_def fset_rel_alt_def by blast
   4.117 +  "(A ===> rel_fset A ===> rel_fset A) finsert finsert"
   4.118 +  unfolding fun_rel_def rel_fset_alt_def by blast
   4.119  
   4.120  lemma funion_transfer [transfer_rule]:
   4.121 -  "(fset_rel A ===> fset_rel A ===> fset_rel A) funion funion"
   4.122 -  unfolding fun_rel_def fset_rel_alt_def by blast
   4.123 +  "(rel_fset A ===> rel_fset A ===> rel_fset A) funion funion"
   4.124 +  unfolding fun_rel_def rel_fset_alt_def by blast
   4.125  
   4.126  lemma ffUnion_transfer [transfer_rule]:
   4.127 -  "(fset_rel (fset_rel A) ===> fset_rel A) ffUnion ffUnion"
   4.128 -  unfolding fun_rel_def fset_rel_alt_def by transfer (simp, fast)
   4.129 +  "(rel_fset (rel_fset A) ===> rel_fset A) ffUnion ffUnion"
   4.130 +  unfolding fun_rel_def rel_fset_alt_def by transfer (simp, fast)
   4.131  
   4.132  lemma fimage_transfer [transfer_rule]:
   4.133 -  "((A ===> B) ===> fset_rel A ===> fset_rel B) fimage fimage"
   4.134 -  unfolding fun_rel_def fset_rel_alt_def by simp blast
   4.135 +  "((A ===> B) ===> rel_fset A ===> rel_fset B) fimage fimage"
   4.136 +  unfolding fun_rel_def rel_fset_alt_def by simp blast
   4.137  
   4.138  lemma fBall_transfer [transfer_rule]:
   4.139 -  "(fset_rel A ===> (A ===> op =) ===> op =) fBall fBall"
   4.140 -  unfolding fset_rel_alt_def fun_rel_def by blast
   4.141 +  "(rel_fset A ===> (A ===> op =) ===> op =) fBall fBall"
   4.142 +  unfolding rel_fset_alt_def fun_rel_def by blast
   4.143  
   4.144  lemma fBex_transfer [transfer_rule]:
   4.145 -  "(fset_rel A ===> (A ===> op =) ===> op =) fBex fBex"
   4.146 -  unfolding fset_rel_alt_def fun_rel_def by blast
   4.147 +  "(rel_fset A ===> (A ===> op =) ===> op =) fBex fBex"
   4.148 +  unfolding rel_fset_alt_def fun_rel_def by blast
   4.149  
   4.150  (* FIXME transfer doesn't work here *)
   4.151  lemma fPow_transfer [transfer_rule]:
   4.152 -  "(fset_rel A ===> fset_rel (fset_rel A)) fPow fPow"
   4.153 +  "(rel_fset A ===> rel_fset (rel_fset A)) fPow fPow"
   4.154    unfolding fun_rel_def
   4.155    using Pow_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred]
   4.156    by blast
   4.157  
   4.158 -lemma fset_rel_transfer [transfer_rule]:
   4.159 -  "((A ===> B ===> op =) ===> fset_rel A ===> fset_rel B ===> op =)
   4.160 -    fset_rel fset_rel"
   4.161 +lemma rel_fset_transfer [transfer_rule]:
   4.162 +  "((A ===> B ===> op =) ===> rel_fset A ===> rel_fset B ===> op =)
   4.163 +    rel_fset rel_fset"
   4.164    unfolding fun_rel_def
   4.165    using set_rel_transfer[unfolded fun_rel_def,rule_format, Transfer.transferred, where A = A and B = B]
   4.166    by simp
   4.167  
   4.168  lemma bind_transfer [transfer_rule]:
   4.169 -  "(fset_rel A ===> (A ===> fset_rel B) ===> fset_rel B) fbind fbind"
   4.170 +  "(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind"
   4.171    using assms unfolding fun_rel_def
   4.172    using bind_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   4.173  
   4.174 @@ -923,29 +923,29 @@
   4.175  
   4.176  lemma fmember_transfer [transfer_rule]:
   4.177    assumes "bi_unique A"
   4.178 -  shows "(A ===> fset_rel A ===> op =) (op |\<in>|) (op |\<in>|)"
   4.179 -  using assms unfolding fun_rel_def fset_rel_alt_def bi_unique_def by metis
   4.180 +  shows "(A ===> rel_fset A ===> op =) (op |\<in>|) (op |\<in>|)"
   4.181 +  using assms unfolding fun_rel_def rel_fset_alt_def bi_unique_def by metis
   4.182  
   4.183  lemma finter_transfer [transfer_rule]:
   4.184    assumes "bi_unique A"
   4.185 -  shows "(fset_rel A ===> fset_rel A ===> fset_rel A) finter finter"
   4.186 +  shows "(rel_fset A ===> rel_fset A ===> rel_fset A) finter finter"
   4.187    using assms unfolding fun_rel_def
   4.188    using inter_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   4.189  
   4.190  lemma fminus_transfer [transfer_rule]:
   4.191    assumes "bi_unique A"
   4.192 -  shows "(fset_rel A ===> fset_rel A ===> fset_rel A) (op |-|) (op |-|)"
   4.193 +  shows "(rel_fset A ===> rel_fset A ===> rel_fset A) (op |-|) (op |-|)"
   4.194    using assms unfolding fun_rel_def
   4.195    using Diff_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   4.196  
   4.197  lemma fsubset_transfer [transfer_rule]:
   4.198    assumes "bi_unique A"
   4.199 -  shows "(fset_rel A ===> fset_rel A ===> op =) (op |\<subseteq>|) (op |\<subseteq>|)"
   4.200 +  shows "(rel_fset A ===> rel_fset A ===> op =) (op |\<subseteq>|) (op |\<subseteq>|)"
   4.201    using assms unfolding fun_rel_def
   4.202    using subset_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   4.203  
   4.204  lemma fSup_transfer [transfer_rule]:
   4.205 -  "bi_unique A \<Longrightarrow> (set_rel (fset_rel A) ===> fset_rel A) Sup Sup"
   4.206 +  "bi_unique A \<Longrightarrow> (set_rel (rel_fset A) ===> rel_fset A) Sup Sup"
   4.207    using assms unfolding fun_rel_def
   4.208    apply clarify
   4.209    apply transfer'
   4.210 @@ -955,7 +955,7 @@
   4.211  
   4.212  lemma fInf_transfer [transfer_rule]:
   4.213    assumes "bi_unique A" and "bi_total A"
   4.214 -  shows "(set_rel (fset_rel A) ===> fset_rel A) Inf Inf"
   4.215 +  shows "(set_rel (rel_fset A) ===> rel_fset A) Inf Inf"
   4.216    using assms unfolding fun_rel_def
   4.217    apply clarify
   4.218    apply transfer'
   4.219 @@ -963,12 +963,12 @@
   4.220  
   4.221  lemma ffilter_transfer [transfer_rule]:
   4.222    assumes "bi_unique A"
   4.223 -  shows "((A ===> op=) ===> fset_rel A ===> fset_rel A) ffilter ffilter"
   4.224 +  shows "((A ===> op=) ===> rel_fset A ===> rel_fset A) ffilter ffilter"
   4.225    using assms unfolding fun_rel_def
   4.226    using Lifting_Set.filter_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   4.227  
   4.228  lemma card_transfer [transfer_rule]:
   4.229 -  "bi_unique A \<Longrightarrow> (fset_rel A ===> op =) fcard fcard"
   4.230 +  "bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard"
   4.231    using assms unfolding fun_rel_def
   4.232    using card_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
   4.233  
   4.234 @@ -984,8 +984,8 @@
   4.235  includes fset.lifting
   4.236  begin
   4.237  
   4.238 -lemma fset_rel_alt:
   4.239 -  "fset_rel 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)"
   4.240 +lemma rel_fset_alt:
   4.241 +  "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)"
   4.242  by transfer (simp add: set_rel_def)
   4.243  
   4.244  lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
   4.245 @@ -994,7 +994,7 @@
   4.246  apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
   4.247  .
   4.248  
   4.249 -lemma fset_rel_aux:
   4.250 +lemma rel_fset_aux:
   4.251  "(\<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>
   4.252   ((BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
   4.253    BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
   4.254 @@ -1023,7 +1023,7 @@
   4.255    sets: fset 
   4.256    bd: natLeq
   4.257    wits: "{||}"
   4.258 -  rel: fset_rel
   4.259 +  rel: rel_fset
   4.260  apply -
   4.261            apply transfer' apply simp
   4.262           apply transfer' apply force
   4.263 @@ -1032,12 +1032,12 @@
   4.264        apply (rule natLeq_card_order)
   4.265       apply (rule natLeq_cinfinite)
   4.266      apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
   4.267 -   apply (fastforce simp: fset_rel_alt)
   4.268 - apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) 
   4.269 +   apply (fastforce simp: rel_fset_alt)
   4.270 + apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt rel_fset_aux) 
   4.271  apply transfer apply simp
   4.272  done
   4.273  
   4.274 -lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
   4.275 +lemma rel_fset_fset: "set_rel \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2"
   4.276    by transfer (rule refl)
   4.277  
   4.278  end