author | ballarin |
Thu, 25 Aug 2016 20:08:41 +0200 | |
changeset 63724 | e7df93d4d9b8 |
parent 61566 | c3d6e570ccef |
child 67349 | 0441f2f1b574 |
permissions | -rw-r--r-- |
27063 | 1 |
theory Examples2 |
2 |
imports Examples |
|
3 |
begin |
|
32982 | 4 |
interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61419
diff
changeset
|
5 |
rewrites "int.less x y = (x < y)" |
32981 | 6 |
proof - |
61419 | 7 |
txt \<open>\normalsize The goals are now: |
32983 | 8 |
@{subgoals [display]} |
61419 | 9 |
The proof that~@{text \<le>} is a partial order is as above.\<close> |
32982 | 10 |
show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)" |
32981 | 11 |
by unfold_locales auto |
61419 | 12 |
txt \<open>\normalsize The second goal is shown by unfolding the |
13 |
definition of @{term "partial_order.less"}.\<close> |
|
43543
eb8b4851b039
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
ballarin
parents:
32983
diff
changeset
|
14 |
show "partial_order.less op \<le> x y = (x < y)" |
61419 | 15 |
unfolding partial_order.less_def [OF \<open>partial_order op \<le>\<close>] |
32981 | 16 |
by auto |
17 |
qed |
|
27063 | 18 |
|
61419 | 19 |
text \<open>Note that the above proof is not in the context of the |
32983 | 20 |
interpreted locale. Hence, the premise of @{text |
21 |
"partial_order.less_def"} is discharged manually with @{text OF}. |
|
61419 | 22 |
\<close> |
27063 | 23 |
end |