equal
deleted
inserted
replaced
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 |
|
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))" |
|
41 by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast) |
38 |
42 |
39 lemma antisym_Restr: |
43 lemma antisym_Restr: |
40 "antisym r \<Longrightarrow> antisym(Restr r A)" |
44 "antisym r \<Longrightarrow> antisym(Restr r A)" |
41 unfolding antisym_def Field_def by auto |
45 unfolding antisym_def Field_def by auto |
42 |
46 |