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