src/HOL/Library/FSet.thy
 changeset 55938 f20d1db5aa3c parent 55933 12ee2c407dad child 55943 5c2df04e97d1
```     1.1 --- a/src/HOL/Library/FSet.thy	Thu Mar 06 14:25:55 2014 +0100
1.2 +++ b/src/HOL/Library/FSet.thy	Thu Mar 06 14:57:14 2014 +0100
1.3 @@ -78,14 +78,14 @@
1.4
1.5  lemma right_total_Inf_fset_transfer:
1.6    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
1.7 -  shows "(set_rel (set_rel A) ===> set_rel A)
1.8 +  shows "(rel_set (rel_set A) ===> rel_set A)
1.9      (\<lambda>S. if finite (Inter S \<inter> Collect (Domainp A)) then Inter S \<inter> Collect (Domainp A) else {})
1.10        (\<lambda>S. if finite (Inf S) then Inf S else {})"
1.11      by transfer_prover
1.12
1.13  lemma Inf_fset_transfer:
1.14    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
1.15 -  shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>A. if finite (Inf A) then Inf A else {})
1.16 +  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Inf A) then Inf A else {})
1.17      (\<lambda>A. if finite (Inf A) then Inf A else {})"
1.18    by transfer_prover
1.19
1.20 @@ -94,7 +94,7 @@
1.21
1.22  lemma Sup_fset_transfer:
1.23    assumes [transfer_rule]: "bi_unique A"
1.24 -  shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>A. if finite (Sup A) then Sup A else {})
1.25 +  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Sup A) then Sup A else {})
1.26    (\<lambda>A. if finite (Sup A) then Sup A else {})" by transfer_prover
1.27
1.28  lift_definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Sup A) then Sup A else {}"
1.29 @@ -103,7 +103,7 @@
1.30  lemma finite_Sup: "\<exists>z. finite z \<and> (\<forall>a. a \<in> X \<longrightarrow> a \<le> z) \<Longrightarrow> finite (Sup X)"
1.31  by (auto intro: finite_subset)
1.32
1.33 -lemma transfer_bdd_below[transfer_rule]: "(set_rel (pcr_fset op =) ===> op =) bdd_below bdd_below"
1.34 +lemma transfer_bdd_below[transfer_rule]: "(rel_set (pcr_fset op =) ===> op =) bdd_below bdd_below"
1.35    by auto
1.36
1.37  instance
1.38 @@ -762,53 +762,53 @@
1.39
1.40  subsubsection {* Relator and predicator properties *}
1.41
1.42 -lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is set_rel
1.43 -parametric set_rel_transfer .
1.44 +lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is rel_set
1.45 +parametric rel_set_transfer .
1.46
1.47  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)
1.48    \<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
1.49  apply (rule ext)+
1.50  apply transfer'
1.51 -apply (subst set_rel_def[unfolded fun_eq_iff])
1.52 +apply (subst rel_set_def[unfolded fun_eq_iff])
1.53  by blast
1.54
1.55  lemma rel_fset_conversep: "rel_fset (conversep R) = conversep (rel_fset R)"
1.56    unfolding rel_fset_alt_def by auto
1.57
1.58 -lemmas rel_fset_eq [relator_eq] = set_rel_eq[Transfer.transferred]
1.59 +lemmas rel_fset_eq [relator_eq] = rel_set_eq[Transfer.transferred]
1.60
1.61  lemma rel_fset_mono[relator_mono]: "A \<le> B \<Longrightarrow> rel_fset A \<le> rel_fset B"
1.62  unfolding rel_fset_alt_def by blast
1.63
1.64 -lemma finite_set_rel:
1.65 +lemma finite_rel_set:
1.66    assumes fin: "finite X" "finite Z"
1.67 -  assumes R_S: "set_rel (R OO S) X Z"
1.68 -  shows "\<exists>Y. finite Y \<and> set_rel R X Y \<and> set_rel S Y Z"
1.69 +  assumes R_S: "rel_set (R OO S) X Z"
1.70 +  shows "\<exists>Y. finite Y \<and> rel_set R X Y \<and> rel_set S Y Z"
1.71  proof -
1.72    obtain f where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)"
1.73    apply atomize_elim
1.74    apply (subst bchoice_iff[symmetric])
1.75 -  using R_S[unfolded set_rel_def OO_def] by blast
1.76 +  using R_S[unfolded rel_set_def OO_def] by blast
1.77
1.78    obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R  x (g z))"
1.79    apply atomize_elim
1.80    apply (subst bchoice_iff[symmetric])
1.81 -  using R_S[unfolded set_rel_def OO_def] by blast
1.82 +  using R_S[unfolded rel_set_def OO_def] by blast
1.83
1.84    let ?Y = "f ` X \<union> g ` Z"
1.85    have "finite ?Y" by (simp add: fin)
1.86 -  moreover have "set_rel R X ?Y"
1.87 -    unfolding set_rel_def
1.88 +  moreover have "rel_set R X ?Y"
1.89 +    unfolding rel_set_def
1.90      using f g by clarsimp blast
1.91 -  moreover have "set_rel S ?Y Z"
1.92 -    unfolding set_rel_def
1.93 +  moreover have "rel_set S ?Y Z"
1.94 +    unfolding rel_set_def
1.95      using f g by clarsimp blast
1.96    ultimately show ?thesis by metis
1.97  qed
1.98
1.99  lemma rel_fset_OO[relator_distr]: "rel_fset R OO rel_fset S = rel_fset (R OO S)"
1.100  apply (rule ext)+
1.101 -by transfer (auto intro: finite_set_rel set_rel_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
1.102 +by transfer (auto intro: finite_rel_set rel_set_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
1.103
1.104  lemma Domainp_fset[relator_domain]:
1.105    assumes "Domainp T = P"
1.106 @@ -832,7 +832,7 @@
1.107  apply (subst(asm) choice_iff)
1.108  apply clarsimp
1.109  apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
1.110 -by (auto simp add: set_rel_def)
1.111 +by (auto simp add: rel_set_def)
1.112
1.113  lemma left_total_rel_fset[reflexivity_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
1.114  unfolding left_total_def
1.115 @@ -840,10 +840,10 @@
1.116  apply (subst(asm) choice_iff)
1.117  apply clarsimp
1.118  apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
1.119 -by (auto simp add: set_rel_def)
1.120 +by (auto simp add: rel_set_def)
1.121
1.122 -lemmas right_unique_rel_fset[transfer_rule] = right_unique_set_rel[Transfer.transferred]
1.123 -lemmas left_unique_rel_fset[reflexivity_rule] = left_unique_set_rel[Transfer.transferred]
1.124 +lemmas right_unique_rel_fset[transfer_rule] = right_unique_rel_set[Transfer.transferred]
1.125 +lemmas left_unique_rel_fset[reflexivity_rule] = left_unique_rel_set[Transfer.transferred]
1.126
1.127  thm right_unique_rel_fset left_unique_rel_fset
1.128
1.129 @@ -911,7 +911,7 @@
1.130    "((A ===> B ===> op =) ===> rel_fset A ===> rel_fset B ===> op =)
1.131      rel_fset rel_fset"
1.132    unfolding fun_rel_def
1.133 -  using set_rel_transfer[unfolded fun_rel_def,rule_format, Transfer.transferred, where A = A and B = B]
1.134 +  using rel_set_transfer[unfolded fun_rel_def,rule_format, Transfer.transferred, where A = A and B = B]
1.135    by simp
1.136
1.137  lemma bind_transfer [transfer_rule]:
1.138 @@ -945,7 +945,7 @@
1.139    using subset_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
1.140
1.141  lemma fSup_transfer [transfer_rule]:
1.142 -  "bi_unique A \<Longrightarrow> (set_rel (rel_fset A) ===> rel_fset A) Sup Sup"
1.143 +  "bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup"
1.144    using assms unfolding fun_rel_def
1.145    apply clarify
1.146    apply transfer'
1.147 @@ -955,7 +955,7 @@
1.148
1.149  lemma fInf_transfer [transfer_rule]:
1.150    assumes "bi_unique A" and "bi_total A"
1.151 -  shows "(set_rel (rel_fset A) ===> rel_fset A) Inf Inf"
1.152 +  shows "(rel_set (rel_fset A) ===> rel_fset A) Inf Inf"
1.153    using assms unfolding fun_rel_def
1.154    apply clarify
1.155    apply transfer'
1.156 @@ -986,7 +986,7 @@
1.157
1.158  lemma rel_fset_alt:
1.159    "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)"
1.160 -by transfer (simp add: set_rel_def)
1.161 +by transfer (simp add: rel_set_def)
1.162
1.163  lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
1.164  apply (rule f_the_inv_into_f[unfolded inj_on_def])
1.165 @@ -1037,7 +1037,7 @@
1.166  apply transfer apply simp
1.167  done
1.168
1.169 -lemma rel_fset_fset: "set_rel \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2"
1.170 +lemma rel_fset_fset: "rel_set \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2"
1.171    by transfer (rule refl)
1.172
1.173  end
1.174 @@ -1049,50 +1049,50 @@
1.175
1.176  (* Set vs. sum relators: *)
1.177
1.178 -lemma set_rel_sum_rel[simp]:
1.179 -"set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow>
1.180 - set_rel \<chi> (Inl -` A1) (Inl -` A2) \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
1.181 +lemma rel_set_sum_rel[simp]:
1.182 +"rel_set (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow>
1.183 + rel_set \<chi> (Inl -` A1) (Inl -` A2) \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
1.184  (is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
1.185  proof safe
1.186    assume L: "?L"
1.187 -  show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe
1.188 +  show ?Rl unfolding rel_set_def Bex_def vimage_eq proof safe
1.189      fix l1 assume "Inl l1 \<in> A1"
1.190      then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2"
1.191 -    using L unfolding set_rel_def by auto
1.192 +    using L unfolding rel_set_def by auto
1.193      then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto)
1.194      thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto
1.195    next
1.196      fix l2 assume "Inl l2 \<in> A2"
1.197      then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)"
1.198 -    using L unfolding set_rel_def by auto
1.199 +    using L unfolding rel_set_def by auto
1.200      then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto)
1.201      thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto
1.202    qed
1.203 -  show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe
1.204 +  show ?Rr unfolding rel_set_def Bex_def vimage_eq proof safe
1.205      fix r1 assume "Inr r1 \<in> A1"
1.206      then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2"
1.207 -    using L unfolding set_rel_def by auto
1.208 +    using L unfolding rel_set_def by auto
1.209      then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto)
1.210      thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto
1.211    next
1.212      fix r2 assume "Inr r2 \<in> A2"
1.213      then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)"
1.214 -    using L unfolding set_rel_def by auto
1.215 +    using L unfolding rel_set_def by auto
1.216      then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto)
1.217      thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto
1.218    qed
1.219  next
1.220    assume Rl: "?Rl" and Rr: "?Rr"
1.221 -  show ?L unfolding set_rel_def Bex_def vimage_eq proof safe
1.222 +  show ?L unfolding rel_set_def Bex_def vimage_eq proof safe
1.223      fix a1 assume a1: "a1 \<in> A1"
1.224      show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2"
1.225      proof(cases a1)
1.226        case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2"
1.227 -      using Rl a1 unfolding set_rel_def by blast
1.228 +      using Rl a1 unfolding rel_set_def by blast
1.229        thus ?thesis unfolding Inl by auto
1.230      next
1.231        case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2"
1.232 -      using Rr a1 unfolding set_rel_def by blast
1.233 +      using Rr a1 unfolding rel_set_def by blast
1.234        thus ?thesis unfolding Inr by auto
1.235      qed
1.236    next
1.237 @@ -1100,11 +1100,11 @@
1.238      show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2"
1.239      proof(cases a2)
1.240        case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2"
1.241 -      using Rl a2 unfolding set_rel_def by blast
1.242 +      using Rl a2 unfolding rel_set_def by blast
1.243        thus ?thesis unfolding Inl by auto
1.244      next
1.245        case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2"
1.246 -      using Rr a2 unfolding set_rel_def by blast
1.247 +      using Rr a2 unfolding rel_set_def by blast
1.248        thus ?thesis unfolding Inr by auto
1.249      qed
1.250    qed
```