--- a/NEWS Fri Sep 25 16:54:31 2015 +0200
+++ b/NEWS Fri Sep 25 23:41:24 2015 +0200
@@ -177,6 +177,9 @@
*** Pure ***
+* Command 'print_definitions' prints dependencies of definitional
+specifications. This functionality used to be part of 'print_theory'.
+
* The vacuous fact "TERM x" may be established "by fact" or as `TERM x`
as well, not just "by this" or "." as before.
@@ -194,6 +197,13 @@
*** HOL ***
+* The 'typedef' command has been upgraded from a partially checked
+"axiomatization", to a full definitional specification that takes the
+global collection of overloaded constant / type definitions into
+account. Type definitions with open dependencies on overloaded
+definitions need to be specified as "typedef (overloaded)". This
+provides extra robustness in theory construction. Rare INCOMPATIBILITY.
+
* Qualification of various formal entities in the libraries is done more
uniformly via "context begin qualified definition ... end" instead of
old-style "hide_const (open) ...". Consequently, both the defined
@@ -319,6 +329,10 @@
*** ML ***
+* The auxiliary module Pure/display.ML has been eliminated. Its
+elementary thm print operations are now in Pure/more_thm.ML and thus
+called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.
+
* Simproc programming interfaces have been simplified:
Simplifier.make_simproc and Simplifier.define_simproc supersede various
forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that
--- a/src/Doc/Implementation/Logic.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy Fri Sep 25 23:41:24 2015 +0200
@@ -662,12 +662,12 @@
binding * term -> theory -> (string * thm) * theory"} \\
@{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
(string * ('a -> thm)) * theory"} \\
- @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->
+ @{index_ML Thm.add_def: "Defs.context -> bool -> bool ->
binding * term -> theory -> (string * thm) * theory"} \\
\end{mldecls}
\begin{mldecls}
- @{index_ML Theory.add_deps: "Proof.context -> string ->
- string * typ -> (string * typ) list -> theory -> theory"} \\
+ @{index_ML Theory.add_deps: "Defs.context -> string ->
+ Defs.entry -> Defs.entry list -> theory -> theory"} \\
\end{mldecls}
\begin{description}
@@ -766,7 +766,7 @@
\item @{ML Theory.add_deps}~@{text "ctxt name c\<^sub>\<tau> \<^vec>d\<^sub>\<sigma>"}
declares dependencies of a named specification for constant @{text
"c\<^sub>\<tau>"}, relative to existing specifications for constants @{text
- "\<^vec>d\<^sub>\<sigma>"}.
+ "\<^vec>d\<^sub>\<sigma>"}. This also works for type constructors.
\end{description}
\<close>
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Sep 25 23:41:24 2015 +0200
@@ -932,7 +932,7 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) record} @{syntax typespec_sorts} '=' \<newline>
+ @@{command (HOL) record} @{syntax "overloaded"}? @{syntax typespec_sorts} '=' \<newline>
(@{syntax type} '+')? (constdecl +)
;
constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
@@ -1100,61 +1100,90 @@
text \<open>See @{file "~~/src/HOL/ex/Records.thy"}, for example.\<close>
-section \<open>Typedef axiomatization \label{sec:hol-typedef}\<close>
+section \<open>Semantic subtype definitions \label{sec:hol-typedef}\<close>
text \<open>
\begin{matharray}{rcl}
@{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
\end{matharray}
- A Gordon/HOL-style type definition is a certain axiom scheme that
- identifies a new type with a subset of an existing type. More
- precisely, the new type is defined by exhibiting an existing type
- @{text \<tau>}, a set @{text "A :: \<tau> set"}, and a theorem that proves
- @{prop "\<exists>x. x \<in> A"}. Thus @{text A} is a non-empty subset of @{text
- \<tau>}, and the new type denotes this subset. New functions are
- postulated that establish an isomorphism between the new type and
- the subset. In general, the type @{text \<tau>} may involve type
- variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} which means that the type definition
- produces a type constructor @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} depending on
- those type arguments.
-
- The axiomatization can be considered a ``definition'' in the sense of the
- particular set-theoretic interpretation of HOL @{cite pitts93}, where the
- universe of types is required to be downwards-closed wrt.\ arbitrary
- non-empty subsets. Thus genuinely new types introduced by @{command
- "typedef"} stay within the range of HOL models by construction.
-
- In contrast, the command @{command_ref type_synonym} from Isabelle/Pure
- merely introduces syntactic abbreviations, without any logical
- significance. Thus it is more faithful to the idea of a genuine type
- definition, but less powerful in practice.
+ A type definition identifies a new type with a non-empty subset of an
+ existing type. More precisely, the new type is defined by exhibiting an
+ existing type @{text \<tau>}, a set @{text "A :: \<tau> set"}, and proving @{prop
+ "\<exists>x. x \<in> A"}. Thus @{text A} is a non-empty subset of @{text \<tau>}, and the
+ new type denotes this subset. New functions are postulated that establish
+ an isomorphism between the new type and the subset. In general, the type
+ @{text \<tau>} may involve type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} which means
+ that the type definition produces a type constructor @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n)
+ t"} depending on those type arguments.
@{rail \<open>
- @@{command (HOL) typedef} abs_type '=' rep_set
+ @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set
+ ;
+ @{syntax_def "overloaded"}: ('(' @'overloaded' ')')
;
abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
;
rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
\<close>}
+ To understand the concept of type definition better, we need to recount
+ its somewhat complex history. The HOL logic goes back to the ``Simple
+ Theory of Types'' (STT) of A. Church @{cite "church40"}, which is further
+ explained in the book by P. Andrews @{cite "andrews86"}. The overview
+ article by W. Farmer @{cite "Farmer:2008"} points out the ``seven
+ virtues'' of this relatively simple family of logics. STT has only ground
+ types, without polymorphism and without type definitions.
+
+ \medskip M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by
+ adding schematic polymorphism (type variables and type constructors) and a
+ facility to introduce new types as semantic subtypes from existing types.
+ This genuine extension of the logic was explained semantically by A. Pitts
+ in the book of the original Cambridge HOL88 system @{cite "pitts93"}. Type
+ definitions work in this setting, because the general model-theory of STT
+ is restricted to models that ensure that the universe of type
+ interpretations is closed by forming subsets (via predicates taken from
+ the logic).
+
+ \medskip Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded
+ constant definitions @{cite "Wenzel:1997:TPHOL" and
+ "Haftmann-Wenzel:2006:classes"}, which are actually a concept of
+ Isabelle/Pure and do not depend on particular set-theoretic semantics of
+ HOL. Over many years, there was no formal checking of semantic type
+ definitions in Isabelle/HOL versus syntactic constant definitions in
+ Isabelle/Pure. So the @{command typedef} command was described as
+ ``axiomatic'' in the sense of \secref{sec:axiomatizations}, only with some
+ local checks of the given type and its representing set.
+
+ Recent clarification of overloading in the HOL logic proper @{cite
+ "Kuncar-Popescu:2015"} demonstrate how the dissimilar concepts of constant
+ definitions versus type definitions may be understood uniformly. This
+ requires an interpretation of Isabelle/HOL that substantially reforms the
+ set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic
+ view on polymorphism and interpreting only ground types in the
+ set-theoretic sense of HOL88. Moreover, type-constructors may be
+ explicitly overloaded, e.g.\ by making the subset depend on type-class
+ parameters (cf.\ \secref{sec:class}). This is semantically like a
+ dependent type: the meaning relies on the operations provided by different
+ type-class instances.
+
\begin{description}
- \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} produces an
- axiomatization (\secref{sec:axiomatizations}) for a type definition in the
- background theory of the current context, depending on a non-emptiness
- result of the set @{text A} that needs to be proven here. The set @{text
- A} may contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} as specified on the
- LHS, but no term variables.
-
- Even though a local theory specification, the newly introduced type
- constructor cannot depend on parameters or assumptions of the
- context: this is structurally impossible in HOL. In contrast, the
- non-emptiness proof may use local assumptions in unusual situations,
- which could result in different interpretations in target contexts:
- the meaning of the bijection between the representing set @{text A}
- and the new type @{text t} may then change in different application
- contexts.
+ \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} defines a
+ new type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} from the set @{text A} over an existing
+ type. The set @{text A} may contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"}
+ as specified on the LHS, but no term variables. Non-emptiness of @{text A}
+ needs to be proven on the spot, in order to turn the internal conditional
+ characterization into usable theorems.
+
+ The ``@{text "(overloaded)"}'' option allows the @{command
+ "typedef"} specification to depend on constants that are not (yet)
+ specified and thus left open as parameters, e.g.\ type-class parameters.
+
+ Within a local theory specification, the newly introduced type constructor
+ cannot depend on parameters or assumptions of the context: this is
+ syntactically impossible in HOL. The non-emptiness proof may formally
+ depend on local assumptions, but this has little practical relevance.
For @{command (HOL) "typedef"}~@{text "t = A"} the newly introduced
type @{text t} is accompanied by a pair of morphisms to relate it to
@@ -1163,11 +1192,11 @@
Abs_t}: An explicit @{keyword (HOL) "morphisms"} specification
allows to provide alternative names.
- The core axiomatization uses the locale predicate @{const
- type_definition} as defined in Isabelle/HOL. Various basic
- consequences of that are instantiated accordingly, re-using the
- locale facts with names derived from the new type constructor. Thus
- the generic @{thm type_definition.Rep} is turned into the specific
+ The logical characterization of @{command typedef} uses the predicate of
+ locale @{const type_definition} that is defined in Isabelle/HOL. Various
+ basic consequences of that are instantiated accordingly, re-using the
+ locale facts with names derived from the new type constructor. Thus the
+ generic theorem @{thm type_definition.Rep} is turned into the specific
@{text "Rep_t"}, for example.
Theorems @{thm type_definition.Rep}, @{thm
@@ -1191,27 +1220,8 @@
subsubsection \<open>Examples\<close>
-text \<open>Type definitions permit the introduction of abstract data
- types in a safe way, namely by providing models based on already
- existing types. Given some abstract axiomatic description @{text P}
- of a type, this involves two steps:
-
- \begin{enumerate}
-
- \item Find an appropriate type @{text \<tau>} and subset @{text A} which
- has the desired properties @{text P}, and make a type definition
- based on this representation.
-
- \item Prove that @{text P} holds for @{text \<tau>} by lifting @{text P}
- from the representation.
-
- \end{enumerate}
-
- You can later forget about the representation and work solely in
- terms of the abstract properties @{text P}.
-
- \medskip The following trivial example pulls a three-element type
- into existence within the formal logical environment of HOL.\<close>
+text \<open>The following trivial example pulls a three-element type into
+existence within the formal logical environment of Isabelle/HOL.\<close>
(*<*)experiment begin(*>*)
typedef three = "{(True, True), (True, False), (False, True)}"
@@ -1299,8 +1309,9 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) quotient_type} @{syntax typespec} @{syntax mixfix}? '='
- quot_type \<newline> quot_morphisms? quot_parametric?
+ @@{command (HOL) quotient_type} @{syntax "overloaded"}? \<newline>
+ @{syntax typespec} @{syntax mixfix}? '=' quot_type \<newline>
+ quot_morphisms? quot_parametric?
;
quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term}
;
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Sep 25 23:41:24 2015 +0200
@@ -462,6 +462,7 @@
text \<open>
\begin{matharray}{rcl}
@{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_definitions"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -475,6 +476,7 @@
@{rail \<open>
(@@{command print_theory} |
+ @@{command print_definitions} |
@@{command print_methods} |
@@{command print_attributes} |
@@{command print_theorems} |
@@ -504,6 +506,12 @@
\item @{command "print_theory"} prints the main logical content of the
background theory; the ``@{text "!"}'' option indicates extra verbosity.
+ \item @{command "print_definitions"} prints dependencies of definitional
+ specifications within the background theory, which may be constants
+ \secref{sec:consts} or types (\secref{sec:types-pure},
+ \secref{sec:hol-typedef}); the ``@{text "!"}'' option indicates extra
+ verbosity.
+
\item @{command "print_methods"} prints all proof methods available in the
current theory context; the ``@{text "!"}'' option indicates extra
verbosity.
--- a/src/Doc/manual.bib Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Doc/manual.bib Fri Sep 25 23:41:24 2015 +0200
@@ -601,6 +601,17 @@
year = 1993,
pages = {213-248}}
+@article{Farmer:2008,
+ author = {William M. Farmer},
+ title = {The seven virtues of simple type theory},
+ journal = {J. Applied Logic},
+ volume = {6},
+ number = {3},
+ pages = {267--286},
+ year = {2008},
+ url = {http://dx.doi.org/10.1016/j.jal.2007.11.001},
+}
+
@InProceedings{felty91a,
Author = {Amy Felty},
Title = {A Logic Program for Transforming Sequent Proofs to Natural
@@ -679,6 +690,14 @@
publisher = CUP,
note = {Translated by Yves Lafont and Paul Taylor}}
+@TechReport{Gordon:1985:HOL,
+ author = {M. J. C. Gordon},
+ title = {{HOL}: A machine oriented formulation of higher order logic},
+ institution = {University of Cambridge Computer Laboratory},
+ year = 1985,
+ number = 68
+}
+
@Book{mgordon-hol,
editor = {M. J. C. Gordon and T. F. Melham},
title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
@@ -978,6 +997,20 @@
note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
}
+@inproceedings{Kuncar-Popescu:2015,
+ author = {Ondrej Kuncar and Andrei Popescu},
+ title = {A Consistent Foundation for {Isabelle/HOL}},
+ editor = {Christian Urban and Xingyuan Zhang},
+ booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP}
+ 2015, Nanjing, China, August 24-27, 2015, Proceedings},
+ year = {2015},
+ url = {http://dx.doi.org/10.1007/978-3-319-22102-1_16},
+ series = {Lecture Notes in Computer Science},
+ volume = {9236},
+ publisher = {Springer},
+ year = {2015},
+}
+
@Book{kunen80,
author = {Kenneth Kunen},
title = {Set Theory: An Introduction to Independence Proofs},
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Sep 25 23:41:24 2015 +0200
@@ -151,7 +151,7 @@
fun check_syntax ctxt thm expected =
let
val obtained =
- Print_Mode.setmp [] (Display.string_of_thm (Config.put show_markup false ctxt)) thm;
+ Print_Mode.setmp [] (Thm.string_of_thm (Config.put show_markup false ctxt)) thm;
in
if obtained <> expected
then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
--- a/src/FOLP/classical.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/FOLP/classical.ML Fri Sep 25 23:41:24 2015 +0200
@@ -124,10 +124,10 @@
fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) =
writeln (cat_lines
- (["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @
- ["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @
- ["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @
- ["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs));
+ (["Introduction rules"] @ map (Thm.string_of_thm ctxt) hazIs @
+ ["Safe introduction rules"] @ map (Thm.string_of_thm ctxt) safeIs @
+ ["Elimination rules"] @ map (Thm.string_of_thm ctxt) hazEs @
+ ["Safe elimination rules"] @ map (Thm.string_of_thm ctxt) safeEs));
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
--- a/src/FOLP/simp.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/FOLP/simp.ML Fri Sep 25 23:41:24 2015 +0200
@@ -306,8 +306,8 @@
fun print_ss ctxt (SS{congs,simps,...}) =
writeln (cat_lines
- (["Congruences:"] @ map (Display.string_of_thm ctxt) congs @
- ["Rewrite Rules:"] @ map (Display.string_of_thm ctxt o #1) simps));
+ (["Congruences:"] @ map (Thm.string_of_thm ctxt) congs @
+ ["Rewrite Rules:"] @ map (Thm.string_of_thm ctxt o #1) simps));
(* Rewriting with conditionals *)
--- a/src/HOL/Datatype_Examples/Misc_N2M.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Datatype_Examples/Misc_N2M.thy Fri Sep 25 23:41:24 2015 +0200
@@ -11,6 +11,9 @@
imports "~~/src/HOL/Library/BNF_Axiomatization"
begin
+declare [[typedef_overloaded]]
+
+
locale misc
begin
--- a/src/HOL/Datatype_Examples/Stream_Processor.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Datatype_Examples/Stream_Processor.thy Fri Sep 25 23:41:24 2015 +0200
@@ -12,6 +12,9 @@
imports "~~/src/HOL/Library/Stream" "~~/src/HOL/Library/BNF_Axiomatization"
begin
+declare [[typedef_overloaded]]
+
+
section {* Continuous Functions on Streams *}
datatype ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
--- a/src/HOL/Eisbach/Eisbach_Tools.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy Fri Sep 25 23:41:24 2015 +0200
@@ -31,7 +31,7 @@
(Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms)
(fn ctxt => fn (tok, thms) =>
(* FIXME proper formatting!? *)
- Token.unparse tok ^ ": " ^ commas (map (Display.string_of_thm ctxt) thms)) #>
+ Token.unparse tok ^ ": " ^ commas (map (Thm.string_of_thm ctxt) thms)) #>
setup_trace_method @{binding print_term}
(Scan.lift (Scan.ahead Parse.not_eof) -- Args.term)
(fn ctxt => fn (tok, t) =>
--- a/src/HOL/HOLCF/Porder.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/HOLCF/Porder.thy Fri Sep 25 23:41:24 2015 +0200
@@ -8,6 +8,9 @@
imports Main
begin
+declare [[typedef_overloaded]]
+
+
subsection {* Type class for partial orders *}
class below =
--- a/src/HOL/HOLCF/Tools/cpodef.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Fri Sep 25 23:41:24 2015 +0200
@@ -165,7 +165,7 @@
let
val name = #1 typ
val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
- |> Typedef.add_typedef_global typ set opt_bindings tac
+ |> Typedef.add_typedef_global {overloaded = false} typ set opt_bindings tac
val oldT = #rep_type (#1 info)
val newT = #abs_type (#1 info)
val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
--- a/src/HOL/IMP/Abs_State.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/IMP/Abs_State.thy Fri Sep 25 23:41:24 2015 +0200
@@ -19,7 +19,7 @@
hide_type st --"hide previous def to avoid long names"
-quotient_type 'a st = "('a::top) st_rep" / eq_st
+quotient_type (overloaded) 'a st = "('a::top) st_rep" / eq_st
morphisms rep_st St
by (metis eq_st_def equivpI reflpI sympI transpI)
--- a/src/HOL/Import/import_rule.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Import/import_rule.ML Fri Sep 25 23:41:24 2015 +0200
@@ -222,7 +222,8 @@
Typedef.make_morphisms (Binding.name tycname)
(SOME (Binding.name rep_name, Binding.name abs_name))
val ((_, typedef_info), thy') =
- Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
+ Typedef.add_typedef_global {overloaded = false}
+ (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
(SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy
val aty = #abs_type (#1 typedef_info)
val th = freezeT thy' (#type_definition (#2 typedef_info))
--- a/src/HOL/Library/Fraction_Field.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Fri Sep 25 23:41:24 2015 +0200
@@ -47,7 +47,7 @@
end
-quotient_type 'a fract = "'a :: idom \<times> 'a" / partial: "fractrel"
+quotient_type (overloaded) 'a fract = "'a :: idom \<times> 'a" / partial: "fractrel"
by(rule part_equivp_fractrel)
subsubsection \<open>Representation and basic operations\<close>
--- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Sep 25 23:41:24 2015 +0200
@@ -21,7 +21,7 @@
fun drop_fact_warning ctxt =
Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
- Display.string_of_thm ctxt)
+ Thm.string_of_thm ctxt)
(* general theorem normalizations *)
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Sep 25 23:41:24 2015 +0200
@@ -105,7 +105,7 @@
fun trace_assms ctxt =
Old_SMT_Config.trace_msg ctxt (Pretty.string_of o
- Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
+ Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd))
fun trace_recon_data ({context=ctxt, typs, terms, ...} : Old_SMT_Translate.recon) =
let
@@ -327,7 +327,7 @@
if Config.get ctxt Old_SMT_Config.trace_used_facts andalso length wthms > 0
then
tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
- (map (Display.pretty_thm ctxt o snd) wthms)))
+ (map (Thm.pretty_thm ctxt o snd) wthms)))
else ()
end
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Sep 25 23:41:24 2015 +0200
@@ -72,7 +72,7 @@
fun pretty_goal ctxt thms t =
[Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
|> not (null thms) ? cons (Pretty.big_list "assumptions:"
- (map (Display.pretty_thm ctxt) thms))
+ (map (Thm.pretty_thm ctxt) thms))
fun try_apply ctxt thms =
let
--- a/src/HOL/Library/Polynomial.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy Fri Sep 25 23:41:24 2015 +0200
@@ -52,7 +52,7 @@
subsection \<open>Definition of type @{text poly}\<close>
-typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
+typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
setup_lifting type_definition_poly
--- a/src/HOL/Library/Quotient_Type.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Library/Quotient_Type.thy Fri Sep 25 23:41:24 2015 +0200
@@ -62,7 +62,7 @@
definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
-typedef 'a quot = "quot :: 'a::eqv set set"
+typedef (overloaded) 'a quot = "quot :: 'a::eqv set set"
unfolding quot_def by blast
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
--- a/src/HOL/Library/RBT.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Library/RBT.thy Fri Sep 25 23:41:24 2015 +0200
@@ -10,7 +10,7 @@
subsection \<open>Type definition\<close>
-typedef ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}"
+typedef (overloaded) ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}"
morphisms impl_of RBT
proof -
have "RBT_Impl.Empty \<in> ?rbt" by simp
--- a/src/HOL/Library/Saturated.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Library/Saturated.thy Fri Sep 25 23:41:24 2015 +0200
@@ -12,7 +12,7 @@
subsection \<open>The type of saturated naturals\<close>
-typedef ('a::len) sat = "{.. len_of TYPE('a)}"
+typedef (overloaded) ('a::len) sat = "{.. len_of TYPE('a)}"
morphisms nat_of Abs_sat
by auto
--- a/src/HOL/Library/bnf_axiomatization.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML Fri Sep 25 23:41:24 2015 +0200
@@ -35,9 +35,9 @@
fun mk_b name user_b =
(if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
|> Binding.qualify false (Binding.name_of b);
- val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy;
- val (bd_type_Tname, lthy) =
- Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
+ val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy;
+ val (bd_type_Tname, lthy) = lthy
+ |> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn);
val T = Type (Tname, map TFree vars);
val bd_type_T = Type (bd_type_Tname, map TFree deads);
val lives = map TFree (filter_out (member (op =) deads) vars);
--- a/src/HOL/Library/old_recdef.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Fri Sep 25 23:41:24 2015 +0200
@@ -375,8 +375,8 @@
(case find_thms_split splitths 1 th of
NONE =>
(writeln (cat_lines
- (["th:", Display.string_of_thm ctxt th, "split ths:"] @
- map (Display.string_of_thm ctxt) splitths @ ["\n--"]));
+ (["th:", Thm.string_of_thm ctxt th, "split ths:"] @
+ map (Thm.string_of_thm ctxt) splitths @ ["\n--"]));
error "splitto: cannot find variable to split on")
| SOME v =>
let
@@ -1342,7 +1342,7 @@
fun say s = if !tracing then writeln s else ();
fun print_thms ctxt s L =
- say (cat_lines (s :: map (Display.string_of_thm ctxt) L));
+ say (cat_lines (s :: map (Thm.string_of_thm ctxt) L));
fun print_term ctxt s t =
say (cat_lines [s, Syntax.string_of_term ctxt t]);
@@ -1458,7 +1458,7 @@
val cntxt = Simplifier.prems_of ctxt
val _ = print_thms ctxt "cntxt:" cntxt
val _ = say "cong rule:"
- val _ = say (Display.string_of_thm ctxt thm)
+ val _ = say (Thm.string_of_thm ctxt thm)
(* Unquantified eliminate *)
fun uq_eliminate (thm,imp) =
let val tych = Thm.cterm_of ctxt
@@ -2390,7 +2390,7 @@
fun trace_thms ctxt s L =
- if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L))
+ if !trace then writeln (cat_lines (s :: map (Thm.string_of_thm ctxt) L))
else ();
fun trace_cterm ctxt s ct =
--- a/src/HOL/Matrix_LP/Matrix.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy Fri Sep 25 23:41:24 2015 +0200
@@ -13,7 +13,7 @@
definition "matrix = {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
-typedef 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
+typedef (overloaded) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
unfolding matrix_def
proof
show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Fri Sep 25 23:41:24 2015 +0200
@@ -9,7 +9,8 @@
definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
-typedef ('a, 'b) bcontfun = "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
+typedef (overloaded) ('a, 'b) bcontfun =
+ "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)
lemma bcontfunE:
--- a/src/HOL/Nominal/Nominal.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Nominal/Nominal.thy Fri Sep 25 23:41:24 2015 +0200
@@ -6,6 +6,9 @@
"avoids"
begin
+declare [[typedef_overloaded]]
+
+
section {* Permutations *}
(*======================*)
@@ -3378,7 +3381,7 @@
definition "ABS = ABS_set"
-typedef ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+typedef ('x, 'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
"ABS::('x\<Rightarrow>('a noption)) set"
morphisms Rep_ABS Abs_ABS
unfolding ABS_def
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Sep 25 23:41:24 2015 +0200
@@ -586,7 +586,7 @@
val (typedefs, thy6) =
thy4
|> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
- Typedef.add_typedef_global
+ Typedef.add_typedef_global {overloaded = false}
(name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *)
(Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
Const (cname, U --> HOLogic.boolT)) NONE
--- a/src/HOL/Nominal/nominal_thmdecls.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Sep 25 23:41:24 2015 +0200
@@ -156,7 +156,7 @@
fold (fn thm => Data.map (flag thm)) thms_to_be_added context
end
handle EQVT_FORM s =>
- error (Display.string_of_thm (Context.proof_of context) orig_thm ^
+ error (Thm.string_of_thm (Context.proof_of context) orig_thm ^
" does not comply with the form of an equivariance lemma (" ^ s ^").")
--- a/src/HOL/SPARK/Tools/spark_commands.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Sep 25 23:41:24 2015 +0200
@@ -78,7 +78,7 @@
Pretty.chunks (map (fn (b, th) => Pretty.block
[Binding.pretty b, Pretty.str ":",
Pretty.brk 1,
- Display.pretty_thm ctxt th])
+ Thm.pretty_thm ctxt th])
defs),
Pretty.str "Verification conditions:",
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Sep 25 23:41:24 2015 +0200
@@ -359,7 +359,7 @@
map (rpair (mk_type thy prfx ty)) flds) fldtys
in case get_type thy prfx s of
NONE =>
- Record.add_record ([], Binding.name s) NONE
+ Record.add_record {overloaded = false} ([], Binding.name s) NONE
(map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
| SOME (rT, cmap) =>
(case get_record_info thy rT of
@@ -388,8 +388,7 @@
(ids,
case get_type thy prfx s of
SOME _ => thy
- | NONE => Typedecl.typedecl_global
- (Binding.name s, [], NoSyn) thy |> snd);
+ | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd);
fun term_of_expr thy prfx types pfuns =
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Sep 25 23:41:24 2015 +0200
@@ -198,9 +198,8 @@
val final_fqn = Sign.full_name thy binding
val tyargs =
List.tabulate (arity, rpair @{sort type} o prefix "'" o string_of_int)
- val thy' =
- Typedecl.typedecl_global (mk_binding config type_name, tyargs, NoSyn) thy
- |> snd
+ val (_, thy') =
+ Typedecl.typedecl_global {final = true} (mk_binding config type_name, tyargs, NoSyn) thy
val typ_map_entry = (thf_type, (final_fqn, arity))
val ty_map' = typ_map_entry :: ty_map
in (ty_map', thy') end
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 25 23:41:24 2015 +0200
@@ -1923,7 +1923,8 @@
||>> variant_tfrees fp_b_names;
fun add_fake_type spec =
- Typedecl.basic_typedecl (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
+ Typedecl.basic_typedecl {final = true}
+ (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy;
--- a/src/HOL/Tools/BNF/bnf_util.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Fri Sep 25 23:41:24 2015 +0200
@@ -159,7 +159,7 @@
val ((name, info), (lthy, lthy_old)) =
lthy
|> Local_Theory.open_target |> snd
- |> Typedef.add_typedef (b', Ts, mx) set (SOME bindings) tac
+ |> Typedef.add_typedef {overloaded = false} (b', Ts, mx) set (SOME bindings) tac
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
in
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 25 23:41:24 2015 +0200
@@ -202,14 +202,14 @@
raise QUOT_ERROR [Pretty.block
[Pretty.str "The Quotient theorem has extra assumptions:",
Pretty.brk 1,
- Display.pretty_thm ctxt quot_thm]]
+ Thm.pretty_thm ctxt quot_thm]]
else ()
val _ = quot_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
handle TERM _ => raise QUOT_ERROR
[Pretty.block
[Pretty.str "The Quotient theorem is not of the right form:",
Pretty.brk 1,
- Display.pretty_thm ctxt quot_thm]]
+ Thm.pretty_thm ctxt quot_thm]]
val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt
val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
val rty_tfreesT = Term.add_tfree_namesT rty []
@@ -837,13 +837,13 @@
handle TERM _ => raise PCR_ERROR [Pretty.block
[Pretty.str "The pcr definiton theorem is not a plain meta equation:",
Pretty.brk 1,
- Display.pretty_thm ctxt pcrel_def]]
+ Thm.pretty_thm ctxt pcrel_def]]
val pcr_const_def = head_of def_lhs
val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of pcr_cr_eq))
handle TERM _ => raise PCR_ERROR [Pretty.block
[Pretty.str "The pcr_cr equation theorem is not a plain equation:",
Pretty.brk 1,
- Display.pretty_thm ctxt pcr_cr_eq]]
+ Thm.pretty_thm ctxt pcr_cr_eq]]
val (pcr_const_eq, eqs) = strip_comb eq_lhs
fun is_eq (Const (@{const_name HOL.eq}, _)) = true
| is_eq _ = false
@@ -853,7 +853,7 @@
[Pretty.block
[Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
Pretty.brk 1,
- Display.pretty_thm ctxt pcr_cr_eq]]
+ Thm.pretty_thm ctxt pcr_cr_eq]]
else []
val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
[Pretty.block
--- a/src/HOL/Tools/Meson/meson.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Fri Sep 25 23:41:24 2015 +0200
@@ -186,8 +186,8 @@
| tacf prems =
error (cat_lines
("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
- Display.string_of_thm ctxt st ::
- "Premises:" :: map (Display.string_of_thm ctxt) prems))
+ Thm.string_of_thm ctxt st ::
+ "Premises:" :: map (Thm.string_of_thm ctxt) prems))
in
case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS ctxt tacf) st) of
SOME (th, _) => th
@@ -395,7 +395,7 @@
val cls =
if has_too_many_clauses ctxt (Thm.concl_of th) then
(trace_msg ctxt (fn () =>
- "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
+ "cnf is ignoring: " ^ Thm.string_of_thm ctxt th); ths)
else
cnf_aux (th, ths)
in (cls, !ctxt_ref) end
@@ -652,7 +652,7 @@
|> tap (fn NONE =>
trace_msg ctxt (fn () =>
"Failed to skolemize " ^
- Display.string_of_thm ctxt th)
+ Thm.string_of_thm ctxt th)
| _ => ()))
end
@@ -751,8 +751,8 @@
val horns = make_horns (cls @ ths)
val _ = trace_msg ctxt (fn () =>
cat_lines ("meson method called:" ::
- map (Display.string_of_thm ctxt) (cls @ ths) @
- ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
+ map (Thm.string_of_thm ctxt) (cls @ ths) @
+ ["clauses:"] @ map (Thm.string_of_thm ctxt) horns))
in
THEN_ITER_DEEPEN iter_deepen_limit
(resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 25 23:41:24 2015 +0200
@@ -170,7 +170,7 @@
val eqth = introduce_combinators_in_cterm ctxt (Thm.cprop_of th)
in Thm.equal_elim eqth th end
handle THM (msg, _, _) =>
- (warning ("Error in the combinator translation of " ^ Display.string_of_thm ctxt th ^
+ (warning ("Error in the combinator translation of " ^ Thm.string_of_thm ctxt th ^
"\nException message: " ^ msg);
(* A type variable of sort "{}" will make "abstraction" fail. *)
TrueI)
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 25 23:41:24 2015 +0200
@@ -134,11 +134,11 @@
end
handle Option.Option =>
(trace_msg ctxt (fn () =>
- "\"find_var\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th);
+ "\"find_var\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th);
NONE)
| TYPE _ =>
(trace_msg ctxt (fn () =>
- "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th);
+ "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
let val a = Metis_Name.toString a in
@@ -149,7 +149,7 @@
SOME _ => NONE (* type instantiations are forbidden *)
| NONE => SOME (a, t) (* internal Metis var? *)))
end
- val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
+ val _ = trace_msg ctxt (fn () => " isa th: " ^ Thm.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
val (vars, tms) =
ListPair.unzip (map_filter subst_translation substs)
@@ -269,8 +269,8 @@
let
val (i_th1, i_th2) = apply2 (lookth th_pairs) (th1, th2)
val _ = trace_msg ctxt (fn () =>
- " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
- \ isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
+ " isa th1 (pos): " ^ Thm.string_of_thm ctxt i_th1 ^ "\n\
+ \ isa th2 (neg): " ^ Thm.string_of_thm ctxt i_th2)
in
(* Trivial cases where one operand is type info *)
if Thm.eq_thm (TrueI, i_th1) then
@@ -369,7 +369,7 @@
val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill-typed but gives right max*)
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
- val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
+ val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst')
val eq_terms =
map (apply2 (Thm.cterm_of ctxt))
(ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
@@ -462,7 +462,7 @@
val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
|> flexflex_first_order ctxt
|> resynchronize ctxt fol_th
- val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
+ val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Thm.string_of_thm ctxt th)
val _ = trace_msg ctxt (fn () => "=============================================")
in
(fol_th, th) :: th_pairs
--- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Sep 25 23:41:24 2015 +0200
@@ -160,7 +160,7 @@
val dischargers = map (fst o snd) th_cls_pairs
val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES")
- val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
+ val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
val type_enc = type_enc_of_string Strict type_enc
val (sym_tab, axioms, ord_info, concealed) =
@@ -172,7 +172,7 @@
| get_isa_thm _ (Isa_Raw ith) = ith
val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
val _ = trace_msg ctxt (K "ISABELLE CLAUSES")
- val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
+ val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms
val _ = trace_msg ctxt (K "METIS CLAUSES")
val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
val _ = trace_msg ctxt (K "START METIS PROVE PROCESS")
@@ -200,7 +200,7 @@
val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms
val used = map_filter (used_axioms axioms) proof
val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
- val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
+ val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
val (used_th_cls_pairs, unused_th_cls_pairs) =
List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
val unused_ths = maps (snd o snd) unused_th_cls_pairs
@@ -217,7 +217,7 @@
();
(case result of
(_, ith) :: _ =>
- (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
+ (trace_msg ctxt (fn () => "Success: " ^ Thm.string_of_thm ctxt ith);
[discharge_skolem_premises ctxt dischargers ith])
| _ => (trace_msg ctxt (K "Metis: No result"); []))
end
@@ -251,7 +251,7 @@
val unused = Unsynchronized.ref []
val type_encs = if null type_encs0 then partial_type_encs else type_encs0
val _ = trace_msg ctxt (fn () =>
- "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths))
+ "Metis called with theorems\n" ^ cat_lines (map (Thm.string_of_thm ctxt) ths))
val type_encs = type_encs |> maps unalias_type_enc
val combs = (lam_trans = combsN)
fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Sep 25 23:41:24 2015 +0200
@@ -186,7 +186,7 @@
|> Sign.parent_path
|> fold_map
(fn (((name, mx), tvs), c) =>
- Typedef.add_typedef_global (name, tvs, mx)
+ Typedef.add_typedef_global {overloaded = false} (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
(fn ctxt =>
resolve_tac ctxt [exI] 1 THEN
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Sep 25 23:41:24 2015 +0200
@@ -355,7 +355,7 @@
fun print_intros ctxt gr consts =
tracing (cat_lines (map (fn const =>
"Constant " ^ const ^ "has intros:\n" ^
- cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts))
+ cat_lines (map (Thm.string_of_thm ctxt) (Graph.get_node gr const))) consts))
(* translation of moded predicates *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Sep 25 23:41:24 2015 +0200
@@ -23,14 +23,14 @@
tracing (msg ^
(cat_lines (map
(fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^
- commas (map (Display.string_of_thm_global thy) intros)) intross)))
+ commas (map (Thm.string_of_thm_global thy) intros)) intross)))
else ()
fun print_specs options thy specs =
if show_intermediate_results options then
map (fn (c, thms) =>
"Constant " ^ c ^ " has specification:\n" ^
- (cat_lines (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
+ (cat_lines (map (Thm.string_of_thm_global thy) thms)) ^ "\n") specs
|> cat_lines |> tracing
else ()
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 25 23:41:24 2015 +0200
@@ -1079,7 +1079,7 @@
error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
" (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
" and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
- " in " ^ Display.string_of_thm ctxt' th)
+ " in " ^ Thm.string_of_thm ctxt' th)
in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end
fun instantiate_typ th =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 25 23:41:24 2015 +0200
@@ -130,11 +130,11 @@
let
val _ = writeln ("predicate: " ^ pred)
val _ = writeln ("introrules: ")
- val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm))
+ val _ = fold (fn thm => fn _ => writeln (Thm.string_of_thm ctxt thm))
(rev (Core_Data.intros_of ctxt pred)) ()
in
if Core_Data.has_elim ctxt pred then
- writeln ("elimrule: " ^ Display.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred))
+ writeln ("elimrule: " ^ Thm.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred))
else
writeln ("no elimrule defined")
end
@@ -1295,7 +1295,7 @@
else
error ("Format of introduction rule is invalid: tuples must be expanded:"
^ (Syntax.string_of_term_global thy arg) ^ " in " ^
- (Display.string_of_thm_global thy intro))
+ (Thm.string_of_thm_global thy intro))
| _ => true
val prems = Logic.strip_imp_prems (prop_of intro)
fun check_prem (Prem t) = forall check_arg args
@@ -1387,7 +1387,7 @@
(*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
val _ =
if show_intermediate_results options then
- tracing (commas (map (Display.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames)))
+ tracing (commas (map (Thm.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames)))
else ()
val (preds, all_vs, param_vs, all_modes, clauses) =
prepare_intrs options ctxt prednames (maps (Core_Data.intros_of ctxt) prednames)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Sep 25 23:41:24 2015 +0200
@@ -217,7 +217,7 @@
val _ =
if show_intermediate_results options then
tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
- commas (map (Display.string_of_thm_global thy) spec))
+ commas (map (Thm.string_of_thm_global thy) spec))
else ()
in
spec
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Sep 25 23:41:24 2015 +0200
@@ -310,7 +310,7 @@
fun rewrite_intro thy intro =
let
fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
- (*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*)
+ (*val _ = tracing ("Rewriting intro " ^ Thm.string_of_thm_global thy intro)*)
val intro_t = Logic.unvarify_global (Thm.prop_of intro)
val (prems, concl) = Logic.strip_horn intro_t
val frees = map fst (Term.add_frees intro_t [])
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Sep 25 23:41:24 2015 +0200
@@ -192,7 +192,7 @@
fun print_specs options thy msg ths =
if show_intermediate_results options then
- (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths)))
+ (tracing (msg); tracing (commas (map (Thm.string_of_thm_global thy) ths)))
else
()
@@ -209,7 +209,7 @@
map (rewrite_intros ctxt) specs
else
error ("unexpected specification for constant " ^ quote constname ^ ":\n"
- ^ commas (map (quote o Display.string_of_thm_global thy) specs))
+ ^ commas (map (quote o Thm.string_of_thm_global thy) specs))
val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros
val _ = print_specs options thy "normalized intros" intros
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 25 23:41:24 2015 +0200
@@ -306,7 +306,7 @@
val (_, ts) = strip_comb t
in
trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
- " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
+ " splitting with rules \n" ^ Thm.string_of_thm ctxt split_asm)
THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1
THEN (trace_tac ctxt options "after splitting with split_asm rules")
(* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Sep 25 23:41:24 2015 +0200
@@ -6,14 +6,17 @@
signature QUOTIENT_TYPE =
sig
- val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) *
- ((binding * binding) option * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
-
- val quotient_type: (string list * binding * mixfix) * (typ * term * bool) *
- ((binding * binding) option * thm option) -> Proof.context -> Proof.state
-
- val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
- (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state
+ val add_quotient_type: {overloaded: bool} ->
+ ((string list * binding * mixfix) * (typ * term * bool) *
+ ((binding * binding) option * thm option)) * thm -> local_theory ->
+ Quotient_Info.quotients * local_theory
+ val quotient_type: {overloaded: bool} ->
+ (string list * binding * mixfix) * (typ * term * bool) *
+ ((binding * binding) option * thm option) -> Proof.context -> Proof.state
+ val quotient_type_cmd: {overloaded: bool} ->
+ (((((string list * binding) * mixfix) * string) * (bool * string)) *
+ (binding * binding) option) * (Facts.ref * Token.src list) option ->
+ Proof.context -> Proof.state
end;
structure Quotient_Type: QUOTIENT_TYPE =
@@ -40,12 +43,12 @@
(* makes the new type definitions and proves non-emptyness *)
-fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
+fun typedef_make overloaded (vs, qty_name, mx, rel, rty) equiv_thm lthy =
let
fun typedef_tac ctxt =
EVERY1 (map (resolve_tac ctxt o single) [@{thm part_equivp_typedef}, equiv_thm])
in
- Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
+ Typedef.add_typedef overloaded (qty_name, map (rpair dummyS) vs, mx)
(typedef_term rel rty lthy) NONE typedef_tac lthy
end
@@ -152,7 +155,8 @@
end
(* main function for constructing a quotient type *)
-fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy =
+fun add_quotient_type overloaded
+ (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy =
let
val part_equiv =
if partial
@@ -161,7 +165,7 @@
(* generates the typedef *)
val ((_, typedef_info), lthy1) =
- typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
+ typedef_make overloaded (vs, qty_name, mx, rel, rty) part_equiv lthy
(* abs and rep functions from the typedef *)
val Abs_ty = #abs_type (#1 typedef_info)
@@ -290,7 +294,7 @@
relations are equivalence relations
*)
-fun quotient_type quot lthy =
+fun quotient_type overloaded quot lthy =
let
(* sanity check *)
val _ = sanity_check quot
@@ -307,12 +311,12 @@
val goal = (mk_goal o #2) quot
- fun after_qed [[thm]] = (snd oo add_quotient_type) (quot, thm)
+ fun after_qed [[thm]] = (snd oo add_quotient_type overloaded) (quot, thm)
in
Proof.theorem NONE after_qed [[(goal, [])]] lthy
end
-fun quotient_type_cmd spec lthy =
+fun quotient_type_cmd overloaded spec lthy =
let
fun parse_spec ((((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy =
let
@@ -330,7 +334,7 @@
val (spec', _) = parse_spec spec lthy
in
- quotient_type spec' lthy
+ quotient_type overloaded spec' lthy
end
@@ -340,11 +344,11 @@
Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type}
"quotient type definitions (require equivalence proofs)"
(* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
- (Parse.type_args -- Parse.binding --
+ (Parse_Spec.overloaded -- (Parse.type_args -- Parse.binding --
Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |--
Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -- Parse.term) --
Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) --
- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)
- >> quotient_type_cmd)
+ Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm))
+ >> (fn (overloaded, spec) => quotient_type_cmd {overloaded = overloaded} spec))
end
--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 25 23:41:24 2015 +0200
@@ -23,7 +23,7 @@
fun drop_fact_warning ctxt =
SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
- Display.string_of_thm ctxt)
+ Thm.string_of_thm ctxt)
(* general theorem normalizations *)
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 25 23:41:24 2015 +0200
@@ -103,7 +103,7 @@
fun trace_assms ctxt =
SMT_Config.trace_msg ctxt (Pretty.string_of o
- Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
+ Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd))
fun trace_replay_data ({context = ctxt, typs, terms, ...} : SMT_Translate.replay_data) =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Sep 25 23:41:24 2015 +0200
@@ -89,7 +89,7 @@
val ctxt = ctxt |> Config.put show_markup true
val assms = op @ assmsp
val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]")
- val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms)
+ val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms)
val concl = Syntax.pretty_term ctxt concl
in
tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl])))
--- a/src/HOL/Tools/choice_specification.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML Fri Sep 25 23:41:24 2015 +0200
@@ -148,7 +148,7 @@
fun add_final (thm, thy) =
if name = ""
then (thm, thy)
- else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
+ else (writeln (" " ^ name ^ ": " ^ Thm.string_of_thm_global thy thm);
Global_Theory.store_thm (Binding.name name, thm) thy)
in
swap args
--- a/src/HOL/Tools/inductive.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Sep 25 23:41:24 2015 +0200
@@ -236,7 +236,7 @@
(Pretty.str "(co)inductives:" ::
map (Pretty.mark_str o #1)
(Name_Space.markup_entries verbose ctxt space (Symtab.dest infos)))),
- Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
+ Pretty.big_list "monotonicity rules:" (map (Thm.pretty_thm_item ctxt) monos)]
end |> Pretty.writeln_chunks;
@@ -269,7 +269,7 @@
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}])) thm))
| _ => thm)
- end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
+ end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Thm.string_of_thm ctxt thm);
val mono_add =
Thm.declaration_attribute (fn thm => fn context =>
--- a/src/HOL/Tools/inductive_set.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Sep 25 23:41:24 2015 +0200
@@ -298,7 +298,7 @@
val _ =
if Context_Position.is_really_visible ctxt then
warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
- "\n" ^ Display.string_of_thm ctxt thm)
+ "\n" ^ Thm.string_of_thm ctxt thm)
else ();
in tab end;
--- a/src/HOL/Tools/lin_arith.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Sep 25 23:41:24 2015 +0200
@@ -303,11 +303,11 @@
@{const_name Rings.divide}] a
| _ =>
(if Context_Position.is_visible ctxt then
- warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
+ warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm)
else (); false))
| _ =>
(if Context_Position.is_visible ctxt then
- warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
+ warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm)
else (); false));
(* substitute new for occurrences of old in a term, incrementing bound *)
--- a/src/HOL/Tools/record.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/record.ML Fri Sep 25 23:41:24 2015 +0200
@@ -26,8 +26,8 @@
val get_info: theory -> string -> info option
val the_info: theory -> string -> info
val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list
- val add_record: (string * sort) list * binding -> (typ list * string) option ->
- (binding * typ * mixfix) list -> theory -> theory
+ val add_record: {overloaded: bool} -> (string * sort) list * binding ->
+ (typ list * string) option -> (binding * typ * mixfix) list -> theory -> theory
val last_extT: typ -> (string * typ list) option
val dest_recTs: typ -> (string * typ list) list
@@ -55,7 +55,7 @@
signature ISO_TUPLE_SUPPORT =
sig
- val add_iso_tuple_type: binding * (string * sort) list ->
+ val add_iso_tuple_type: {overloaded: bool} -> binding * (string * sort) list ->
typ * typ -> theory -> (term * term) * theory
val mk_cons_tuple: term * term -> term
val dest_cons_tuple: term -> term * term
@@ -93,13 +93,13 @@
|> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
end
-fun do_typedef raw_tyco repT raw_vs thy =
+fun do_typedef overloaded raw_tyco repT raw_vs thy =
let
val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT;
val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
in
thy
- |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
+ |> Typedef.add_typedef_global overloaded (raw_tyco, vs, NoSyn)
(HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1)
|-> (fn (tyco, info) => get_typedef_info tyco vs info)
end;
@@ -117,13 +117,13 @@
fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
| dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
-fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
+fun add_iso_tuple_type overloaded (b, alphas) (leftT, rightT) thy =
let
val repT = HOLogic.mk_prodT (leftT, rightT);
val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
thy
- |> do_typedef b repT alphas
+ |> do_typedef overloaded b repT alphas
||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
val typ_ctxt = Proof_Context.init_global typ_thy;
@@ -1499,7 +1499,7 @@
in compose_tac ctxt (false, rule'', Thm.nprems_of rule) i end);
-fun extension_definition name fields alphas zeta moreT more vars thy =
+fun extension_definition overloaded name fields alphas zeta moreT more vars thy =
let
val ctxt = Proof_Context.init_global thy;
@@ -1525,7 +1525,7 @@
let
val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
val ((_, cons), thy') = thy
- |> Iso_Tuple_Support.add_iso_tuple_type
+ |> Iso_Tuple_Support.add_iso_tuple_type overloaded
(Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
(fastype_of left, fastype_of right);
in
@@ -1808,7 +1808,7 @@
(* definition *)
-fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy0 =
+fun definition overloaded (alphas, binding) parent (parents: parent_info list) raw_fields thy0 =
let
val ctxt0 = Proof_Context.init_global thy0;
@@ -1867,7 +1867,7 @@
extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
thy0
|> Sign.qualified_path false binding
- |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
+ |> extension_definition overloaded extension_name fields alphas_ext zeta moreT more vars;
val ext_ctxt = Proof_Context.init_global ext_thy;
val _ = timing_msg ext_ctxt "record preparing definitions";
@@ -2277,7 +2277,7 @@
in
-fun add_record (params, binding) raw_parent raw_fields thy =
+fun add_record overloaded (params, binding) raw_parent raw_fields thy =
let
val ctxt = Proof_Context.init_global thy;
fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
@@ -2327,11 +2327,11 @@
err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
val _ = if null errs then () else error (cat_lines errs);
in
- thy |> definition (params, binding) parent parents bfields
+ thy |> definition overloaded (params, binding) parent parents bfields
end
handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
-fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy =
+fun add_record_cmd overloaded (raw_params, binding) raw_parent raw_fields thy =
let
val ctxt = Proof_Context.init_global thy;
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
@@ -2339,7 +2339,7 @@
val (parent, ctxt2) = read_parent raw_parent ctxt1;
val (fields, ctxt3) = read_fields raw_fields ctxt2;
val params' = map (Proof_Context.check_tfree ctxt3) params;
- in thy |> add_record (params', binding) parent fields end;
+ in thy |> add_record overloaded (params', binding) parent fields end;
end;
@@ -2348,9 +2348,10 @@
val _ =
Outer_Syntax.command @{command_keyword record} "define extensible record"
- (Parse.type_args_constrained -- Parse.binding --
+ (Parse_Spec.overloaded -- (Parse.type_args_constrained -- Parse.binding) --
(@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
Scan.repeat1 Parse.const_binding)
- >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));
+ >> (fn ((overloaded, x), (y, z)) =>
+ Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
end;
--- a/src/HOL/Tools/sat.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/sat.ML Fri Sep 25 23:41:24 2015 +0200
@@ -155,9 +155,9 @@
let
val _ =
cond_tracing ctxt (fn () =>
- "Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
+ "Resolving clause: " ^ Thm.string_of_thm ctxt c1 ^
" (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^
- ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
+ ")\nwith clause: " ^ Thm.string_of_thm ctxt c2 ^
" (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")")
(* the two literals used for resolution *)
@@ -176,7 +176,7 @@
val _ =
cond_tracing ctxt
- (fn () => "Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
+ (fn () => "Resolution theorem: " ^ Thm.string_of_thm ctxt res_thm)
(* Gamma1, Gamma2 |- False *)
val c_new =
@@ -186,7 +186,7 @@
val _ =
cond_tracing ctxt (fn () =>
- "Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
+ "Resulting clause: " ^ Thm.string_of_thm ctxt c_new ^
" (hyps: " ^
ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")")
--- a/src/HOL/Tools/typedef.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Tools/typedef.ML Fri Sep 25 23:41:24 2015 +0200
@@ -20,16 +20,17 @@
val default_bindings: binding -> bindings
val make_bindings: binding -> bindings option -> bindings
val make_morphisms: binding -> (binding * binding) option -> bindings
- val add_typedef: binding * (string * sort) list * mixfix ->
+ val overloaded: bool Config.T
+ val add_typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
term -> bindings option -> (Proof.context -> tactic) -> local_theory ->
(string * info) * local_theory
- val add_typedef_global: binding * (string * sort) list * mixfix ->
+ val add_typedef_global: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
term -> bindings option -> (Proof.context -> tactic) -> theory ->
(string * info) * theory
- val typedef: binding * (string * sort) list * mixfix -> term -> bindings option ->
- local_theory -> Proof.state
- val typedef_cmd: binding * (string * string option) list * mixfix -> string -> bindings option ->
- local_theory -> Proof.state
+ val typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
+ term -> bindings option -> local_theory -> Proof.state
+ val typedef_cmd: {overloaded: bool} -> binding * (string * string option) list * mixfix ->
+ string -> bindings option -> local_theory -> Proof.state
end;
structure Typedef: TYPEDEF =
@@ -98,6 +99,8 @@
(* primitive typedef axiomatization -- for fresh typedecl *)
+val typedef_overloaded = Attrib.setup_config_bool @{binding typedef_overloaded} (K false);
+
fun mk_inhabited A =
let val T = HOLogic.dest_setT (Term.fastype_of A)
in HOLogic.mk_Trueprop (HOLogic.exists_const T $ Abs ("x", T, HOLogic.mk_mem (Bound 0, A))) end;
@@ -109,7 +112,7 @@
(newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
-fun primitive_typedef type_definition_name newT oldT Rep_name Abs_name A lthy =
+fun primitive_typedef {overloaded} type_definition_name newT oldT Rep_name Abs_name A lthy =
let
(* errors *)
@@ -118,11 +121,13 @@
val lhs_tfrees = Term.add_tfreesT newT [];
val rhs_tfrees = Term.add_tfreesT oldT [];
val _ =
- (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => ()
+ (case fold (remove (op =)) lhs_tfrees rhs_tfrees of
+ [] => ()
| extras => error ("Extra type variables in representing set: " ^ show_names extras));
val _ =
- (case Term.add_frees A [] of [] => []
+ (case Term.add_frees A [] of [] =>
+ []
| xs => error ("Illegal variables in representing set: " ^ show_names xs));
@@ -132,15 +137,38 @@
|> Local_Theory.background_theory_result
(Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>>
Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn));
+ val const_dep = Theory.const_dep (Proof_Context.theory_of consts_lthy);
+ val defs_context = Proof_Context.defs_context consts_lthy;
- val typedef_deps = Term.add_consts A [];
+ val A_consts = fold_aterms (fn Const c => insert (op =) (const_dep c) | _ => I) A [];
+ val A_types =
+ (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) A [];
+ val typedef_deps = A_consts @ A_types;
+
+ val newT_dep = Theory.type_dep (dest_Type newT);
val ((axiom_name, axiom), axiom_lthy) = consts_lthy
|> Local_Theory.background_theory_result
(Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##>
- Theory.add_deps consts_lthy "" (dest_Const RepC) typedef_deps ##>
- Theory.add_deps consts_lthy "" (dest_Const AbsC) typedef_deps);
+ Theory.add_deps defs_context "" newT_dep typedef_deps ##>
+ Theory.add_deps defs_context "" (const_dep (dest_Const RepC)) [newT_dep] ##>
+ Theory.add_deps defs_context "" (const_dep (dest_Const AbsC)) [newT_dep]);
+ val axiom_defs = Theory.defs_of (Proof_Context.theory_of axiom_lthy);
+ val newT_deps = maps #2 (Defs.get_deps axiom_defs (#1 newT_dep));
+ val _ =
+ if null newT_deps orelse overloaded orelse Config.get lthy typedef_overloaded then ()
+ else
+ error (Pretty.string_of (Pretty.chunks
+ [Pretty.paragraph
+ (Pretty.text "Type definition with open dependencies, use" @
+ [Pretty.brk 1, Pretty.str "\"", Pretty.keyword1 "typedef", Pretty.brk 1,
+ Pretty.str "(", Pretty.keyword2 "overloaded", Pretty.str ")\"", Pretty.brk 1] @
+ Pretty.text "or enable configuration option \"typedef_overloaded\" in the context."),
+ Pretty.block [Pretty.str " Type:", Pretty.brk 2, Syntax.pretty_typ axiom_lthy newT],
+ Pretty.block (Pretty.str " Deps:" :: Pretty.brk 2 ::
+ Pretty.commas
+ (map (Defs.pretty_entry (Proof_Context.defs_context axiom_lthy)) newT_deps))]))
in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
@@ -164,7 +192,7 @@
(* prepare_typedef *)
-fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_bindings lthy =
+fun prepare_typedef prep_term overloaded (name, raw_args, mx) raw_set opt_bindings lthy =
let
val bname = Binding.name_of name;
@@ -187,7 +215,7 @@
val args = map (Proof_Context.check_tfree tmp_ctxt') raw_args;
val (newT, typedecl_lthy) = lthy
- |> Typedecl.typedecl (name, args, mx)
+ |> Typedecl.typedecl {final = false} (name, args, mx)
||> Variable.declare_term set;
val Type (full_name, _) = newT;
@@ -198,7 +226,7 @@
val {Rep_name, Abs_name, type_definition_name} = make_bindings name opt_bindings;
val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy
- |> primitive_typedef type_definition_name newT oldT Rep_name Abs_name set;
+ |> primitive_typedef overloaded type_definition_name newT oldT Rep_name Abs_name set;
val alias_lthy = typedef_lthy
|> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
@@ -262,18 +290,18 @@
(* add_typedef: tactic interface *)
-fun add_typedef typ set opt_bindings tac lthy =
+fun add_typedef overloaded typ set opt_bindings tac lthy =
let
val ((goal, _, typedef_result), lthy') =
- prepare_typedef Syntax.check_term typ set opt_bindings lthy;
+ prepare_typedef Syntax.check_term overloaded typ set opt_bindings lthy;
val inhabited =
Goal.prove lthy' [] [] goal (tac o #context)
|> Goal.norm_result lthy' |> Thm.close_derivation;
in typedef_result inhabited lthy' end;
-fun add_typedef_global typ set opt_bindings tac =
+fun add_typedef_global overloaded typ set opt_bindings tac =
Named_Target.theory_init
- #> add_typedef typ set opt_bindings tac
+ #> add_typedef overloaded typ set opt_bindings tac
#> Local_Theory.exit_result_global (apsnd o transform_info);
@@ -281,11 +309,11 @@
local
-fun gen_typedef prep_term prep_constraint (b, raw_args, mx) set opt_bindings lthy =
+fun gen_typedef prep_term prep_constraint overloaded (b, raw_args, mx) set opt_bindings lthy =
let
val args = map (apsnd (prep_constraint lthy)) raw_args;
val ((goal, goal_pat, typedef_result), lthy') =
- prepare_typedef prep_term (b, args, mx) set opt_bindings lthy;
+ prepare_typedef prep_term overloaded (b, args, mx) set opt_bindings lthy;
fun after_qed [[th]] = snd o typedef_result th;
in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
@@ -303,10 +331,14 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_keyword typedef}
"HOL type definition (requires non-emptiness proof)"
- (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
+ (Parse_Spec.overloaded -- Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
(@{keyword "="} |-- Parse.term) --
Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
- >> (fn ((((vs, t), mx), A), opt_morphs) => fn lthy =>
- typedef_cmd (t, vs, mx) A (SOME (make_morphisms t opt_morphs)) lthy));
+ >> (fn (((((overloaded, vs), t), mx), A), opt_morphs) => fn lthy =>
+ typedef_cmd {overloaded = overloaded} (t, vs, mx) A
+ (SOME (make_morphisms t opt_morphs)) lthy));
+
+
+val overloaded = typedef_overloaded;
end;
--- a/src/HOL/Word/Word.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/Word/Word.thy Fri Sep 25 23:41:24 2015 +0200
@@ -18,7 +18,7 @@
subsection {* Type definition *}
-typedef 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
+typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
morphisms uint Abs_word by auto
lemma uint_nonnegative:
--- a/src/HOL/ex/PER.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/HOL/ex/PER.thy Fri Sep 25 23:41:24 2015 +0200
@@ -154,7 +154,7 @@
definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
-typedef 'a quot = "quot :: 'a::partial_equiv set set"
+typedef (overloaded) 'a quot = "quot :: 'a::partial_equiv set set"
unfolding quot_def by blast
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Sep 25 23:41:24 2015 +0200
@@ -349,7 +349,7 @@
fun trace_thm ctxt msgs th =
(if Config.get ctxt LA_Data.trace
- then tracing (cat_lines (msgs @ [Display.string_of_thm ctxt th]))
+ then tracing (cat_lines (msgs @ [Thm.string_of_thm ctxt th]))
else (); th);
fun trace_term ctxt msgs t =
@@ -468,8 +468,8 @@
if LA_Logic.is_False fls then ()
else
(tracing (cat_lines
- (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
- ["Proved:", Display.string_of_thm ctxt fls, ""]));
+ (["Assumptions:"] @ map (Thm.string_of_thm ctxt) asms @ [""] @
+ ["Proved:", Thm.string_of_thm ctxt fls, ""]));
warning "Linear arithmetic should have refuted the assumptions.\n\
\Please inform Tobias Nipkow.")
in fls end
--- a/src/Provers/blast.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Provers/blast.ML Fri Sep 25 23:41:24 2015 +0200
@@ -484,7 +484,7 @@
| cond_tracing false _ = ();
fun TRACE ctxt rl tac i st =
- (cond_tracing (Config.get ctxt trace) (fn () => Display.string_of_thm ctxt rl); tac i st);
+ (cond_tracing (Config.get ctxt trace) (fn () => Thm.string_of_thm ctxt rl); tac i st);
(*Resolution/matching tactics: if upd then the proof state may be updated.
Matching makes the tactics more deterministic in the presence of Vars.*)
@@ -509,13 +509,13 @@
handle
ElimBadPrem => (*reject: prems don't preserve conclusion*)
(if Context_Position.is_visible ctxt then
- warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl0)
+ warning ("Ignoring weak elimination rule\n" ^ Thm.string_of_thm ctxt rl0)
else ();
Option.NONE)
| ElimBadConcl => (*ignore: conclusion is not just a variable*)
(cond_tracing (Config.get ctxt trace)
(fn () => "Ignoring ill-formed elimination rule:\n" ^
- "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl0);
+ "conclusion should be a variable\n" ^ Thm.string_of_thm ctxt rl0);
Option.NONE);
--- a/src/Provers/classical.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Provers/classical.ML Fri Sep 25 23:41:24 2015 +0200
@@ -282,7 +282,7 @@
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
fun delete x = delete_tagged_list (joinrules x);
-fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Display.string_of_thm ctxt th);
+fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
fun make_elim ctxt th =
if has_fewer_prems 1 th then bad_thm ctxt "Ill-formed destruction rule" th
@@ -290,7 +290,7 @@
fun warn_thm ctxt msg th =
if Context_Position.is_really_visible ctxt
- then warning (msg ^ Display.string_of_thm ctxt th) else ();
+ then warning (msg ^ Thm.string_of_thm ctxt th) else ();
fun warn_rules ctxt msg rules (r: rule) =
Item_Net.member rules r andalso (warn_thm ctxt msg (#1 r); true);
@@ -634,7 +634,7 @@
fun print_claset ctxt =
let
val {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
- val pretty_thms = map (Display.pretty_thm_item ctxt o #1) o Item_Net.content;
+ val pretty_thms = map (Thm.pretty_thm_item ctxt o #1) o Item_Net.content;
in
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
Pretty.big_list "introduction rules (intro):" (pretty_thms unsafeIs),
--- a/src/Pure/Isar/attrib.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Sep 25 23:41:24 2015 +0200
@@ -532,9 +532,9 @@
register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
register_config Goal_Display.show_main_goal_raw #>
- register_config Goal_Display.show_consts_raw #>
- register_config Display.show_hyps_raw #>
- register_config Display.show_tags_raw #>
+ register_config Thm.show_consts_raw #>
+ register_config Thm.show_hyps_raw #>
+ register_config Thm.show_tags_raw #>
register_config Pattern.unify_trace_failure_raw #>
register_config Unify.trace_bound_raw #>
register_config Unify.search_bound_raw #>
--- a/src/Pure/Isar/bundle.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/bundle.ML Fri Sep 25 23:41:24 2015 +0200
@@ -124,7 +124,7 @@
fun print_bundles verbose ctxt =
let
- val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
+ val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
fun prt_fact (ths, []) = map prt_thm ths
| prt_fact (ths, atts) = Pretty.enclose "(" ")"
--- a/src/Pure/Isar/calculation.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/calculation.ML Fri Sep 25 23:41:24 2015 +0200
@@ -41,7 +41,7 @@
fun print_rules ctxt =
let
- val pretty_thm = Display.pretty_thm_item ctxt;
+ val pretty_thm = Thm.pretty_thm_item ctxt;
val (trans, sym) = get_rules ctxt;
in
[Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)),
@@ -137,8 +137,8 @@
fun calculate prep_rules final raw_rules int state =
let
val ctxt = Proof.context_of state;
- val pretty_thm = Display.pretty_thm ctxt;
- val pretty_thm_item = Display.pretty_thm_item ctxt;
+ val pretty_thm = Thm.pretty_thm ctxt;
+ val pretty_thm_item = Thm.pretty_thm_item ctxt;
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
val eq_prop = op aconv o apply2 (Envir.beta_eta_contract o strip_assums_concl);
--- a/src/Pure/Isar/class.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/class.ML Fri Sep 25 23:41:24 2015 +0200
@@ -599,7 +599,7 @@
fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
| matchings _ = I;
val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
- handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.pretty ctxt) e);
+ handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.Proof ctxt) e);
val inst = map_type_tvar
(fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
@@ -657,7 +657,7 @@
val primary_constraints = map (apsnd
(map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
val algebra = Sign.classes_of thy
- |> fold (fn tyco => Sorts.add_arities (Context.pretty_global thy)
+ |> fold (fn tyco => Sorts.add_arities (Context.Theory thy)
(tyco, map (fn class => (class, map snd vs)) sort)) tycos;
val consts = Sign.consts_of thy;
val improve_constraints = AList.lookup (op =)
--- a/src/Pure/Isar/code.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/code.ML Fri Sep 25 23:41:24 2015 +0200
@@ -443,11 +443,11 @@
exception BAD_THM of string;
fun bad_thm msg = raise BAD_THM msg;
fun error_thm f thy (thm, proper) = f (thm, proper)
- handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm);
+ handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm);
fun error_abs_thm f thy thm = f thm
- handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm);
+ handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm);
fun warning_thm f thy (thm, proper) = SOME (f (thm, proper))
- handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); NONE)
+ handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm); NONE)
fun try_thm f thm_proper = SOME (f thm_proper)
handle BAD_THM _ => NONE;
@@ -764,7 +764,7 @@
val (thms, propers) = split_list eqns;
val _ = map (fn thm => if c = const_eqn thy thm then ()
else error ("Wrong head of code equation,\nexpected constant "
- ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)) thms;
+ ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms;
fun tvars_of T = rev (Term.add_tvarsT T []);
val vss = map (tvars_of o snd o head_eqn) thms;
fun inter_sorts vs =
@@ -794,7 +794,7 @@
val _ = assert_abs_eqn thy (SOME tyco) abs_thm;
val _ = if c = const_abs_eqn thy abs_thm then ()
else error ("Wrong head of abstract code equation,\nexpected constant "
- ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm);
+ ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy abs_thm);
in Abstract (Thm.legacy_freezeT abs_thm, tyco) end;
fun constrain_cert_thm thy sorts cert_thm =
@@ -888,12 +888,12 @@
fun pretty_cert thy (cert as Nothing _) =
[Pretty.str "(not implemented)"]
| pretty_cert thy (cert as Equations _) =
- (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
+ (map_filter (Option.map (Thm.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
o these o snd o equations_of_cert thy) cert
| pretty_cert thy (Projection (t, _)) =
[Syntax.pretty_term_global thy (Logic.varify_types_global t)]
| pretty_cert thy (Abstract (abs_thm, _)) =
- [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
+ [(Thm.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
end;
@@ -927,7 +927,7 @@
fun cert_of_eqns_preprocess ctxt functrans c =
let
fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks)
- (Pretty.str s :: map (Display.pretty_thm ctxt o fst) eqns);
+ (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns);
val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) ();
in
tap (tracing "before function transformation")
@@ -1010,7 +1010,7 @@
val exec = the_exec thy;
fun pretty_equations const thms =
(Pretty.block o Pretty.fbreaks)
- (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms);
+ (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
pretty_equations const (map fst (Lazy.force eqns_lazy))
| pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
@@ -1096,7 +1096,7 @@
fun drop (thm', proper') = if (proper orelse not proper')
andalso matches_args (args_of thm') then
(if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
- Display.string_of_thm_global thy thm') else (); true)
+ Thm.string_of_thm_global thy thm') else (); true)
else false;
in (thm, proper) :: filter_out drop eqns end;
fun natural_order eqns =
--- a/src/Pure/Isar/context_rules.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/context_rules.ML Fri Sep 25 23:41:24 2015 +0200
@@ -121,7 +121,7 @@
fun prt_kind (i, b) =
Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
(map_filter (fn (_, (k, th)) =>
- if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE)
+ if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE)
(sort (int_ord o apply2 fst) rules));
in Pretty.writeln_chunks (map prt_kind rule_kinds) end;
--- a/src/Pure/Isar/element.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/element.ML Fri Sep 25 23:41:24 2015 +0200
@@ -152,7 +152,7 @@
let
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
- val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
+ val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
fun prt_binding (b, atts) =
Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
--- a/src/Pure/Isar/generic_target.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML Fri Sep 25 23:41:24 2015 +0200
@@ -162,7 +162,7 @@
val ((_, def), lthy3) = lthy2
|> Local_Theory.background_theory_result
- (Thm.add_def lthy2 false false
+ (Thm.add_def (Proof_Context.defs_context lthy2) false false
(Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
in ((lhs, def), lthy3) end;
--- a/src/Pure/Isar/isar_cmd.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Sep 25 23:41:24 2015 +0200
@@ -238,12 +238,12 @@
Proof_Context.pretty_local_facts verbose (Toplevel.context_of st)
else
let
- val thy = Toplevel.theory_of st;
+ val ctxt = Toplevel.context_of st;
val prev_thys =
(case Toplevel.previous_context_of st of
SOME prev => [Proof_Context.theory_of prev]
- | NONE => Theory.parents_of thy);
- in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
+ | NONE => Theory.parents_of (Proof_Context.theory_of ctxt));
+ in Proof_Display.pretty_theorems_diff verbose prev_thys ctxt end;
(* print theorems, terms, types etc. *)
--- a/src/Pure/Isar/isar_syn.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Sep 25 23:41:24 2015 +0200
@@ -22,7 +22,8 @@
val _ =
Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
(Parse.type_args -- Parse.binding -- Parse.opt_mixfix
- >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
+ >> (fn ((args, a), mx) =>
+ Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
val _ =
Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
@@ -767,7 +768,13 @@
Outer_Syntax.command @{command_keyword print_theory}
"print logical theory contents"
(Parse.opt_bang >> (fn b =>
- Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
+ Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of)));
+
+val _ =
+ Outer_Syntax.command @{command_keyword print_definitions}
+ "print dependencies of definitional theory content"
+ (Parse.opt_bang >> (fn b =>
+ Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_syntax}
--- a/src/Pure/Isar/local_defs.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML Fri Sep 25 23:41:24 2015 +0200
@@ -176,7 +176,7 @@
fun print_rules ctxt =
Pretty.writeln (Pretty.big_list "definitional rewrite rules:"
- (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
+ (map (Thm.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm o Thm.trim_context);
val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm o Thm.trim_context);
--- a/src/Pure/Isar/method.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/method.ML Fri Sep 25 23:41:24 2015 +0200
@@ -218,7 +218,7 @@
fun trace ctxt rules =
if Config.get ctxt rule_trace andalso not (null rules) then
- Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules)
+ Pretty.big_list "rules:" (map (Thm.pretty_thm_item ctxt) rules)
|> Pretty.string_of |> tracing
else ();
--- a/src/Pure/Isar/object_logic.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/object_logic.ML Fri Sep 25 23:41:24 2015 +0200
@@ -87,10 +87,13 @@
local
fun gen_add_judgment add_consts (b, T, mx) thy =
- let val c = Sign.full_name thy b in
- thy
- |> add_consts [(b, T, mx)]
- |> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy')
+ let
+ val c = Sign.full_name thy b;
+ val thy' = thy |> add_consts [(b, T, mx)];
+ val T' = Logic.unvarifyT_global (Sign.the_const_type thy' c);
+ in
+ thy'
+ |> Theory.add_deps_global "" (Theory.const_dep thy' (c, T')) []
|> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
if is_some judgment then error "Attempt to redeclare object-logic judgment"
else (base_sort, SOME c, atomize_rulify))
--- a/src/Pure/Isar/obtain.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Fri Sep 25 23:41:24 2015 +0200
@@ -257,9 +257,9 @@
[prem] =>
if Thm.concl_of th aconv thesis andalso
Logic.strip_assums_concl prem aconv thesis then th
- else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
+ else error ("Guessed a different clause:\n" ^ Thm.string_of_thm ctxt th)
| [] => error "Goal solved -- nothing guessed"
- | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
+ | _ => error ("Guess split into several cases:\n" ^ Thm.string_of_thm ctxt th));
fun result tac facts ctxt =
let
@@ -308,7 +308,7 @@
val thy = Proof_Context.theory_of ctxt;
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
- fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
+ fun err msg th = error (msg ^ ":\n" ^ Thm.string_of_thm ctxt th);
val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
--- a/src/Pure/Isar/parse_spec.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML Fri Sep 25 23:41:24 2015 +0200
@@ -29,6 +29,7 @@
val obtains: Element.obtains parser
val general_statement: (Element.context list * Element.statement) parser
val statement_keyword: string parser
+ val overloaded: bool parser
end;
structure Parse_Spec: PARSE_SPEC =
@@ -155,4 +156,10 @@
val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
+
+(* options *)
+
+val overloaded =
+ Scan.optional (Parse.$$$ "(" -- Parse.$$$ "overloaded" -- Parse.$$$ ")" >> K true) false;
+
end;
--- a/src/Pure/Isar/proof.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/proof.ML Fri Sep 25 23:41:24 2015 +0200
@@ -495,7 +495,7 @@
error "Bad background theory of goal state";
val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
- fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
+ fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
val th =
(Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
@@ -511,7 +511,7 @@
handle THM _ => err_lost ();
val _ =
Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results))
- orelse error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
+ orelse error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th);
fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
| recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
--- a/src/Pure/Isar/proof_context.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Sep 25 23:41:24 2015 +0200
@@ -44,6 +44,7 @@
val class_space: Proof.context -> Name_Space.T
val type_space: Proof.context -> Name_Space.T
val const_space: Proof.context -> Name_Space.T
+ val defs_context: Proof.context -> Defs.context
val intern_class: Proof.context -> xstring -> string
val intern_type: Proof.context -> xstring -> string
val intern_const: Proof.context -> xstring -> string
@@ -286,7 +287,7 @@
val tsig_of = #1 o #tsig o rep_data;
val set_defsort = map_tsig o apfst o Type.set_defsort;
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
-fun arity_sorts ctxt = Type.arity_sorts (Context.pretty ctxt) (tsig_of ctxt);
+fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt);
val consts_of = #1 o #consts o rep_data;
val cases_of = #cases o rep_data;
@@ -322,6 +323,8 @@
val type_space = Type.type_space o tsig_of;
val const_space = Consts.space_of o consts_of;
+fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt));
+
val intern_class = Name_Space.intern o class_space;
val intern_type = Name_Space.intern o type_space;
val intern_const = Name_Space.intern o const_space;
@@ -346,7 +349,7 @@
map_tsig (fn tsig as (local_tsig, global_tsig) =>
let val thy_tsig = Sign.tsig_of thy in
if Type.eq_tsig (thy_tsig, global_tsig) then tsig
- else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*)
+ else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*)
end) |>
map_consts (fn consts as (local_consts, global_consts) =>
let val thy_consts = Sign.consts_of thy in
@@ -393,8 +396,8 @@
fun pretty_fact ctxt =
let
- val pretty_thm = Display.pretty_thm ctxt;
- val pretty_thms = map (Display.pretty_thm_item ctxt);
+ val pretty_thm = Thm.pretty_thm ctxt;
+ val pretty_thms = map (Thm.pretty_thm_item ctxt);
in
fn ("", [th]) => pretty_thm th
| ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
@@ -552,7 +555,7 @@
fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
- in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
+ in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end;
in
@@ -577,8 +580,9 @@
local
-fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt)
- (not (abbrev_mode ctxt)) (consts_of ctxt);
+fun certify_consts ctxt =
+ Consts.certify (Context.Proof ctxt) (tsig_of ctxt)
+ (not (abbrev_mode ctxt)) (consts_of ctxt);
fun expand_binds ctxt =
let
@@ -761,7 +765,7 @@
t
|> expand_abbrevs ctxt
|> (fn t' =>
- #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t')
+ #1 (Sign.certify' prop (Context.Proof ctxt) false (consts_of ctxt) (theory_of ctxt) t')
handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
in
--- a/src/Pure/Isar/proof_display.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML Fri Sep 25 23:41:24 2015 +0200
@@ -12,10 +12,10 @@
val pp_term: (unit -> theory) -> term -> Pretty.T
val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T
val pp_cterm: (unit -> theory) -> cterm -> Pretty.T
- val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list
- val pretty_theorems: bool -> theory -> Pretty.T list
- val pretty_full_theory: bool -> theory -> Pretty.T
- val print_theory: theory -> unit
+ val pretty_theory: bool -> Proof.context -> Pretty.T
+ val pretty_definitions: bool -> Proof.context -> Pretty.T
+ val pretty_theorems_diff: bool -> theory list -> Proof.context -> Pretty.T list
+ val pretty_theorems: bool -> Proof.context -> Pretty.T list
val string_of_rule: Proof.context -> string -> thm -> string
val pretty_goal_header: thm -> Pretty.T
val string_of_goal: Proof.context -> thm -> string
@@ -31,7 +31,7 @@
structure Proof_Display: PROOF_DISPLAY =
struct
-(* toplevel pretty printing *)
+(** toplevel pretty printing **)
fun pp_context ctxt =
(if Config.get ctxt Proof_Context.debug then
@@ -48,7 +48,7 @@
| NONE => Syntax.init_pretty_global (mk_thy ()));
fun pp_thm mk_thy th =
- Display.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
+ Thm.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T);
fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t);
@@ -57,30 +57,165 @@
fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct);
-(* theorems and theory *)
+
+(** theory content **)
+
+fun pretty_theory verbose ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+
+ fun prt_cls c = Syntax.pretty_sort ctxt [c];
+ fun prt_sort S = Syntax.pretty_sort ctxt S;
+ fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
+ fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
+ val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
+ fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
+ val prt_term_no_vars = prt_term o Logic.unvarify_global;
+ fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
+
+ fun pretty_classrel (c, []) = prt_cls c
+ | pretty_classrel (c, cs) = Pretty.block
+ (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs));
+
+ fun pretty_default S = Pretty.block
+ [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
+
+ val tfrees = map (fn v => TFree (v, []));
+ fun pretty_type syn (t, Type.LogicalType n) =
+ if syn then NONE
+ else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
+ | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) =
+ if syn <> syn' then NONE
+ else SOME (Pretty.block
+ [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
+ | pretty_type syn (t, Type.Nonterminal) =
+ if not syn then NONE
+ else SOME (prt_typ (Type (t, [])));
+
+ val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
+
+ fun pretty_abbrev (c, (ty, t)) = Pretty.block
+ (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]);
+
+ fun pretty_axm (a, t) =
+ Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
-fun pretty_theorems_diff verbose prev_thys thy =
+ val tsig = Sign.tsig_of thy;
+ val consts = Sign.consts_of thy;
+ val {const_space, constants, constraints} = Consts.dest consts;
+ val {classes, default, types, ...} = Type.rep_tsig tsig;
+ val type_space = Type.type_space tsig;
+ val (class_space, class_algebra) = classes;
+ val classes = Sorts.classes_of class_algebra;
+ val arities = Sorts.arities_of class_algebra;
+
+ val clsses =
+ Name_Space.extern_entries verbose ctxt class_space
+ (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
+ |> map (apfst #1);
+ val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1);
+ val arties =
+ Name_Space.extern_entries verbose ctxt type_space (Symtab.dest arities)
+ |> map (apfst #1);
+
+ val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
+ val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
+ val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
+ val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
+
+ val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
+ in
+ Pretty.chunks
+ [Pretty.big_list "classes:" (map pretty_classrel clsses),
+ pretty_default default,
+ Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
+ Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
+ Pretty.big_list "type arities:" (pretty_arities arties),
+ Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
+ Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
+ Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
+ Pretty.big_list "axioms:" (map pretty_axm axms),
+ Pretty.block
+ (Pretty.breaks (Pretty.str "oracles:" ::
+ map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))]
+ end;
+
+
+(* theorems *)
+
+fun pretty_theorems_diff verbose prev_thys ctxt =
let
- val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
- val facts = Global_Theory.facts_of thy;
+ val pretty_fact = Proof_Context.pretty_fact ctxt;
+ val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss));
in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
-fun pretty_theorems verbose thy =
- pretty_theorems_diff verbose (Theory.parents_of thy) thy;
+fun pretty_theorems verbose ctxt =
+ pretty_theorems_diff verbose (Theory.parents_of (Proof_Context.theory_of ctxt)) ctxt;
+
+
+(* definitions *)
+
+fun pretty_definitions verbose ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val context = Proof_Context.defs_context ctxt;
+
+ val const_space = Proof_Context.const_space ctxt;
+ val type_space = Proof_Context.type_space ctxt;
+ val item_space = fn Defs.Const => const_space | Defs.Type => type_space;
+ fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
+
+ fun extern_item (kind, name) =
+ let val xname = Name_Space.extern ctxt (item_space kind) name
+ in (xname, (kind, name)) end;
+
+ fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) =
+ (case Defs.item_kind_ord (kind1, kind2) of
+ EQUAL => string_ord (xname1, xname2)
+ | ord => ord);
+
+ fun sort_items f = sort (extern_item_ord o apply2 f);
+
+ fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args);
-fun pretty_full_theory verbose thy =
- Pretty.chunks (Display.pretty_full_theory verbose thy @ pretty_theorems verbose thy);
+ fun pretty_reduct (lhs, rhs) = Pretty.block
+ ([pretty_entry lhs, Pretty.str " ->", Pretty.brk 2] @
+ Pretty.commas (map pretty_entry (sort_items fst rhs)));
+
+ fun pretty_restrict (entry, name) =
+ Pretty.block ([pretty_entry entry, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
+
+ val defs = Theory.defs_of thy;
+ val {restricts, reducts} = Defs.dest defs;
-val print_theory = Pretty.writeln o pretty_full_theory false;
+ val (reds1, reds2) =
+ filter_out (prune_item o #1 o #1) reducts
+ |> map (fn (lhs, rhs) =>
+ (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
+ |> sort_items (#1 o #1)
+ |> filter_out (null o #2)
+ |> List.partition (Defs.plain_args o #2 o #1);
+ val rests = restricts |> map (apfst (apfst extern_item)) |> sort_items (#1 o #1);
+ in
+ Pretty.big_list "definitions:"
+ (map (Pretty.text_fold o single)
+ [Pretty.big_list "non-overloaded LHS:" (map pretty_reduct reds1),
+ Pretty.big_list "overloaded LHS:" (map pretty_reduct reds2),
+ Pretty.big_list "pattern restrictions due to incomplete LHS:" (map pretty_restrict rests)])
+ end;
+
+
+
+(** proof items **)
(* refinement rule *)
fun pretty_rule ctxt s thm =
Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
- Pretty.fbrk, Display.pretty_thm ctxt thm];
+ Pretty.fbrk, Thm.pretty_thm ctxt thm];
val string_of_rule = Pretty.string_of ooo pretty_rule;
--- a/src/Pure/Isar/runtime.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/runtime.ML Fri Sep 25 23:41:24 2015 +0200
@@ -119,7 +119,7 @@
(msg :: robust_context context Syntax.string_of_term (map Thm.term_of cts))
| THM (msg, i, thms) =>
raised exn ("THM " ^ string_of_int i)
- (msg :: robust_context context Display.string_of_thm thms)
+ (msg :: robust_context context Thm.string_of_thm thms)
| _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []);
in [((i, msg), id)] end)
and sorted_msgs context exn =
--- a/src/Pure/Isar/token.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/token.ML Fri Sep 25 23:41:24 2015 +0200
@@ -498,7 +498,7 @@
| SOME (Typ T) => Syntax.pretty_typ ctxt T
| SOME (Term t) => Syntax.pretty_term ctxt t
| SOME (Fact (_, ths)) =>
- Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
+ Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Thm.pretty_thm ctxt) ths))
| _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
fun pretty_src ctxt src =
--- a/src/Pure/Isar/typedecl.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Isar/typedecl.ML Fri Sep 25 23:41:24 2015 +0200
@@ -7,9 +7,12 @@
signature TYPEDECL =
sig
val read_constraint: Proof.context -> string option -> sort
- val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory
- val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
- val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory
+ val basic_typedecl: {final: bool} -> binding * int * mixfix ->
+ local_theory -> string * local_theory
+ val typedecl: {final: bool} -> binding * (string * sort) list * mixfix ->
+ local_theory -> typ * local_theory
+ val typedecl_global: {final: bool} -> binding * (string * sort) list * mixfix ->
+ theory -> typ * theory
val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory
val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory
val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory
@@ -35,13 +38,6 @@
|> pair name
end;
-fun basic_typedecl (b, n, mx) lthy =
- basic_decl (fn name =>
- Sign.add_type lthy (b, n, NoSyn) #>
- (case Object_Logic.get_base_sort lthy of
- SOME S => Axclass.arity_axiomatization (name, replicate n S, S)
- | NONE => I)) (b, n, mx) lthy;
-
(* global type -- without dependencies on type parameters of the context *)
@@ -61,21 +57,39 @@
commas_quote (map (Syntax.string_of_typ lthy) bad_args));
in T end;
+fun final_type (b, n) lthy =
+ let
+ val c = Local_Theory.full_name lthy b;
+ val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
+ in
+ Local_Theory.background_theory
+ (Theory.add_deps (Proof_Context.defs_context lthy) "" (Theory.type_dep (c, args)) []) lthy
+ end;
+
+fun basic_typedecl {final} (b, n, mx) lthy =
+ lthy
+ |> basic_decl (fn name =>
+ Sign.add_type lthy (b, n, NoSyn) #>
+ (case Object_Logic.get_base_sort lthy of
+ SOME S => Axclass.arity_axiomatization (name, replicate n S, S)
+ | NONE => I)) (b, n, mx)
+ ||> final ? final_type (b, n);
+
(* type declarations *)
-fun typedecl (b, raw_args, mx) lthy =
+fun typedecl {final} (b, raw_args, mx) lthy =
let val T = global_type lthy (b, raw_args) in
lthy
- |> basic_typedecl (b, length raw_args, mx)
+ |> basic_typedecl {final = final} (b, length raw_args, mx)
|> snd
|> Variable.declare_typ T
|> pair T
end;
-fun typedecl_global decl =
+fun typedecl_global {final} decl =
Named_Target.theory_init
- #> typedecl decl
+ #> typedecl {final = final} decl
#> Local_Theory.exit_result_global Morphism.typ;
@@ -121,4 +135,3 @@
#> Local_Theory.exit_result_global (K I);
end;
-
--- a/src/Pure/Proof/reconstruct.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Proof/reconstruct.ML Fri Sep 25 23:41:24 2015 +0200
@@ -254,8 +254,8 @@
let
fun search env [] = error ("Unsolvable constraints:\n" ^
Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
- Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (apply2
- (Envir.norm_term bigenv) p)) cs)))
+ Thm.pretty_flexpair (Syntax.init_pretty_global thy)
+ (apply2 (Envir.norm_term bigenv) p)) cs)))
| search env ((u, p as (t1, t2), vs)::ps) =
if u then
let
--- a/src/Pure/Pure.thy Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Pure.thy Fri Sep 25 23:41:24 2015 +0200
@@ -74,8 +74,8 @@
and "also" "moreover" :: prf_decl % "proof"
and "finally" "ultimately" :: prf_chain % "proof"
and "back" :: prf_script % "proof"
- and "help" "print_commands" "print_options" "print_context"
- "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
+ and "help" "print_commands" "print_options" "print_context" "print_theory"
+ "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules"
"print_theorems" "print_locales" "print_classes" "print_locale"
"print_interps" "print_dependencies" "print_attributes"
"print_simpset" "print_rules" "print_trans_rules" "print_methods"
--- a/src/Pure/ROOT Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/ROOT Fri Sep 25 23:41:24 2015 +0200
@@ -247,7 +247,6 @@
"context_position.ML"
"conv.ML"
"defs.ML"
- "display.ML"
"drule.ML"
"envir.ML"
"facts.ML"
--- a/src/Pure/ROOT.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/ROOT.ML Fri Sep 25 23:41:24 2015 +0200
@@ -170,8 +170,8 @@
use "envir.ML";
use "consts.ML";
use "primitive_defs.ML";
+use "sign.ML";
use "defs.ML";
-use "sign.ML";
use "term_sharing.ML";
use "pattern.ML";
use "unify.ML";
@@ -195,7 +195,6 @@
use "raw_simplifier.ML";
use "conjunction.ML";
use "assumption.ML";
-use "display.ML";
(* Isar -- Intelligible Semi-Automated Reasoning *)
--- a/src/Pure/Syntax/syntax.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Sep 25 23:41:24 2015 +0200
@@ -65,7 +65,7 @@
val is_pretty_global: Proof.context -> bool
val set_pretty_global: bool -> Proof.context -> Proof.context
val init_pretty_global: theory -> Proof.context
- val init_pretty: Context.pretty -> Proof.context
+ val init_pretty: Context.generic -> Proof.context
val pretty_term_global: theory -> term -> Pretty.T
val pretty_typ_global: theory -> typ -> Pretty.T
val pretty_sort_global: theory -> sort -> Pretty.T
@@ -324,7 +324,7 @@
fun is_pretty_global ctxt = Config.get ctxt pretty_global;
val set_pretty_global = Config.put pretty_global;
val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
-val init_pretty = Context.pretty_context init_pretty_global;
+val init_pretty = Context.cases init_pretty_global I;
val pretty_term_global = pretty_term o init_pretty_global;
val pretty_typ_global = pretty_typ o init_pretty_global;
--- a/src/Pure/Tools/class_deps.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML Fri Sep 25 23:41:24 2015 +0200
@@ -29,7 +29,7 @@
Graph_Display.content_node (Name_Space.extern ctxt space c)
(Class.pretty_specification (Proof_Context.theory_of ctxt) c);
in
- Sorts.subalgebra (Context.pretty ctxt) pred (K NONE) algebra
+ Sorts.subalgebra (Context.Proof ctxt) pred (K NONE) algebra
|> #2 |> Sorts.classes_of |> Graph.dest
|> map (fn ((c, _), ds) => ((c, node c), ds))
end;
--- a/src/Pure/Tools/find_theorems.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Fri Sep 25 23:41:24 2015 +0200
@@ -462,7 +462,7 @@
in
fun pretty_thm ctxt (thmref, thm) =
- Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]);
+ Pretty.block (pretty_ref ctxt thmref @ [Thm.pretty_thm ctxt thm]);
fun pretty_theorems state opt_limit rem_dups raw_criteria =
let
--- a/src/Pure/axclass.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/axclass.ML Fri Sep 25 23:41:24 2015 +0200
@@ -82,25 +82,25 @@
Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
proven_arities = proven_arities, inst_params = inst_params};
-structure Data = Theory_Data_PP
+structure Data = Theory_Data'
(
type T = data;
val empty =
make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty));
val extend = I;
- fun merge pp
+ fun merge old_thys
(Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
proven_arities = proven_arities1, inst_params = inst_params1},
Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
proven_arities = proven_arities2, inst_params = inst_params2}) =
let
- val ctxt = Syntax.init_pretty pp;
+ val old_ctxt = Syntax.init_pretty_global (fst old_thys);
val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
val params' =
if null params1 then params2
else
- fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p)
+ fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p)
params2 params1;
(*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
@@ -596,6 +596,9 @@
fun class_const c =
(Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
+fun class_const_dep c =
+ ((Defs.Const, Logic.const_of_class c), [Term.aT []]);
+
in
val classrel_axiomatization =
@@ -614,7 +617,7 @@
thy
|> Sign.primitive_class (bclass, super)
|> classrel_axiomatization (map (fn c => (class, c)) super)
- |> Theory.add_deps_global "" (class_const class) (map class_const super)
+ |> Theory.add_deps_global "" (class_const_dep class) (map class_const_dep super)
end;
end;
--- a/src/Pure/consts.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/consts.ML Fri Sep 25 23:41:24 2015 +0200
@@ -27,7 +27,7 @@
val intern: T -> xstring -> string
val intern_syntax: T -> xstring -> string
val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
- val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
+ val certify: Context.generic -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
val declare: Context.generic -> binding * typ -> T -> T
@@ -155,11 +155,11 @@
(* certify *)
-fun certify pp tsig do_expand consts =
+fun certify context tsig do_expand consts =
let
fun err msg (c, T) =
raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
- Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
+ Syntax.string_of_typ (Syntax.init_pretty context) T, [], []);
val certT = Type.cert_typ tsig;
fun cert tm =
let
@@ -272,9 +272,8 @@
fun abbreviate context tsig mode (b, raw_rhs) consts =
let
- val pp = Context.pretty_generic context;
- val cert_term = certify pp tsig false consts;
- val expand_term = certify pp tsig true consts;
+ val cert_term = certify context tsig false consts;
+ val expand_term = certify context tsig true consts;
val force_expand = mode = Print_Mode.internal;
val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
--- a/src/Pure/context.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/context.ML Fri Sep 25 23:41:24 2015 +0200
@@ -31,14 +31,11 @@
type theory_id
val theory_id: theory -> theory_id
val timing: bool Unsynchronized.ref
- type pretty
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
val theory_id_name: theory_id -> string
val theory_name: theory -> string
val PureN: string
- val display_name: theory_id -> string
- val display_names: theory -> string list
val pretty_thy: theory -> Pretty.T
val string_of_thy: theory -> string
val pretty_abbrev_thy: theory -> Pretty.T
@@ -52,7 +49,7 @@
val subthy_id: theory_id * theory_id -> bool
val subthy: theory * theory -> bool
val finish_thy: theory -> theory
- val begin_thy: (theory -> pretty) -> string -> theory list -> theory
+ val begin_thy: string -> theory list -> theory
(*proof context*)
val raw_transfer: theory -> Proof.context -> Proof.context
(*certificate*)
@@ -77,11 +74,6 @@
val proof_map: (generic -> generic) -> Proof.context -> Proof.context
val theory_of: generic -> theory (*total*)
val proof_of: generic -> Proof.context (*total*)
- (*pretty printing context*)
- val pretty: Proof.context -> pretty
- val pretty_global: theory -> pretty
- val pretty_generic: generic -> pretty
- val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
(*thread data*)
val thread_data: unit -> generic option
val the_thread_data: unit -> generic
@@ -97,7 +89,7 @@
structure Theory_Data:
sig
val declare: Position.T -> Any.T -> (Any.T -> Any.T) ->
- (pretty -> Any.T * Any.T -> Any.T) -> serial
+ (theory * theory -> Any.T * Any.T -> Any.T) -> serial
val get: serial -> (Any.T -> 'a) -> theory -> 'a
val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
end
@@ -114,55 +106,9 @@
(*** theory context ***)
-(** theory data **)
-
-(* data kinds and access methods *)
-
-val timing = Unsynchronized.ref false;
-
(*private copy avoids potential conflict of table exceptions*)
structure Datatab = Table(type key = int val ord = int_ord);
-datatype pretty = Pretty of Any.T;
-
-local
-
-type kind =
- {pos: Position.T,
- empty: Any.T,
- extend: Any.T -> Any.T,
- merge: pretty -> Any.T * Any.T -> Any.T};
-
-val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
-
-fun invoke name f k x =
- (case Datatab.lookup (Synchronized.value kinds) k of
- SOME kind =>
- if ! timing andalso name <> "" then
- Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
- (fn () => f kind x)
- else f kind x
- | NONE => raise Fail "Invalid theory data identifier");
-
-in
-
-fun invoke_empty k = invoke "" (K o #empty) k ();
-val invoke_extend = invoke "extend" #extend;
-fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
-
-fun declare_theory_data pos empty extend merge =
- let
- val k = serial ();
- val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
- val _ = Synchronized.change kinds (Datatab.update (k, kind));
- in k end;
-
-val extend_data = Datatab.map invoke_extend;
-fun merge_data pp = Datatab.join (invoke_merge pp) o apply2 extend_data;
-
-end;
-
-
(** datatype theory **)
@@ -288,6 +234,51 @@
+(** theory data **)
+
+(* data kinds and access methods *)
+
+val timing = Unsynchronized.ref false;
+
+local
+
+type kind =
+ {pos: Position.T,
+ empty: Any.T,
+ extend: Any.T -> Any.T,
+ merge: theory * theory -> Any.T * Any.T -> Any.T};
+
+val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
+
+fun invoke name f k x =
+ (case Datatab.lookup (Synchronized.value kinds) k of
+ SOME kind =>
+ if ! timing andalso name <> "" then
+ Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
+ (fn () => f kind x)
+ else f kind x
+ | NONE => raise Fail "Invalid theory data identifier");
+
+in
+
+fun invoke_empty k = invoke "" (K o #empty) k ();
+val invoke_extend = invoke "extend" #extend;
+fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
+
+fun declare_theory_data pos empty extend merge =
+ let
+ val k = serial ();
+ val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
+ val _ = Synchronized.change kinds (Datatab.update (k, kind));
+ in k end;
+
+val extend_data = Datatab.map invoke_extend;
+fun merge_data thys = Datatab.join (invoke_merge thys) o apply2 extend_data;
+
+end;
+
+
+
(** build theories **)
(* primitives *)
@@ -325,12 +316,12 @@
local
-fun merge_thys pp (thy1, thy2) =
+fun merge_thys (thy1, thy2) =
let
val ids = merge_ids thy1 thy2;
val history = make_history "" 0;
val ancestry = make_ancestry [] [];
- val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
+ val data = merge_data (thy1, thy2) (data_of thy1, data_of thy2);
in create_thy ids history ancestry data end;
fun maximal_thys thys =
@@ -338,7 +329,7 @@
in
-fun begin_thy pp name imports =
+fun begin_thy name imports =
if name = "" then error ("Bad theory name: " ^ quote name)
else
let
@@ -351,7 +342,7 @@
(case parents of
[] => error "Missing theory imports"
| [thy] => extend_thy thy
- | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
+ | thy :: thys => Library.foldl merge_thys (thy, thys));
val history = make_history name 0;
val ancestry = make_ancestry parents ancestors;
@@ -498,17 +489,6 @@
val proof_of = cases Proof_Context.init_global I;
-(* pretty printing context *)
-
-exception PRETTY of generic;
-
-val pretty_generic = Pretty o PRETTY;
-val pretty = pretty_generic o Proof;
-val pretty_global = pretty_generic o Theory;
-
-fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
-
-
(** thread data **)
@@ -551,12 +531,12 @@
(** theory data **)
-signature THEORY_DATA_PP_ARGS =
+signature THEORY_DATA'_ARGS =
sig
type T
val empty: T
val extend: T -> T
- val merge: Context.pretty -> T * T -> T
+ val merge: theory * theory -> T * T -> T
end;
signature THEORY_DATA_ARGS =
@@ -575,7 +555,7 @@
val map: (T -> T) -> theory -> theory
end;
-functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
+functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA =
struct
type T = Data.T;
@@ -586,7 +566,7 @@
(Position.thread_data ())
(Data Data.empty)
(fn Data x => Data (Data.extend x))
- (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
+ (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)));
val get = Context.Theory_Data.get kind (fn Data x => x);
val put = Context.Theory_Data.put kind Data;
@@ -595,7 +575,7 @@
end;
functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
- Theory_Data_PP
+ Theory_Data'
(
type T = Data.T;
val empty = Data.empty;
--- a/src/Pure/defs.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/defs.ML Fri Sep 25 23:41:24 2015 +0200
@@ -7,39 +7,76 @@
signature DEFS =
sig
- val pretty_const: Proof.context -> string * typ list -> Pretty.T
+ datatype item_kind = Const | Type
+ type item = item_kind * string
+ type entry = item * typ list
+ val item_kind_ord: item_kind * item_kind -> order
val plain_args: typ list -> bool
+ type context = Proof.context * (Name_Space.T * Name_Space.T)
+ val global_context: theory -> context
+ val space: context -> item_kind -> Name_Space.T
+ val pretty_item: context -> item -> Pretty.T
+ val pretty_args: Proof.context -> typ list -> Pretty.T list
+ val pretty_entry: context -> entry -> Pretty.T
type T
type spec =
{def: string option,
description: string,
pos: Position.T,
lhs: typ list,
- rhs: (string * typ list) list}
- val all_specifications_of: T -> (string * spec list) list
- val specifications_of: T -> string -> spec list
+ rhs: entry list}
+ val all_specifications_of: T -> (item * spec list) list
+ val specifications_of: T -> item -> spec list
val dest: T ->
- {restricts: ((string * typ list) * string) list,
- reducts: ((string * typ list) * (string * typ list) list) list}
+ {restricts: (entry * string) list,
+ reducts: (entry * entry list) list}
val empty: T
- val merge: Proof.context -> T * T -> T
- val define: Proof.context -> bool -> string option -> string ->
- string * typ list -> (string * typ list) list -> T -> T
-end
+ val merge: context -> T * T -> T
+ val define: context -> bool -> string option -> string -> entry -> entry list -> T -> T
+ val get_deps: T -> item -> (typ list * entry list) list
+end;
structure Defs: DEFS =
struct
-(* type arguments *)
+(* specification items *)
+
+datatype item_kind = Const | Type;
+type item = item_kind * string;
+type entry = item * typ list;
-type args = typ list;
+fun item_kind_ord (Const, Type) = LESS
+ | item_kind_ord (Type, Const) = GREATER
+ | item_kind_ord _ = EQUAL;
+
+structure Itemtab = Table(type key = item val ord = prod_ord item_kind_ord fast_string_ord);
+
+
+(* pretty printing *)
+
+type context = Proof.context * (Name_Space.T * Name_Space.T)
-fun pretty_const ctxt (c, args) =
- let
- val prt_args =
- if null args then []
- else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
- in Pretty.block (Pretty.str c :: prt_args) end;
+fun global_context thy =
+ (Syntax.init_pretty_global thy, (Sign.const_space thy, Sign.type_space thy));
+
+fun space ((ctxt, spaces): context) kind =
+ if kind = Const then #1 spaces else #2 spaces;
+
+fun pretty_item (context as (ctxt, _)) (kind, name) =
+ let val prt_name = Name_Space.pretty ctxt (space context kind) name in
+ if kind = Const then prt_name
+ else Pretty.block [Pretty.keyword1 "type", Pretty.brk 1, prt_name]
+ end;
+
+fun pretty_args ctxt args =
+ if null args then []
+ else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
+
+fun pretty_entry context (c, args) =
+ Pretty.block (pretty_item context c :: pretty_args (#1 context) args);
+
+
+(* type arguments *)
fun plain_args args =
forall Term.is_TVar args andalso not (has_duplicates (op =) args);
@@ -62,32 +99,32 @@
{def: string option,
description: string,
pos: Position.T,
- lhs: args,
- rhs: (string * args) list};
+ lhs: typ list,
+ rhs: entry list};
type def =
{specs: spec Inttab.table, (*source specifications*)
- restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*)
- reducts: (args * (string * args) list) list}; (*specifications as reduction system*)
+ restricts: (typ list * string) list, (*global restrictions imposed by incomplete patterns*)
+ reducts: (typ list * entry list) list}; (*specifications as reduction system*)
fun make_def (specs, restricts, reducts) =
{specs = specs, restricts = restricts, reducts = reducts}: def;
fun map_def c f =
- Symtab.default (c, make_def (Inttab.empty, [], [])) #>
- Symtab.map_entry c (fn {specs, restricts, reducts}: def =>
+ Itemtab.default (c, make_def (Inttab.empty, [], [])) #>
+ Itemtab.map_entry c (fn {specs, restricts, reducts}: def =>
make_def (f (specs, restricts, reducts)));
-datatype T = Defs of def Symtab.table;
+datatype T = Defs of def Itemtab.table;
fun lookup_list which defs c =
- (case Symtab.lookup defs c of
+ (case Itemtab.lookup defs c of
SOME (def: def) => which def
| NONE => []);
fun all_specifications_of (Defs defs) =
- (map o apsnd) (map snd o Inttab.dest o #specs) (Symtab.dest defs);
+ (map o apsnd) (map snd o Inttab.dest o #specs) (Itemtab.dest defs);
fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
@@ -96,56 +133,58 @@
fun dest (Defs defs) =
let
- val restricts = Symtab.fold (fn (c, {restricts, ...}) =>
+ val restricts = Itemtab.fold (fn (c, {restricts, ...}) =>
fold (fn (args, description) => cons ((c, args), description)) restricts) defs [];
- val reducts = Symtab.fold (fn (c, {reducts, ...}) =>
+ val reducts = Itemtab.fold (fn (c, {reducts, ...}) =>
fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
in {restricts = restricts, reducts = reducts} end;
-val empty = Defs Symtab.empty;
+val empty = Defs Itemtab.empty;
(* specifications *)
-fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
+fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
i = j orelse disjoint_args (Ts, Us) orelse
- error ("Clash of specifications for constant " ^ quote c ^ ":\n" ^
+ error ("Clash of specifications for " ^ Pretty.str_of (pretty_item context c) ^ ":\n" ^
" " ^ quote a ^ Position.here pos_a ^ "\n" ^
" " ^ quote b ^ Position.here pos_b));
-fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
+fun join_specs context c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
let
val specs' =
- Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1;
+ Inttab.fold (fn spec2 => (disjoint_specs context c spec2 specs1; Inttab.update spec2))
+ specs2 specs1;
in make_def (specs', restricts, reducts) end;
-fun update_specs c spec = map_def c (fn (specs, restricts, reducts) =>
- (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts)));
+fun update_specs context c spec = map_def c (fn (specs, restricts, reducts) =>
+ (disjoint_specs context c spec specs; (Inttab.update spec specs, restricts, reducts)));
(* normalized dependencies: reduction with well-formedness check *)
local
-val prt = Pretty.string_of oo pretty_const;
-fun err ctxt (c, args) (d, Us) s1 s2 =
- error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
+val prt = Pretty.string_of oo pretty_entry;
-fun acyclic ctxt (c, args) (d, Us) =
+fun err context (c, args) (d, Us) s1 s2 =
+ error (s1 ^ " dependency of " ^ prt context (c, args) ^ " -> " ^ prt context (d, Us) ^ s2);
+
+fun acyclic context (c, args) (d, Us) =
c <> d orelse
is_none (match_args (args, Us)) orelse
- err ctxt (c, args) (d, Us) "Circular" "";
+ err context (c, args) (d, Us) "Circular" "";
-fun wellformed ctxt defs (c, args) (d, Us) =
+fun wellformed context defs (c, args) (d, Us) =
plain_args Us orelse
(case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
SOME (Ts, description) =>
- err ctxt (c, args) (d, Us) "Malformed"
- ("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")")
+ err context (c, args) (d, Us) "Malformed"
+ ("\n(restriction " ^ prt context (d, Ts) ^ " from " ^ quote description ^ ")")
| NONE => true);
-fun reduction ctxt defs const deps =
+fun reduction context defs const deps =
let
fun reduct Us (Ts, rhs) =
(case match_args (Ts, Us) of
@@ -158,67 +197,69 @@
if forall (is_none o #1) reds then NONE
else SOME (fold_rev
(fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
- val _ = forall (acyclic ctxt const) (the_default deps deps');
+ val _ = forall (acyclic context const) (the_default deps deps');
in deps' end;
in
-fun normalize ctxt =
+fun normalize context =
let
fun norm_update (c, {reducts, ...}: def) (changed, defs) =
let
val reducts' = reducts |> map (fn (args, deps) =>
- (args, perhaps (reduction ctxt defs (c, args)) deps));
+ (args, perhaps (reduction context defs (c, args)) deps));
in
if reducts = reducts' then (changed, defs)
else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
end;
fun norm_all defs =
- (case Symtab.fold norm_update defs (false, defs) of
+ (case Itemtab.fold norm_update defs (false, defs) of
(true, defs') => norm_all defs'
| (false, _) => defs);
fun check defs (c, {reducts, ...}: def) =
- reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps);
- in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
+ reducts |> forall (fn (args, deps) => forall (wellformed context defs (c, args)) deps);
+ in norm_all #> (fn defs => tap (Itemtab.forall (check defs)) defs) end;
-fun dependencies ctxt (c, args) restr deps =
+fun dependencies context (c, args) restr deps =
map_def c (fn (specs, restricts, reducts) =>
let
val restricts' = Library.merge (op =) (restricts, restr);
val reducts' = insert (op =) (args, deps) reducts;
in (specs, restricts', reducts') end)
- #> normalize ctxt;
+ #> normalize context;
end;
(* merge *)
-fun merge ctxt (Defs defs1, Defs defs2) =
+fun merge context (Defs defs1, Defs defs2) =
let
fun add_deps (c, args) restr deps defs =
if AList.defined (op =) (reducts_of defs c) args then defs
- else dependencies ctxt (c, args) restr deps defs;
+ else dependencies context (c, args) restr deps defs;
fun add_def (c, {restricts, reducts, ...}: def) =
fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
in
- Defs (Symtab.join join_specs (defs1, defs2)
- |> normalize ctxt |> Symtab.fold add_def defs2)
+ Defs (Itemtab.join (join_specs context) (defs1, defs2)
+ |> normalize context |> Itemtab.fold add_def defs2)
end;
(* define *)
-fun define ctxt unchecked def description (c, args) deps (Defs defs) =
+fun define context unchecked def description (c, args) deps (Defs defs) =
let
val pos = Position.thread_data ();
val restr =
if plain_args args orelse
- (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false)
+ (case args of [Term.Type (_, rec_args)] => plain_args rec_args | _ => false)
then [] else [(args, description)];
val spec =
(serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps});
- val defs' = defs |> update_specs c spec;
- in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
+ val defs' = defs |> update_specs context c spec;
+ in Defs (defs' |> (if unchecked then I else dependencies context (c, args) restr deps)) end;
+
+fun get_deps (Defs defs) c = reducts_of defs c;
end;
--- a/src/Pure/display.ML Fri Sep 25 16:54:31 2015 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,205 +0,0 @@
-(* Title: Pure/display.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Author: Makarius
-
-Printing of theorems, results etc.
-*)
-
-signature BASIC_DISPLAY =
-sig
- val show_consts: bool Config.T
- val show_hyps_raw: Config.raw
- val show_hyps: bool Config.T
- val show_tags_raw: Config.raw
- val show_tags: bool Config.T
-end;
-
-signature DISPLAY =
-sig
- include BASIC_DISPLAY
- val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
- val pretty_thm: Proof.context -> thm -> Pretty.T
- val pretty_thm_item: Proof.context -> thm -> Pretty.T
- val pretty_thm_global: theory -> thm -> Pretty.T
- val string_of_thm: Proof.context -> thm -> string
- val string_of_thm_global: theory -> thm -> string
- val pretty_full_theory: bool -> theory -> Pretty.T list
-end;
-
-structure Display: DISPLAY =
-struct
-
-(** options **)
-
-val show_consts = Goal_Display.show_consts;
-
-val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
-val show_hyps = Config.bool show_hyps_raw;
-
-val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
-val show_tags = Config.bool show_tags_raw;
-
-
-
-(** print thm **)
-
-fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
-val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
-
-fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
- let
- val show_tags = Config.get ctxt show_tags;
- val show_hyps = Config.get ctxt show_hyps;
-
- val th = raw_th
- |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt)))
- |> perhaps (try Thm.strip_shyps);
-
- val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th;
- val extra_shyps = Thm.extra_shyps th;
- val tags = Thm.get_tags th;
- val tpairs = Thm.tpairs_of th;
-
- val q = if quote then Pretty.quote else I;
- val prt_term = q o Syntax.pretty_term ctxt;
-
-
- val hlen = length extra_shyps + length hyps + length tpairs;
- val hsymbs =
- if hlen = 0 then []
- else if show_hyps orelse show_hyps' then
- [Pretty.brk 2, Pretty.list "[" "]"
- (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
- map (Syntax.pretty_sort ctxt) extra_shyps)]
- else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
- val tsymbs =
- if null tags orelse not show_tags then []
- else [Pretty.brk 1, pretty_tags tags];
- in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end;
-
-fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
-fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
-
-fun pretty_thm_global thy =
- pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
-
-val string_of_thm = Pretty.string_of oo pretty_thm;
-val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
-
-
-
-(** print theory **)
-
-(* pretty_full_theory *)
-
-fun pretty_full_theory verbose thy =
- let
- val ctxt = Syntax.init_pretty_global thy;
-
- fun prt_cls c = Syntax.pretty_sort ctxt [c];
- fun prt_sort S = Syntax.pretty_sort ctxt S;
- fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
- fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
- val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
- fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
- val prt_term_no_vars = prt_term o Logic.unvarify_global;
- fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
- val prt_const' = Defs.pretty_const ctxt;
-
- fun pretty_classrel (c, []) = prt_cls c
- | pretty_classrel (c, cs) = Pretty.block
- (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs));
-
- fun pretty_default S = Pretty.block
- [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
-
- val tfrees = map (fn v => TFree (v, []));
- fun pretty_type syn (t, (Type.LogicalType n)) =
- if syn then NONE
- else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
- | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) =
- if syn <> syn' then NONE
- else SOME (Pretty.block
- [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
- | pretty_type syn (t, Type.Nonterminal) =
- if not syn then NONE
- else SOME (prt_typ (Type (t, [])));
-
- val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
-
- fun pretty_abbrev (c, (ty, t)) = Pretty.block
- (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]);
-
- fun pretty_axm (a, t) =
- Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
-
- fun pretty_finals reds = Pretty.block
- (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o fst) reds));
-
- fun pretty_reduct (lhs, rhs) = Pretty.block
- ([prt_const' lhs, Pretty.str " ->", Pretty.brk 2] @
- Pretty.commas (map prt_const' (sort_by #1 rhs)));
-
- fun pretty_restrict (const, name) =
- Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
-
- val defs = Theory.defs_of thy;
- val {restricts, reducts} = Defs.dest defs;
- val tsig = Sign.tsig_of thy;
- val consts = Sign.consts_of thy;
- val {const_space, constants, constraints} = Consts.dest consts;
- val extern_const = Name_Space.extern ctxt const_space;
- val {classes, default, types, ...} = Type.rep_tsig tsig;
- val (class_space, class_algebra) = classes;
- val classes = Sorts.classes_of class_algebra;
- val arities = Sorts.arities_of class_algebra;
-
- val clsses =
- Name_Space.extern_entries verbose ctxt class_space
- (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
- |> map (apfst #1);
- val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1);
- val arties =
- Name_Space.extern_entries verbose ctxt (Type.type_space tsig) (Symtab.dest arities)
- |> map (apfst #1);
-
- val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
- val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
- val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
- val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
-
- val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
-
- fun prune_const c = not verbose andalso Consts.is_concealed consts c;
- val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
- |> map (fn (lhs, rhs) =>
- (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
- |> sort_by (#1 o #1)
- |> List.partition (null o #2)
- ||> List.partition (Defs.plain_args o #2 o #1);
- val rests = restricts |> map (apfst (apfst extern_const)) |> sort_by (#1 o #1);
- in
- [Pretty.strs ("names:" :: Context.display_names thy)] @
- [Pretty.big_list "classes:" (map pretty_classrel clsses),
- pretty_default default,
- Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
- Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
- Pretty.big_list "type arities:" (pretty_arities arties),
- Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
- Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
- Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
- Pretty.big_list "axioms:" (map pretty_axm axms),
- Pretty.block
- (Pretty.breaks (Pretty.str "oracles:" ::
- map Pretty.mark_str (Thm.extern_oracles verbose ctxt))),
- Pretty.big_list "definitions:"
- [pretty_finals reds0,
- Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
- Pretty.big_list "overloaded:" (map pretty_reduct reds2),
- Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]
- end;
-
-end;
-
-structure Basic_Display: BASIC_DISPLAY = Display;
-open Basic_Display;
--- a/src/Pure/global_theory.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/global_theory.ML Fri Sep 25 23:41:24 2015 +0200
@@ -205,9 +205,9 @@
fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
let
- val ctxt = Syntax.init_pretty_global thy;
+ val context as (ctxt, _) = Defs.global_context thy;
val prop = prep ctxt (b, raw_prop);
- val ((_, def), thy') = Thm.add_def ctxt unchecked overloaded (b, prop) thy;
+ val ((_, def), thy') = Thm.add_def context unchecked overloaded (b, prop) thy;
val thm = def
|> Thm.forall_intr_frees
|> Thm.forall_elim_vars 0
--- a/src/Pure/goal_display.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/goal_display.ML Fri Sep 25 23:41:24 2015 +0200
@@ -11,9 +11,6 @@
val goals_limit: int Config.T
val show_main_goal_raw: Config.raw
val show_main_goal: bool Config.T
- val show_consts_raw: Config.raw
- val show_consts: bool Config.T
- val pretty_flexpair: Proof.context -> term * term -> Pretty.T
val pretty_goals: Proof.context -> thm -> Pretty.T list
val pretty_goal: Proof.context -> thm -> Pretty.T
val string_of_goal: Proof.context -> thm -> string
@@ -28,12 +25,6 @@
val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here});
val show_main_goal = Config.bool show_main_goal_raw;
-val show_consts_raw = Config.declare_option ("show_consts", @{here});
-val show_consts = Config.bool show_consts_raw;
-
-fun pretty_flexpair ctxt (t, u) = Pretty.block
- [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
-
(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
@@ -107,7 +98,7 @@
Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
- val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
+ val pretty_ffpairs = pretty_list "flex-flex pairs:" (Thm.pretty_flexpair ctxt);
val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
--- a/src/Pure/more_thm.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/more_thm.ML Fri Sep 25 23:41:24 2015 +0200
@@ -9,6 +9,9 @@
signature BASIC_THM =
sig
include BASIC_THM
+ val show_consts: bool Config.T
+ val show_hyps: bool Config.T
+ val show_tags: bool Config.T
structure Ctermtab: TABLE
structure Thmtab: TABLE
val aconvc: cterm * cterm -> bool
@@ -72,7 +75,7 @@
val rename_boundvars: term -> term -> thm -> thm
val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory
val add_axiom_global: binding * term -> theory -> (string * thm) * theory
- val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
+ val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
type attribute = Context.generic * thm -> Context.generic option * thm option
type binding = binding * attribute list
@@ -105,6 +108,19 @@
val kind: string -> attribute
val register_proofs: thm list -> theory -> theory
val join_theory_proofs: theory -> unit
+ val show_consts_raw: Config.raw
+ val show_consts: bool Config.T
+ val show_hyps_raw: Config.raw
+ val show_hyps: bool Config.T
+ val show_tags_raw: Config.raw
+ val show_tags: bool Config.T
+ val pretty_flexpair: Proof.context -> term * term -> Pretty.T
+ val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
+ val pretty_thm: Proof.context -> thm -> Pretty.T
+ val pretty_thm_item: Proof.context -> thm -> Pretty.T
+ val pretty_thm_global: theory -> thm -> Pretty.T
+ val string_of_thm: Proof.context -> thm -> string
+ val string_of_thm_global: theory -> thm -> string
end;
structure Thm: THM =
@@ -290,12 +306,8 @@
(case undeclared_hyps context th of
[] => th
| undeclared =>
- let
- val ctxt = Context.cases Syntax.init_pretty_global I context;
- in
- error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
- (map (Pretty.item o single o Syntax.pretty_term ctxt) undeclared)))
- end);
+ error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
+ (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared))));
@@ -475,13 +487,13 @@
fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy;
-fun add_def ctxt unchecked overloaded (b, prop) thy =
+fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy =
let
val _ = Sign.no_vars ctxt prop;
val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop);
val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
- val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy;
+ val thy' = Theory.add_def context unchecked overloaded (b, concl') thy;
val axm_name = Sign.full_name thy' b;
val axm' = Thm.axiom thy' axm_name;
val thm =
@@ -491,7 +503,7 @@
in ((axm_name, thm), thy') end;
fun add_def_global unchecked overloaded arg thy =
- add_def (Syntax.init_pretty_global thy) unchecked overloaded arg thy;
+ add_def (Defs.global_context thy) unchecked overloaded arg thy;
@@ -590,6 +602,70 @@
Thm.join_proofs (map (Thm.transfer thy) (rev (Proofs.get thy)));
+
+(** print theorems **)
+
+(* options *)
+
+val show_consts_raw = Config.declare_option ("show_consts", @{here});
+val show_consts = Config.bool show_consts_raw;
+
+val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
+val show_hyps = Config.bool show_hyps_raw;
+
+val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
+val show_tags = Config.bool show_tags_raw;
+
+
+(* pretty_thm etc. *)
+
+fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
+val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
+
+fun pretty_flexpair ctxt (t, u) = Pretty.block
+ [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
+
+fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
+ let
+ val show_tags = Config.get ctxt show_tags;
+ val show_hyps = Config.get ctxt show_hyps;
+
+ val th = raw_th
+ |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt)))
+ |> perhaps (try Thm.strip_shyps);
+
+ val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th;
+ val extra_shyps = Thm.extra_shyps th;
+ val tags = Thm.get_tags th;
+ val tpairs = Thm.tpairs_of th;
+
+ val q = if quote then Pretty.quote else I;
+ val prt_term = q o Syntax.pretty_term ctxt;
+
+
+ val hlen = length extra_shyps + length hyps + length tpairs;
+ val hsymbs =
+ if hlen = 0 then []
+ else if show_hyps orelse show_hyps' then
+ [Pretty.brk 2, Pretty.list "[" "]"
+ (map (q o pretty_flexpair ctxt) tpairs @ map prt_term hyps @
+ map (Syntax.pretty_sort ctxt) extra_shyps)]
+ else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
+ val tsymbs =
+ if null tags orelse not show_tags then []
+ else [Pretty.brk 1, pretty_tags tags];
+ in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end;
+
+fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
+fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
+
+fun pretty_thm_global thy =
+ pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
+
+val string_of_thm = Pretty.string_of oo pretty_thm;
+val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
+
+
open Thm;
end;
--- a/src/Pure/pure_thy.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/pure_thy.ML Fri Sep 25 23:41:24 2015 +0200
@@ -66,6 +66,10 @@
(Binding.make ("prop", @{here}), 0, NoSyn),
(Binding.make ("itself", @{here}), 1, NoSyn),
(Binding.make ("dummy", @{here}), 0, NoSyn)]
+ #> Theory.add_deps_global "fun" ((Defs.Type, "fun"), [typ "'a", typ "'b"]) []
+ #> Theory.add_deps_global "prop" ((Defs.Type, "prop"), []) []
+ #> Theory.add_deps_global "itself" ((Defs.Type, "itself"), [typ "'a"]) []
+ #> Theory.add_deps_global "dummy" ((Defs.Type, "dummy"), []) []
#> Sign.add_nonterminals_global
(map (fn name => Binding.make (name, @{here}))
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
@@ -194,11 +198,11 @@
(qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
(qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
(qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
- #> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") []
- #> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") []
- #> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") []
- #> Theory.add_deps_global "Pure.type" ("Pure.type", typ "'a itself") []
- #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") []
+ #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
+ #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) []
+ #> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []
+ #> Theory.add_deps_global "Pure.type" ((Defs.Const, "Pure.type"), [typ "'a"]) []
+ #> Theory.add_deps_global "Pure.dummy_pattern" ((Defs.Const, "Pure.dummy_pattern"), [typ "'a"]) []
#> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
#> Sign.parse_translation Syntax_Trans.pure_parse_translation
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
--- a/src/Pure/sign.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/sign.ML Fri Sep 25 23:41:24 2015 +0200
@@ -62,7 +62,7 @@
val certify_sort: theory -> sort -> sort
val certify_typ: theory -> typ -> typ
val certify_typ_mode: Type.mode -> theory -> typ -> typ
- val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int
+ val certify': bool -> Context.generic -> bool -> Consts.T -> theory -> term -> term * typ * int
val certify_term: theory -> term -> term * typ * int
val cert_term: theory -> term -> term
val cert_prop: theory -> term -> term
@@ -133,20 +133,20 @@
fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
-structure Data = Theory_Data_PP
+structure Data = Theory_Data'
(
type T = sign;
fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
- fun merge pp (sign1, sign2) =
+ fun merge old_thys (sign1, sign2) =
let
val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
val syn = Syntax.merge_syntax (syn1, syn2);
- val tsig = Type.merge_tsig pp (tsig1, tsig2);
+ val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2);
val consts = Consts.merge (consts1, consts2);
in make_sign (syn, tsig, consts) end;
);
@@ -257,7 +257,7 @@
(* certify wrt. type signature *)
val arity_number = Type.arity_number o tsig_of;
-fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
+fun arity_sorts thy = Type.arity_sorts (Context.Theory thy) (tsig_of thy);
val certify_class = Type.cert_class o tsig_of;
val certify_sort = Type.cert_sort o tsig_of;
@@ -269,14 +269,14 @@
local
-fun type_check pp tm =
+fun type_check context tm =
let
fun err_appl bs t T u U =
let
val xs = map Free bs; (*we do not rename here*)
val t' = subst_bounds (xs, t);
val u' = subst_bounds (xs, u);
- val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
+ val msg = Type.appl_error (Syntax.init_pretty context) t' T u' U;
in raise TYPE (msg, [T, U], [t', u']) end;
fun typ_of (_, Const (_, T)) = T
@@ -306,20 +306,19 @@
in
-fun certify' prop pp do_expand consts thy tm =
+fun certify' prop context do_expand consts thy tm =
let
val _ = check_vars tm;
val tm' = Term.map_types (certify_typ thy) tm;
- val T = type_check pp tm';
+ val T = type_check context tm';
val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
- val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
+ val tm'' = Consts.certify context (tsig_of thy) do_expand consts tm';
in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
-fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy;
-fun cert_term_abbrev thy =
- #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy;
+fun certify_term thy = certify' false (Context.Theory thy) true (consts_of thy) thy;
+fun cert_term_abbrev thy = #1 o certify' false (Context.Theory thy) false (consts_of thy) thy;
val cert_term = #1 oo certify_term;
-fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
+fun cert_prop thy = #1 o certify' true (Context.Theory thy) true (consts_of thy) thy;
end;
@@ -474,10 +473,10 @@
|> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
fun primitive_classrel arg thy =
- thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
+ thy |> map_tsig (Type.add_classrel (Context.Theory thy) arg);
fun primitive_arity arg thy =
- thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
+ thy |> map_tsig (Type.add_arity (Context.Theory thy) arg);
(* add translation functions *)
--- a/src/Pure/simplifier.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/simplifier.ML Fri Sep 25 23:41:24 2015 +0200
@@ -162,8 +162,8 @@
fun pretty_simpset verbose ctxt =
let
val pretty_term = Syntax.pretty_term ctxt;
- val pretty_thm = Display.pretty_thm ctxt;
- val pretty_thm_item = Display.pretty_thm_item ctxt;
+ val pretty_thm = Thm.pretty_thm ctxt;
+ val pretty_thm_item = Thm.pretty_thm_item ctxt;
fun pretty_simproc (name, lhss) =
Pretty.block
--- a/src/Pure/sorts.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/sorts.ML Fri Sep 25 23:41:24 2015 +0200
@@ -38,15 +38,15 @@
val minimize_sort: algebra -> sort -> sort
val complete_sort: algebra -> sort -> sort
val minimal_sorts: algebra -> sort list -> sort Ord_List.T
- val add_class: Context.pretty -> class * class list -> algebra -> algebra
- val add_classrel: Context.pretty -> class * class -> algebra -> algebra
- val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra
+ val add_class: Context.generic -> class * class list -> algebra -> algebra
+ val add_classrel: Context.generic -> class * class -> algebra -> algebra
+ val add_arities: Context.generic -> string * (class * sort list) list -> algebra -> algebra
val empty_algebra: algebra
- val merge_algebra: Context.pretty -> algebra * algebra -> algebra
- val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
+ val merge_algebra: Context.generic -> algebra * algebra -> algebra
+ val subalgebra: Context.generic -> (class -> bool) -> (class * string -> sort list option)
-> algebra -> (sort -> sort) * algebra
type class_error
- val class_error: Context.pretty -> class_error -> string
+ val class_error: Context.generic -> class_error -> string
exception CLASS_ERROR of class_error
val has_instance: algebra -> string -> sort -> bool
val mg_domain: algebra -> string -> sort -> sort list (*exception CLASS_ERROR*)
@@ -188,16 +188,16 @@
fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
-fun err_cyclic_classes pp css =
+fun err_cyclic_classes context css =
error (cat_lines (map (fn cs =>
- "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) cs) css));
+ "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty context) cs) css));
-fun add_class pp (c, cs) = map_classes (fn classes =>
+fun add_class context (c, cs) = map_classes (fn classes =>
let
val classes' = classes |> Graph.new_node (c, serial ())
handle Graph.DUP dup => err_dup_class dup;
val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
- handle Graph.CYCLES css => err_cyclic_classes pp css;
+ handle Graph.CYCLES css => err_cyclic_classes context css;
in classes'' end);
@@ -208,14 +208,14 @@
fun for_classes _ NONE = ""
| for_classes ctxt (SOME (c1, c2)) = " for classes " ^ Syntax.string_of_classrel ctxt [c1, c2];
-fun err_conflict pp t cc (c, Ss) (c', Ss') =
- let val ctxt = Syntax.init_pretty pp in
+fun err_conflict context t cc (c, Ss) (c', Ss') =
+ let val ctxt = Syntax.init_pretty context in
error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n " ^
Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n " ^
Syntax.string_of_arity ctxt (t, Ss', [c']))
end;
-fun coregular pp algebra t (c, Ss) ars =
+fun coregular context algebra t (c, Ss) ars =
let
fun conflict (c', Ss') =
if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
@@ -225,62 +225,62 @@
else NONE;
in
(case get_first conflict ars of
- SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
+ SOME ((c1, c2), (c', Ss')) => err_conflict context t (SOME (c1, c2)) (c, Ss) (c', Ss')
| NONE => (c, Ss) :: ars)
end;
fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
-fun insert pp algebra t (c, Ss) ars =
+fun insert context algebra t (c, Ss) ars =
(case AList.lookup (op =) ars c of
- NONE => coregular pp algebra t (c, Ss) ars
+ NONE => coregular context algebra t (c, Ss) ars
| SOME Ss' =>
if sorts_le algebra (Ss, Ss') then ars
else if sorts_le algebra (Ss', Ss)
- then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
- else err_conflict pp t NONE (c, Ss) (c, Ss'));
+ then coregular context algebra t (c, Ss) (remove (op =) (c, Ss') ars)
+ else err_conflict context t NONE (c, Ss) (c, Ss'));
in
-fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
+fun insert_ars context algebra t = fold_rev (insert context algebra t);
-fun insert_complete_ars pp algebra (t, ars) arities =
+fun insert_complete_ars context algebra (t, ars) arities =
let val ars' =
Symtab.lookup_list arities t
- |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
+ |> fold_rev (insert_ars context algebra t) (map (complete algebra) ars);
in Symtab.update (t, ars') arities end;
-fun add_arities pp arg algebra =
- algebra |> map_arities (insert_complete_ars pp algebra arg);
+fun add_arities context arg algebra =
+ algebra |> map_arities (insert_complete_ars context algebra arg);
-fun add_arities_table pp algebra =
- Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
+fun add_arities_table context algebra =
+ Symtab.fold (fn (t, ars) => insert_complete_ars context algebra (t, ars));
end;
(* classrel *)
-fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
+fun rebuild_arities context algebra = algebra |> map_arities (fn arities =>
Symtab.empty
- |> add_arities_table pp algebra arities);
+ |> add_arities_table context algebra arities);
-fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
+fun add_classrel context rel = rebuild_arities context o map_classes (fn classes =>
classes |> Graph.add_edge_trans_acyclic rel
- handle Graph.CYCLES css => err_cyclic_classes pp css);
+ handle Graph.CYCLES css => err_cyclic_classes context css);
(* empty and merge *)
val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
-fun merge_algebra pp
+fun merge_algebra context
(Algebra {classes = classes1, arities = arities1},
Algebra {classes = classes2, arities = arities2}) =
let
val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
handle Graph.DUP c => err_dup_class c
- | Graph.CYCLES css => err_cyclic_classes pp css;
+ | Graph.CYCLES css => err_cyclic_classes context css;
val algebra0 = make_algebra (classes', Symtab.empty);
val arities' =
(case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
@@ -288,20 +288,20 @@
| (true, false) => (*no completion*)
(arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
if pointer_eq (ars1, ars2) then raise Symtab.SAME
- else insert_ars pp algebra0 t ars2 ars1)
+ else insert_ars context algebra0 t ars2 ars1)
| (false, true) => (*unary completion*)
Symtab.empty
- |> add_arities_table pp algebra0 arities1
+ |> add_arities_table context algebra0 arities1
| (false, false) => (*binary completion*)
Symtab.empty
- |> add_arities_table pp algebra0 arities1
- |> add_arities_table pp algebra0 arities2);
+ |> add_arities_table context algebra0 arities1
+ |> add_arities_table context algebra0 arities2);
in make_algebra (classes', arities') end;
(* algebra projections *) (* FIXME potentially violates abstract type integrity *)
-fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
+fun subalgebra context P sargs (algebra as Algebra {classes, arities}) =
let
val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
fun restrict_arity t (c, Ss) =
@@ -313,7 +313,7 @@
else NONE;
val classes' = classes |> Graph.restrict P;
val arities' = arities |> Symtab.map (map_filter o restrict_arity);
- in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
+ in (restrict_sort, rebuild_arities context (make_algebra (classes', arities'))) end;
@@ -326,8 +326,8 @@
No_Arity of string * class |
No_Subsort of sort * sort;
-fun class_error pp =
- let val ctxt = Syntax.init_pretty pp in
+fun class_error context =
+ let val ctxt = Syntax.init_pretty context in
fn No_Classrel (c1, c2) => "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
| No_Arity (a, c) => "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
| No_Subsort (S1, S2) =>
--- a/src/Pure/term.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/term.ML Fri Sep 25 23:41:24 2015 +0200
@@ -107,6 +107,7 @@
val maxidx_of_typ: typ -> int
val maxidx_of_typs: typ list -> int
val maxidx_of_term: term -> int
+ val fold_subtypes: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
val exists_subtype: (typ -> bool) -> typ -> bool
val exists_type: (typ -> bool) -> term -> bool
val exists_subterm: (term -> bool) -> term -> bool
@@ -878,6 +879,12 @@
(* substructure *)
+fun fold_subtypes f =
+ let
+ fun iter ty =
+ (case ty of Type (_, Ts) => f ty #> fold iter Ts | _ => f ty);
+ in iter end;
+
fun exists_subtype P =
let
fun ex ty = P ty orelse
--- a/src/Pure/theory.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/theory.ML Fri Sep 25 23:41:24 2015 +0200
@@ -23,9 +23,11 @@
val begin_theory: string * Position.T -> theory list -> theory
val end_theory: theory -> theory
val add_axiom: Proof.context -> binding * term -> theory -> theory
- val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory
- val add_deps_global: string -> string * typ -> (string * typ) list -> theory -> theory
- val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory
+ val const_dep: theory -> string * typ -> Defs.entry
+ val type_dep: string * typ list -> Defs.entry
+ val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
+ val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
+ val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
val specify_const: (binding * typ) * mixfix -> theory -> term * theory
val check_overloading: Proof.context -> bool -> string * typ -> unit
end
@@ -62,7 +64,7 @@
fun make_thy (pos, id, axioms, defs, wrappers) =
Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
-structure Thy = Theory_Data_PP
+structure Thy = Theory_Data'
(
type T = thy;
val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
@@ -71,14 +73,13 @@
fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) =
make_thy (Position.none, 0, empty_axioms, defs, wrappers);
- fun merge pp (thy1, thy2) =
+ fun merge old_thys (thy1, thy2) =
let
- val ctxt = Syntax.init_pretty pp;
val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
val axioms' = empty_axioms;
- val defs' = Defs.merge ctxt (defs1, defs2);
+ val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
val ens' = Library.merge (eq_snd op =) (ens1, ens2);
in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
@@ -163,7 +164,7 @@
| _ => error "Bad bootstrapping of theory Pure")
else
let
- val thy = Context.begin_thy Context.pretty_global name imports;
+ val thy = Context.begin_thy name imports;
val wrappers = begin_wrappers thy;
in
thy
@@ -211,35 +212,48 @@
(* dependencies *)
-fun dependencies ctxt unchecked def description lhs rhs =
+fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T));
+fun type_dep (c, args) = ((Defs.Type, c), args);
+
+fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs =
let
val thy = Proof_Context.theory_of ctxt;
val consts = Sign.consts_of thy;
- fun prep const =
- let val Const (c, T) = Sign.no_vars ctxt (Const const)
- in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end;
- val lhs_vars = Term.add_tfreesT (#2 lhs) [];
- val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
- if member (op =) lhs_vars v then I else insert (op =) v | _ => I)) rhs [];
+ fun prep (item, args) =
+ (case fold Term.add_tvarsT args [] of
+ [] => (item, map Logic.varifyT_global args)
+ | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
+
+ val lhs_vars = fold Term.add_tfreesT (snd lhs) [];
+ val rhs_extras =
+ fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v =>
+ if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
val _ =
if null rhs_extras then ()
else error ("Specification depends on extra type variables: " ^
commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
"\nThe error(s) above occurred in " ^ quote description);
- in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
+ in Defs.define context unchecked def description (prep lhs) (map prep rhs) end;
-fun add_deps ctxt a raw_lhs raw_rhs thy =
+fun cert_entry thy ((Defs.Const, c), args) =
+ Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
+ |> dest_Const |> const_dep thy
+ | cert_entry thy ((Defs.Type, c), args) =
+ Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep;
+
+fun add_deps context a raw_lhs raw_rhs thy =
let
- val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs);
- val description = if a = "" then #1 lhs ^ " axiom" else a;
- in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end;
+ val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs);
+ val description = if a = "" then lhs_name ^ " axiom" else a;
+ in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
-fun add_deps_global a x y thy = add_deps (Syntax.init_pretty_global thy) a x y thy;
+fun add_deps_global a x y thy =
+ add_deps (Defs.global_context thy) a x y thy;
fun specify_const decl thy =
- let val (t as Const const, thy') = Sign.declare_const_global decl thy;
- in (t, add_deps_global "" const [] thy') end;
+ let val (t, thy') = Sign.declare_const_global decl thy;
+ in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end;
(* overloading *)
@@ -271,25 +285,31 @@
local
-fun check_def ctxt thy unchecked overloaded (b, tm) defs =
+fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
let
val name = Sign.full_name thy b;
val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
handle TERM (msg, _) => error msg;
val lhs_const = Term.dest_Const (Term.head_of lhs);
- val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
+
+ val rhs_consts =
+ fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs [];
+ val rhs_types =
+ (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs [];
+ val rhs_deps = rhs_consts @ rhs_types;
+
val _ = check_overloading ctxt overloaded lhs_const;
- in defs |> dependencies ctxt unchecked (SOME name) name lhs_const rhs_consts end
+ in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
[Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
in
-fun add_def ctxt unchecked overloaded raw_axm thy =
+fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy =
let val axm = cert_axm ctxt raw_axm in
thy
- |> map_defs (check_def ctxt thy unchecked overloaded axm)
+ |> map_defs (check_def context thy unchecked overloaded axm)
|> add_axiom ctxt axm
end;
--- a/src/Pure/type.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Pure/type.ML Fri Sep 25 23:41:24 2015 +0200
@@ -55,7 +55,7 @@
val cert_typ_mode: mode -> tsig -> typ -> typ
val cert_typ: tsig -> typ -> typ
val arity_number: tsig -> string -> int
- val arity_sorts: Context.pretty -> tsig -> string -> sort -> sort list
+ val arity_sorts: Context.generic -> tsig -> string -> sort -> sort list
(*special treatment of type vars*)
val sort_of_atyp: typ -> sort
@@ -96,9 +96,9 @@
val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig
val add_nonterminal: Context.generic -> binding -> tsig -> tsig
val hide_type: bool -> string -> tsig -> tsig
- val add_arity: Context.pretty -> arity -> tsig -> tsig
- val add_classrel: Context.pretty -> class * class -> tsig -> tsig
- val merge_tsig: Context.pretty -> tsig * tsig -> tsig
+ val add_arity: Context.generic -> arity -> tsig -> tsig
+ val add_classrel: Context.generic -> class * class -> tsig -> tsig
+ val merge_tsig: Context.generic -> tsig * tsig -> tsig
end;
structure Type: TYPE =
@@ -321,9 +321,9 @@
| _ => error (undecl_type a));
fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
- | arity_sorts pp (TSig {classes, ...}) a S =
+ | arity_sorts context (TSig {classes, ...}) a S =
Sorts.mg_domain (#2 classes) a S
- handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
+ handle Sorts.CLASS_ERROR err => error (Sorts.class_error context err);
@@ -609,7 +609,7 @@
handle TYPE (msg, _, _) => error msg;
val _ = Binding.check c;
val (c', space') = space |> Name_Space.declare context true c;
- val classes' = classes |> Sorts.add_class (Context.pretty_generic context) (c', cs');
+ val classes' = classes |> Sorts.add_class context (c', cs');
in ((space', classes'), default, types) end);
fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
@@ -618,7 +618,7 @@
(* arities *)
-fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
+fun add_arity context (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val _ =
(case lookup_type tsig t of
@@ -627,18 +627,18 @@
| NONE => error (undecl_type t));
val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
+ val classes' = classes |> Sorts.add_arities context ((t, map (fn c' => (c', Ss')) S'));
in ((space, classes'), default, types) end);
(* classrel *)
-fun add_classrel pp rel tsig =
+fun add_classrel context rel tsig =
tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val rel' = apply2 (cert_class tsig) rel
handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Sorts.add_classrel pp rel';
+ val classes' = classes |> Sorts.add_classrel context rel';
in ((space, classes'), default, types) end);
@@ -701,7 +701,7 @@
(* merge type signatures *)
-fun merge_tsig pp (tsig1, tsig2) =
+fun merge_tsig context (tsig1, tsig2) =
let
val (TSig {classes = (space1, classes1), default = default1, types = types1,
log_types = _}) = tsig1;
@@ -709,7 +709,7 @@
log_types = _}) = tsig2;
val space' = Name_Space.merge (space1, space2);
- val classes' = Sorts.merge_algebra pp (classes1, classes2);
+ val classes' = Sorts.merge_algebra context (classes1, classes2);
val default' = Sorts.inter_sort classes' (default1, default2);
val types' = Name_Space.merge_tables (types1, types2);
in build_tsig ((space', classes'), default', types') end;
--- a/src/Sequents/prover.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Sequents/prover.ML Fri Sep 25 23:41:24 2015 +0200
@@ -63,8 +63,8 @@
fun pretty_pack ctxt =
let val (safes, unsafes) = get_rules ctxt in
Pretty.chunks
- [Pretty.big_list "safe rules:" (map (Display.pretty_thm ctxt) safes),
- Pretty.big_list "unsafe rules:" (map (Display.pretty_thm ctxt) unsafes)]
+ [Pretty.big_list "safe rules:" (map (Thm.pretty_thm ctxt) safes),
+ Pretty.big_list "unsafe rules:" (map (Thm.pretty_thm ctxt) unsafes)]
end;
val _ =
@@ -82,7 +82,7 @@
(case context of
Context.Proof ctxt =>
if Context_Position.is_really_visible ctxt then
- warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
+ warning ("Ignoring duplicate theorems:\n" ^ Thm.string_of_thm ctxt th)
else ()
| _ => ());
in ths end
--- a/src/Sequents/simpdata.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Sequents/simpdata.ML Fri Sep 25 23:41:24 2015 +0200
@@ -38,7 +38,7 @@
| (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
| (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T})
- | _ => error ("addsimps: unable to use theorem\n" ^ Display.string_of_thm ctxt th));
+ | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th));
(*Replace premises x=y, X<->Y by X==Y*)
fun mk_meta_prems ctxt =
--- a/src/Tools/Code/code_preproc.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML Fri Sep 25 23:41:24 2015 +0200
@@ -517,7 +517,7 @@
|> fold (ensure_fun ctxt arities eqngr) cs
|> fold (ensure_rhs ctxt arities eqngr) cs_rhss;
val arities' = fold (add_arity ctxt vardeps) insts arities;
- val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
+ val algebra = Sorts.subalgebra (Context.Theory thy) (is_proper_class thy)
(AList.lookup (op =) arities') (Sign.classes_of thy);
val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr);
fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra)
--- a/src/Tools/Code/code_printer.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Tools/Code/code_printer.ML Fri Sep 25 23:41:24 2015 +0200
@@ -111,7 +111,7 @@
(** generic nonsense *)
fun eqn_error thy (SOME thm) s =
- error (s ^ ",\nin equation " ^ Display.string_of_thm_global thy thm)
+ error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm)
| eqn_error _ NONE s = error s;
val code_presentationN = "code_presentation";
--- a/src/Tools/Code/code_thingol.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri Sep 25 23:41:24 2015 +0200
@@ -396,7 +396,7 @@
else
let
val thm_msg =
- Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm;
+ Option.map (fn thm => "in code equation " ^ Thm.string_of_thm ctxt thm) some_thm;
val dep_msg = if null (tl deps) then NONE
else SOME ("with dependency "
^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps)));
@@ -412,7 +412,7 @@
fun not_wellsorted ctxt permissive some_thm deps ty sort e =
let
- val err_class = Sorts.class_error (Context.pretty ctxt) e;
+ val err_class = Sorts.class_error (Context.Proof ctxt) e;
val err_typ =
"Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
Syntax.string_of_sort ctxt sort;
--- a/src/Tools/coherent.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Tools/coherent.ML Fri Sep 25 23:41:24 2015 +0200
@@ -175,7 +175,7 @@
let
val _ =
cond_trace ctxt (fn () =>
- Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms)));
+ Pretty.string_of (Pretty.big_list "asms:" (map (Thm.pretty_thm ctxt) asms)));
val th' =
Drule.implies_elim_list
(Thm.instantiate
--- a/src/Tools/induct.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Tools/induct.ML Fri Sep 25 23:41:24 2015 +0200
@@ -207,7 +207,7 @@
fun pretty_rules ctxt kind rs =
let val thms = map snd (Item_Net.content rs)
- in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end;
+ in Pretty.big_list kind (map (Thm.pretty_thm_item ctxt) thms) end;
(* context data *)
--- a/src/Tools/nbe.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/Tools/nbe.ML Fri Sep 25 23:41:24 2015 +0200
@@ -50,17 +50,17 @@
let
val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
of SOME ofclass_eq => ofclass_eq
- | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
+ | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm);
val (T, class) = case try Logic.dest_of_class ofclass
of SOME T_class => T_class
- | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
+ | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm);
val tvar = case try Term.dest_TVar T
of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort)
then tvar
- else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
- | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
+ else error ("Bad sort: " ^ Thm.string_of_thm_global thy thm)
+ | _ => error ("Bad type: " ^ Thm.string_of_thm_global thy thm);
val _ = if Term.add_tvars eqn [] = [tvar] then ()
- else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm);
+ else error ("Inconsistent type: " ^ Thm.string_of_thm_global thy thm);
val lhs_rhs = case try Logic.dest_equals eqn
of SOME lhs_rhs => lhs_rhs
| _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
@@ -69,7 +69,7 @@
| _ => error ("Not an equation with two constants: "
^ Syntax.string_of_term_global thy eqn);
val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then ()
- else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
+ else error ("Inconsistent class: " ^ Thm.string_of_thm_global thy thm);
in Triv_Class_Data.map (AList.update (op =) (class, Thm.trim_context thm)) thy end;
local
--- a/src/ZF/Tools/inductive_package.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Sep 25 23:41:24 2015 +0200
@@ -319,7 +319,7 @@
if ! Ind_Syntax.trace then
writeln (cat_lines
(["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @
- ["raw_induct:", Display.string_of_thm ctxt1 raw_induct]))
+ ["raw_induct:", Thm.string_of_thm ctxt1 raw_induct]))
else ();
@@ -352,7 +352,7 @@
val dummy =
if ! Ind_Syntax.trace then
- writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct)
+ writeln ("quant_induct:\n" ^ Thm.string_of_thm ctxt1 quant_induct)
else ();
@@ -429,7 +429,7 @@
val dummy =
if ! Ind_Syntax.trace then
- writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma)
+ writeln ("lemma: " ^ Thm.string_of_thm ctxt1 lemma)
else ();
--- a/src/ZF/Tools/typechk.ML Fri Sep 25 16:54:31 2015 +0200
+++ b/src/ZF/Tools/typechk.ML Fri Sep 25 23:41:24 2015 +0200
@@ -26,7 +26,7 @@
fun add_rule ctxt th (tcs as TC {rules, net}) =
if member Thm.eq_thm_prop rules th then
- (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs)
+ (warning ("Ignoring duplicate type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs)
else
TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net};
@@ -34,7 +34,7 @@
if member Thm.eq_thm_prop rules th then
TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
rules = remove Thm.eq_thm_prop th rules}
- else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs);
+ else (warning ("No such type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs);
(* generic data *)
@@ -61,7 +61,7 @@
fun print_tcset ctxt =
let val TC {rules, ...} = tcset_of ctxt in
Pretty.writeln (Pretty.big_list "type-checking rules:"
- (map (Display.pretty_thm_item ctxt) rules))
+ (map (Thm.pretty_thm_item ctxt) rules))
end;