src/Doc/IsarImplementation/Logic.thy
changeset 52406 1e57c3c4e05c
parent 50126 3dec88149176
child 52407 e4662afb3483
     1.1 --- a/src/Doc/IsarImplementation/Logic.thy	Fri Jun 21 16:21:33 2013 -0700
     1.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Thu Jun 13 17:40:58 2013 +0200
     1.3 @@ -932,6 +932,72 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsection {* Sort hypotheses *}
     1.8 +
     1.9 +text {* Type variables are decorated with sorts, as explained in
    1.10 +  \secref{sec:types}.  This constrains type instantiation to certain
    1.11 +  ranges of types: variable @{text "\<alpha>\<^sub>s"} may only be assigned to types
    1.12 +  @{text "\<tau>"} that belong to sort @{text "s"}.  Within the logic, sort
    1.13 +  constraints act like implicit preconditions on the result @{text
    1.14 +  "\<lparr>\<alpha>\<^sub>1 : s\<^sub>1\<rparr>, \<dots>, \<lparr>\<alpha>\<^sub>n : s\<^sub>n\<rparr>, \<Gamma> \<turnstile> \<phi>"} where the type variables @{text
    1.15 +  "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} cover the propositions @{text "\<Gamma>"}, @{text "\<phi>"}, as
    1.16 +  well as the proof of @{text "\<Gamma> \<turnstile> \<phi>"}.
    1.17 +
    1.18 +  These \emph{sort hypothesis} of a theorem are passed monotonically
    1.19 +  through further derivations.  They are redundant, as long as the
    1.20 +  statement of a theorem still contains the type variables that are
    1.21 +  accounted here.  The logical significance of sort hypotheses is
    1.22 +  limited to the boundary case where type variables disappear from the
    1.23 +  proposition, e.g.\ @{text "\<lparr>\<alpha>\<^sub>s : s\<rparr> \<turnstile> \<phi>"}.  Since such dangling type
    1.24 +  variables can be renamed arbitrarily without changing the
    1.25 +  proposition @{text "\<phi>"}, the inference kernel maintains sort
    1.26 +  hypotheses in anonymous form @{text "s \<turnstile> \<phi>"}.
    1.27 +
    1.28 +  In most practical situations, such extra sort hypotheses may be
    1.29 +  stripped in a final bookkeeping step, e.g.\ at the end of a proof:
    1.30 +  they are typically left over from intermediate reasoning with type
    1.31 +  classes that can be satisfied by some concrete type @{text "\<tau>"} of
    1.32 +  sort @{text "s"} to replace the hypothetical type variable @{text
    1.33 +  "\<alpha>\<^sub>s"}.  *}
    1.34 +
    1.35 +text %mlref {*
    1.36 +  \begin{mldecls}
    1.37 +  @{index_ML Thm.extra_shyps: "thm -> sort list"} \\
    1.38 +  @{index_ML Thm.strip_shyps: "thm -> thm"} \\
    1.39 +  \end{mldecls}
    1.40 +
    1.41 +  \begin{description}
    1.42 +
    1.43 +  \item @{ML Thm.extra_shyps}~@{text "thm"} determines the extraneous
    1.44 +  sort hypotheses of the given theorem, i.e.\ the sorts that are not
    1.45 +  present within type variables of the statement.
    1.46 +
    1.47 +  \item @{ML Thm.strip_shyps}~@{text "thm"} removes any extraneous
    1.48 +  sort hypotheses that can be witnessed from the type signature.
    1.49 +
    1.50 +  \end{description}
    1.51 +*}
    1.52 +
    1.53 +text %mlex {* The following artificial example demonstrates the
    1.54 +  derivation of @{prop False} with a pending sort hypothesis involving
    1.55 +  a logically empty sort.  *}
    1.56 +
    1.57 +class empty =
    1.58 +  assumes bad: "\<And>(x::'a) y. x \<noteq> y"
    1.59 +
    1.60 +theorem (in empty) false: False
    1.61 +  using bad by blast
    1.62 +
    1.63 +ML {*
    1.64 +  @{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])
    1.65 +*}
    1.66 +
    1.67 +text {* Thanks to the inference kernel managing sort hypothesis
    1.68 +  according to their logical significance, this example is merely an
    1.69 +  instance of \emph{ex falso quodlibet consequitur} --- not a collapse
    1.70 +  of the logical framework! *}
    1.71 +
    1.72 +
    1.73  section {* Object-level rules \label{sec:obj-rules} *}
    1.74  
    1.75  text {*