src/Doc/Locales/Examples2.thy
 author haftmann Mon Feb 06 20:56:34 2017 +0100 (2017-02-06) changeset 64990 c6a7de505796 parent 61566 c3d6e570ccef child 67349 0441f2f1b574 permissions -rw-r--r--
more explicit errors in pathological cases
```     1 theory Examples2
```
```     2 imports Examples
```
```     3 begin
```
```     4   interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
```
```     5     rewrites "int.less x y = (x < y)"
```
```     6   proof -
```
```     7     txt \<open>\normalsize The goals are now:
```
```     8       @{subgoals [display]}
```
```     9       The proof that~@{text \<le>} is a partial order is as above.\<close>
```
```    10     show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
```
```    11       by unfold_locales auto
```
```    12     txt \<open>\normalsize The second goal is shown by unfolding the
```
```    13       definition of @{term "partial_order.less"}.\<close>
```
```    14     show "partial_order.less op \<le> x y = (x < y)"
```
```    15       unfolding partial_order.less_def [OF \<open>partial_order op \<le>\<close>]
```
```    16       by auto
```
```    17   qed
```
```    18
```
```    19 text \<open>Note that the above proof is not in the context of the
```
```    20   interpreted locale.  Hence, the premise of @{text
```
```    21   "partial_order.less_def"} is discharged manually with @{text OF}.
```
```    22 \<close>
```
```    23 end
```