equal
deleted
inserted
replaced
11 |
11 |
12 definition |
12 definition |
13 precedence_le_def: "x \<le> y \<longleftrightarrow> (case (x, y) of |
13 precedence_le_def: "x \<le> y \<longleftrightarrow> (case (x, y) of |
14 (Prc fx sx, Prc fy sy) \<Rightarrow> |
14 (Prc fx sx, Prc fy sy) \<Rightarrow> |
15 fx < fy \<or> (fx \<le> fy \<and> sy \<le> sx))" |
15 fx < fy \<or> (fx \<le> fy \<and> sy \<le> sx))" |
|
16 |
|
17 lemma preced_leI1[intro]: |
|
18 assumes "fx < fy" |
|
19 shows "Prc fx sx \<le> Prc fy sy" |
|
20 using assms |
|
21 by (simp add: precedence_le_def) |
|
22 |
|
23 lemma preced_leI2[intro]: |
|
24 assumes "fx \<le> fy" |
|
25 and "sy \<le> sx" |
|
26 shows "Prc fx sx \<le> Prc fy sy" |
|
27 using assms |
|
28 by (simp add: precedence_le_def) |
16 |
29 |
17 definition |
30 definition |
18 precedence_less_def: "x < y \<longleftrightarrow> (case (x, y) of |
31 precedence_less_def: "x < y \<longleftrightarrow> (case (x, y) of |
19 (Prc fx sx, Prc fy sy) \<Rightarrow> |
32 (Prc fx sx, Prc fy sy) \<Rightarrow> |
20 fx < fy \<or> (fx \<le> fy \<and> sy < sx))" |
33 fx < fy \<or> (fx \<le> fy \<and> sy < sx))" |