author | ballarin |
Sat, 28 Mar 2009 22:14:21 +0100 | |
changeset 30780 | c3f1e8a9e0b5 |
parent 30580 | cc5a55d7a5be |
child 30826 | a53f4872400e |
permissions | -rw-r--r-- |
27063 | 1 |
theory Examples2 |
2 |
imports Examples |
|
3 |
begin |
|
4 |
||
5 |
text {* This is achieved by unfolding suitable equations during |
|
6 |
interpretation. These equations are given after the keyword |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
7 |
\isakeyword{where} and require proofs. The revised command |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
8 |
that replaces @{text "\<sqsubset>"} by @{text "<"}, is: *} |
27063 | 9 |
|
30780 | 10 |
interpretation %visible nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" |
27063 | 11 |
where "partial_order.less op \<le> (x::nat) y = (x < y)" |
12 |
proof - |
|
13 |
txt {* The goals are @{subgoals [display]} |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
29293
diff
changeset
|
14 |
The proof that @{text \<le>} is a partial order is as above. *} |
27063 | 15 |
show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)" |
16 |
by unfold_locales auto |
|
17 |
txt {* The second goal is shown by unfolding the |
|
18 |
definition of @{term "partial_order.less"}. *} |
|
19 |
show "partial_order.less op \<le> (x::nat) y = (x < y)" |
|
20 |
unfolding partial_order.less_def [OF `partial_order op \<le>`] |
|
21 |
by auto |
|
22 |
qed |
|
23 |
||
24 |
text {* Note that the above proof is not in the context of a locale. |
|
25 |
Hence, the correct interpretation of @{text |
|
26 |
"partial_order.less_def"} is obtained manually with @{text OF}. |
|
27 |
*} |
|
28 |
||
29 |
end |