| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Tue, 04 Mar 2014 08:45:11 +0000 | |
| changeset 23 | 24e6884d9258 |
| parent 0 | 110247f9d47e |
| child 33 | 9b9f2117561f |
| permissions | -rw-r--r-- |
|
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
header {* Order on product types *}
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
theory Precedence_ord |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
imports Main |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
begin |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
datatype precedence = Prc nat nat |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
instantiation precedence :: order |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
begin |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
definition |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
precedence_le_def: "x \<le> y \<longleftrightarrow> (case (x, y) of |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
(Prc fx sx, Prc fy sy) \<Rightarrow> |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
fx < fy \<or> (fx \<le> fy \<and> sy \<le> sx))" |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
definition |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
precedence_less_def: "x < y \<longleftrightarrow> (case (x, y) of |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
(Prc fx sx, Prc fy sy) \<Rightarrow> |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
fx < fy \<or> (fx \<le> fy \<and> sy < sx))" |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
instance |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
proof |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
qed (auto simp: precedence_le_def precedence_less_def |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
intro: order_trans split:precedence.splits) |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
end |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
instance precedence :: preorder .. |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
instance precedence :: linorder proof |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
qed (auto simp: precedence_le_def precedence_less_def |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
intro: order_trans split:precedence.splits) |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
|
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
end |