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