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