author | kuncar |
Thu, 10 Apr 2014 17:48:14 +0200 | |
changeset 56518 | beb3b6851665 |
parent 56085 | 3d11892ea537 |
child 56520 | 3373f5d1e074 |
permissions | -rw-r--r-- |
47325 | 1 |
(* Title: HOL/Transfer.thy |
2 |
Author: Brian Huffman, TU Muenchen |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
3 |
Author: Ondrej Kuncar, TU Muenchen |
47325 | 4 |
*) |
5 |
||
6 |
header {* Generic theorem transfer using relations *} |
|
7 |
||
8 |
theory Transfer |
|
55811 | 9 |
imports Hilbert_Choice Basic_BNFs Metis |
47325 | 10 |
begin |
11 |
||
12 |
subsection {* Relator for function space *} |
|
13 |
||
53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
14 |
locale lifting_syntax |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
15 |
begin |
55945 | 16 |
notation rel_fun (infixr "===>" 55) |
53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
17 |
notation map_fun (infixr "--->" 55) |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
18 |
end |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
19 |
|
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
20 |
context |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
21 |
begin |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
22 |
interpretation lifting_syntax . |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
23 |
|
55945 | 24 |
lemma rel_funD2: |
25 |
assumes "rel_fun A B f g" and "A x x" |
|
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47924
diff
changeset
|
26 |
shows "B (f x) (g x)" |
55945 | 27 |
using assms by (rule rel_funD) |
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47924
diff
changeset
|
28 |
|
55945 | 29 |
lemma rel_funE: |
30 |
assumes "rel_fun A B f g" and "A x y" |
|
47325 | 31 |
obtains "B (f x) (g y)" |
55945 | 32 |
using assms by (simp add: rel_fun_def) |
47325 | 33 |
|
55945 | 34 |
lemmas rel_fun_eq = fun.rel_eq |
47325 | 35 |
|
55945 | 36 |
lemma rel_fun_eq_rel: |
37 |
shows "rel_fun (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))" |
|
38 |
by (simp add: rel_fun_def) |
|
47325 | 39 |
|
40 |
||
41 |
subsection {* Transfer method *} |
|
42 |
||
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
43 |
text {* Explicit tag for relation membership allows for |
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
44 |
backward proof methods. *} |
47325 | 45 |
|
46 |
definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
|
47 |
where "Rel r \<equiv> r" |
|
48 |
||
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
49 |
text {* Handling of equality relations *} |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
50 |
|
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
51 |
definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
52 |
where "is_equality R \<longleftrightarrow> R = (op =)" |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
53 |
|
51437
8739f8abbecb
fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset
|
54 |
lemma is_equality_eq: "is_equality (op =)" |
8739f8abbecb
fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset
|
55 |
unfolding is_equality_def by simp |
8739f8abbecb
fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset
|
56 |
|
52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
57 |
text {* Reverse implication for monotonicity rules *} |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
58 |
|
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
59 |
definition rev_implies where |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
60 |
"rev_implies x y \<longleftrightarrow> (y \<longrightarrow> x)" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
61 |
|
47325 | 62 |
text {* Handling of meta-logic connectives *} |
63 |
||
64 |
definition transfer_forall where |
|
65 |
"transfer_forall \<equiv> All" |
|
66 |
||
67 |
definition transfer_implies where |
|
68 |
"transfer_implies \<equiv> op \<longrightarrow>" |
|
69 |
||
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
70 |
definition transfer_bforall :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
71 |
where "transfer_bforall \<equiv> (\<lambda>P Q. \<forall>x. P x \<longrightarrow> Q x)" |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
72 |
|
47325 | 73 |
lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))" |
74 |
unfolding atomize_all transfer_forall_def .. |
|
75 |
||
76 |
lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)" |
|
77 |
unfolding atomize_imp transfer_implies_def .. |
|
78 |
||
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
79 |
lemma transfer_bforall_unfold: |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
80 |
"Trueprop (transfer_bforall P (\<lambda>x. Q x)) \<equiv> (\<And>x. P x \<Longrightarrow> Q x)" |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
81 |
unfolding transfer_bforall_def atomize_imp atomize_all .. |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
82 |
|
47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47637
diff
changeset
|
83 |
lemma transfer_start: "\<lbrakk>P; Rel (op =) P Q\<rbrakk> \<Longrightarrow> Q" |
47325 | 84 |
unfolding Rel_def by simp |
85 |
||
47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47637
diff
changeset
|
86 |
lemma transfer_start': "\<lbrakk>P; Rel (op \<longrightarrow>) P Q\<rbrakk> \<Longrightarrow> Q" |
47325 | 87 |
unfolding Rel_def by simp |
88 |
||
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
89 |
lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y" |
47618
1568dadd598a
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents:
47612
diff
changeset
|
90 |
by simp |
1568dadd598a
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents:
47612
diff
changeset
|
91 |
|
52358
f4c4bcb0d564
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents:
52354
diff
changeset
|
92 |
lemma untransfer_start: "\<lbrakk>Q; Rel (op =) P Q\<rbrakk> \<Longrightarrow> P" |
f4c4bcb0d564
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents:
52354
diff
changeset
|
93 |
unfolding Rel_def by simp |
f4c4bcb0d564
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents:
52354
diff
changeset
|
94 |
|
47325 | 95 |
lemma Rel_eq_refl: "Rel (op =) x x" |
96 |
unfolding Rel_def .. |
|
97 |
||
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
98 |
lemma Rel_app: |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
99 |
assumes "Rel (A ===> B) f g" and "Rel A x y" |
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
100 |
shows "Rel B (f x) (g y)" |
55945 | 101 |
using assms unfolding Rel_def rel_fun_def by fast |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
102 |
|
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
103 |
lemma Rel_abs: |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
104 |
assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)" |
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
105 |
shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)" |
55945 | 106 |
using assms unfolding Rel_def rel_fun_def by fast |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
107 |
|
53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
108 |
end |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
109 |
|
48891 | 110 |
ML_file "Tools/transfer.ML" |
47325 | 111 |
setup Transfer.setup |
112 |
||
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
113 |
declare refl [transfer_rule] |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
114 |
|
55945 | 115 |
declare rel_fun_eq [relator_eq] |
47503 | 116 |
|
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
117 |
hide_const (open) Rel |
47325 | 118 |
|
53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
119 |
context |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
120 |
begin |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
121 |
interpretation lifting_syntax . |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
122 |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
123 |
text {* Handling of domains *} |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
124 |
|
55760
aaaccc8e015f
transfer domain rule for special case of functions - was missing
kuncar
parents:
55415
diff
changeset
|
125 |
lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)" |
aaaccc8e015f
transfer domain rule for special case of functions - was missing
kuncar
parents:
55415
diff
changeset
|
126 |
by auto |
aaaccc8e015f
transfer domain rule for special case of functions - was missing
kuncar
parents:
55415
diff
changeset
|
127 |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
128 |
lemma Domaimp_refl[transfer_domain_rule]: |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
129 |
"Domainp T = Domainp T" .. |
47325 | 130 |
|
55760
aaaccc8e015f
transfer domain rule for special case of functions - was missing
kuncar
parents:
55415
diff
changeset
|
131 |
lemma Domainp_prod_fun_eq[transfer_domain_rule]: |
aaaccc8e015f
transfer domain rule for special case of functions - was missing
kuncar
parents:
55415
diff
changeset
|
132 |
assumes "Domainp T = P" |
aaaccc8e015f
transfer domain rule for special case of functions - was missing
kuncar
parents:
55415
diff
changeset
|
133 |
shows "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. P (f x))" |
55945 | 134 |
by (auto intro: choice simp: assms[symmetric] Domainp_iff rel_fun_def fun_eq_iff) |
55760
aaaccc8e015f
transfer domain rule for special case of functions - was missing
kuncar
parents:
55415
diff
changeset
|
135 |
|
47325 | 136 |
subsection {* Predicates on relations, i.e. ``class constraints'' *} |
137 |
||
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
138 |
definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
139 |
where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
140 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
141 |
definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
142 |
where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
143 |
|
47325 | 144 |
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
145 |
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)" |
|
146 |
||
147 |
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
148 |
where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)" |
|
149 |
||
150 |
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
151 |
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)" |
|
152 |
||
153 |
definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
154 |
where "bi_unique R \<longleftrightarrow> |
|
155 |
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and> |
|
156 |
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" |
|
157 |
||
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
158 |
lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
159 |
unfolding left_unique_def by blast |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
160 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
161 |
lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
162 |
unfolding left_unique_def by blast |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
163 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
164 |
lemma left_totalI: |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
165 |
"(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
166 |
unfolding left_total_def by blast |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
167 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
168 |
lemma left_totalE: |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
169 |
assumes "left_total R" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
170 |
obtains "(\<And>x. \<exists>y. R x y)" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
171 |
using assms unfolding left_total_def by blast |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
172 |
|
53927 | 173 |
lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z" |
174 |
by(simp add: bi_unique_def) |
|
175 |
||
176 |
lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z" |
|
177 |
by(simp add: bi_unique_def) |
|
178 |
||
179 |
lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A" |
|
56085 | 180 |
unfolding right_unique_def by fast |
53927 | 181 |
|
182 |
lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z" |
|
56085 | 183 |
unfolding right_unique_def by fast |
53927 | 184 |
|
47325 | 185 |
lemma right_total_alt_def: |
186 |
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All" |
|
55945 | 187 |
unfolding right_total_def rel_fun_def |
47325 | 188 |
apply (rule iffI, fast) |
189 |
apply (rule allI) |
|
190 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
191 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
192 |
apply fast |
|
193 |
done |
|
194 |
||
195 |
lemma right_unique_alt_def: |
|
196 |
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)" |
|
55945 | 197 |
unfolding right_unique_def rel_fun_def by auto |
47325 | 198 |
|
199 |
lemma bi_total_alt_def: |
|
200 |
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All" |
|
55945 | 201 |
unfolding bi_total_def rel_fun_def |
47325 | 202 |
apply (rule iffI, fast) |
203 |
apply safe |
|
204 |
apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec) |
|
205 |
apply (drule_tac x="\<lambda>y. True" in spec) |
|
206 |
apply fast |
|
207 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
208 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
209 |
apply fast |
|
210 |
done |
|
211 |
||
212 |
lemma bi_unique_alt_def: |
|
213 |
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)" |
|
55945 | 214 |
unfolding bi_unique_def rel_fun_def by auto |
47325 | 215 |
|
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
216 |
lemma [simp]: |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
217 |
shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
218 |
and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
219 |
by(auto simp add: left_unique_def right_unique_def) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
220 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
221 |
lemma [simp]: |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
222 |
shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
223 |
and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
224 |
by(simp_all add: left_total_def right_total_def) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
225 |
|
53944 | 226 |
lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R" |
227 |
by(auto simp add: bi_unique_def) |
|
228 |
||
229 |
lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R" |
|
230 |
by(auto simp add: bi_total_def) |
|
231 |
||
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
232 |
lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
233 |
unfolding left_total_def right_total_def bi_total_def by blast |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
234 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
235 |
lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
236 |
by(simp add: left_total_def right_total_def bi_total_def) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
237 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
238 |
lemma bi_unique_iff: "bi_unique A \<longleftrightarrow> right_unique A \<and> left_unique A" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
239 |
unfolding left_unique_def right_unique_def bi_unique_def by blast |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
240 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
241 |
lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
242 |
by(auto simp add: left_unique_def right_unique_def bi_unique_def) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
243 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
244 |
lemma bi_totalI: "left_total R \<Longrightarrow> right_total R \<Longrightarrow> bi_total R" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
245 |
unfolding bi_total_iff .. |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
246 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
247 |
lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
248 |
unfolding bi_unique_iff .. |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
249 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
250 |
|
47660 | 251 |
text {* Properties are preserved by relation composition. *} |
252 |
||
253 |
lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)" |
|
254 |
by auto |
|
255 |
||
256 |
lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)" |
|
56085 | 257 |
unfolding bi_total_def OO_def by fast |
47660 | 258 |
|
259 |
lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)" |
|
56085 | 260 |
unfolding bi_unique_def OO_def by blast |
47660 | 261 |
|
262 |
lemma right_total_OO: |
|
263 |
"\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)" |
|
56085 | 264 |
unfolding right_total_def OO_def by fast |
47660 | 265 |
|
266 |
lemma right_unique_OO: |
|
267 |
"\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)" |
|
56085 | 268 |
unfolding right_unique_def OO_def by fast |
47660 | 269 |
|
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
270 |
lemma left_total_OO: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
271 |
unfolding left_total_def OO_def by fast |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
272 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
273 |
lemma left_unique_OO: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
274 |
unfolding left_unique_def OO_def by blast |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
275 |
|
47325 | 276 |
|
277 |
subsection {* Properties of relators *} |
|
278 |
||
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
279 |
lemma left_total_eq[transfer_rule]: "left_total op=" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
280 |
unfolding left_total_def by blast |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
281 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
282 |
lemma left_unique_eq[transfer_rule]: "left_unique op=" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
283 |
unfolding left_unique_def by blast |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
284 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
285 |
lemma right_total_eq [transfer_rule]: "right_total op=" |
47325 | 286 |
unfolding right_total_def by simp |
287 |
||
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
288 |
lemma right_unique_eq [transfer_rule]: "right_unique op=" |
47325 | 289 |
unfolding right_unique_def by simp |
290 |
||
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
291 |
lemma bi_total_eq[transfer_rule]: "bi_total (op =)" |
47325 | 292 |
unfolding bi_total_def by simp |
293 |
||
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
294 |
lemma bi_unique_eq[transfer_rule]: "bi_unique (op =)" |
47325 | 295 |
unfolding bi_unique_def by simp |
296 |
||
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
297 |
lemma left_total_fun[transfer_rule]: |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
298 |
"\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
299 |
unfolding left_total_def rel_fun_def |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
300 |
apply (rule allI, rename_tac f) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
301 |
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
302 |
apply clarify |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
303 |
apply (subgoal_tac "(THE x. A x y) = x", simp) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
304 |
apply (rule someI_ex) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
305 |
apply (simp) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
306 |
apply (rule the_equality) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
307 |
apply assumption |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
308 |
apply (simp add: left_unique_def) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
309 |
done |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
310 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
311 |
lemma left_unique_fun[transfer_rule]: |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
312 |
"\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
313 |
unfolding left_total_def left_unique_def rel_fun_def |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
314 |
by (clarify, rule ext, fast) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
315 |
|
47325 | 316 |
lemma right_total_fun [transfer_rule]: |
317 |
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)" |
|
55945 | 318 |
unfolding right_total_def rel_fun_def |
47325 | 319 |
apply (rule allI, rename_tac g) |
320 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) |
|
321 |
apply clarify |
|
322 |
apply (subgoal_tac "(THE y. A x y) = y", simp) |
|
323 |
apply (rule someI_ex) |
|
324 |
apply (simp) |
|
325 |
apply (rule the_equality) |
|
326 |
apply assumption |
|
327 |
apply (simp add: right_unique_def) |
|
328 |
done |
|
329 |
||
330 |
lemma right_unique_fun [transfer_rule]: |
|
331 |
"\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)" |
|
55945 | 332 |
unfolding right_total_def right_unique_def rel_fun_def |
47325 | 333 |
by (clarify, rule ext, fast) |
334 |
||
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
335 |
lemma bi_total_fun[transfer_rule]: |
47325 | 336 |
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)" |
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
337 |
unfolding bi_unique_iff bi_total_iff |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
338 |
by (blast intro: right_total_fun left_total_fun) |
47325 | 339 |
|
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
340 |
lemma bi_unique_fun[transfer_rule]: |
47325 | 341 |
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)" |
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
342 |
unfolding bi_unique_iff bi_total_iff |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
343 |
by (blast intro: right_unique_fun left_unique_fun) |
47325 | 344 |
|
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
345 |
subsection {* Transfer rules *} |
47325 | 346 |
|
53952 | 347 |
lemma Domainp_forall_transfer [transfer_rule]: |
348 |
assumes "right_total A" |
|
349 |
shows "((A ===> op =) ===> op =) |
|
350 |
(transfer_bforall (Domainp A)) transfer_forall" |
|
351 |
using assms unfolding right_total_def |
|
55945 | 352 |
unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff |
56085 | 353 |
by fast |
53952 | 354 |
|
47684 | 355 |
text {* Transfer rules using implication instead of equality on booleans. *} |
356 |
||
52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
357 |
lemma transfer_forall_transfer [transfer_rule]: |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
358 |
"bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
359 |
"right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
360 |
"right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
361 |
"bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
362 |
"bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall" |
55945 | 363 |
unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def |
56085 | 364 |
by fast+ |
52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
365 |
|
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
366 |
lemma transfer_implies_transfer [transfer_rule]: |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
367 |
"(op = ===> op = ===> op = ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
368 |
"(rev_implies ===> implies ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
369 |
"(rev_implies ===> op = ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
370 |
"(op = ===> implies ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
371 |
"(op = ===> op = ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
372 |
"(implies ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
373 |
"(implies ===> op = ===> rev_implies) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
374 |
"(op = ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
375 |
"(op = ===> op = ===> rev_implies) transfer_implies transfer_implies" |
55945 | 376 |
unfolding transfer_implies_def rev_implies_def rel_fun_def by auto |
52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
377 |
|
47684 | 378 |
lemma eq_imp_transfer [transfer_rule]: |
379 |
"right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)" |
|
380 |
unfolding right_unique_alt_def . |
|
381 |
||
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
382 |
text {* Transfer rules using equality. *} |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
383 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
384 |
lemma left_unique_transfer [transfer_rule]: |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
385 |
assumes "right_total A" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
386 |
assumes "right_total B" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
387 |
assumes "bi_unique A" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
388 |
shows "((A ===> B ===> op=) ===> implies) left_unique left_unique" |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
389 |
using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
390 |
by metis |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
391 |
|
47636 | 392 |
lemma eq_transfer [transfer_rule]: |
47325 | 393 |
assumes "bi_unique A" |
394 |
shows "(A ===> A ===> op =) (op =) (op =)" |
|
55945 | 395 |
using assms unfolding bi_unique_def rel_fun_def by auto |
47325 | 396 |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
397 |
lemma right_total_Ex_transfer[transfer_rule]: |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
398 |
assumes "right_total A" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
399 |
shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex" |
55945 | 400 |
using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def] |
56085 | 401 |
by fast |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
402 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
403 |
lemma right_total_All_transfer[transfer_rule]: |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
404 |
assumes "right_total A" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
405 |
shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All" |
55945 | 406 |
using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def] |
56085 | 407 |
by fast |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
408 |
|
47636 | 409 |
lemma All_transfer [transfer_rule]: |
47325 | 410 |
assumes "bi_total A" |
411 |
shows "((A ===> op =) ===> op =) All All" |
|
55945 | 412 |
using assms unfolding bi_total_def rel_fun_def by fast |
47325 | 413 |
|
47636 | 414 |
lemma Ex_transfer [transfer_rule]: |
47325 | 415 |
assumes "bi_total A" |
416 |
shows "((A ===> op =) ===> op =) Ex Ex" |
|
55945 | 417 |
using assms unfolding bi_total_def rel_fun_def by fast |
47325 | 418 |
|
47636 | 419 |
lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If" |
55945 | 420 |
unfolding rel_fun_def by simp |
47325 | 421 |
|
47636 | 422 |
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" |
55945 | 423 |
unfolding rel_fun_def by simp |
47612 | 424 |
|
47636 | 425 |
lemma id_transfer [transfer_rule]: "(A ===> A) id id" |
55945 | 426 |
unfolding rel_fun_def by simp |
47625 | 427 |
|
47636 | 428 |
lemma comp_transfer [transfer_rule]: |
47325 | 429 |
"((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)" |
55945 | 430 |
unfolding rel_fun_def by simp |
47325 | 431 |
|
47636 | 432 |
lemma fun_upd_transfer [transfer_rule]: |
47325 | 433 |
assumes [transfer_rule]: "bi_unique A" |
434 |
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" |
|
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
435 |
unfolding fun_upd_def [abs_def] by transfer_prover |
47325 | 436 |
|
55415 | 437 |
lemma case_nat_transfer [transfer_rule]: |
438 |
"(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat" |
|
55945 | 439 |
unfolding rel_fun_def by (simp split: nat.split) |
47627
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
440 |
|
55415 | 441 |
lemma rec_nat_transfer [transfer_rule]: |
442 |
"(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat" |
|
55945 | 443 |
unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all) |
47924 | 444 |
|
445 |
lemma funpow_transfer [transfer_rule]: |
|
446 |
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow" |
|
447 |
unfolding funpow_def by transfer_prover |
|
448 |
||
53952 | 449 |
lemma mono_transfer[transfer_rule]: |
450 |
assumes [transfer_rule]: "bi_total A" |
|
451 |
assumes [transfer_rule]: "(A ===> A ===> op=) op\<le> op\<le>" |
|
452 |
assumes [transfer_rule]: "(B ===> B ===> op=) op\<le> op\<le>" |
|
453 |
shows "((A ===> B) ===> op=) mono mono" |
|
454 |
unfolding mono_def[abs_def] by transfer_prover |
|
455 |
||
456 |
lemma right_total_relcompp_transfer[transfer_rule]: |
|
457 |
assumes [transfer_rule]: "right_total B" |
|
458 |
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) |
|
459 |
(\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO" |
|
460 |
unfolding OO_def[abs_def] by transfer_prover |
|
461 |
||
462 |
lemma relcompp_transfer[transfer_rule]: |
|
463 |
assumes [transfer_rule]: "bi_total B" |
|
464 |
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO" |
|
465 |
unfolding OO_def[abs_def] by transfer_prover |
|
47627
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
466 |
|
53952 | 467 |
lemma right_total_Domainp_transfer[transfer_rule]: |
468 |
assumes [transfer_rule]: "right_total B" |
|
469 |
shows "((A ===> B ===> op=) ===> A ===> op=) (\<lambda>T x. \<exists>y\<in>Collect(Domainp B). T x y) Domainp" |
|
470 |
apply(subst(2) Domainp_iff[abs_def]) by transfer_prover |
|
471 |
||
472 |
lemma Domainp_transfer[transfer_rule]: |
|
473 |
assumes [transfer_rule]: "bi_total B" |
|
474 |
shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp" |
|
475 |
unfolding Domainp_iff[abs_def] by transfer_prover |
|
476 |
||
477 |
lemma reflp_transfer[transfer_rule]: |
|
478 |
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp" |
|
479 |
"right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp" |
|
480 |
"right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp" |
|
481 |
"bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp" |
|
482 |
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp" |
|
55945 | 483 |
using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def |
53952 | 484 |
by fast+ |
485 |
||
486 |
lemma right_unique_transfer [transfer_rule]: |
|
487 |
assumes [transfer_rule]: "right_total A" |
|
488 |
assumes [transfer_rule]: "right_total B" |
|
489 |
assumes [transfer_rule]: "bi_unique B" |
|
490 |
shows "((A ===> B ===> op=) ===> implies) right_unique right_unique" |
|
55945 | 491 |
using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def |
53952 | 492 |
by metis |
47325 | 493 |
|
494 |
end |
|
53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
495 |
|
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
496 |
end |