22 |
22 |
23 |
23 |
24 subsection \<open>Restriction to a set\<close> |
24 subsection \<open>Restriction to a set\<close> |
25 |
25 |
26 abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel" |
26 abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel" |
27 where "Restr r A \<equiv> r Int (A \<times> A)" |
27 where "Restr r A \<equiv> r Int (A \<times> A)" |
28 |
28 |
29 lemma Restr_subset: |
29 lemma Restr_subset: |
30 "A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A" |
30 "A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A" |
31 by blast |
31 by blast |
32 |
32 |
33 lemma Restr_Field: "Restr r (Field r) = r" |
33 lemma Restr_Field: "Restr r (Field r) = r" |
34 unfolding Field_def by auto |
34 unfolding Field_def by auto |
35 |
35 |
36 lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)" |
36 lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)" |
37 unfolding refl_on_def Field_def by auto |
37 unfolding refl_on_def Field_def by auto |
38 |
38 |
39 lemma linear_order_on_Restr: |
39 lemma linear_order_on_Restr: |
40 "linear_order_on A r \<Longrightarrow> linear_order_on (A \<inter> above r x) (Restr r (above r x))" |
40 "linear_order_on A r \<Longrightarrow> linear_order_on (A \<inter> above r x) (Restr r (above r x))" |
41 by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast) |
41 by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast) |
42 |
42 |
43 lemma antisym_Restr: |
43 lemma antisym_Restr: |
44 "antisym r \<Longrightarrow> antisym(Restr r A)" |
44 "antisym r \<Longrightarrow> antisym(Restr r A)" |
45 unfolding antisym_def Field_def by auto |
45 unfolding antisym_def Field_def by auto |
46 |
46 |
47 lemma Total_Restr: |
47 lemma Total_Restr: |
48 "Total r \<Longrightarrow> Total(Restr r A)" |
48 "Total r \<Longrightarrow> Total(Restr r A)" |
49 unfolding total_on_def Field_def by auto |
49 unfolding total_on_def Field_def by auto |
|
50 |
|
51 lemma total_on_imp_Total_Restr: "total_on A r \<Longrightarrow> Total (Restr r A)" |
|
52 by (auto simp: Field_def total_on_def) |
50 |
53 |
51 lemma trans_Restr: |
54 lemma trans_Restr: |
52 "trans r \<Longrightarrow> trans(Restr r A)" |
55 "trans r \<Longrightarrow> trans(Restr r A)" |
53 unfolding trans_def Field_def by blast |
56 unfolding trans_def Field_def by blast |
54 |
57 |
55 lemma Preorder_Restr: |
58 lemma Preorder_Restr: |
56 "Preorder r \<Longrightarrow> Preorder(Restr r A)" |
59 "Preorder r \<Longrightarrow> Preorder(Restr r A)" |
57 unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr) |
60 unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr) |
58 |
61 |
59 lemma Partial_order_Restr: |
62 lemma Partial_order_Restr: |
60 "Partial_order r \<Longrightarrow> Partial_order(Restr r A)" |
63 "Partial_order r \<Longrightarrow> Partial_order(Restr r A)" |
61 unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr) |
64 unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr) |
62 |
65 |
63 lemma Linear_order_Restr: |
66 lemma Linear_order_Restr: |
64 "Linear_order r \<Longrightarrow> Linear_order(Restr r A)" |
67 "Linear_order r \<Longrightarrow> Linear_order(Restr r A)" |
65 unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr) |
68 unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr) |
66 |
69 |
67 lemma Well_order_Restr: |
70 lemma Well_order_Restr: |
68 assumes "Well_order r" |
71 assumes "Well_order r" |
69 shows "Well_order(Restr r A)" |
72 shows "Well_order(Restr r A)" |
70 proof- |
73 proof- |
71 have "Restr r A - Id \<le> r - Id" using Restr_subset by blast |
74 have "Restr r A - Id \<le> r - Id" using Restr_subset by blast |
72 hence "wf(Restr r A - Id)" using assms |
75 hence "wf(Restr r A - Id)" using assms |
73 using well_order_on_def wf_subset by blast |
76 using well_order_on_def wf_subset by blast |
74 thus ?thesis using assms unfolding well_order_on_def |
77 thus ?thesis using assms unfolding well_order_on_def |
75 by (simp add: Linear_order_Restr) |
78 by (simp add: Linear_order_Restr) |
76 qed |
79 qed |
77 |
80 |
78 lemma Field_Restr_subset: "Field(Restr r A) \<le> A" |
81 lemma Field_Restr_subset: "Field(Restr r A) \<le> A" |
79 by (auto simp add: Field_def) |
82 by (auto simp add: Field_def) |
80 |
83 |
81 lemma Refl_Field_Restr: |
84 lemma Refl_Field_Restr: |
82 "Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A" |
85 "Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A" |
83 unfolding refl_on_def Field_def by blast |
86 unfolding refl_on_def Field_def by blast |
84 |
87 |
85 lemma Refl_Field_Restr2: |
88 lemma Refl_Field_Restr2: |
86 "\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A" |
89 "\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A" |
87 by (auto simp add: Refl_Field_Restr) |
90 by (auto simp add: Refl_Field_Restr) |
88 |
91 |
89 lemma well_order_on_Restr: |
92 lemma well_order_on_Restr: |
90 assumes WELL: "Well_order r" and SUB: "A \<le> Field r" |
93 assumes WELL: "Well_order r" and SUB: "A \<le> Field r" |
91 shows "well_order_on A (Restr r A)" |
94 shows "well_order_on A (Restr r A)" |
92 using assms |
95 using assms |
93 using Well_order_Restr[of r A] Refl_Field_Restr2[of r A] |
96 using Well_order_Restr[of r A] Refl_Field_Restr2[of r A] |
94 order_on_defs[of "Field r" r] by auto |
97 order_on_defs[of "Field r" r] by auto |
95 |
98 |
96 |
99 |
97 subsection \<open>Order filters versus restrictions and embeddings\<close> |
100 subsection \<open>Order filters versus restrictions and embeddings\<close> |
98 |
101 |
99 lemma Field_Restr_ofilter: |
102 lemma Field_Restr_ofilter: |