36 lemma left_totalE: |
36 lemma left_totalE: |
37 assumes "left_total R" |
37 assumes "left_total R" |
38 obtains "(\<And>x. \<exists>y. R x y)" |
38 obtains "(\<And>x. \<exists>y. R x y)" |
39 using assms unfolding left_total_def by blast |
39 using assms unfolding left_total_def by blast |
40 |
40 |
|
41 lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)" |
|
42 unfolding left_total_def right_total_def bi_total_def by blast |
|
43 |
41 lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R" |
44 lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R" |
42 by(simp add: left_total_def right_total_def bi_total_def) |
45 by(simp add: left_total_def right_total_def bi_total_def) |
43 |
46 |
44 definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
47 definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
45 where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" |
48 where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" |
|
49 |
|
50 lemma left_unique_transfer [transfer_rule]: |
|
51 assumes [transfer_rule]: "right_total A" |
|
52 assumes [transfer_rule]: "right_total B" |
|
53 assumes [transfer_rule]: "bi_unique A" |
|
54 shows "((A ===> B ===> op=) ===> implies) left_unique left_unique" |
|
55 using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def |
|
56 by metis |
|
57 |
|
58 lemma bi_unique_iff: "bi_unique A = (right_unique A \<and> left_unique A)" |
|
59 unfolding left_unique_def right_unique_def bi_unique_def by blast |
46 |
60 |
47 lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R" |
61 lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R" |
48 by(auto simp add: left_unique_def right_unique_def bi_unique_def) |
62 by(auto simp add: left_unique_def right_unique_def bi_unique_def) |
49 |
63 |
50 lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A" |
64 lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A" |
284 |
298 |
285 lemma invariant_same_args: |
299 lemma invariant_same_args: |
286 shows "invariant P x x \<equiv> P x" |
300 shows "invariant P x x \<equiv> P x" |
287 using assms by (auto simp add: invariant_def) |
301 using assms by (auto simp add: invariant_def) |
288 |
302 |
|
303 lemma invariant_transfer [transfer_rule]: |
|
304 assumes [transfer_rule]: "bi_unique A" |
|
305 shows "((A ===> op=) ===> A ===> A ===> op=) Lifting.invariant Lifting.invariant" |
|
306 unfolding invariant_def[abs_def] by transfer_prover |
|
307 |
289 lemma UNIV_typedef_to_Quotient: |
308 lemma UNIV_typedef_to_Quotient: |
290 assumes "type_definition Rep Abs UNIV" |
309 assumes "type_definition Rep Abs UNIV" |
291 and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |
310 and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |
292 shows "Quotient (op =) Abs Rep T" |
311 shows "Quotient (op =) Abs Rep T" |
293 proof - |
312 proof - |