author | haftmann |
Wed, 09 Apr 2014 10:04:31 +0200 | |
changeset 56482 | 39ac12b655ab |
parent 56218 | 1c3f1f2431f9 |
child 56518 | beb3b6851665 |
permissions | -rw-r--r-- |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
1 |
(* Title: HOL/Lifting_Set.thy |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
2 |
Author: Brian Huffman and Ondrej Kuncar |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
3 |
*) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
4 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
5 |
header {* Setup for Lifting/Transfer for the set type *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
6 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
7 |
theory Lifting_Set |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
8 |
imports Lifting |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
9 |
begin |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
10 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
11 |
subsection {* Relator and predicator properties *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
12 |
|
55938 | 13 |
definition rel_set :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" |
14 |
where "rel_set R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))" |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
15 |
|
55938 | 16 |
lemma rel_setI: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
17 |
assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
18 |
assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y" |
55938 | 19 |
shows "rel_set R A B" |
20 |
using assms unfolding rel_set_def by simp |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
21 |
|
55938 | 22 |
lemma rel_setD1: "\<lbrakk> rel_set R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y" |
23 |
and rel_setD2: "\<lbrakk> rel_set R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y" |
|
24 |
by(simp_all add: rel_set_def) |
|
53927 | 25 |
|
55938 | 26 |
lemma rel_set_conversep [simp]: "rel_set A\<inverse>\<inverse> = (rel_set A)\<inverse>\<inverse>" |
27 |
unfolding rel_set_def by auto |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
28 |
|
55938 | 29 |
lemma rel_set_eq [relator_eq]: "rel_set (op =) = (op =)" |
30 |
unfolding rel_set_def fun_eq_iff by auto |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
31 |
|
55938 | 32 |
lemma rel_set_mono[relator_mono]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
33 |
assumes "A \<le> B" |
55938 | 34 |
shows "rel_set A \<le> rel_set B" |
35 |
using assms unfolding rel_set_def by blast |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
36 |
|
55938 | 37 |
lemma rel_set_OO[relator_distr]: "rel_set R OO rel_set S = rel_set (R OO S)" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
38 |
apply (rule sym) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
39 |
apply (intro ext, rename_tac X Z) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
40 |
apply (rule iffI) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
41 |
apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI) |
55938 | 42 |
apply (simp add: rel_set_def, fast) |
43 |
apply (simp add: rel_set_def, fast) |
|
44 |
apply (simp add: rel_set_def, fast) |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
45 |
done |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
46 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
47 |
lemma Domainp_set[relator_domain]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
48 |
assumes "Domainp T = R" |
55938 | 49 |
shows "Domainp (rel_set T) = (\<lambda>A. Ball A R)" |
50 |
using assms unfolding rel_set_def Domainp_iff[abs_def] |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
51 |
apply (intro ext) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
52 |
apply (rule iffI) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
53 |
apply blast |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
54 |
apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
55 |
done |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
56 |
|
55938 | 57 |
lemma left_total_rel_set[reflexivity_rule]: |
58 |
"left_total A \<Longrightarrow> left_total (rel_set A)" |
|
59 |
unfolding left_total_def rel_set_def |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
60 |
apply safe |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
61 |
apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
62 |
done |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
63 |
|
55938 | 64 |
lemma left_unique_rel_set[reflexivity_rule]: |
65 |
"left_unique A \<Longrightarrow> left_unique (rel_set A)" |
|
66 |
unfolding left_unique_def rel_set_def |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
67 |
by fast |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
68 |
|
55938 | 69 |
lemma right_total_rel_set [transfer_rule]: |
70 |
"right_total A \<Longrightarrow> right_total (rel_set A)" |
|
71 |
using left_total_rel_set[of "A\<inverse>\<inverse>"] by simp |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
72 |
|
55938 | 73 |
lemma right_unique_rel_set [transfer_rule]: |
74 |
"right_unique A \<Longrightarrow> right_unique (rel_set A)" |
|
75 |
unfolding right_unique_def rel_set_def by fast |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
76 |
|
55938 | 77 |
lemma bi_total_rel_set [transfer_rule]: |
78 |
"bi_total A \<Longrightarrow> bi_total (rel_set A)" |
|
79 |
by(simp add: bi_total_conv_left_right left_total_rel_set right_total_rel_set) |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
80 |
|
55938 | 81 |
lemma bi_unique_rel_set [transfer_rule]: |
82 |
"bi_unique A \<Longrightarrow> bi_unique (rel_set A)" |
|
83 |
unfolding bi_unique_def rel_set_def by fast |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
84 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
85 |
lemma set_invariant_commute [invariant_commute]: |
55938 | 86 |
"rel_set (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)" |
87 |
unfolding fun_eq_iff rel_set_def Lifting.invariant_def Ball_def by fast |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
88 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
89 |
subsection {* Quotient theorem for the Lifting package *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
90 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
91 |
lemma Quotient_set[quot_map]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
92 |
assumes "Quotient R Abs Rep T" |
55938 | 93 |
shows "Quotient (rel_set R) (image Abs) (image Rep) (rel_set T)" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
94 |
using assms unfolding Quotient_alt_def4 |
55938 | 95 |
apply (simp add: rel_set_OO[symmetric]) |
96 |
apply (simp add: rel_set_def, fast) |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
97 |
done |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
98 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
99 |
subsection {* Transfer rules for the Transfer package *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
100 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
101 |
subsubsection {* Unconditional transfer rules *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
102 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
103 |
context |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
104 |
begin |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
105 |
interpretation lifting_syntax . |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
106 |
|
55938 | 107 |
lemma empty_transfer [transfer_rule]: "(rel_set A) {} {}" |
108 |
unfolding rel_set_def by simp |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
109 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
110 |
lemma insert_transfer [transfer_rule]: |
55938 | 111 |
"(A ===> rel_set A ===> rel_set A) insert insert" |
55945 | 112 |
unfolding rel_fun_def rel_set_def by auto |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
113 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
114 |
lemma union_transfer [transfer_rule]: |
55938 | 115 |
"(rel_set A ===> rel_set A ===> rel_set A) union union" |
55945 | 116 |
unfolding rel_fun_def rel_set_def by auto |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
117 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
118 |
lemma Union_transfer [transfer_rule]: |
55938 | 119 |
"(rel_set (rel_set A) ===> rel_set A) Union Union" |
55945 | 120 |
unfolding rel_fun_def rel_set_def by simp fast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
121 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
122 |
lemma image_transfer [transfer_rule]: |
55938 | 123 |
"((A ===> B) ===> rel_set A ===> rel_set B) image image" |
55945 | 124 |
unfolding rel_fun_def rel_set_def by simp fast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
125 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
126 |
lemma UNION_transfer [transfer_rule]: |
55938 | 127 |
"(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION" |
56166 | 128 |
unfolding Union_image_eq [symmetric, abs_def] by transfer_prover |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
129 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
130 |
lemma Ball_transfer [transfer_rule]: |
55938 | 131 |
"(rel_set A ===> (A ===> op =) ===> op =) Ball Ball" |
55945 | 132 |
unfolding rel_set_def rel_fun_def by fast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
133 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
134 |
lemma Bex_transfer [transfer_rule]: |
55938 | 135 |
"(rel_set A ===> (A ===> op =) ===> op =) Bex Bex" |
55945 | 136 |
unfolding rel_set_def rel_fun_def by fast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
137 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
138 |
lemma Pow_transfer [transfer_rule]: |
55938 | 139 |
"(rel_set A ===> rel_set (rel_set A)) Pow Pow" |
55945 | 140 |
apply (rule rel_funI, rename_tac X Y, rule rel_setI) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
141 |
apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp) |
55938 | 142 |
apply (simp add: rel_set_def, fast) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
143 |
apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp) |
55938 | 144 |
apply (simp add: rel_set_def, fast) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
145 |
done |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
146 |
|
55938 | 147 |
lemma rel_set_transfer [transfer_rule]: |
56482
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
148 |
"((A ===> B ===> op =) ===> rel_set A ===> rel_set B ===> op =) rel_set rel_set" |
55945 | 149 |
unfolding rel_fun_def rel_set_def by fast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
150 |
|
53952 | 151 |
lemma bind_transfer [transfer_rule]: |
55938 | 152 |
"(rel_set A ===> (A ===> rel_set B) ===> rel_set B) Set.bind Set.bind" |
56482
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
153 |
unfolding bind_UNION [abs_def] by transfer_prover |
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
154 |
|
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
155 |
lemma INF_parametric [transfer_rule]: |
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
156 |
"(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM" |
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
157 |
unfolding INF_def [abs_def] by transfer_prover |
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
158 |
|
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
159 |
lemma SUP_parametric [transfer_rule]: |
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
160 |
"(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM" |
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
161 |
unfolding SUP_def [abs_def] by transfer_prover |
39ac12b655ab
parametricity transfer rule for INFIMUM, SUPREMUM
haftmann
parents:
56218
diff
changeset
|
162 |
|
53952 | 163 |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
164 |
subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
165 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
166 |
lemma member_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
167 |
assumes "bi_unique A" |
55938 | 168 |
shows "(A ===> rel_set A ===> op =) (op \<in>) (op \<in>)" |
55945 | 169 |
using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
170 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
171 |
lemma right_total_Collect_transfer[transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
172 |
assumes "right_total A" |
55938 | 173 |
shows "((A ===> op =) ===> rel_set A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect" |
55945 | 174 |
using assms unfolding right_total_def rel_set_def rel_fun_def Domainp_iff by fast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
175 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
176 |
lemma Collect_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
177 |
assumes "bi_total A" |
55938 | 178 |
shows "((A ===> op =) ===> rel_set A) Collect Collect" |
55945 | 179 |
using assms unfolding rel_fun_def rel_set_def bi_total_def by fast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
180 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
181 |
lemma inter_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
182 |
assumes "bi_unique A" |
55938 | 183 |
shows "(rel_set A ===> rel_set A ===> rel_set A) inter inter" |
55945 | 184 |
using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
185 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
186 |
lemma Diff_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
187 |
assumes "bi_unique A" |
55938 | 188 |
shows "(rel_set A ===> rel_set A ===> rel_set A) (op -) (op -)" |
55945 | 189 |
using assms unfolding rel_fun_def rel_set_def bi_unique_def |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
190 |
unfolding Ball_def Bex_def Diff_eq |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
191 |
by (safe, simp, metis, simp, metis) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
192 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
193 |
lemma subset_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
194 |
assumes [transfer_rule]: "bi_unique A" |
55938 | 195 |
shows "(rel_set A ===> rel_set A ===> op =) (op \<subseteq>) (op \<subseteq>)" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
196 |
unfolding subset_eq [abs_def] by transfer_prover |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
197 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
198 |
lemma right_total_UNIV_transfer[transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
199 |
assumes "right_total A" |
55938 | 200 |
shows "(rel_set A) (Collect (Domainp A)) UNIV" |
201 |
using assms unfolding right_total_def rel_set_def Domainp_iff by blast |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
202 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
203 |
lemma UNIV_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
204 |
assumes "bi_total A" |
55938 | 205 |
shows "(rel_set A) UNIV UNIV" |
206 |
using assms unfolding rel_set_def bi_total_def by simp |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
207 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
208 |
lemma right_total_Compl_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
209 |
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" |
55938 | 210 |
shows "(rel_set A ===> rel_set A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
211 |
unfolding Compl_eq [abs_def] |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
212 |
by (subst Collect_conj_eq[symmetric]) transfer_prover |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
213 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
214 |
lemma Compl_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
215 |
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" |
55938 | 216 |
shows "(rel_set A ===> rel_set A) uminus uminus" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
217 |
unfolding Compl_eq [abs_def] by transfer_prover |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
218 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
219 |
lemma right_total_Inter_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
220 |
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" |
55938 | 221 |
shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
222 |
unfolding Inter_eq[abs_def] |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
223 |
by (subst Collect_conj_eq[symmetric]) transfer_prover |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
224 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
225 |
lemma Inter_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
226 |
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" |
55938 | 227 |
shows "(rel_set (rel_set A) ===> rel_set A) Inter Inter" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
228 |
unfolding Inter_eq [abs_def] by transfer_prover |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
229 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
230 |
lemma filter_transfer [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
231 |
assumes [transfer_rule]: "bi_unique A" |
55938 | 232 |
shows "((A ===> op=) ===> rel_set A ===> rel_set A) Set.filter Set.filter" |
55945 | 233 |
unfolding Set.filter_def[abs_def] rel_fun_def rel_set_def by blast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
234 |
|
55938 | 235 |
lemma bi_unique_rel_set_lemma: |
236 |
assumes "bi_unique R" and "rel_set R X Y" |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
237 |
obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
238 |
proof |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
239 |
let ?f = "\<lambda>x. THE y. R x y" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
240 |
from assms show f: "\<forall>x\<in>X. R x (?f x)" |
55938 | 241 |
apply (clarsimp simp add: rel_set_def) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
242 |
apply (drule (1) bspec, clarify) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
243 |
apply (rule theI2, assumption) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
244 |
apply (simp add: bi_unique_def) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
245 |
apply assumption |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
246 |
done |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
247 |
from assms show "Y = image ?f X" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
248 |
apply safe |
55938 | 249 |
apply (clarsimp simp add: rel_set_def) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
250 |
apply (drule (1) bspec, clarify) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
251 |
apply (rule image_eqI) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
252 |
apply (rule the_equality [symmetric], assumption) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
253 |
apply (simp add: bi_unique_def) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
254 |
apply assumption |
55938 | 255 |
apply (clarsimp simp add: rel_set_def) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
256 |
apply (frule (1) bspec, clarify) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
257 |
apply (rule theI2, assumption) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
258 |
apply (clarsimp simp add: bi_unique_def) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
259 |
apply (simp add: bi_unique_def, metis) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
260 |
done |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
261 |
show "inj_on ?f X" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
262 |
apply (rule inj_onI) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
263 |
apply (drule f [rule_format]) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
264 |
apply (drule f [rule_format]) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
265 |
apply (simp add: assms(1) [unfolded bi_unique_def]) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
266 |
done |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
267 |
qed |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
268 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
269 |
lemma finite_transfer [transfer_rule]: |
55938 | 270 |
"bi_unique A \<Longrightarrow> (rel_set A ===> op =) finite finite" |
55945 | 271 |
by (rule rel_funI, erule (1) bi_unique_rel_set_lemma, |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
272 |
auto dest: finite_imageD) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
273 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
274 |
lemma card_transfer [transfer_rule]: |
55938 | 275 |
"bi_unique A \<Longrightarrow> (rel_set A ===> op =) card card" |
55945 | 276 |
by (rule rel_funI, erule (1) bi_unique_rel_set_lemma, simp add: card_image) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
277 |
|
53927 | 278 |
lemma vimage_parametric [transfer_rule]: |
279 |
assumes [transfer_rule]: "bi_total A" "bi_unique B" |
|
55938 | 280 |
shows "((A ===> B) ===> rel_set B ===> rel_set A) vimage vimage" |
53927 | 281 |
unfolding vimage_def[abs_def] by transfer_prover |
282 |
||
283 |
lemma setsum_parametric [transfer_rule]: |
|
284 |
assumes "bi_unique A" |
|
55938 | 285 |
shows "((A ===> op =) ===> rel_set A ===> op =) setsum setsum" |
55945 | 286 |
proof(rule rel_funI)+ |
53927 | 287 |
fix f :: "'a \<Rightarrow> 'c" and g S T |
288 |
assume fg: "(A ===> op =) f g" |
|
55938 | 289 |
and ST: "rel_set A S T" |
53927 | 290 |
show "setsum f S = setsum g T" |
291 |
proof(rule setsum_reindex_cong) |
|
292 |
let ?f = "\<lambda>t. THE s. A s t" |
|
293 |
show "S = ?f ` T" |
|
55938 | 294 |
by(blast dest: rel_setD1[OF ST] rel_setD2[OF ST] bi_uniqueDl[OF assms] |
53927 | 295 |
intro: rev_image_eqI the_equality[symmetric] subst[rotated, where P="\<lambda>x. x \<in> S"]) |
296 |
||
297 |
show "inj_on ?f T" |
|
298 |
proof(rule inj_onI) |
|
299 |
fix t1 t2 |
|
300 |
assume "t1 \<in> T" "t2 \<in> T" "?f t1 = ?f t2" |
|
55938 | 301 |
from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: rel_setD2) |
53927 | 302 |
hence "?f t1 = s1" by(auto dest: bi_uniqueDl[OF assms]) |
303 |
moreover |
|
55938 | 304 |
from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: rel_setD2) |
53927 | 305 |
hence "?f t2 = s2" by(auto dest: bi_uniqueDl[OF assms]) |
306 |
ultimately have "s1 = s2" using `?f t1 = ?f t2` by simp |
|
307 |
with `A s1 t1` `A s2 t2` show "t1 = t2" by(auto dest: bi_uniqueDr[OF assms]) |
|
308 |
qed |
|
309 |
||
310 |
fix t |
|
311 |
assume "t \<in> T" |
|
55938 | 312 |
with ST obtain s where "A s t" "s \<in> S" by(auto dest: rel_setD2) |
53927 | 313 |
hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms]) |
55945 | 314 |
moreover from fg `A s t` have "f s = g t" by(rule rel_funD) |
53927 | 315 |
ultimately show "g t = f (?f t)" by simp |
316 |
qed |
|
317 |
qed |
|
318 |
||
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
319 |
end |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
320 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
321 |
end |