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