27063
|
1 |
theory Examples2
|
|
2 |
imports Examples
|
|
3 |
begin
|
32981
|
4 |
text {* \vspace{-5ex} *}
|
32982
|
5 |
interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
|
|
6 |
where "partial_order.less op \<le> (x::int) y = (x < y)"
|
32981
|
7 |
proof -
|
32983
|
8 |
txt {* \normalsize The goals are now:
|
|
9 |
@{subgoals [display]}
|
|
10 |
The proof that~@{text \<le>} is a partial order is as above. *}
|
32982
|
11 |
show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
|
32981
|
12 |
by unfold_locales auto
|
|
13 |
txt {* \normalsize The second goal is shown by unfolding the
|
|
14 |
definition of @{term "partial_order.less"}. *}
|
32982
|
15 |
show "partial_order.less op \<le> (x::int) y = (x < y)"
|
32981
|
16 |
unfolding partial_order.less_def [OF `partial_order op \<le>`]
|
|
17 |
by auto
|
|
18 |
qed
|
27063
|
19 |
|
32981
|
20 |
text {* Note that the above proof is not in the context of the
|
32983
|
21 |
interpreted locale. Hence, the premise of @{text
|
|
22 |
"partial_order.less_def"} is discharged manually with @{text OF}.
|
27063
|
23 |
*}
|
|
24 |
end
|