equal
deleted
inserted
replaced
48 |
48 |
49 |
49 |
50 lemma well_order_on_Well_order: |
50 lemma well_order_on_Well_order: |
51 "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r" |
51 "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r" |
52 using well_order_on_Field by simp |
52 using well_order_on_Field by simp |
53 |
|
54 |
|
55 lemma Total_Id_Field: |
|
56 assumes TOT: "Total r" and NID: "\<not> (r <= Id)" |
|
57 shows "Field r = Field(r - Id)" |
|
58 using mono_Field[of "r - Id" r] Diff_subset[of r Id] |
|
59 proof(auto) |
|
60 have "r \<noteq> {}" using NID by fast |
|
61 then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by fast |
|
62 hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def) |
|
63 (* *) |
|
64 fix a assume *: "a \<in> Field r" |
|
65 obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a" |
|
66 using * 1 by auto |
|
67 hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT |
|
68 by (simp add: total_on_def) |
|
69 thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast |
|
70 qed |
|
71 |
53 |
72 |
54 |
73 lemma Total_subset_Id: |
55 lemma Total_subset_Id: |
74 assumes TOT: "Total r" and SUB: "r \<le> Id" |
56 assumes TOT: "Total r" and SUB: "r \<le> Id" |
75 shows "r = {} \<or> (\<exists>a. r = {(a,a)})" |
57 shows "r = {} \<or> (\<exists>a. r = {(a,a)})" |