author | wenzelm |
Tue, 31 Mar 2015 22:31:05 +0200 | |
changeset 59886 | e0dc738eb08c |
parent 59523 | 860fb1c65553 |
child 60229 | 4cd6462c1fda |
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 |
||
58889 | 6 |
section {* Generic theorem transfer using relations *} |
47325 | 7 |
|
8 |
theory Transfer |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59141
diff
changeset
|
9 |
imports Basic_BNF_LFPs Hilbert_Choice 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 |
|
47325 | 108 |
subsection {* Predicates on relations, i.e. ``class constraints'' *} |
109 |
||
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
|
110 |
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
|
111 |
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
|
112 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
113 |
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
|
114 |
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
|
115 |
|
47325 | 116 |
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
117 |
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)" |
|
118 |
||
119 |
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
120 |
where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)" |
|
121 |
||
122 |
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
123 |
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)" |
|
124 |
||
125 |
definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
126 |
where "bi_unique R \<longleftrightarrow> |
|
127 |
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and> |
|
128 |
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" |
|
129 |
||
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
|
130 |
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
|
131 |
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
|
132 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
133 |
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
|
134 |
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
|
135 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
136 |
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
|
137 |
"(\<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
|
138 |
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
|
139 |
|
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 |
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
|
141 |
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
|
142 |
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
|
143 |
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
|
144 |
|
53927 | 145 |
lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z" |
146 |
by(simp add: bi_unique_def) |
|
147 |
||
148 |
lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z" |
|
149 |
by(simp add: bi_unique_def) |
|
150 |
||
151 |
lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A" |
|
56085 | 152 |
unfolding right_unique_def by fast |
53927 | 153 |
|
154 |
lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z" |
|
56085 | 155 |
unfolding right_unique_def by fast |
53927 | 156 |
|
59514
509caf5edfa6
add intro and elim rules for right_total
Andreas Lochbihler
parents:
59276
diff
changeset
|
157 |
lemma right_totalI: "(\<And>y. \<exists>x. A x y) \<Longrightarrow> right_total A" |
509caf5edfa6
add intro and elim rules for right_total
Andreas Lochbihler
parents:
59276
diff
changeset
|
158 |
by(simp add: right_total_def) |
509caf5edfa6
add intro and elim rules for right_total
Andreas Lochbihler
parents:
59276
diff
changeset
|
159 |
|
509caf5edfa6
add intro and elim rules for right_total
Andreas Lochbihler
parents:
59276
diff
changeset
|
160 |
lemma right_totalE: |
509caf5edfa6
add intro and elim rules for right_total
Andreas Lochbihler
parents:
59276
diff
changeset
|
161 |
assumes "right_total A" |
509caf5edfa6
add intro and elim rules for right_total
Andreas Lochbihler
parents:
59276
diff
changeset
|
162 |
obtains x where "A x y" |
509caf5edfa6
add intro and elim rules for right_total
Andreas Lochbihler
parents:
59276
diff
changeset
|
163 |
using assms by(auto simp add: right_total_def) |
509caf5edfa6
add intro and elim rules for right_total
Andreas Lochbihler
parents:
59276
diff
changeset
|
164 |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
165 |
lemma right_total_alt_def2: |
47325 | 166 |
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All" |
55945 | 167 |
unfolding right_total_def rel_fun_def |
47325 | 168 |
apply (rule iffI, fast) |
169 |
apply (rule allI) |
|
170 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
171 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
172 |
apply fast |
|
173 |
done |
|
174 |
||
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
175 |
lemma right_unique_alt_def2: |
47325 | 176 |
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)" |
55945 | 177 |
unfolding right_unique_def rel_fun_def by auto |
47325 | 178 |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
179 |
lemma bi_total_alt_def2: |
47325 | 180 |
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All" |
55945 | 181 |
unfolding bi_total_def rel_fun_def |
47325 | 182 |
apply (rule iffI, fast) |
183 |
apply safe |
|
184 |
apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec) |
|
185 |
apply (drule_tac x="\<lambda>y. True" in spec) |
|
186 |
apply fast |
|
187 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
188 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
189 |
apply fast |
|
190 |
done |
|
191 |
||
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
192 |
lemma bi_unique_alt_def2: |
47325 | 193 |
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)" |
55945 | 194 |
unfolding bi_unique_def rel_fun_def by auto |
47325 | 195 |
|
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
|
196 |
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
|
197 |
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
|
198 |
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
|
199 |
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
|
200 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
201 |
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
|
202 |
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
|
203 |
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
|
204 |
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
|
205 |
|
53944 | 206 |
lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R" |
207 |
by(auto simp add: bi_unique_def) |
|
208 |
||
209 |
lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R" |
|
210 |
by(auto simp add: bi_total_def) |
|
211 |
||
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
212 |
lemma right_unique_alt_def: "right_unique R = (conversep R OO R \<le> op=)" unfolding right_unique_def by blast |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
213 |
lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \<le> op=)" unfolding left_unique_def by blast |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
214 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
215 |
lemma right_total_alt_def: "right_total R = (conversep R OO R \<ge> op=)" unfolding right_total_def by blast |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
216 |
lemma left_total_alt_def: "left_total R = (R OO conversep R \<ge> op=)" unfolding left_total_def by blast |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
217 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
218 |
lemma bi_total_alt_def: "bi_total A = (left_total A \<and> right_total A)" |
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
|
219 |
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
|
220 |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
221 |
lemma bi_unique_alt_def: "bi_unique A = (left_unique A \<and> right_unique A)" |
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
|
222 |
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
|
223 |
|
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 |
lemma bi_totalI: "left_total R \<Longrightarrow> right_total R \<Longrightarrow> bi_total R" |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
225 |
unfolding bi_total_alt_def .. |
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
|
226 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
227 |
lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R" |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
228 |
unfolding bi_unique_alt_def .. |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
229 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
230 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
231 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
232 |
subsection {* Equality restricted by a predicate *} |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
233 |
|
58182 | 234 |
definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
235 |
where "eq_onp R = (\<lambda>x y. R x \<and> x = y)" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
236 |
|
58182 | 237 |
lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id" |
238 |
unfolding eq_onp_def Grp_def by auto |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
239 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
240 |
lemma eq_onp_to_eq: |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
241 |
assumes "eq_onp P x y" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
242 |
shows "x = y" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
243 |
using assms by (simp add: eq_onp_def) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
244 |
|
58182 | 245 |
lemma eq_onp_top_eq_eq: "eq_onp top = op=" |
56677
660ffb526069
predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents:
56654
diff
changeset
|
246 |
by (simp add: eq_onp_def) |
660ffb526069
predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents:
56654
diff
changeset
|
247 |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
248 |
lemma eq_onp_same_args: |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
249 |
shows "eq_onp P x x = P x" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
250 |
using assms by (auto simp add: eq_onp_def) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
251 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
252 |
lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))" |
57260
8747af0d1012
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
blanchet
parents:
56677
diff
changeset
|
253 |
by auto |
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
|
254 |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
255 |
ML_file "Tools/Transfer/transfer.ML" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
256 |
declare refl [transfer_rule] |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
257 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
258 |
hide_const (open) Rel |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
259 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
260 |
context |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
261 |
begin |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
262 |
interpretation lifting_syntax . |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
263 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
264 |
text {* Handling of domains *} |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
265 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
266 |
lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
267 |
by auto |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
268 |
|
58386 | 269 |
lemma Domainp_refl[transfer_domain_rule]: |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
270 |
"Domainp T = Domainp T" .. |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
271 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
272 |
lemma Domainp_prod_fun_eq[relator_domain]: |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
273 |
"Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
274 |
by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff) |
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
|
275 |
|
47660 | 276 |
text {* Properties are preserved by relation composition. *} |
277 |
||
278 |
lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)" |
|
279 |
by auto |
|
280 |
||
281 |
lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)" |
|
56085 | 282 |
unfolding bi_total_def OO_def by fast |
47660 | 283 |
|
284 |
lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)" |
|
56085 | 285 |
unfolding bi_unique_def OO_def by blast |
47660 | 286 |
|
287 |
lemma right_total_OO: |
|
288 |
"\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)" |
|
56085 | 289 |
unfolding right_total_def OO_def by fast |
47660 | 290 |
|
291 |
lemma right_unique_OO: |
|
292 |
"\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)" |
|
56085 | 293 |
unfolding right_unique_def OO_def by fast |
47660 | 294 |
|
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
|
295 |
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
|
296 |
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
|
297 |
|
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 |
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
|
299 |
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
|
300 |
|
47325 | 301 |
|
302 |
subsection {* Properties of relators *} |
|
303 |
||
58182 | 304 |
lemma left_total_eq[transfer_rule]: "left_total op=" |
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
|
305 |
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
|
306 |
|
58182 | 307 |
lemma left_unique_eq[transfer_rule]: "left_unique op=" |
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
|
308 |
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
|
309 |
|
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 |
lemma right_total_eq [transfer_rule]: "right_total op=" |
47325 | 311 |
unfolding right_total_def by simp |
312 |
||
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
|
313 |
lemma right_unique_eq [transfer_rule]: "right_unique op=" |
47325 | 314 |
unfolding right_unique_def by simp |
315 |
||
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
|
316 |
lemma bi_total_eq[transfer_rule]: "bi_total (op =)" |
47325 | 317 |
unfolding bi_total_def by simp |
318 |
||
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
|
319 |
lemma bi_unique_eq[transfer_rule]: "bi_unique (op =)" |
47325 | 320 |
unfolding bi_unique_def by simp |
321 |
||
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
|
322 |
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
|
323 |
"\<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
|
324 |
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
|
325 |
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
|
326 |
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
|
327 |
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
|
328 |
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
|
329 |
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
|
330 |
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
|
331 |
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
|
332 |
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
|
333 |
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
|
334 |
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
|
335 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
336 |
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
|
337 |
"\<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
|
338 |
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
|
339 |
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
|
340 |
|
47325 | 341 |
lemma right_total_fun [transfer_rule]: |
342 |
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)" |
|
55945 | 343 |
unfolding right_total_def rel_fun_def |
47325 | 344 |
apply (rule allI, rename_tac g) |
345 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) |
|
346 |
apply clarify |
|
347 |
apply (subgoal_tac "(THE y. A x y) = y", simp) |
|
348 |
apply (rule someI_ex) |
|
349 |
apply (simp) |
|
350 |
apply (rule the_equality) |
|
351 |
apply assumption |
|
352 |
apply (simp add: right_unique_def) |
|
353 |
done |
|
354 |
||
355 |
lemma right_unique_fun [transfer_rule]: |
|
356 |
"\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)" |
|
55945 | 357 |
unfolding right_total_def right_unique_def rel_fun_def |
47325 | 358 |
by (clarify, rule ext, fast) |
359 |
||
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
|
360 |
lemma bi_total_fun[transfer_rule]: |
47325 | 361 |
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)" |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
362 |
unfolding bi_unique_alt_def bi_total_alt_def |
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
|
363 |
by (blast intro: right_total_fun left_total_fun) |
47325 | 364 |
|
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
|
365 |
lemma bi_unique_fun[transfer_rule]: |
47325 | 366 |
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)" |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
367 |
unfolding bi_unique_alt_def bi_total_alt_def |
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
|
368 |
by (blast intro: right_unique_fun left_unique_fun) |
47325 | 369 |
|
56543
9bd56f2e4c10
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents:
56524
diff
changeset
|
370 |
end |
9bd56f2e4c10
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents:
56524
diff
changeset
|
371 |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59141
diff
changeset
|
372 |
lemma if_conn: |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59141
diff
changeset
|
373 |
"(if P \<and> Q then t else e) = (if P then if Q then t else e else e)" |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59141
diff
changeset
|
374 |
"(if P \<or> Q then t else e) = (if P then t else if Q then t else e)" |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59141
diff
changeset
|
375 |
"(if P \<longrightarrow> Q then t else e) = (if P then if Q then t else e else t)" |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59141
diff
changeset
|
376 |
"(if \<not> P then t else e) = (if P then e else t)" |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59141
diff
changeset
|
377 |
by auto |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59141
diff
changeset
|
378 |
|
58182 | 379 |
ML_file "Tools/Transfer/transfer_bnf.ML" |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59141
diff
changeset
|
380 |
ML_file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML" |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
59141
diff
changeset
|
381 |
|
56543
9bd56f2e4c10
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents:
56524
diff
changeset
|
382 |
declare pred_fun_def [simp] |
9bd56f2e4c10
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents:
56524
diff
changeset
|
383 |
declare rel_fun_eq [relator_eq] |
9bd56f2e4c10
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents:
56524
diff
changeset
|
384 |
|
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
385 |
subsection {* Transfer rules *} |
47325 | 386 |
|
56543
9bd56f2e4c10
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents:
56524
diff
changeset
|
387 |
context |
9bd56f2e4c10
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents:
56524
diff
changeset
|
388 |
begin |
9bd56f2e4c10
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents:
56524
diff
changeset
|
389 |
interpretation lifting_syntax . |
9bd56f2e4c10
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
kuncar
parents:
56524
diff
changeset
|
390 |
|
53952 | 391 |
lemma Domainp_forall_transfer [transfer_rule]: |
392 |
assumes "right_total A" |
|
393 |
shows "((A ===> op =) ===> op =) |
|
394 |
(transfer_bforall (Domainp A)) transfer_forall" |
|
395 |
using assms unfolding right_total_def |
|
55945 | 396 |
unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff |
56085 | 397 |
by fast |
53952 | 398 |
|
47684 | 399 |
text {* Transfer rules using implication instead of equality on booleans. *} |
400 |
||
52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
401 |
lemma transfer_forall_transfer [transfer_rule]: |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
402 |
"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
|
403 |
"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
|
404 |
"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
|
405 |
"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
|
406 |
"bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall" |
55945 | 407 |
unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def |
56085 | 408 |
by fast+ |
52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
409 |
|
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
410 |
lemma transfer_implies_transfer [transfer_rule]: |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
411 |
"(op = ===> op = ===> op = ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
412 |
"(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
|
413 |
"(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
|
414 |
"(op = ===> implies ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
415 |
"(op = ===> op = ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
416 |
"(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
|
417 |
"(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
|
418 |
"(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
|
419 |
"(op = ===> op = ===> rev_implies) transfer_implies transfer_implies" |
55945 | 420 |
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
|
421 |
|
47684 | 422 |
lemma eq_imp_transfer [transfer_rule]: |
423 |
"right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)" |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
424 |
unfolding right_unique_alt_def2 . |
47684 | 425 |
|
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
|
426 |
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
|
427 |
|
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56085
diff
changeset
|
428 |
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
|
429 |
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
|
430 |
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
|
431 |
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
|
432 |
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
|
433 |
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
|
434 |
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
|
435 |
|
47636 | 436 |
lemma eq_transfer [transfer_rule]: |
47325 | 437 |
assumes "bi_unique A" |
438 |
shows "(A ===> A ===> op =) (op =) (op =)" |
|
55945 | 439 |
using assms unfolding bi_unique_def rel_fun_def by auto |
47325 | 440 |
|
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
|
441 |
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
|
442 |
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
|
443 |
shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex" |
55945 | 444 |
using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def] |
56085 | 445 |
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
|
446 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
447 |
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
|
448 |
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
|
449 |
shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All" |
55945 | 450 |
using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def] |
56085 | 451 |
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
|
452 |
|
47636 | 453 |
lemma All_transfer [transfer_rule]: |
47325 | 454 |
assumes "bi_total A" |
455 |
shows "((A ===> op =) ===> op =) All All" |
|
55945 | 456 |
using assms unfolding bi_total_def rel_fun_def by fast |
47325 | 457 |
|
47636 | 458 |
lemma Ex_transfer [transfer_rule]: |
47325 | 459 |
assumes "bi_total A" |
460 |
shows "((A ===> op =) ===> op =) Ex Ex" |
|
55945 | 461 |
using assms unfolding bi_total_def rel_fun_def by fast |
47325 | 462 |
|
59515 | 463 |
lemma Ex1_parametric [transfer_rule]: |
464 |
assumes [transfer_rule]: "bi_unique A" "bi_total A" |
|
465 |
shows "((A ===> op =) ===> op =) Ex1 Ex1" |
|
466 |
unfolding Ex1_def[abs_def] by transfer_prover |
|
467 |
||
58448 | 468 |
declare If_transfer [transfer_rule] |
47325 | 469 |
|
47636 | 470 |
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" |
55945 | 471 |
unfolding rel_fun_def by simp |
47612 | 472 |
|
58916 | 473 |
declare id_transfer [transfer_rule] |
47625 | 474 |
|
58444 | 475 |
declare comp_transfer [transfer_rule] |
47325 | 476 |
|
58916 | 477 |
lemma curry_transfer [transfer_rule]: |
478 |
"((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry" |
|
479 |
unfolding curry_def by transfer_prover |
|
480 |
||
47636 | 481 |
lemma fun_upd_transfer [transfer_rule]: |
47325 | 482 |
assumes [transfer_rule]: "bi_unique A" |
483 |
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" |
|
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
484 |
unfolding fun_upd_def [abs_def] by transfer_prover |
47325 | 485 |
|
55415 | 486 |
lemma case_nat_transfer [transfer_rule]: |
487 |
"(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat" |
|
55945 | 488 |
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
|
489 |
|
55415 | 490 |
lemma rec_nat_transfer [transfer_rule]: |
491 |
"(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat" |
|
55945 | 492 |
unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all) |
47924 | 493 |
|
494 |
lemma funpow_transfer [transfer_rule]: |
|
495 |
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow" |
|
496 |
unfolding funpow_def by transfer_prover |
|
497 |
||
53952 | 498 |
lemma mono_transfer[transfer_rule]: |
499 |
assumes [transfer_rule]: "bi_total A" |
|
500 |
assumes [transfer_rule]: "(A ===> A ===> op=) op\<le> op\<le>" |
|
501 |
assumes [transfer_rule]: "(B ===> B ===> op=) op\<le> op\<le>" |
|
502 |
shows "((A ===> B) ===> op=) mono mono" |
|
503 |
unfolding mono_def[abs_def] by transfer_prover |
|
504 |
||
58182 | 505 |
lemma right_total_relcompp_transfer[transfer_rule]: |
53952 | 506 |
assumes [transfer_rule]: "right_total B" |
58182 | 507 |
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) |
53952 | 508 |
(\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO" |
509 |
unfolding OO_def[abs_def] by transfer_prover |
|
510 |
||
58182 | 511 |
lemma relcompp_transfer[transfer_rule]: |
53952 | 512 |
assumes [transfer_rule]: "bi_total B" |
513 |
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO" |
|
514 |
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
|
515 |
|
53952 | 516 |
lemma right_total_Domainp_transfer[transfer_rule]: |
517 |
assumes [transfer_rule]: "right_total B" |
|
518 |
shows "((A ===> B ===> op=) ===> A ===> op=) (\<lambda>T x. \<exists>y\<in>Collect(Domainp B). T x y) Domainp" |
|
519 |
apply(subst(2) Domainp_iff[abs_def]) by transfer_prover |
|
520 |
||
521 |
lemma Domainp_transfer[transfer_rule]: |
|
522 |
assumes [transfer_rule]: "bi_total B" |
|
523 |
shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp" |
|
524 |
unfolding Domainp_iff[abs_def] by transfer_prover |
|
525 |
||
58182 | 526 |
lemma reflp_transfer[transfer_rule]: |
53952 | 527 |
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp" |
528 |
"right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp" |
|
529 |
"right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp" |
|
530 |
"bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp" |
|
531 |
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp" |
|
58182 | 532 |
using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def |
53952 | 533 |
by fast+ |
534 |
||
535 |
lemma right_unique_transfer [transfer_rule]: |
|
59523 | 536 |
"\<lbrakk> right_total A; right_total B; bi_unique B \<rbrakk> |
537 |
\<Longrightarrow> ((A ===> B ===> op=) ===> implies) right_unique right_unique" |
|
538 |
unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def |
|
53952 | 539 |
by metis |
47325 | 540 |
|
59523 | 541 |
lemma left_total_parametric [transfer_rule]: |
542 |
assumes [transfer_rule]: "bi_total A" "bi_total B" |
|
543 |
shows "((A ===> B ===> op =) ===> op =) left_total left_total" |
|
544 |
unfolding left_total_def[abs_def] by transfer_prover |
|
545 |
||
546 |
lemma right_total_parametric [transfer_rule]: |
|
547 |
assumes [transfer_rule]: "bi_total A" "bi_total B" |
|
548 |
shows "((A ===> B ===> op =) ===> op =) right_total right_total" |
|
549 |
unfolding right_total_def[abs_def] by transfer_prover |
|
550 |
||
551 |
lemma left_unique_parametric [transfer_rule]: |
|
552 |
assumes [transfer_rule]: "bi_unique A" "bi_total A" "bi_total B" |
|
553 |
shows "((A ===> B ===> op =) ===> op =) left_unique left_unique" |
|
554 |
unfolding left_unique_def[abs_def] by transfer_prover |
|
555 |
||
556 |
lemma prod_pred_parametric [transfer_rule]: |
|
557 |
"((A ===> op =) ===> (B ===> op =) ===> rel_prod A B ===> op =) pred_prod pred_prod" |
|
558 |
unfolding pred_prod_def[abs_def] Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps |
|
559 |
by simp transfer_prover |
|
560 |
||
561 |
lemma apfst_parametric [transfer_rule]: |
|
562 |
"((A ===> B) ===> rel_prod A C ===> rel_prod B C) apfst apfst" |
|
563 |
unfolding apfst_def[abs_def] by transfer_prover |
|
564 |
||
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
565 |
lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
566 |
unfolding eq_onp_def rel_fun_def by auto |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
567 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
568 |
lemma rel_fun_eq_onp_rel: |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
569 |
shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
570 |
by (auto simp add: eq_onp_def rel_fun_def) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
571 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
572 |
lemma eq_onp_transfer [transfer_rule]: |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
573 |
assumes [transfer_rule]: "bi_unique A" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
574 |
shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
575 |
unfolding eq_onp_def[abs_def] by transfer_prover |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56520
diff
changeset
|
576 |
|
57599 | 577 |
lemma rtranclp_parametric [transfer_rule]: |
578 |
assumes "bi_unique A" "bi_total A" |
|
579 |
shows "((A ===> A ===> op =) ===> A ===> A ===> op =) rtranclp rtranclp" |
|
580 |
proof(rule rel_funI iffI)+ |
|
581 |
fix R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and R' x y x' y' |
|
582 |
assume R: "(A ===> A ===> op =) R R'" and "A x x'" |
|
583 |
{ |
|
584 |
assume "R\<^sup>*\<^sup>* x y" "A y y'" |
|
585 |
thus "R'\<^sup>*\<^sup>* x' y'" |
|
586 |
proof(induction arbitrary: y') |
|
587 |
case base |
|
588 |
with `bi_unique A` `A x x'` have "x' = y'" by(rule bi_uniqueDr) |
|
589 |
thus ?case by simp |
|
590 |
next |
|
591 |
case (step y z z') |
|
592 |
from `bi_total A` obtain y' where "A y y'" unfolding bi_total_def by blast |
|
593 |
hence "R'\<^sup>*\<^sup>* x' y'" by(rule step.IH) |
|
594 |
moreover from R `A y y'` `A z z'` `R y z` |
|
595 |
have "R' y' z'" by(auto dest: rel_funD) |
|
596 |
ultimately show ?case .. |
|
597 |
qed |
|
598 |
next |
|
599 |
assume "R'\<^sup>*\<^sup>* x' y'" "A y y'" |
|
600 |
thus "R\<^sup>*\<^sup>* x y" |
|
601 |
proof(induction arbitrary: y) |
|
602 |
case base |
|
603 |
with `bi_unique A` `A x x'` have "x = y" by(rule bi_uniqueDl) |
|
604 |
thus ?case by simp |
|
605 |
next |
|
606 |
case (step y' z' z) |
|
607 |
from `bi_total A` obtain y where "A y y'" unfolding bi_total_def by blast |
|
608 |
hence "R\<^sup>*\<^sup>* x y" by(rule step.IH) |
|
609 |
moreover from R `A y y'` `A z z'` `R' y' z'` |
|
610 |
have "R y z" by(auto dest: rel_funD) |
|
611 |
ultimately show ?case .. |
|
612 |
qed |
|
613 |
} |
|
614 |
qed |
|
615 |
||
59523 | 616 |
lemma right_unique_parametric [transfer_rule]: |
617 |
assumes [transfer_rule]: "bi_total A" "bi_unique B" "bi_total B" |
|
618 |
shows "((A ===> B ===> op =) ===> op =) right_unique right_unique" |
|
619 |
unfolding right_unique_def[abs_def] by transfer_prover |
|
620 |
||
47325 | 621 |
end |
53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
622 |
|
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
623 |
end |