| author | zhangx |
| Thu, 28 Jan 2016 07:43:05 +0800 | |
| changeset 85 | d239aa953315 |
| parent 65 | 633b1fc8631b |
| permissions | -rw-r--r-- |
|
65
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
1 |
header {* Order on product types *}
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
2 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
3 |
theory Precedence_ord |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
4 |
imports Main |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
5 |
begin |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
6 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
7 |
datatype precedence = Prc nat nat |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
8 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
9 |
instantiation precedence :: order |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
10 |
begin |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
11 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
12 |
definition |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
13 |
precedence_le_def: "x \<le> y \<longleftrightarrow> (case (x, y) of |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
14 |
(Prc fx sx, Prc fy sy) \<Rightarrow> |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
15 |
fx < fy \<or> (fx \<le> fy \<and> sy \<le> sx))" |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
16 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
17 |
definition |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
18 |
precedence_less_def: "x < y \<longleftrightarrow> (case (x, y) of |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
19 |
(Prc fx sx, Prc fy sy) \<Rightarrow> |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
20 |
fx < fy \<or> (fx \<le> fy \<and> sy < sx))" |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
21 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
22 |
instance |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
23 |
proof |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
24 |
qed (auto simp: precedence_le_def precedence_less_def |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
25 |
intro: order_trans split:precedence.splits) |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
26 |
end |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
27 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
28 |
instance precedence :: preorder .. |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
29 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
30 |
instance precedence :: linorder |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
31 |
proof |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
32 |
qed (auto simp: precedence_le_def precedence_less_def |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
33 |
intro: order_trans split:precedence.splits) |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
34 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
35 |
instantiation precedence :: zero |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
36 |
begin |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
37 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
38 |
definition Zero_precedence_def: |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
39 |
"0 = Prc 0 0" |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
40 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
41 |
instance .. |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
42 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
43 |
end |
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
44 |
|
|
633b1fc8631b
Reorganization completed, added "scripts_structure.pdf" and "scirpts_structure.pptx".
zhangx
parents:
diff
changeset
|
45 |
end |