--- a/Admin/makedist Tue Jun 01 17:52:00 2010 +0200
+++ b/Admin/makedist Tue Jun 01 17:52:19 2010 +0200
@@ -148,6 +148,8 @@
cp doc/isabelle*.eps lib/logo
+rm Isabelle Isabelle.exe
+
if [ -z "$RELEASE" ]; then
{
--- a/NEWS Tue Jun 01 17:52:00 2010 +0200
+++ b/NEWS Tue Jun 01 17:52:19 2010 +0200
@@ -506,9 +506,12 @@
OuterLex ~> Token
OuterParse ~> Parse
OuterSyntax ~> Outer_Syntax
+ PrintMode ~> Print_Mode
SpecParse ~> Parse_Spec
+ ThyInfo ~> Thy_Info
+ ThyLoad ~> Thy_Load
+ ThyOutput ~> Thy_Output
TypeInfer ~> Type_Infer
- PrintMode ~> Print_Mode
Note that "open Legacy" simplifies porting of sources, but forgetting
to remove it again will complicate porting again in the future.
@@ -591,6 +594,11 @@
ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
+* The preliminary Isabelle/jEdit application demonstrates the emerging
+Isabelle/Scala layer for advanced prover interaction and integration.
+See src/Tools/jEdit or "isabelle jedit" provided by the properly built
+component.
+
New in Isabelle2009-1 (December 2009)
--- a/doc-src/Classes/Thy/document/Classes.tex Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Tue Jun 01 17:52:19 2010 +0200
@@ -792,8 +792,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Isabelle locales support a concept of local definitions
- in locales:%
+Isabelle locales are targets which support local definitions:%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/Integration.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy Tue Jun 01 17:52:19 2010 +0200
@@ -368,13 +368,13 @@
@{index_ML theory: "string -> theory"} \\
@{index_ML use_thy: "string -> unit"} \\
@{index_ML use_thys: "string list -> unit"} \\
- @{index_ML ThyInfo.touch_thy: "string -> unit"} \\
- @{index_ML ThyInfo.remove_thy: "string -> unit"} \\[1ex]
- @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
- @{index_ML ThyInfo.end_theory: "theory -> unit"} \\
- @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
+ @{index_ML Thy_Info.touch_thy: "string -> unit"} \\
+ @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
+ @{index_ML Thy_Info.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
+ @{index_ML Thy_Info.end_theory: "theory -> unit"} \\
+ @{index_ML Thy_Info.register_theory: "theory -> unit"} \\[1ex]
@{verbatim "datatype action = Update | Outdate | Remove"} \\
- @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
+ @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
\end{mldecls}
\begin{description}
@@ -395,24 +395,24 @@
intrinsic parallelism can be exploited by the system, to speedup
loading.
- \item @{ML ThyInfo.touch_thy}~@{text A} performs and @{text outdate} action
+ \item @{ML Thy_Info.touch_thy}~@{text A} performs and @{text outdate} action
on theory @{text A} and all descendants.
- \item @{ML ThyInfo.remove_thy}~@{text A} deletes theory @{text A} and all
+ \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
descendants from the theory database.
- \item @{ML ThyInfo.begin_theory} is the basic operation behind a
+ \item @{ML Thy_Info.begin_theory} is the basic operation behind a
@{text \<THEORY>} header declaration. This {\ML} function is
normally not invoked directly.
- \item @{ML ThyInfo.end_theory} concludes the loading of a theory
+ \item @{ML Thy_Info.end_theory} concludes the loading of a theory
proper and stores the result in the theory database.
- \item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
+ \item @{ML Thy_Info.register_theory}~@{text "text thy"} registers an
existing theory value with the theory loader database. There is no
management of associated sources.
- \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
+ \item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text
f} as a hook for theory database actions. The function will be
invoked with the action and theory name being involved; thus derived
actions may be performed in associated system components, e.g.\
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Tue Jun 01 17:52:19 2010 +0200
@@ -440,13 +440,13 @@
\indexdef{}{ML}{theory}\verb|theory: string -> theory| \\
\indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
\indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
- \indexdef{}{ML}{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
- \indexdef{}{ML}{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
- \indexdef{}{ML}{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
- \indexdef{}{ML}{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
- \indexdef{}{ML}{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
+ \indexdef{}{ML}{Thy\_Info.touch\_thy}\verb|Thy_Info.touch_thy: string -> unit| \\
+ \indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex]
+ \indexdef{}{ML}{Thy\_Info.begin\_theory}\verb|Thy_Info.begin_theory|\verb|: ... -> bool -> theory| \\
+ \indexdef{}{ML}{Thy\_Info.end\_theory}\verb|Thy_Info.end_theory: theory -> unit| \\
+ \indexdef{}{ML}{Thy\_Info.register\_theory}\verb|Thy_Info.register_theory: theory -> unit| \\[1ex]
\verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
- \indexdef{}{ML}{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
+ \indexdef{}{ML}{Thy\_Info.add\_hook}\verb|Thy_Info.add_hook: (Thy_Info.action -> string -> unit) -> unit| \\
\end{mldecls}
\begin{description}
@@ -466,24 +466,24 @@
intrinsic parallelism can be exploited by the system, to speedup
loading.
- \item \verb|ThyInfo.touch_thy|~\isa{A} performs and \isa{outdate} action
+ \item \verb|Thy_Info.touch_thy|~\isa{A} performs and \isa{outdate} action
on theory \isa{A} and all descendants.
- \item \verb|ThyInfo.remove_thy|~\isa{A} deletes theory \isa{A} and all
+ \item \verb|Thy_Info.remove_thy|~\isa{A} deletes theory \isa{A} and all
descendants from the theory database.
- \item \verb|ThyInfo.begin_theory| is the basic operation behind a
+ \item \verb|Thy_Info.begin_theory| is the basic operation behind a
\isa{{\isasymTHEORY}} header declaration. This {\ML} function is
normally not invoked directly.
- \item \verb|ThyInfo.end_theory| concludes the loading of a theory
+ \item \verb|Thy_Info.end_theory| concludes the loading of a theory
proper and stores the result in the theory database.
- \item \verb|ThyInfo.register_theory|~\isa{text\ thy} registers an
+ \item \verb|Thy_Info.register_theory|~\isa{text\ thy} registers an
existing theory value with the theory loader database. There is no
management of associated sources.
- \item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
+ \item \verb|Thy_Info.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
invoked with the action and theory name being involved; thus derived
actions may be performed in associated system components, e.g.\
maintaining the state of an editor for the theory sources.
--- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML Tue Jun 01 17:52:19 2010 +0200
@@ -1,4 +1,4 @@
-Unsynchronized.set ThyOutput.source;
+Unsynchronized.set Thy_Output.source;
use "../../antiquote_setup.ML";
use_thy "HOLCF_Specific";
--- a/doc-src/IsarRef/Thy/ROOT-ZF.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML Tue Jun 01 17:52:19 2010 +0200
@@ -1,4 +1,4 @@
-Unsynchronized.set ThyOutput.source;
+Unsynchronized.set Thy_Output.source;
use "../../antiquote_setup.ML";
use_thy "ZF_Specific";
--- a/doc-src/IsarRef/Thy/ROOT.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML Tue Jun 01 17:52:19 2010 +0200
@@ -1,5 +1,5 @@
Unsynchronized.set quick_and_dirty;
-Unsynchronized.set ThyOutput.source;
+Unsynchronized.set Thy_Output.source;
use "../../antiquote_setup.ML";
use_thys [
--- a/doc-src/Main/Docs/Main_Doc.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy Tue Jun 01 17:52:19 2010 +0200
@@ -9,10 +9,10 @@
else error "term_type_only: type mismatch";
Syntax.pretty_typ ctxt T)
-val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
+val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
(fn {source, context, ...} => fn arg =>
- ThyOutput.output
- (ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg]));
+ Thy_Output.output
+ (Thy_Output.maybe_pretty_source (pretty_term_type_only context) source [arg]));
*}
(*>*)
text{*
--- a/doc-src/System/Thy/ROOT.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/System/Thy/ROOT.ML Tue Jun 01 17:52:19 2010 +0200
@@ -1,4 +1,4 @@
-Unsynchronized.set ThyOutput.source;
+Unsynchronized.set Thy_Output.source;
use "../../antiquote_setup.ML";
use_thys ["Basics", "Interfaces", "Presentation", "Misc"];
--- a/doc-src/TutorialI/Rules/Primes.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy Tue Jun 01 17:52:19 2010 +0200
@@ -10,7 +10,7 @@
ML "Pretty.margin_default := 64"
-ML "ThyOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*)
+ML "Thy_Output.indent := 5" (*that is, Doc/TutorialI/settings.ML*)
text {*Now in Basic.thy!
--- a/doc-src/TutorialI/Types/Numbers.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy Tue Jun 01 17:52:19 2010 +0200
@@ -3,7 +3,7 @@
begin
ML "Pretty.margin_default := 64"
-ML "ThyOutput.indent := 0" (*we don't want 5 for listing theorems*)
+ML "Thy_Output.indent := 0" (*we don't want 5 for listing theorems*)
text{*
--- a/doc-src/TutorialI/Types/document/Numbers.tex Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Jun 01 17:52:19 2010 +0200
@@ -28,7 +28,7 @@
\isacommand{ML}\isamarkupfalse%
\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
\isacommand{ML}\isamarkupfalse%
-\ {\isachardoublequoteopen}ThyOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}Thy{\isacharunderscore}Output{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
\endisatagML
{\isafoldML}%
%
--- a/doc-src/TutorialI/Types/document/Pairs.tex Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Tue Jun 01 17:52:19 2010 +0200
@@ -60,7 +60,7 @@
Internally, \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} becomes \isa{split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}}, where
\cdx{split} is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as
\begin{center}
-\isa{split\ {\isasymequiv}\ {\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}}
+\isa{split\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}}
\hfill(\isa{split{\isacharunderscore}def})
\end{center}
Pattern matching in
--- a/doc-src/TutorialI/settings.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/TutorialI/settings.ML Tue Jun 01 17:52:19 2010 +0200
@@ -1,3 +1,3 @@
(* $Id$ *)
-ThyOutput.indent := 5;
+Thy_Output.indent := 5;
--- a/doc-src/antiquote_setup.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/antiquote_setup.ML Tue Jun 01 17:52:19 2010 +0200
@@ -35,7 +35,7 @@
val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
-val _ = ThyOutput.antiquotation "verbatim" (Scan.lift Args.name)
+val _ = Thy_Output.antiquotation "verbatim" (Scan.lift Args.name)
(K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
@@ -56,7 +56,7 @@
fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt;
-fun index_ml name kind ml = ThyOutput.antiquotation name
+fun index_ml name kind ml = Thy_Output.antiquotation name
(Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
(fn {context = ctxt, ...} => fn (txt1, txt2) =>
let
@@ -71,8 +71,8 @@
in
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
(txt'
- |> (if ! ThyOutput.quotes then quote else I)
- |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+ |> (if ! Thy_Output.quotes then quote else I)
+ |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
end);
@@ -89,30 +89,30 @@
(* named theorems *)
-val _ = ThyOutput.antiquotation "named_thms"
+val _ = Thy_Output.antiquotation "named_thms"
(Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
(fn {context = ctxt, ...} =>
- map (apfst (ThyOutput.pretty_thm ctxt))
- #> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
- #> (if ! ThyOutput.display
+ map (apfst (Thy_Output.pretty_thm ctxt))
+ #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I)
+ #> (if ! Thy_Output.display
then
map (fn (p, name) =>
- Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
- "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
+ Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^
+ "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
#> space_implode "\\par\\smallskip%\n"
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
else
map (fn (p, name) =>
Output.output (Pretty.str_of p) ^
- "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
+ "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
#> space_implode "\\par\\smallskip%\n"
#> enclose "\\isa{" "}"));
(* theory file *)
-val _ = ThyOutput.antiquotation "thy_file" (Scan.lift Args.name)
- (fn _ => fn name => (ThyLoad.check_thy Path.current name; ThyOutput.output [Pretty.str name]));
+val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
+ (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name]));
(* Isabelle/Isar entities (with index) *)
@@ -131,7 +131,7 @@
val arg = enclose "{" "}" o clean_string;
fun entity check markup kind index =
- ThyOutput.antiquotation
+ Thy_Output.antiquotation
(translate (fn " " => "_" | c => c) kind ^
(case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))
(Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
@@ -152,8 +152,8 @@
idx ^
(Output.output name
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
- |> (if ! ThyOutput.quotes then quote else I)
- |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ |> (if ! Thy_Output.quotes then quote else I)
+ |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
else hyper o enclose "\\mbox{\\isa{" "}}"))
else error ("Bad " ^ kind ^ " " ^ quote name)
end);
@@ -174,14 +174,14 @@
val _ = entity_antiqs no_check "" "fact";
val _ = entity_antiqs no_check "" "variable";
val _ = entity_antiqs no_check "" "case";
-val _ = entity_antiqs (K ThyOutput.defined_command) "" "antiquotation";
-val _ = entity_antiqs (K ThyOutput.defined_option) "" "antiquotation option";
+val _ = entity_antiqs (K Thy_Output.defined_command) "" "antiquotation";
+val _ = entity_antiqs (K Thy_Output.defined_option) "" "antiquotation option";
val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
val _ = entity_antiqs no_check "" "inference";
val _ = entity_antiqs no_check "isatt" "executable";
val _ = entity_antiqs (K check_tool) "isatt" "tool";
val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
-val _ = entity_antiqs (K ThyInfo.known_thy) "" "theory";
+val _ = entity_antiqs (K Thy_Info.known_thy) "" "theory";
end;
--- a/doc-src/more_antiquote.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/more_antiquote.ML Tue Jun 01 17:52:19 2010 +0200
@@ -64,8 +64,8 @@
in
-val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
-val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
+val _ = Thy_Output.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
+val _ = Thy_Output.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
end;
@@ -95,11 +95,11 @@
|> snd
|> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
|> map (holize o no_vars ctxt o AxClass.overload thy);
- in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
+ in Thy_Output.output (Thy_Output.maybe_pretty_source (pretty_thm ctxt) src thms) end;
in
-val _ = ThyOutput.antiquotation "code_thms" Args.term
+val _ = Thy_Output.antiquotation "code_thms" Args.term
(fn {source, context, ...} => pretty_code_thm source context);
end;
@@ -123,7 +123,7 @@
in
-val _ = ThyOutput.antiquotation "code_stmts"
+val _ = Thy_Output.antiquotation "code_stmts"
(parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
(fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
let val thy = ProofContext.theory_of ctxt in
--- a/doc-src/rail.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/doc-src/rail.ML Tue Jun 01 17:52:19 2010 +0200
@@ -67,14 +67,14 @@
("fact", ("", no_check, true)),
("variable", ("", no_check, true)),
("case", ("", no_check, true)),
- ("antiquotation", ("", K ThyOutput.defined_command, true)),
- ("antiquotation option", ("", K ThyOutput.defined_option, true)), (* kann mein scanner nicht erkennen *)
+ ("antiquotation", ("", K Thy_Output.defined_command, true)),
+ ("antiquotation option", ("", K Thy_Output.defined_option, true)), (* kann mein scanner nicht erkennen *)
("setting", ("isatt", (fn _ => fn name => is_some (OS.Process.getEnv name)), true)),
("inference", ("", no_check, true)),
("executable", ("isatt", no_check, true)),
("tool", ("isatt", K check_tool, true)),
("file", ("isatt", K (File.exists o Path.explode), true)),
- ("theory", ("", K ThyInfo.known_thy, true))
+ ("theory", ("", K Thy_Info.known_thy, true))
];
in
@@ -97,8 +97,8 @@
(idx ^
(Output.output name
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
- |> (if ! ThyOutput.quotes then quote else I)
- |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ |> (if ! Thy_Output.quotes then quote else I)
+ |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
else hyper o enclose "\\mbox{\\isa{" "}}")), style)
else ("Bad " ^ kind ^ " " ^ name, false)
end;
@@ -473,7 +473,7 @@
|> parse
|> print;
-val _ = ThyOutput.antiquotation "rail" (Scan.lift (Parse.position Args.name))
+val _ = Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
(fn {context = ctxt,...} => fn txt => process txt ctxt);
end;
--- a/src/HOL/Extraction.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Extraction.thy Tue Jun 01 17:52:19 2010 +0200
@@ -18,7 +18,8 @@
Proofterm.rewrite_proof_notypes
([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
Proofterm.rewrite_proof thy
- (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
+ (RewriteHOLProof.rews,
+ ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
ProofRewriteRules.elim_vars (curry Const @{const_name default}))
*}
@@ -199,223 +200,212 @@
theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow>
(\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp
-setup {*
- Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"})
-*}
-
realizers
impI (P, Q): "\<lambda>pq. pq"
- "\<Lambda> P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
+ "\<Lambda> (c: _) (d: _) P Q pq (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
impI (P): "Null"
- "\<Lambda> P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
+ "\<Lambda> (c: _) P Q (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
- impI (Q): "\<lambda>q. q" "\<Lambda> P Q q. impI \<cdot> _ \<cdot> _"
+ impI (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. impI \<cdot> _ \<cdot> _"
impI: "Null" "impI"
mp (P, Q): "\<lambda>pq. pq"
- "\<Lambda> P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
+ "\<Lambda> (c: _) (d: _) P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
mp (P): "Null"
- "\<Lambda> P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
+ "\<Lambda> (c: _) P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
- mp (Q): "\<lambda>q. q" "\<Lambda> P Q q. mp \<cdot> _ \<cdot> _"
+ mp (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. mp \<cdot> _ \<cdot> _"
mp: "Null" "mp"
- allI (P): "\<lambda>p. p" "\<Lambda> P p. allI \<cdot> _"
+ allI (P): "\<lambda>p. p" "\<Lambda> (c: _) P (d: _) p. allI \<cdot> _ \<bullet> d"
allI: "Null" "allI"
- spec (P): "\<lambda>x p. p x" "\<Lambda> P x p. spec \<cdot> _ \<cdot> x"
+ spec (P): "\<lambda>x p. p x" "\<Lambda> (c: _) P x (d: _) p. spec \<cdot> _ \<cdot> x \<bullet> d"
spec: "Null" "spec"
- exI (P): "\<lambda>x p. (x, p)" "\<Lambda> P x p. exI_realizer \<cdot> P \<cdot> p \<cdot> x"
+ exI (P): "\<lambda>x p. (x, p)" "\<Lambda> (c: _) P x (d: _) p. exI_realizer \<cdot> P \<cdot> p \<cdot> x \<bullet> c \<bullet> d"
- exI: "\<lambda>x. x" "\<Lambda> P x (h: _). h"
+ exI: "\<lambda>x. x" "\<Lambda> P x (c: _) (h: _). h"
exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y"
- "\<Lambda> P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h"
+ "\<Lambda> (c: _) (d: _) P Q (e: _) p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> c \<bullet> e \<bullet> d \<bullet> h"
exE (P): "Null"
- "\<Lambda> P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q (d: _) p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d"
exE (Q): "\<lambda>x pq. pq x"
- "\<Lambda> P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"
+ "\<Lambda> (c: _) P Q (d: _) x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"
exE: "Null"
- "\<Lambda> P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1"
+ "\<Lambda> P Q (c: _) x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1"
conjI (P, Q): "Pair"
- "\<Lambda> P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> h"
+ "\<Lambda> (c: _) (d: _) P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> c \<bullet> d \<bullet> h"
conjI (P): "\<lambda>p. p"
- "\<Lambda> P Q p. conjI \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q p. conjI \<cdot> _ \<cdot> _"
conjI (Q): "\<lambda>q. q"
- "\<Lambda> P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h"
+ "\<Lambda> (c: _) P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h"
conjI: "Null" "conjI"
conjunct1 (P, Q): "fst"
- "\<Lambda> P Q pq. conjunct1 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) (d: _) P Q pq. conjunct1 \<cdot> _ \<cdot> _"
conjunct1 (P): "\<lambda>p. p"
- "\<Lambda> P Q p. conjunct1 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q p. conjunct1 \<cdot> _ \<cdot> _"
conjunct1 (Q): "Null"
- "\<Lambda> P Q q. conjunct1 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q q. conjunct1 \<cdot> _ \<cdot> _"
conjunct1: "Null" "conjunct1"
conjunct2 (P, Q): "snd"
- "\<Lambda> P Q pq. conjunct2 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) (d: _) P Q pq. conjunct2 \<cdot> _ \<cdot> _"
conjunct2 (P): "Null"
- "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _"
conjunct2 (Q): "\<lambda>p. p"
- "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _"
conjunct2: "Null" "conjunct2"
disjI1 (P, Q): "Inl"
- "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p)"
+ "\<Lambda> (c: _) (d: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
disjI1 (P): "Some"
- "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p)"
+ "\<Lambda> (c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)"
disjI1 (Q): "None"
- "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
+ "\<Lambda> (c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
disjI1: "Left"
- "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)"
+ "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
disjI2 (P, Q): "Inr"
- "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)"
+ "\<Lambda> (d: _) (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
disjI2 (P): "None"
- "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
+ "\<Lambda> (c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
disjI2 (Q): "Some"
- "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)"
+ "\<Lambda> (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)"
disjI2: "Right"
- "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)"
+ "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
disjE (P, Q, R): "\<lambda>pq pr qr.
(case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)"
- "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
- disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
+ "\<Lambda> (c: _) (d: _) (e: _) P Q R pq (h1: _) pr (h2: _) qr.
+ disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> e \<bullet> h1 \<bullet> h2"
disjE (Q, R): "\<lambda>pq pr qr.
(case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)"
- "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
- disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
+ "\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr.
+ disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h2"
disjE (P, R): "\<lambda>pq pr qr.
(case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)"
- "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr (h3: _).
- disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2"
+ "\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr (h3: _).
+ disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h3 \<bullet> h2"
disjE (R): "\<lambda>pq pr qr.
(case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)"
- "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
- disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
+ "\<Lambda> (c: _) P Q R pq (h1: _) pr (h2: _) qr.
+ disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> h1 \<bullet> h2"
disjE (P, Q): "Null"
- "\<Lambda> P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) (d: _) P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d \<bullet> arity_type_bool"
disjE (Q): "Null"
- "\<Lambda> P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool"
disjE (P): "Null"
- "\<Lambda> P Q R pq (h1: _) (h2: _) (h3: _).
- disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2"
+ "\<Lambda> (c: _) P Q R pq (h1: _) (h2: _) (h3: _).
+ disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool \<bullet> h1 \<bullet> h3 \<bullet> h2"
disjE: "Null"
- "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
+ "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> arity_type_bool"
FalseE (P): "default"
- "\<Lambda> P. FalseE \<cdot> _"
+ "\<Lambda> (c: _) P. FalseE \<cdot> _"
FalseE: "Null" "FalseE"
notI (P): "Null"
- "\<Lambda> P (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))"
+ "\<Lambda> (c: _) P (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))"
notI: "Null" "notI"
notE (P, R): "\<lambda>p. default"
- "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
+ "\<Lambda> (c: _) (d: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
notE (P): "Null"
- "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
+ "\<Lambda> (c: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
notE (R): "default"
- "\<Lambda> P R. notE \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P R. notE \<cdot> _ \<cdot> _"
notE: "Null" "notE"
subst (P): "\<lambda>s t ps. ps"
- "\<Lambda> s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> h"
+ "\<Lambda> (c: _) s t P (d: _) (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> d \<bullet> h"
subst: "Null" "subst"
iffD1 (P, Q): "fst"
- "\<Lambda> Q P pq (h: _) p.
- mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
+ "\<Lambda> (d: _) (c: _) Q P pq (h: _) p.
+ mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> d \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
iffD1 (P): "\<lambda>p. p"
- "\<Lambda> Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)"
+ "\<Lambda> (c: _) Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)"
iffD1 (Q): "Null"
- "\<Lambda> Q P q1 (h: _) q2.
- mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
+ "\<Lambda> (c: _) Q P q1 (h: _) q2.
+ mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
iffD1: "Null" "iffD1"
iffD2 (P, Q): "snd"
- "\<Lambda> P Q pq (h: _) q.
- mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
+ "\<Lambda> (c: _) (d: _) P Q pq (h: _) q.
+ mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> d \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
iffD2 (P): "\<lambda>p. p"
- "\<Lambda> P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)"
+ "\<Lambda> (c: _) P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)"
iffD2 (Q): "Null"
- "\<Lambda> P Q q1 (h: _) q2.
- mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
+ "\<Lambda> (c: _) P Q q1 (h: _) q2.
+ mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
iffD2: "Null" "iffD2"
iffI (P, Q): "Pair"
- "\<Lambda> P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>
+ "\<Lambda> (c: _) (d: _) P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>
(\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot>
(\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet>
- (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
- (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
+ (arity_type_fun \<bullet> c \<bullet> d) \<bullet>
+ (arity_type_fun \<bullet> d \<bullet> c) \<bullet>
+ (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
+ (allI \<cdot> _ \<bullet> d \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
iffI (P): "\<lambda>p. p"
- "\<Lambda> P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
- (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
+ "\<Lambda> (c: _) P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
+ (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
(impI \<cdot> _ \<cdot> _ \<bullet> h2)"
iffI (Q): "\<lambda>q. q"
- "\<Lambda> P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
+ "\<Lambda> (c: _) P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
(impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet>
- (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
+ (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
iffI: "Null" "iffI"
-(*
- classical: "Null"
- "\<Lambda> P. classical \<cdot> _"
-*)
-
-setup {*
- Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"})
-*}
-
end
--- a/src/HOL/Lambda/WeakNorm.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Tue Jun 01 17:52:19 2010 +0200
@@ -264,6 +264,7 @@
lemmas [extraction_expand] = conj_assoc listall_cons_eq
extract type_NF
+
lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
apply (rule iffI)
apply (erule rtranclpR.induct)
--- a/src/HOL/Library/Char_nat.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Library/Char_nat.thy Tue Jun 01 17:52:19 2010 +0200
@@ -75,7 +75,7 @@
unfolding nibble_of_nat_def by auto
lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
- [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
+ [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc One_nat_def]
lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
@@ -193,12 +193,12 @@
text {* Code generator setup *}
code_modulename SML
- Char_nat List
+ Char_nat String
code_modulename OCaml
- Char_nat List
+ Char_nat String
code_modulename Haskell
- Char_nat List
+ Char_nat String
end
\ No newline at end of file
--- a/src/HOL/Library/Code_Char.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy Tue Jun 01 17:52:19 2010 +0200
@@ -12,9 +12,10 @@
(SML "char")
(OCaml "char")
(Haskell "Char")
+ (Scala "Char")
setup {*
- fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"]
+ fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"]
#> String_Code.add_literal_list_string "Haskell"
*}
@@ -27,10 +28,14 @@
code_reserved OCaml
char
+code_reserved Scala
+ char
+
code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
(SML "!((_ : char) = _)")
(OCaml "!((_ : char) = _)")
(Haskell infixl 4 "==")
+ (Scala infixl 5 "==")
code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
(Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
@@ -53,10 +58,12 @@
(SML "String.implode")
(OCaml "failwith/ \"implode\"")
(Haskell "_")
+ (Scala "List.toString((_))")
code_const explode
(SML "String.explode")
(OCaml "failwith/ \"explode\"")
(Haskell "_")
+ (Scala "List.fromString((_))")
end
--- a/src/HOL/Library/Code_Char_chr.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy Tue Jun 01 17:52:19 2010 +0200
@@ -22,23 +22,10 @@
"char_of_nat = char_of_int o int"
unfolding char_of_int_def by (simp add: expand_fun_eq)
-lemmas [code del] = char.recs char.cases char.size
-
-lemma [code, code_unfold]:
- "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
- by (cases c) (auto simp add: nibble_pair_of_nat_char)
-
-lemma [code, code_unfold]:
- "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
- by (cases c) (auto simp add: nibble_pair_of_nat_char)
-
-lemma [code]:
- "size (c\<Colon>char) = 0"
- by (cases c) auto
-
code_const int_of_char and char_of_int
(SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
(OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
- (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
+ (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . fromInteger)")
+ (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Jun 01 17:52:19 2010 +0200
@@ -317,7 +317,7 @@
else error("Int value too big:" + this.value.toString)
def +(that: Nat): Nat = new Nat(this.value + that.value)
- def -(that: Nat): Nat = Nat(this.value + that.value)
+ def -(that: Nat): Nat = Nat(this.value - that.value)
def *(that: Nat): Nat = new Nat(this.value * that.value)
def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 01 17:52:19 2010 +0200
@@ -219,7 +219,7 @@
then NONE
else
let
- val _ = List.app (SimpleThread.interrupt o #1) cancelling;
+ val _ = List.app (Simple_Thread.interrupt o #1) cancelling;
val cancelling' = filter (Thread.isActive o #1) cancelling;
val state' = make_state manager timeout_heap' active cancelling' messages store;
in SOME (map #2 timeout_threads, state') end
--- a/src/HOL/Tools/Datatype/datatype_data.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Tue Jun 01 17:52:19 2010 +0200
@@ -236,7 +236,7 @@
(** document antiquotation **)
-val _ = ThyOutput.antiquotation "datatype" (Args.type_name true)
+val _ = Thy_Output.antiquotation "datatype" (Args.type_name true)
(fn {source = src, context = ctxt, ...} => fn dtco =>
let
val thy = ProofContext.theory_of ctxt;
@@ -257,7 +257,7 @@
Pretty.str " =" :: Pretty.brk 1 ::
flat (separate [Pretty.brk 1, Pretty.str "| "]
(map (single o pretty_constr) cos)));
- in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
+ in Thy_Output.output (Thy_Output.maybe_pretty_source (K pretty_datatype) src [()]) end);
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 01 17:52:19 2010 +0200
@@ -22,10 +22,6 @@
in map (fn ks => i::ks) is @ is end
else [[]];
-fun forall_intr_prf (t, prf) =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
-
fun prf_of thm =
Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
@@ -130,12 +126,12 @@
val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
- val ivs1 = map Var (filter_out (fn (_, T) => (* FIXME set (!??) *)
- member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs);
+ val ivs1 = map Var (filter_out (fn (_, T) =>
+ @{type_name bool} = tname_of (body_type T)) ivs);
val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
val prf =
- List.foldr forall_intr_prf
+ Extraction.abs_corr_shyps thy' induct vs ivs2
(fold_rev (fn (f, p) => fn prf =>
(case head_of (strip_abs_body f) of
Free (s, T) =>
@@ -145,7 +141,7 @@
end
| _ => AbsP ("H", SOME p, prf)))
(rec_fns ~~ prems_of thm)
- (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2;
+ (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
val r' =
if null is then r
@@ -198,18 +194,21 @@
||> Sign.restore_naming thy;
val P = Var (("P", 0), rT' --> HOLogic.boolT);
- val prf = forall_intr_prf (y, forall_intr_prf (P,
- fold_rev (fn (p, r) => fn prf =>
- forall_intr_prf (Logic.varify_global r, AbsP ("H", SOME (Logic.varify_global p), prf)))
+ val prf = Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
+ (fold_rev (fn (p, r) => fn prf =>
+ Proofterm.forall_intr_proof' (Logic.varify_global r)
+ (AbsP ("H", SOME (Logic.varify_global p), prf)))
(prems ~~ rs)
- (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
+ (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
+ val prf' = Extraction.abs_corr_shyps thy' exhaust []
+ (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
val r' = Logic.varify_global (Abs ("y", T,
list_abs (map dest_Free rs, list_comb (r,
map Bound ((length rs - 1 downto 0) @ [length rs])))));
in Extraction.add_realizers_i
[(exh_name, (["P"], r', prf)),
- (exh_name, ([], Extraction.nullt, prf_of exhaust))] thy'
+ (exh_name, ([], Extraction.nullt, prf'))] thy'
end;
fun add_dt_realizers config names thy =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Jun 01 17:52:19 2010 +0200
@@ -183,7 +183,7 @@
val ctxt = Proof.context_of state
(* FIXME: reintroduce code before new release:
- val nitpick_thy = ThyInfo.get_theory "Nitpick"
+ val nitpick_thy = Thy_Info.get_theory "Nitpick"
val _ = Theory.subthy (nitpick_thy, thy) orelse
error "You must import the theory \"Nitpick\" to use Nitpick"
*)
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 01 17:52:19 2010 +0200
@@ -21,18 +21,12 @@
[name] => name
| _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
-val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
-
fun prf_of thm =
let
val thy = Thm.theory_of_thm thm;
val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
-fun forall_intr_prf t prf =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
-
fun subsets [] = [[]]
| subsets (x::xs) =
let val ys = subsets xs
@@ -55,15 +49,19 @@
(subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
| strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
-fun relevant_vars prop = List.foldr (fn
- (Var ((a, i), T), vs) => (case strip_type T of
+fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
+ (case strip_type T of
(_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
- | _ => vs)
- | (_, vs) => vs) [] (OldTerm.term_vars prop);
+ | _ => vs)) (Term.add_vars prop []) [];
+
+val attach_typeS = map_types (map_atyps
+ (fn TFree (s, []) => TFree (s, HOLogic.typeS)
+ | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
+ | T => T));
fun dt_of_intrs thy vs nparms intrs =
let
- val iTs = OldTerm.term_tvars (prop_of (hd intrs));
+ val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
(Logic.strip_imp_concl (prop_of (hd intrs))));
val params = map dest_Var (take nparms ts);
@@ -84,7 +82,7 @@
fun gen_rvar vs (t as Var ((a, 0), T)) =
if body_type T <> HOLogic.boolT then t else
let
- val U = TVar (("'" ^ a, 0), HOLogic.typeS)
+ val U = TVar (("'" ^ a, 0), [])
val Ts = binder_types T;
val i = length Ts;
val xs = map (pair "x") Ts;
@@ -98,8 +96,9 @@
fun mk_realizes_eqn n vs nparms intrs =
let
- val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
- val iTs = OldTerm.term_tvars concl;
+ val intr = map_types Type.strip_sorts (prop_of (hd intrs));
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr);
+ val iTs = rev (Term.add_tvars intr []);
val Tvs = map TVar iTs;
val (h as Const (s, T), us) = strip_comb concl;
val params = List.take (us, nparms);
@@ -110,7 +109,7 @@
(Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
val rT = if n then Extraction.nullT
else Type (space_implode "_" (s ^ "T" :: vs),
- map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
+ map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs);
val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
val S = list_comb (h, params @ xs);
val rvs = relevant_vars S;
@@ -121,7 +120,7 @@
let val T = (the o AList.lookup (op =) rvs) v
in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
Extraction.mk_typ (if n then Extraction.nullT
- else TVar (("'" ^ v, 0), HOLogic.typeS)))
+ else TVar (("'" ^ v, 0), [])))
end;
val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
@@ -261,12 +260,12 @@
val rlzvs = rev (Term.add_vars (prop_of rrule) []);
val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
- val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
- val rlz'' = fold_rev Logic.all vs2 rlz
+ val rlz' = fold_rev Logic.all rs (prop_of rrule)
in (name, (vs,
if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
- ProofRewriteRules.un_hhf_proof rlz' rlz''
- (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
+ Extraction.abs_corr_shyps thy rule vs vs2
+ (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
+ (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
end;
fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
@@ -275,7 +274,7 @@
let
val qualifier = Long_Name.qualifier (name_of_thm induct);
val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
- val iTs = OldTerm.term_tvars (prop_of (hd intrs));
+ val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
val ar = length vs + length iTs;
val params = Inductive.params_of raw_induct;
val arities = Inductive.arities_of raw_induct;
@@ -297,8 +296,6 @@
val thy1' = thy1 |>
Theory.copy |>
Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
- fold (fn s => AxClass.axiomatize_arity
- (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
Extraction.add_typeof_eqns_i ty_eqs;
val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
@@ -328,10 +325,10 @@
end
else (replicate (length rs) Extraction.nullt, (recs, dummies)))
rss (rec_thms, dummies);
- val rintrs = map (fn (intr, c) => Envir.eta_contract
+ val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract
(Extraction.realizes_of thy2 vs
(if c = Extraction.nullt then c else list_comb (c, map Var (rev
- (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))
+ (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr))))
(maps snd rss ~~ flat constrss);
val (rlzpreds, rlzpreds') =
rintrs |> map (fn rintr =>
@@ -390,7 +387,9 @@
val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
(fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
- val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
+ val thm = Goal.prove_global thy []
+ (map attach_typeS prems) (attach_typeS concl)
+ (fn {prems, ...} => EVERY
[rtac (#raw_induct ind_info) 1,
rewrite_goals_tac rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
@@ -408,10 +407,10 @@
in
Extraction.add_realizers_i
(map (fn (((ind, corr), rlz), r) =>
- mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
+ mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
realizers @ (case realizers of
[(((ind, corr), rlz), r)] =>
- [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
+ [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
ind, corr, rlz, r)]
| _ => [])) thy''
end;
@@ -445,7 +444,7 @@
map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
[Bound (length prems)]));
val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
- val rlz' = strip_all (Logic.unvarify_global rlz);
+ val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
val rews = map mk_meta_eq case_thms;
val thm = Goal.prove_global thy []
(Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
@@ -488,7 +487,7 @@
val vss = sort (int_ord o pairself length)
(subsets (map fst (relevant_vars (concl_of (hd intrs)))))
in
- fold (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
+ fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
end
fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
--- a/src/HOL/Tools/list_code.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Tools/list_code.ML Tue Jun 01 17:52:19 2010 +0200
@@ -31,11 +31,11 @@
end;
fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
- Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
+ Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
Code_Printer.str target_cons,
pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
- ];
+ );
fun add_literal_list target =
let
--- a/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 01 17:52:19 2010 +0200
@@ -7,7 +7,7 @@
signature REWRITE_HOL_PROOF =
sig
val rews: (Proofterm.proof * Proofterm.proof) list
- val elim_cong: typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
+ val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
end;
structure RewriteHOLProof : REWRITE_HOL_PROOF =
@@ -16,7 +16,7 @@
open Proofterm;
val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
- Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} propT)
+ Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
(** eliminate meta-equality rules **)
@@ -24,237 +24,258 @@
\ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \
\ (axm.reflexive % TYPE('T3) % x4) %% prf1)) == \
\ (iffD1 % A % B %% \
- \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
+ \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
"(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %% \
\ (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %% \
\ (axm.reflexive % TYPE('T4) % x6) %% prf1))) == \
\ (iffD2 % A % B %% \
- \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
+ \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
- "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% \
+ "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %% \
\ (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) == \
\ (cong % TYPE('T) % TYPE('U) % f % g % x % y %% \
- \ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
-
- "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% \
- \ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \
- \ (HOL.trans % TYPE('T) % x % y % z %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
+ \ (OfClass type_class % TYPE('T)) %% prfU %% \
+ \ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))",
- "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) == \
- \ (HOL.refl % TYPE('T) % x)",
+ "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% \
+ \ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \
+ \ (HOL.trans % TYPE('T) % x % y % z %% prfT %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))",
- "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
+ "(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) == \
+ \ (HOL.refl % TYPE('T) % x %% prfT)",
+
+ "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% \
\ (axm.symmetric % TYPE('T) % x % y %% prf)) == \
- \ (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
+ \ (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))",
- "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% \
+ "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %% \
\ (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) == \
\ (ext % TYPE('T) % TYPE('U) % f % g %% \
- \ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
+ \ (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %% \
+ \ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% \
+ \ (OfClass type_class % TYPE('U)) %% (prf % x)))",
- "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
- \ (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
+ "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% \
+ \ (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf",
- "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
+ "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %% \
\ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \
\ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) == \
\ (iffD1 % A = C % B = D %% \
- \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \
+ \ (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %% \
+ \ prfT %% arity_type_bool %% \
\ (cong % TYPE('T) % TYPE('T=>bool) % \
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
- \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))",
+ \ prfT %% (OfClass type_class % TYPE('T=>bool)) %% \
+ \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %% \
+ \ (OfClass type_class % TYPE('T=>'T=>bool))) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))",
- "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
+ "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %% \
\ (axm.symmetric % TYPE('T2) % x5 % x6 %% \
\ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \
\ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) == \
\ (iffD2 % A = C % B = D %% \
- \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \
+ \ (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %% \
+ \ prfT %% arity_type_bool %% \
\ (cong % TYPE('T) % TYPE('T=>bool) % \
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
- \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))",
+ \ prfT %% (OfClass type_class % TYPE('T=>bool)) %% \
+ \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %% \
+ \ (OfClass type_class % TYPE('T=>'T=>bool))) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))",
(** rewriting on bool: insert proper congruence rules for logical connectives **)
(* All *)
- "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
- \ (allI % TYPE('a) % Q %% \
+ "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
+ \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
+ \ (allI % TYPE('a) % Q %% prfa %% \
\ (Lam x. \
\ iffD1 % P x % Q x %% (prf % x) %% \
- \ (spec % TYPE('a) % P % x %% prf')))",
+ \ (spec % TYPE('a) % P % x %% prfa %% prf')))",
- "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
- \ (allI % TYPE('a) % P %% \
+ "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
+ \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
+ \ (allI % TYPE('a) % P %% prfa %% \
\ (Lam x. \
\ iffD2 % P x % Q x %% (prf % x) %% \
- \ (spec % TYPE('a) % Q % x %% prf')))",
+ \ (spec % TYPE('a) % Q % x %% prfa %% prf')))",
(* Ex *)
- "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
- \ (exE % TYPE('a) % P % EX x. Q x %% prf' %% \
+ "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
+ \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
+ \ (exE % TYPE('a) % P % EX x. Q x %% prfa %% prf' %% \
\ (Lam x H : P x. \
- \ exI % TYPE('a) % Q % x %% \
+ \ exI % TYPE('a) % Q % x %% prfa %% \
\ (iffD1 % P x % Q x %% (prf % x) %% H)))",
- "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
- \ (exE % TYPE('a) % Q % EX x. P x %% prf' %% \
+ "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
+ \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
+ \ (exE % TYPE('a) % Q % EX x. P x %% prfa %% prf' %% \
\ (Lam x H : Q x. \
- \ exI % TYPE('a) % P % x %% \
+ \ exI % TYPE('a) % P % x %% prfa %% \
\ (iffD2 % P x % Q x %% (prf % x) %% H)))",
(* & *)
- "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \
- \ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \
+ "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (conjI % B % D %% \
\ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \
\ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
- "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \
- \ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \
+ "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (conjI % A % C %% \
\ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \
\ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
- "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \
- \ (HOL.refl % TYPE(bool=>bool) % op & A)) == \
- \ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \
+ "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \
+ \ (HOL.refl % TYPE(bool=>bool) % op & A %% prfbb)) == \
+ \ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %% \
- \ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %% \
- \ (HOL.refl % TYPE(bool) % A)))",
+ \ prfb %% prfbb %% \
+ \ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool) %% \
+ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
+ \ (HOL.refl % TYPE(bool) % A %% prfb)))",
(* | *)
- "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \
- \ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \
+ "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (disjE % A % C % B | D %% prf3 %% \
\ (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %% \
\ (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
- "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \
- \ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \
+ "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (disjE % B % D % A | C %% prf3 %% \
\ (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %% \
\ (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
- "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \
- \ (HOL.refl % TYPE(bool=>bool) % op | A)) == \
- \ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \
+ "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %% \
+ \ (HOL.refl % TYPE(bool=>bool) % op | A %% prfbb)) == \
+ \ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %% \
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %% \
- \ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %% \
- \ (HOL.refl % TYPE(bool) % A)))",
+ \ prfb %% prfbb %% \
+ \ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool) %% \
+ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
+ \ (HOL.refl % TYPE(bool) % A %% prfb)))",
(* --> *)
- "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \
- \ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \
+ "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \
\ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
- "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \
- \ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \
+ "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \
\ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
- "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \
- \ (HOL.refl % TYPE(bool=>bool) % op --> A)) == \
- \ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \
+ "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %% \
+ \ (HOL.refl % TYPE(bool=>bool) % op --> A %% prfbb)) == \
+ \ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %% \
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %% \
- \ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %% \
- \ (HOL.refl % TYPE(bool) % A)))",
+ \ prfb %% prfbb %% \
+ \ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool) %% \
+ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
+ \ (HOL.refl % TYPE(bool) % A %% prfb)))",
(* ~ *)
- "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \
- \ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \
+ "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \
\ (notI % Q %% (Lam H: Q. \
\ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
- "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \
- \ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \
+ "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \
\ (notI % P %% (Lam H: P. \
\ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
(* = *)
"(iffD1 % B % D %% \
- \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
- \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
- \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
+ \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \
\ (iffD1 % C % D %% prf2 %% \
\ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
"(iffD2 % B % D %% \
- \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
- \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
- \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
+ \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \
\ (iffD1 % A % B %% prf1 %% \
\ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
"(iffD1 % A % C %% \
- \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
- \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
- \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)== \
+ \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)== \
\ (iffD2 % C % D %% prf2 %% \
\ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
"(iffD2 % A % C %% \
- \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
- \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
- \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
+ \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \
\ (iffD2 % A % B %% prf1 %% \
\ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
- "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
- \ (HOL.refl % TYPE(bool=>bool) % op = A)) == \
- \ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
+ "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %% \
+ \ (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) == \
+ \ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %% \
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %% \
- \ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %% \
- \ (HOL.refl % TYPE(bool) % A)))",
+ \ prfb %% prfbb %% \
+ \ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %% \
+ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
+ \ (HOL.refl % TYPE(bool) % A %% prfb)))",
(** transitivity, reflexivity, and symmetry **)
- "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \
+ "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) == \
\ (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
- "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \
+ "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) == \
\ (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
- "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
+ "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
- "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
+ "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
- "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",
+ "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)",
- "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)",
+ "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)",
(** normalization of HOL proofs **)
@@ -262,13 +283,13 @@
"(impI % A % B %% (mp % A % B %% prf)) == prf",
- "(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x",
+ "(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x",
- "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
+ "(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf",
- "(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)",
+ "(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)",
- "(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf",
+ "(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf",
"(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
@@ -286,26 +307,26 @@
(** Replace congruence rules by substitution rules **)
fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
- prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
- | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps)
+ prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
+ | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps)
| strip_cong _ _ = NONE;
-val subst_prf = fst (strip_combt (Thm.proof_of subst));
-val sym_prf = fst (strip_combt (Thm.proof_of sym));
+val subst_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of subst))));
+val sym_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of sym))));
fun make_subst Ts prf xs (_, []) = prf
- | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
+ | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
let val T = fastype_of1 (Ts, x)
in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
else change_type (SOME [T]) subst_prf %> x %> y %>
Abs ("z", T, list_comb (incr_boundvars 1 f,
map (incr_boundvars 1) xs @ Bound 0 ::
- map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
+ map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
make_subst Ts prf (xs @ [x]) (f, ps)
end;
-fun make_sym Ts ((x, y), prf) =
- ((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
+fun make_sym Ts ((x, y), (prf, clprf)) =
+ ((y, x), (change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
@@ -322,6 +343,6 @@
apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
| elim_cong_aux _ _ = NONE;
-fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
+fun elim_cong Ts hs prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
end;
--- a/src/HOL/Word/WordDefinition.thy Tue Jun 01 17:52:00 2010 +0200
+++ b/src/HOL/Word/WordDefinition.thy Tue Jun 01 17:52:19 2010 +0200
@@ -19,13 +19,31 @@
definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
-- {* representation of words using unsigned or signed bins,
only difference in these is the type class *}
- [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)"
+ "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)"
lemma uint_word_of_int [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = w mod 2 ^ len_of TYPE('a)"
by (auto simp add: word_of_int_def bintrunc_mod2p intro: Abs_word_inverse)
code_datatype word_of_int
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation word :: ("{len0, typerep}") random
+begin
+
+definition
+ "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) o\<rightarrow> (\<lambda>k. Pair (
+ let j = word_of_int (Code_Numeral.int_of k) :: 'a word
+ in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
subsection {* Type conversions and casting *}
--- a/src/Pure/Concurrent/future.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Jun 01 17:52:19 2010 +0200
@@ -126,7 +126,7 @@
val lock = Mutex.mutex ();
in
-fun SYNCHRONIZED name = SimpleThread.synchronized name lock;
+fun SYNCHRONIZED name = Simple_Thread.synchronized name lock;
fun wait cond = (*requires SYNCHRONIZED*)
Multithreading.sync_wait NONE NONE cond lock;
@@ -238,7 +238,7 @@
| SOME work => (execute work; worker_loop name));
fun worker_start name = (*requires SYNCHRONIZED*)
- Unsynchronized.change workers (cons (SimpleThread.fork false (fn () => worker_loop name),
+ Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
Unsynchronized.ref Working));
@@ -371,7 +371,7 @@
fun scheduler_check () = (*requires SYNCHRONIZED*)
(do_shutdown := false;
if scheduler_active () then ()
- else scheduler := SOME (SimpleThread.fork false scheduler_loop));
+ else scheduler := SOME (Simple_Thread.fork false scheduler_loop));
--- a/src/Pure/Concurrent/simple_thread.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML Tue Jun 01 17:52:19 2010 +0200
@@ -12,7 +12,7 @@
val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
end;
-structure SimpleThread: SIMPLE_THREAD =
+structure Simple_Thread: SIMPLE_THREAD =
struct
fun attributes interrupts =
--- a/src/Pure/Concurrent/single_assignment.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML Tue Jun 01 17:52:19 2010 +0200
@@ -32,7 +32,7 @@
fun peek (Var {var, ...}) = SingleAssignment.savalue var;
fun await (v as Var {name, lock, cond, var}) =
- SimpleThread.synchronized name lock (fn () =>
+ Simple_Thread.synchronized name lock (fn () =>
let
fun wait () =
(case peek v of
@@ -44,7 +44,7 @@
in wait () end);
fun assign (v as Var {name, lock, cond, var}) x =
- SimpleThread.synchronized name lock (fn () =>
+ Simple_Thread.synchronized name lock (fn () =>
(case peek v of
SOME _ => raise Fail ("Duplicate assignment to variable " ^ quote name)
| NONE =>
--- a/src/Pure/Concurrent/synchronized.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Tue Jun 01 17:52:19 2010 +0200
@@ -39,7 +39,7 @@
(* synchronized access *)
fun timed_access (Var {name, lock, cond, var}) time_limit f =
- SimpleThread.synchronized name lock (fn () =>
+ Simple_Thread.synchronized name lock (fn () =>
let
fun try_change () =
let val x = ! var in
--- a/src/Pure/Concurrent/task_queue.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Tue Jun 01 17:52:19 2010 +0200
@@ -162,7 +162,7 @@
val tasks = Inttab.lookup_list groups (group_id group);
val running =
fold (get_job jobs #> (fn Running t => insert Thread.equal t | _ => I)) tasks [];
- val _ = List.app SimpleThread.interrupt running;
+ val _ = List.app Simple_Thread.interrupt running;
in null running end;
fun cancel_all (Queue {groups, jobs}) =
@@ -173,7 +173,7 @@
Running t => (insert eq_group group groups, insert Thread.equal t running)
| _ => (groups, running)));
val (running_groups, running) = Task_Graph.fold (cancel_job o #1 o #2) jobs ([], []);
- val _ = List.app SimpleThread.interrupt running;
+ val _ = List.app Simple_Thread.interrupt running;
in running_groups end;
--- a/src/Pure/General/scan.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/General/scan.ML Tue Jun 01 17:52:19 2010 +0200
@@ -322,5 +322,5 @@
end;
-structure BasicScan: BASIC_SCAN = Scan;
-open BasicScan;
+structure Basic_Scan: BASIC_SCAN = Scan;
+open Basic_Scan;
--- a/src/Pure/Isar/class_target.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Tue Jun 01 17:52:19 2010 +0200
@@ -450,7 +450,7 @@
(* target *)
-val sanatize_name = (*FIXME*)
+val sanitize_name = (*FIXME*)
let
fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
orelse s = "'" orelse s = "_";
@@ -467,7 +467,7 @@
fun type_name "*" = "prod"
| type_name "+" = "sum"
- | type_name s = sanatize_name (Long_Name.base_name s);
+ | type_name s = sanitize_name (Long_Name.base_name s);
fun resort_terms pp algebra consts constraints ts =
let
--- a/src/Pure/Isar/isar_cmd.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Jun 01 17:52:19 2010 +0200
@@ -85,7 +85,7 @@
val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
end;
-structure IsarCmd: ISAR_CMD =
+structure Isar_Cmd: ISAR_CMD =
struct
@@ -272,10 +272,10 @@
(* init and exit *)
fun init_theory (name, imports, uses) =
- Toplevel.init_theory name (ThyInfo.begin_theory name imports (map (apfst Path.explode) uses))
+ Toplevel.init_theory name (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
(fn thy =>
- if ThyInfo.check_known_thy (Context.theory_name thy)
- then ThyInfo.end_theory thy else ());
+ if Thy_Info.check_known_thy (Context.theory_name thy)
+ then Thy_Info.end_theory thy else ());
val exit = Toplevel.keep (fn state =>
(Context.set_thread_data (try Toplevel.generic_theory_of state);
@@ -384,18 +384,18 @@
val print_methods = Toplevel.unknown_theory o
Toplevel.keep (Method.print_methods o Toplevel.theory_of);
-val print_antiquotations = Toplevel.imperative ThyOutput.print_antiquotations;
+val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations;
val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
let
val thy = Toplevel.theory_of state;
- val all_thys = sort ThyInfo.thy_ord (thy :: Theory.ancestors_of thy);
+ val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy);
val gr = all_thys |> map (fn node =>
let
val name = Context.theory_name node;
val parents = map Context.theory_name (Theory.parents_of node);
val dir = Present.session_name node;
- val unfold = not (ThyInfo.known_thy name andalso ThyInfo.is_finished name);
+ val unfold = not (Thy_Info.known_thy name andalso Thy_Info.is_finished name);
in {name = name, ID = name, parents = parents, dir = dir, unfold = unfold, path = ""} end);
in Present.display_graph gr end);
@@ -427,8 +427,8 @@
Thm_Deps.unused_thms
(case opt_range of
NONE => (Theory.parents_of thy, [thy])
- | SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy])
- | SOME (xs, SOME ys) => (map ThyInfo.get_theory xs, map ThyInfo.get_theory ys))
+ | SOME (xs, NONE) => (map Thy_Info.get_theory xs, [thy])
+ | SOME (xs, SOME ys) => (map Thy_Info.get_theory xs, map Thy_Info.get_theory ys))
|> map pretty_thm |> Pretty.chunks |> Pretty.writeln
end);
@@ -517,7 +517,7 @@
fun check_text (txt, pos) state =
(Position.report Markup.doc_source pos;
- ignore (ThyOutput.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
+ ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
fun header_markup txt = Toplevel.keep (fn state =>
if Toplevel.is_toplevel state then check_text txt state
--- a/src/Pure/Isar/isar_document.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML Tue Jun 01 17:52:19 2010 +0200
@@ -181,7 +181,7 @@
fun begin_document (id: document_id) path =
let
- val (dir, name) = ThyLoad.split_thy_path path;
+ val (dir, name) = Thy_Load.split_thy_path path;
val _ = define_document id (make_document dir name no_entries);
in () end;
@@ -197,8 +197,8 @@
(case Lazy.force end_state of
SOME st =>
(Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
- ThyInfo.touch_child_thys name;
- ThyInfo.register_thy name)
+ Thy_Info.touch_child_thys name;
+ Thy_Info.register_thy name)
| NONE => error ("Failed to finish theory " ^ quote name)));
in () end);
--- a/src/Pure/Isar/isar_syn.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Jun 01 17:52:19 2010 +0200
@@ -4,7 +4,7 @@
Isar/Pure outer syntax.
*)
-structure IsarSyn: sig end =
+structure Isar_Syn: sig end =
struct
(** keywords **)
@@ -28,7 +28,7 @@
val _ =
Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
- (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
+ (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory));
val _ =
Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
@@ -38,43 +38,43 @@
(** markup commands **)
-val _ = Outer_Syntax.markup_command ThyOutput.Markup "header" "theory header" Keyword.diag
- (Parse.doc_source >> IsarCmd.header_markup);
+val _ = Outer_Syntax.markup_command Thy_Output.Markup "header" "theory header" Keyword.diag
+ (Parse.doc_source >> Isar_Cmd.header_markup);
-val _ = Outer_Syntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
- Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
+val _ = Outer_Syntax.markup_command Thy_Output.Markup "chapter" "chapter heading"
+ Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-val _ = Outer_Syntax.markup_command ThyOutput.Markup "section" "section heading"
- Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
+val _ = Outer_Syntax.markup_command Thy_Output.Markup "section" "section heading"
+ Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
- Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
+val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsection" "subsection heading"
+ Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
val _ =
- Outer_Syntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
- Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
+ Outer_Syntax.markup_command Thy_Output.Markup "subsubsection" "subsubsection heading"
+ Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-val _ = Outer_Syntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
- Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
+val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "text" "formal comment (theory)"
+ Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-val _ = Outer_Syntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text"
- Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
+val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "text_raw" "raw document preparation text"
+ Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-val _ = Outer_Syntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
- (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
+val _ = Outer_Syntax.markup_command Thy_Output.Markup "sect" "formal comment (proof)"
+ (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
-val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
- (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
+val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsect" "formal comment (proof)"
+ (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
-val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)"
- (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
+val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsubsect" "formal comment (proof)"
+ (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
-val _ = Outer_Syntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
- (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> IsarCmd.proof_markup);
+val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "txt" "formal comment (proof)"
+ (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> Isar_Cmd.proof_markup);
-val _ = Outer_Syntax.markup_command ThyOutput.Verbatim "txt_raw"
+val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "txt_raw"
"raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
- (Parse.doc_source >> IsarCmd.proof_markup);
+ (Parse.doc_source >> Isar_Cmd.proof_markup);
@@ -185,7 +185,7 @@
Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
(Scan.repeat1 Parse_Spec.spec >>
(Toplevel.theory o
- (IsarCmd.add_axioms o
+ (Isar_Cmd.add_axioms o
tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
val opt_unchecked_overloaded =
@@ -197,7 +197,7 @@
Outer_Syntax.command "defs" "define constants" Keyword.thy_decl
(opt_unchecked_overloaded --
Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
- >> (Toplevel.theory o IsarCmd.add_defs));
+ >> (Toplevel.theory o Isar_Cmd.add_defs));
(* old constdefs *)
@@ -296,10 +296,10 @@
((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
(Toplevel.theory o uncurry hide));
-val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
-val _ = hide_names "hide_type" IsarCmd.hide_type "types";
-val _ = hide_names "hide_const" IsarCmd.hide_const "constants";
-val _ = hide_names "hide_fact" IsarCmd.hide_fact "facts";
+val _ = hide_names "hide_class" Isar_Cmd.hide_class "classes";
+val _ = hide_names "hide_type" Isar_Cmd.hide_type "types";
+val _ = hide_names "hide_const" Isar_Cmd.hide_const "constants";
+val _ = hide_names "hide_fact" Isar_Cmd.hide_fact "facts";
(* use ML text *)
@@ -314,7 +314,7 @@
val _ =
Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
(Parse.path >>
- (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
+ (fn path => Toplevel.generic_theory (Thy_Info.exec_file false path #> propagate_env)));
val _ =
Outer_Syntax.command "ML" "ML text within theory or local theory"
@@ -331,19 +331,19 @@
val _ =
Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
- (Parse.ML_source >> IsarCmd.ml_diag true);
+ (Parse.ML_source >> Isar_Cmd.ml_diag true);
val _ =
Outer_Syntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
- (Parse.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
+ (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
val _ =
Outer_Syntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
- (Parse.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
+ (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
val _ =
Outer_Syntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
- (Parse.ML_source >> IsarCmd.local_setup);
+ (Parse.ML_source >> Isar_Cmd.local_setup);
val _ =
Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
@@ -357,14 +357,14 @@
val _ =
Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
- (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry IsarCmd.declaration);
+ (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry Isar_Cmd.declaration);
val _ =
Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
(Parse.name --
(Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
- >> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d));
+ >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
(* translation functions *)
@@ -374,27 +374,27 @@
val _ =
Outer_Syntax.command "parse_ast_translation" "install parse ast translation functions"
(Keyword.tag_ml Keyword.thy_decl)
- (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
+ (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
val _ =
Outer_Syntax.command "parse_translation" "install parse translation functions"
(Keyword.tag_ml Keyword.thy_decl)
- (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
+ (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
val _ =
Outer_Syntax.command "print_translation" "install print translation functions"
(Keyword.tag_ml Keyword.thy_decl)
- (trfun >> (Toplevel.theory o IsarCmd.print_translation));
+ (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
val _ =
Outer_Syntax.command "typed_print_translation" "install typed print translation functions"
(Keyword.tag_ml Keyword.thy_decl)
- (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
+ (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
val _ =
Outer_Syntax.command "print_ast_translation" "install print ast translation functions"
(Keyword.tag_ml Keyword.thy_decl)
- (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
+ (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
(* oracles *)
@@ -402,7 +402,7 @@
val _ =
Outer_Syntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
(Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
- (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
+ (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
(* local theories *)
@@ -537,22 +537,22 @@
val _ =
Outer_Syntax.command "have" "state local goal"
(Keyword.tag_proof Keyword.prf_goal)
- (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
+ (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
val _ =
Outer_Syntax.command "hence" "abbreviates \"then have\""
(Keyword.tag_proof Keyword.prf_goal)
- (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
+ (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
val _ =
Outer_Syntax.command "show" "state local goal, solving current obligation"
(Keyword.tag_proof Keyword.prf_asm_goal)
- (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
+ (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
val _ =
Outer_Syntax.command "thus" "abbreviates \"then show\""
(Keyword.tag_proof Keyword.prf_asm_goal)
- (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
+ (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
(* facts *)
@@ -673,32 +673,32 @@
val _ =
Outer_Syntax.command "qed" "conclude (sub-)proof"
(Keyword.tag_proof Keyword.qed_block)
- (Scan.option Method.parse >> IsarCmd.qed);
+ (Scan.option Method.parse >> Isar_Cmd.qed);
val _ =
Outer_Syntax.command "by" "terminal backward proof"
(Keyword.tag_proof Keyword.qed)
- (Method.parse -- Scan.option Method.parse >> IsarCmd.terminal_proof);
+ (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
val _ =
Outer_Syntax.command ".." "default proof"
(Keyword.tag_proof Keyword.qed)
- (Scan.succeed IsarCmd.default_proof);
+ (Scan.succeed Isar_Cmd.default_proof);
val _ =
Outer_Syntax.command "." "immediate proof"
(Keyword.tag_proof Keyword.qed)
- (Scan.succeed IsarCmd.immediate_proof);
+ (Scan.succeed Isar_Cmd.immediate_proof);
val _ =
Outer_Syntax.command "done" "done proof"
(Keyword.tag_proof Keyword.qed)
- (Scan.succeed IsarCmd.done_proof);
+ (Scan.succeed Isar_Cmd.done_proof);
val _ =
Outer_Syntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
(Keyword.tag_proof Keyword.qed)
- (Scan.succeed IsarCmd.skip_proof);
+ (Scan.succeed Isar_Cmd.skip_proof);
val _ =
Outer_Syntax.command "oops" "forget proof"
@@ -796,7 +796,7 @@
val _ =
Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
- Keyword.diag (Parse.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
+ Keyword.diag (Parse.nat >> (Toplevel.no_timing oo Isar_Cmd.pretty_setmargin));
val _ =
Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
@@ -808,32 +808,32 @@
val _ =
Outer_Syntax.improper_command "print_configs" "print configuration options" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs));
val _ =
Outer_Syntax.improper_command "print_context" "print theory context name" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context));
val _ =
Outer_Syntax.improper_command "print_theory" "print logical theory contents (verbose!)"
- Keyword.diag (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
+ Keyword.diag (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
val _ =
Outer_Syntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
- Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
+ Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
val _ =
Outer_Syntax.improper_command "print_abbrevs" "print constant abbreviation of context"
- Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
+ Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
val _ =
Outer_Syntax.improper_command "print_theorems"
"print theorems of local theory or proof context" Keyword.diag
- (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
+ (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
val _ =
Outer_Syntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales));
val _ =
Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
@@ -842,89 +842,89 @@
val _ =
Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
- (opt_bang -- Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
+ (opt_bang -- Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
val _ =
Outer_Syntax.improper_command "print_interps"
"print interpretations of locale for this theory" Keyword.diag
- (Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
+ (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
val _ =
Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
val _ =
Outer_Syntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset));
val _ =
Outer_Syntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules));
val _ =
Outer_Syntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules));
val _ =
Outer_Syntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
val _ =
Outer_Syntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
val _ =
Outer_Syntax.improper_command "thy_deps" "visualize theory dependencies"
- Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
+ Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
val _ =
Outer_Syntax.improper_command "class_deps" "visualize class dependencies"
- Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
+ Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
val _ =
Outer_Syntax.improper_command "thm_deps" "visualize theorem dependencies"
- Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
+ Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
val _ =
Outer_Syntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds));
val _ =
Outer_Syntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts));
val _ =
Outer_Syntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases));
val _ =
Outer_Syntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
- (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
+ (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
val _ =
Outer_Syntax.improper_command "thm" "print theorems" Keyword.diag
- (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
+ (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
val _ =
Outer_Syntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
(opt_modes -- Scan.option Parse_Spec.xthms1
- >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
+ >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
val _ =
Outer_Syntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
- (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
+ (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
val _ =
Outer_Syntax.improper_command "prop" "read and print proposition" Keyword.diag
- (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
+ (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
val _ =
Outer_Syntax.improper_command "term" "read and print term" Keyword.diag
- (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_term));
+ (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
val _ =
Outer_Syntax.improper_command "typ" "read and print type" Keyword.diag
- (opt_modes -- Parse.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
+ (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
val _ =
Outer_Syntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
@@ -936,7 +936,7 @@
Outer_Syntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
(Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
- (Toplevel.no_timing oo IsarCmd.unused_thms));
+ (Toplevel.no_timing oo Isar_Cmd.unused_thms));
@@ -944,54 +944,54 @@
val _ =
Outer_Syntax.improper_command "cd" "change current working directory" Keyword.diag
- (Parse.path >> (Toplevel.no_timing oo IsarCmd.cd));
+ (Parse.path >> (Toplevel.no_timing oo Isar_Cmd.cd));
val _ =
Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
val _ =
Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.diag
(Parse.name >> (fn name =>
- Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name)));
+ Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
val _ =
Outer_Syntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
(Parse.name >> (fn name =>
- Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name)));
+ Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.touch_thy name)));
val _ =
Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
(Parse.name >> (fn name =>
- Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name)));
+ Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
val _ =
Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
Keyword.diag (Parse.name >> (fn name =>
- Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name)));
+ Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
val _ =
Outer_Syntax.improper_command "display_drafts" "display raw source files with symbols"
- Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
+ Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
val _ =
Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
- Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
+ Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
val opt_limits =
Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
val _ =
Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
- (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
+ (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
val _ =
Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
val _ =
Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
val _ =
Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
@@ -999,11 +999,11 @@
val _ =
Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
- (Parse.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
+ (Parse.opt_unit >> (Toplevel.no_timing oo K Isar_Cmd.quit));
val _ =
Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
- (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.exit));
end;
--- a/src/Pure/Isar/method.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Isar/method.ML Tue Jun 01 17:52:19 2010 +0200
@@ -271,15 +271,16 @@
val intros_tac = gen_intros_tac ALLGOALS;
val try_intros_tac = gen_intros_tac TRYALL;
+
(* ML tactics *)
-structure TacticData = Proof_Data
+structure ML_Tactic = Proof_Data
(
type T = thm list -> tactic;
fun init _ = undefined;
);
-val set_tactic = TacticData.put;
+val set_tactic = ML_Tactic.put;
fun ml_tactic (txt, pos) ctxt =
let
@@ -287,7 +288,7 @@
(ML_Context.expression pos
"fun tactic (facts: thm list) : tactic"
"Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read pos txt));
- in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end;
+ in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end;
fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
--- a/src/Pure/Isar/object_logic.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Isar/object_logic.ML Tue Jun 01 17:52:19 2010 +0200
@@ -46,7 +46,7 @@
fun make_data (base_sort, judgment, atomize_rulify) =
Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
-structure ObjectLogicData = Theory_Data
+structure Data = Theory_Data
(
type T = data;
val empty = make_data (NONE, NONE, ([], []));
@@ -63,10 +63,10 @@
(Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2)));
);
-fun map_data f = ObjectLogicData.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
+fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
make_data (f (base_sort, judgment, atomize_rulify)));
-fun get_data thy = ObjectLogicData.get thy |> (fn Data args => args);
+fun get_data thy = Data.get thy |> (fn Data args => args);
--- a/src/Pure/Isar/outer_syntax.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Tue Jun 01 17:52:19 2010 +0200
@@ -11,7 +11,7 @@
sig
val command: string -> string -> Keyword.T ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
- val markup_command: ThyOutput.markup -> string -> string -> Keyword.T ->
+ val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
val improper_command: string -> string -> Keyword.T ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
@@ -43,7 +43,7 @@
datatype command = Command of
{comment: string,
- markup: ThyOutput.markup option,
+ markup: Thy_Output.markup option,
int_only: bool,
parse: (Toplevel.transition -> Toplevel.transition) parser};
@@ -83,7 +83,7 @@
local
val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
-val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
+val global_markups = Unsynchronized.ref ([]: (string * Thy_Output.markup) list);
fun change_commands f = CRITICAL (fn () =>
(Unsynchronized.change global_commands f;
@@ -235,9 +235,9 @@
fun prepare_span commands span =
let
- val range_pos = Position.encode_range (ThySyntax.span_range span);
- val toks = ThySyntax.span_content span;
- val _ = List.app ThySyntax.report_token toks;
+ val range_pos = Position.encode_range (Thy_Syntax.span_range span);
+ val toks = Thy_Syntax.span_content span;
+ val _ = List.app Thy_Syntax.report_token toks;
in
(case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
[tr] => (tr, true)
@@ -257,7 +257,7 @@
fun prepare_command pos str =
let val (lexs, commands) = get_syntax () in
- (case ThySyntax.parse_spans lexs pos str of
+ (case Thy_Syntax.parse_spans lexs pos str of
[span] => #1 (prepare_span commands span)
| _ => Toplevel.malformed pos not_singleton)
end;
@@ -271,21 +271,21 @@
val _ = Present.init_theory name;
- val toks = Source.exhausted (ThySyntax.token_source lexs pos (Source.of_list text));
- val spans = Source.exhaust (ThySyntax.span_source toks);
- val _ = List.app ThySyntax.report_span spans;
- val units = Source.exhaust (ThySyntax.unit_source (Source.of_list spans))
+ val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_list text));
+ val spans = Source.exhaust (Thy_Syntax.span_source toks);
+ val _ = List.app Thy_Syntax.report_span spans;
+ val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
|> maps (prepare_unit commands);
val _ = Present.theory_source name
- (fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans);
+ (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
val results = cond_timeit time "" (fn () => Toplevel.excursion units);
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
fun after_load () =
- ThyOutput.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
+ Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
|> Buffer.content
|> Present.theory_output name;
in after_load end;
--- a/src/Pure/Isar/proof_context.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Jun 01 17:52:19 2010 +0200
@@ -193,7 +193,7 @@
val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
-structure ContextData = Proof_Data
+structure Data = Proof_Data
(
type T = ctxt;
fun init thy =
@@ -202,10 +202,10 @@
(Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
);
-fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
+fun rep_context ctxt = Data.get ctxt |> (fn Ctxt args => args);
fun map_context f =
- ContextData.map (fn Ctxt {mode, naming, syntax, tsig, consts, facts, cases} =>
+ Data.map (fn Ctxt {mode, naming, syntax, tsig, consts, facts, cases} =>
make_ctxt (f (mode, naming, syntax, tsig, consts, facts, cases)));
fun set_mode mode = map_context (fn (_, naming, syntax, tsig, consts, facts, cases) =>
--- a/src/Pure/Isar/specification.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Isar/specification.ML Tue Jun 01 17:52:19 2010 +0200
@@ -361,7 +361,7 @@
#2 #> pair ths);
in ((prems, stmt, SOME facts), goal_ctxt) end);
-structure TheoremHook = Generic_Data
+structure Theorem_Hook = Generic_Data
(
type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
val empty = [];
@@ -407,7 +407,7 @@
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
|> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
error "Illegal schematic goal statement")
- |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
+ |> Library.apply (map (fn (f, _) => f int) (rev (Theorem_Hook.get (Context.Proof goal_ctxt))))
end;
in
@@ -418,7 +418,7 @@
val schematic_theorem = gen_theorem true (K I) Expression.cert_statement;
val schematic_theorem_cmd = gen_theorem true Attrib.intern_src Expression.read_statement;
-fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
+fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
end;
--- a/src/Pure/Isar/toplevel.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Jun 01 17:52:19 2010 +0200
@@ -238,7 +238,7 @@
|> Runtime.debugging
|> Runtime.toplevel_error
(fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
- SimpleThread.attributes interrupts);
+ Simple_Thread.attributes interrupts);
(* node transactions -- maintaining stable checkpoints *)
@@ -638,11 +638,12 @@
fun run_command thy_name tr st =
(case
(case init_of tr of
- SOME name => Exn.capture (fn () => ThyLoad.check_name thy_name name) ()
+ SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
| NONE => Exn.Result ()) of
Exn.Result () =>
(case transition true tr st of
SOME (st', NONE) => (status tr Markup.finished; SOME st')
+ | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
| SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
| NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
| Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
--- a/src/Pure/ML/ml_antiquote.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Tue Jun 01 17:52:19 2010 +0200
@@ -20,7 +20,7 @@
(* ML names *)
-structure NamesData = Proof_Data
+structure Names = Proof_Data
(
type T = Name.context;
fun init _ = ML_Syntax.reserved;
@@ -28,9 +28,9 @@
fun variant a ctxt =
let
- val names = NamesData.get ctxt;
+ val names = Names.get ctxt;
val ([b], names') = Name.variants [a] names;
- val ctxt' = NamesData.put names' ctxt;
+ val ctxt' = Names.put names' ctxt;
in (b, ctxt') end;
@@ -64,12 +64,12 @@
>> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
val _ = value "theory"
- (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
+ (Scan.lift Args.name >> (fn name => "Thy_Info.get_theory " ^ ML_Syntax.print_string name)
|| Scan.succeed "ML_Context.the_global_context ()");
val _ = value "theory_ref"
(Scan.lift Args.name >> (fn name =>
- "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")
+ "Theory.check_thy (Thy_Info.theory " ^ ML_Syntax.print_string name ^ ")")
|| Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Jun 01 17:52:19 2010 +0200
@@ -87,11 +87,7 @@
map (pair (offset_of p)) (String.explode (Symbol.esc sym)))
end);
- val end_pos =
- if null toks then Position.none
- else ML_Lex.end_pos_of (List.last toks);
-
- val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
+ val input_buffer = Unsynchronized.ref input;
val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
--- a/src/Pure/ML/ml_lex.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML Tue Jun 01 17:52:19 2010 +0200
@@ -267,17 +267,24 @@
let
val _ = Position.report Markup.ML_source pos;
val syms = Symbol_Pos.explode (txt, pos);
- in
- (Source.of_list syms
- |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
- (SOME (false, fn msg => recover msg >> map Antiquote.Text))
- |> Source.exhaust
- |> tap (List.app (Antiquote.report report_token))
- |> tap Antiquote.check_nesting
- |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
- handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos)
- end;
+ val termination =
+ if null syms then []
+ else
+ let
+ val pos1 = List.last syms |-> Position.advance;
+ val pos2 = Position.advance Symbol.space pos1;
+ in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
+ val input =
+ (Source.of_list syms
+ |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
+ (SOME (false, fn msg => recover msg >> map Antiquote.Text))
+ |> Source.exhaust
+ |> tap (List.app (Antiquote.report report_token))
+ |> tap Antiquote.check_nesting
+ |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
+ in input @ termination end;
end;
--- a/src/Pure/ML/ml_thms.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/ML/ml_thms.ML Tue Jun 01 17:52:19 2010 +0200
@@ -15,15 +15,15 @@
(* auxiliary facts table *)
-structure AuxFacts = Proof_Data
+structure Aux_Facts = Proof_Data
(
type T = thm list Inttab.table;
fun init _ = Inttab.empty;
);
-val put_thms = AuxFacts.map o Inttab.update;
+val put_thms = Aux_Facts.map o Inttab.update;
-fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name);
+fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name);
fun the_thm ctxt name = the_single (the_thms ctxt name);
fun thm_bind kind a i =
--- a/src/Pure/Proof/extraction.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Jun 01 17:52:19 2010 +0200
@@ -24,6 +24,7 @@
val mk_typ : typ -> term
val etype_of : theory -> string list -> typ list -> term -> typ
val realizes_of: theory -> string list -> term -> term -> term
+ val abs_corr_shyps: theory -> thm -> string list -> term list -> Proofterm.proof -> Proofterm.proof
end;
structure Extraction : EXTRACTION =
@@ -126,11 +127,9 @@
fun frees_of t = map Free (rev (Term.add_frees t []));
fun vfs_of t = vars_of t @ frees_of t;
-fun forall_intr_prf (t, prf) =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in Abst (a, SOME T, prf_abstract_over t prf) end;
+val mkabs = fold_rev (fn v => fn t => Abs ("x", fastype_of v, abstract_over (v, t)));
-val mkabs = List.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
+val mkabsp = fold_rev (fn t => fn prf => AbsP ("H", SOME t, prf));
fun strip_abs 0 t = t
| strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
@@ -161,6 +160,14 @@
| _ => error "get_var_type: not a variable"
end;
+fun read_term thy T s =
+ let
+ val ctxt = ProofContext.init_global thy
+ |> Proof_Syntax.strip_sorts_consttypes
+ |> ProofContext.set_defsort [];
+ val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
+ in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
+
(**** theory data ****)
@@ -175,7 +182,7 @@
(term -> typ -> term -> typ -> term) option)) list,
realizers : (string list * (term * proof)) list Symtab.table,
defs : thm list,
- expand : (string * term) list,
+ expand : string list,
prep : (theory -> proof -> proof) option}
val empty =
@@ -198,14 +205,14 @@
types = AList.merge (op =) (K true) (types1, types2),
realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
defs = Library.merge Thm.eq_thm (defs1, defs2),
- expand = Library.merge (op =) (expand1, expand2), (* FIXME proper aconv !?! *)
+ expand = Library.merge (op =) (expand1, expand2),
prep = (case prep1 of NONE => prep2 | _ => prep1)};
);
fun read_condeq thy =
let val thy' = add_syntax thy
in fn s =>
- let val t = Logic.varify_global (Syntax.read_prop_global thy' s)
+ let val t = Logic.varify_global (read_term thy' propT s)
in
(map Logic.dest_equals (Logic.strip_imp_prems t),
Logic.dest_equals (Logic.strip_imp_concl t))
@@ -274,7 +281,7 @@
fun err () = error ("Unable to determine type of extracted program for\n" ^
Syntax.string_of_term_global thy t)
in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
- [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
+ [typeof_proc [] vs]) (list_abs (map (pair "x") (rev Ts),
Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
| _ => err ()
@@ -300,25 +307,30 @@
val rtypes = map fst types;
val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
val thy' = add_syntax thy;
- val rd = Proof_Syntax.read_proof thy' false;
+ val rd = Proof_Syntax.read_proof thy' true false;
in fn (thm, (vs, s1, s2)) =>
let
val name = Thm.derivation_name thm;
val _ = name <> "" orelse error "add_realizers: unnamed theorem";
- val prop = Pattern.rewrite_term thy'
- (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
+ val prop = Thm.unconstrainT thm |> prop_of |>
+ Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [];
val vars = vars_of prop;
val vars' = filter_out (fn v =>
member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
+ val shyps = maps (fn Var ((x, i), _) =>
+ if member (op =) vs x then Logic.mk_of_sort
+ (TVar (("'" ^ x, i), []), Sign.defaultS thy')
+ else []) vars;
val T = etype_of thy' vs [] prop;
val (T', thw) = Type.legacy_freeze_thaw_type
(if T = nullT then nullT else map fastype_of vars' ---> T);
- val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
+ val t = map_types thw (read_term thy' T' s1);
val r' = freeze_thaw (condrew thy' eqns
- (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
+ (procs @ [typeof_proc [] vs, rlz_proc]))
(Const ("realizes", T --> propT --> propT) $
(if T = nullT then t else list_comb (t, vars')) $ prop);
- val r = fold_rev Logic.all (map (get_var_type r') vars) r';
+ val r = Logic.list_implies (shyps,
+ fold_rev Logic.all (map (get_var_type r') vars) r');
val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
in (name, (vs, (t, prf))) end
end;
@@ -337,10 +349,34 @@
val prop' = Pattern.rewrite_term thy'
(map (Logic.dest_equals o prop_of) defs) [] prop;
in freeze_thaw (condrew thy' eqns
- (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
+ (procs @ [typeof_proc [] vs, rlz_proc]))
(Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop')
end;
+fun abs_corr_shyps thy thm vs xs prf =
+ let
+ val S = Sign.defaultS thy;
+ val ((atyp_map, constraints, _), prop') =
+ Logic.unconstrainT (#shyps (rep_thm thm)) (prop_of thm);
+ val atyps = fold_types (fold_atyps (insert (op =))) (prop_of thm) [];
+ val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
+ SOME (TVar (("'" ^ v, i), [])) else NONE)
+ (rev (Term.add_vars prop' []));
+ val cs = maps (fn T => map (pair T) S) Ts;
+ val constraints' = map Logic.mk_of_class cs;
+ val cs' = rev (cs @ map (Logic.dest_of_class o snd) constraints);
+ fun typ_map T = Type.strip_sorts
+ (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
+ fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
+ val xs' = map (map_types typ_map) xs
+ in
+ prf |>
+ Same.commit (map_proof_same (map_types typ_map) typ_map mk_hyp) |>
+ fold_rev implies_intr_proof' (map snd constraints) |>
+ fold_rev forall_intr_proof' xs' |>
+ fold_rev implies_intr_proof' constraints'
+ end;
+
(** expanding theorems / definitions **)
fun add_expand_thm is_def thm thy =
@@ -354,15 +390,15 @@
thy |> ExtractionData.put
(if is_def then
{realizes_eqns = realizes_eqns,
- typeof_eqns = add_rule ([],
- Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
+ typeof_eqns = add_rule ([], Logic.dest_equals (map_types
+ Type.strip_sorts (prop_of (Drule.abs_def thm)))) typeof_eqns,
types = types,
realizers = realizers, defs = insert Thm.eq_thm thm defs,
expand = expand, prep = prep}
else
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
realizers = realizers, defs = defs,
- expand = insert (op =) (name, prop_of thm) expand, prep = prep})
+ expand = insert (op =) name expand, prep = prep})
end;
fun extraction_expand is_def =
@@ -443,9 +479,9 @@
ExtractionData.get thy;
val procs = maps (rev o fst o snd) types;
val rtypes = map fst types;
- val typroc = typeof_proc (Sign.defaultS thy');
+ val typroc = typeof_proc [];
val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o
- Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
+ Reconstruct.expand_proof thy' (map (rpair NONE) ("" :: expand));
val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
fun find_inst prop Ts ts vs =
@@ -464,6 +500,13 @@
in fold_rev add_args (take n vars ~~ take n ts) ([], []) end;
+ fun mk_shyps tye = maps (fn (ixn, _) =>
+ Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
+
+ fun mk_sprfs cs tye = maps (fn (_, T) =>
+ ProofRewriteRules.mk_of_sort_proof thy (map SOME cs)
+ (T, Sign.defaultS thy)) tye;
+
fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
@@ -474,22 +517,22 @@
fun realizes_null vs prop = app_rlz_rews [] vs
(Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
- fun corr d defs vs ts Ts hs (PBound i) _ _ = (defs, PBound i)
+ fun corr d defs vs ts Ts hs cs (PBound i) _ _ = (defs, PBound i)
- | corr d defs vs ts Ts hs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
+ | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
let val (defs', corr_prf) = corr d defs vs [] (T :: Ts)
- (dummyt :: hs) prf (incr_pboundvars 1 0 prf')
+ (dummyt :: hs) cs prf (incr_pboundvars 1 0 prf')
(case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
in (defs', Abst (s, SOME T, corr_prf)) end
- | corr d defs vs ts Ts hs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
+ | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
let
val T = etype_of thy' vs Ts prop;
val u = if T = nullT then
(case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
val (defs', corr_prf) = corr d defs vs [] (T :: Ts) (prop :: hs)
- (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
+ (prop :: cs) (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
val rlz = Const ("realizes", T --> propT --> propT)
in (defs',
if T = nullT then AbsP ("R",
@@ -500,10 +543,10 @@
(rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
end
- | corr d defs vs ts Ts hs (prf % SOME t) (prf' % _) t' =
+ | corr d defs vs ts Ts hs cs (prf % SOME t) (prf' % _) t' =
let
val (Us, T) = strip_type (fastype_of1 (Ts, t));
- val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf'
+ val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs cs prf prf'
(if member (op =) rtypes (tname_of T) then t'
else (case t' of SOME (u $ _) => SOME u | _ => NONE));
val u = if not (member (op =) rtypes (tname_of T)) then t else
@@ -519,7 +562,7 @@
in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
in (defs', corr_prf % SOME u) end
- | corr d defs vs ts Ts hs (prf1 %% prf2) (prf1' %% prf2') t =
+ | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =
let
val prop = Reconstruct.prop_of' hs prf2';
val T = etype_of thy' vs Ts prop;
@@ -529,17 +572,19 @@
| _ =>
let val (defs1, u) = extr d defs vs [] Ts hs prf2'
in (defs1, NONE, SOME u) end)
- val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs prf1 prf1' f;
- val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs prf2 prf2' u;
+ val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs cs prf1 prf1' f;
+ val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs cs prf2 prf2' u;
in
if T = nullT then (defs3, corr_prf1 %% corr_prf2) else
(defs3, corr_prf1 % u %% corr_prf2)
end
- | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
+ | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
let
val prf = join_proof body;
val (vs', tye) = find_inst prop Ts ts vs;
+ val shyps = mk_shyps tye;
+ val sprfs = mk_sprfs cs tye;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye;
val T = etype_of thy' vs' [] prop;
val defs' = if T = nullT then defs
@@ -555,28 +600,31 @@
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
- val (defs'', corr_prf) =
- corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
+ val (defs'', corr_prf0) = corr (d + 1) defs' vs' [] [] []
+ (rev shyps) prf' prf' NONE;
+ val corr_prf = mkabsp shyps corr_prf0;
val corr_prop = Reconstruct.prop_of corr_prf;
- val corr_prf' = List.foldr forall_intr_prf
- (proof_combt
+ val corr_prf' =
+ proof_combP (proof_combt
(PThm (serial (),
((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
- Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
- (map (get_var_type corr_prop) (vfs_of prop))
+ Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop),
+ map PBound (length shyps - 1 downto 0)) |>
+ fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
+ mkabsp shyps
in
((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
- prf_subst_TVars tye' corr_prf')
+ proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
end
- | SOME (_, (_, prf')) => (defs', prf_subst_TVars tye' prf'))
+ | SOME (_, (_, prf')) => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs)))
| SOME rs => (case find vs' rs of
- SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
+ SOME (_, prf') => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs))
| NONE => error ("corr: no realizer for instance of theorem " ^
quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Reconstruct.prop_of (proof_combt (prf0, ts))))))
end
- | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
+ | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
let
val (vs', tye) = find_inst prop Ts ts vs;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
@@ -584,13 +632,14 @@
if etype_of thy' vs' [] prop = nullT andalso
realizes_null vs' prop aconv prop then (defs, prf0)
else case find vs' (Symtab.lookup_list realizers s) of
- SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
+ SOME (_, prf) => (defs,
+ proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
| NONE => error ("corr: no realizer for instance of axiom " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Reconstruct.prop_of (proof_combt (prf0, ts)))))
end
- | corr d defs vs ts Ts hs _ _ _ = error "corr: bad proof"
+ | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof"
and extr d defs vs ts Ts hs (PBound i) = (defs, Bound i)
@@ -630,6 +679,7 @@
let
val prf = join_proof body;
val (vs', tye) = find_inst prop Ts ts vs;
+ val shyps = mk_shyps tye;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
case Symtab.lookup realizers s of
@@ -641,18 +691,18 @@
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
val (defs', t) = extr (d + 1) defs vs' [] [] [] prf';
- val (defs'', corr_prf) =
- corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
+ val (defs'', corr_prf) = corr (d + 1) defs' vs' [] [] []
+ (rev shyps) prf' prf' (SOME t);
val nt = Envir.beta_norm t;
val args = filter_out (fn v => member (op =) rtypes
(tname_of (body_type (fastype_of v)))) (vfs_of prop);
val args' = filter (fn v => Logic.occs (v, nt)) args;
- val t' = mkabs nt args';
+ val t' = mkabs args' nt;
val T = fastype_of t';
val cname = extr_name s vs';
val c = Const (cname, T);
- val u = mkabs (list_comb (c, args')) args;
+ val u = mkabs args (list_comb (c, args'));
val eqn = Logic.mk_equals (c, t');
val rlz =
Const ("realizes", fastype_of nt --> propT --> propT);
@@ -661,20 +711,22 @@
val f = app_rlz_rews [] vs'
(Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
- val corr_prf' =
- chtype [] equal_elim_axm %> lhs %> rhs %%
+ val corr_prf' = mkabsp shyps
+ (chtype [] equal_elim_axm %> lhs %> rhs %%
(chtype [propT] symmetric_axm %> rhs %> lhs %%
(chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
(chtype [T --> propT] reflexive_axm %> f) %%
PAxm (cname ^ "_def", eqn,
- SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf;
+ SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
val corr_prop = Reconstruct.prop_of corr_prf';
- val corr_prf'' = List.foldr forall_intr_prf
- (proof_combt
+ val corr_prf'' =
+ proof_combP (proof_combt
(PThm (serial (),
((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
- Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
- (map (get_var_type corr_prop) (vfs_of prop));
+ Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop),
+ map PBound (length shyps - 1 downto 0)) |>
+ fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
+ mkabsp shyps
in
((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
subst_TVars tye' u)
@@ -731,7 +783,7 @@
in
thy'
|> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
- Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
+ Thm.varifyT_global (funpow (length (vars_of corr_prop))
(Thm.forall_elim_var 0) (Thm.forall_intr_frees
(ProofChecker.thm_of_proof thy'
(fst (Proofterm.freeze_thaw_prf prf))))))
--- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Jun 01 17:52:19 2010 +0200
@@ -6,14 +6,17 @@
signature PROOF_REWRITE_RULES =
sig
- val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
+ val rew : bool -> typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
val rprocs : bool ->
- (typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
+ (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
+ val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
+ val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
+ (Proofterm.proof * Proofterm.proof) option
end;
structure ProofRewriteRules : PROOF_REWRITE_RULES =
@@ -21,7 +24,7 @@
open Proofterm;
-fun rew b _ =
+fun rew b _ _ =
let
fun ?? x = if b then SOME x else NONE;
fun ax (prf as PAxm (s, prop, _)) Ts =
@@ -219,31 +222,36 @@
fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
fun insert_refl defs Ts (prf1 %% prf2) =
- insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
+ let val (prf1', b) = insert_refl defs Ts prf1
+ in
+ if b then (prf1', true)
+ else (prf1' %% fst (insert_refl defs Ts prf2), false)
+ end
| insert_refl defs Ts (Abst (s, SOME T, prf)) =
- Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
+ (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
| insert_refl defs Ts (AbsP (s, t, prf)) =
- AbsP (s, t, insert_refl defs Ts prf)
+ (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
| insert_refl defs Ts prf = (case strip_combt prf of
(PThm (_, ((s, prop, SOME Ts), _)), ts) =>
if member (op =) defs s then
let
val vs = vars_of prop;
val tvars = Term.add_tvars prop [] |> rev;
- val (_, rhs) = Logic.dest_equals prop;
+ val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
(fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
map the ts);
in
- change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
+ (change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs', true)
end
- else prf
- | (_, []) => prf
- | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
+ else (prf, false)
+ | (_, []) => (prf, false)
+ | (prf', ts) => (proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
fun elim_defs thy r defs prf =
let
- val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
+ val defs' = map (Logic.dest_equals o
+ map_types Type.strip_sorts o prop_of o Drule.abs_def) defs;
val defnames = map Thm.derivation_name defs;
val f = if not r then I else
let
@@ -258,7 +266,7 @@
in Reconstruct.expand_proof thy thms end;
in
rewrite_terms (Pattern.rewrite_term thy defs' [])
- (insert_refl defnames [] (f prf))
+ (fst (insert_refl defnames [] (f prf)))
end;
@@ -327,4 +335,35 @@
mk_prf Q
end;
+
+(**** expand OfClass proofs ****)
+
+fun mk_of_sort_proof thy hs (T, S) =
+ let
+ val hs' = map
+ (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
+ | NONE => NONE) hs;
+ val sorts = AList.coalesce (op =) (rev (map_filter I hs'));
+ fun get_sort T = the_default [] (AList.lookup (op =) sorts T);
+ val subst = map_atyps
+ (fn T as TVar (ixn, _) => TVar (ixn, get_sort T)
+ | T as TFree (s, _) => TFree (s, get_sort T));
+ fun hyp T_c = case find_index (equal (SOME T_c)) hs' of
+ ~1 => error "expand_of_class: missing class hypothesis"
+ | i => PBound i;
+ fun reconstruct prf prop = prf |>
+ Reconstruct.reconstruct_proof thy prop |>
+ Reconstruct.expand_proof thy [("", NONE)] |>
+ Same.commit (map_proof_same Same.same Same.same hyp)
+ in
+ map2 reconstruct
+ (of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
+ (Logic.mk_of_sort (T, S))
+ end;
+
+fun expand_of_class thy Ts hs (OfClass (T, c)) =
+ mk_of_sort_proof thy hs (T, [c]) |>
+ hd |> rpair no_skel |> SOME
+ | expand_of_class thy Ts hs _ = NONE;
+
end;
--- a/src/Pure/Proof/proof_syntax.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Jun 01 17:52:19 2010 +0200
@@ -11,8 +11,9 @@
val proof_of_term: theory -> bool -> term -> Proofterm.proof
val term_of_proof: Proofterm.proof -> term
val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
- val read_term: theory -> typ -> string -> term
- val read_proof: theory -> bool -> string -> Proofterm.proof
+ val strip_sorts_consttypes: Proof.context -> Proof.context
+ val read_term: theory -> bool -> typ -> string -> term
+ val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
val proof_syntax: Proofterm.proof -> theory -> theory
val proof_of: bool -> thm -> Proofterm.proof
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
@@ -109,7 +110,7 @@
| "thm" :: xs =>
let val name = Long_Name.implode xs;
in (case AList.lookup (op =) thms name of
- SOME thm => fst (strip_combt (Thm.proof_of thm))
+ SOME thm => fst (strip_combt (fst (strip_combP (Thm.proof_of thm))))
| NONE => error ("Unknown theorem " ^ quote name))
end
| _ => error ("Illegal proof constant name: " ^ quote s))
@@ -198,7 +199,14 @@
(cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
end;
-fun read_term thy =
+fun strip_sorts_consttypes ctxt =
+ let val {constants = (_, tab), ...} = Consts.dest (ProofContext.consts_of ctxt)
+ in Symtab.fold (fn (s, (T, _)) =>
+ ProofContext.add_const_constraint (s, SOME (Type.strip_sorts T)))
+ tab ctxt
+ end;
+
+fun read_term thy topsort =
let
val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy));
val axm_names = map fst (Theory.all_axioms_of thy);
@@ -208,15 +216,19 @@
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
|> ProofContext.init_global
|> ProofContext.allow_dummies
- |> ProofContext.set_mode ProofContext.mode_schematic;
+ |> ProofContext.set_mode ProofContext.mode_schematic
+ |> (if topsort then
+ strip_sorts_consttypes #>
+ ProofContext.set_defsort []
+ else I);
in
fn ty => fn s =>
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
|> Type_Infer.constrain ty |> Syntax.check_term ctxt
end;
-fun read_proof thy =
- let val rd = read_term thy proofT
+fun read_proof thy topsort =
+ let val rd = read_term thy topsort proofT
in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end;
fun proof_syntax prf =
--- a/src/Pure/Proof/proofchecker.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Proof/proofchecker.ML Tue Jun 01 17:52:19 2010 +0200
@@ -28,6 +28,48 @@
val beta_eta_convert =
Conv.fconv_rule Drule.beta_eta_conversion;
+(* equality modulo renaming of type variables *)
+fun is_equal t t' =
+ let
+ val atoms = fold_types (fold_atyps (insert (op =))) t [];
+ val atoms' = fold_types (fold_atyps (insert (op =))) t' []
+ in
+ length atoms = length atoms' andalso
+ map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
+ end;
+
+fun pretty_prf thy vs Hs prf =
+ let val prf' = prf |> prf_subst_bounds (map Free vs) |>
+ prf_subst_pbounds (map (Hyp o prop_of) Hs)
+ in
+ (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
+ Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
+ end;
+
+fun pretty_term thy vs _ t =
+ let val t' = subst_bounds (map Free vs, t)
+ in
+ (Syntax.pretty_term_global thy t',
+ Syntax.pretty_typ_global thy (fastype_of t'))
+ end;
+
+fun appl_error thy prt vs Hs s f a =
+ let
+ val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
+ val (pp_a, pp_aT) = prt thy vs Hs a
+ in
+ error (cat_lines
+ [s,
+ "",
+ Pretty.string_of (Pretty.block
+ [Pretty.str "Operator:", Pretty.brk 2, pp_f,
+ Pretty.str " ::", Pretty.brk 1, pp_fT]),
+ Pretty.string_of (Pretty.block
+ [Pretty.str "Operand:", Pretty.brk 3, pp_a,
+ Pretty.str " ::", Pretty.brk 1, pp_aT]),
+ ""])
+ end;
+
fun thm_of_proof thy prf =
let
val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
@@ -45,9 +87,9 @@
fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
let
- val thm = Drule.implies_intr_hyps (lookup name);
+ val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
val {prop, ...} = rep_thm thm;
- val _ = if prop aconv prop' then () else
+ val _ = if is_equal prop prop' then () else
error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
Syntax.string_of_term_global thy prop ^ "\n\n" ^
Syntax.string_of_term_global thy prop');
@@ -70,7 +112,10 @@
let
val thm = thm_of (vs, names) Hs prf;
val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
- in Thm.forall_elim ct thm end
+ in
+ Thm.forall_elim ct thm
+ handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
+ end
| thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
let
@@ -86,6 +131,7 @@
val thm' = beta_eta_convert (thm_of vars Hs prf');
in
Thm.implies_elim thm thm'
+ handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
end
| thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
--- a/src/Pure/Proof/reconstruct.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Jun 01 17:52:19 2010 +0200
@@ -28,11 +28,7 @@
fun forall_intr_vfs prop = fold_rev Logic.all
(vars_of prop @ frees_of prop) prop;
-fun forall_intr_prf t prf =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in Abst (a, SOME T, prf_abstract_over t prf) end;
-
-fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
+fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof'
(vars_of prop @ frees_of prop) prf;
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Tue Jun 01 17:52:19 2010 +0200
@@ -80,7 +80,7 @@
NONE => (NONE, NONE)
| SOME fname =>
let val path = Path.explode fname in
- case ThyLoad.check_file Path.current path of
+ case Thy_Load.check_file Path.current path of
SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
| NONE => (NONE, SOME fname)
end);
--- a/src/Pure/ProofGeneral/pgip_parser.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Tue Jun 01 17:52:19 2010 +0200
@@ -91,18 +91,18 @@
fun parse_span span =
let
- val kind = ThySyntax.span_kind span;
- val toks = ThySyntax.span_content span;
- val text = implode (map (Print_Mode.setmp [] ThySyntax.present_token) toks);
+ val kind = Thy_Syntax.span_kind span;
+ val toks = Thy_Syntax.span_content span;
+ val text = implode (map (Print_Mode.setmp [] Thy_Syntax.present_token) toks);
in
(case kind of
- ThySyntax.Command name => parse_command name text
- | ThySyntax.Ignored => [D.Whitespace {text = text}]
- | ThySyntax.Malformed => [D.Unparseable {text = text}])
+ Thy_Syntax.Command name => parse_command name text
+ | Thy_Syntax.Ignored => [D.Whitespace {text = text}]
+ | Thy_Syntax.Malformed => [D.Unparseable {text = text}])
end;
fun pgip_parser pos str =
- maps parse_span (ThySyntax.parse_spans (Keyword.get_lexicons ()) pos str);
+ maps parse_span (Thy_Syntax.parse_spans (Keyword.get_lexicons ()) pos str);
end;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Jun 01 17:52:19 2010 +0200
@@ -113,15 +113,15 @@
local
fun trace_action action name =
- if action = ThyInfo.Update then
- List.app tell_file_loaded (ThyInfo.loaded_files name)
- else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
- List.app tell_file_retracted (ThyInfo.loaded_files name)
+ if action = Thy_Info.Update then
+ List.app tell_file_loaded (Thy_Info.loaded_files name)
+ else if action = Thy_Info.Outdate orelse action = Thy_Info.Remove then
+ List.app tell_file_retracted (Thy_Info.loaded_files name)
else ();
in
- fun setup_thy_loader () = ThyInfo.add_hook trace_action;
- fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
+ fun setup_thy_loader () = Thy_Info.add_hook trace_action;
+ fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
end;
@@ -130,19 +130,19 @@
(*liberal low-level version*)
val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
-val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
+val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
fun inform_file_processed file =
let
val name = thy_name file;
val _ = name = "" andalso error ("Bad file name: " ^ quote file);
val _ =
- if ThyInfo.check_known_thy name then
+ if Thy_Info.check_known_thy name then
(Isar.>> (Toplevel.commit_exit Position.none);
- ThyInfo.touch_child_thys name; ThyInfo.register_thy name)
+ Thy_Info.touch_child_thys name; Thy_Info.register_thy name)
handle ERROR msg =>
(warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
- tell_file_retracted (ThyLoad.thy_path name))
+ tell_file_retracted (Thy_Load.thy_path name))
else ();
val _ = Isar.init ();
in () end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jun 01 17:52:19 2010 +0200
@@ -198,18 +198,18 @@
operations).
*)
fun trace_action action name =
- if action = ThyInfo.Update then
- List.app (tell_file_loaded true) (ThyInfo.loaded_files name)
- else if action = ThyInfo.Outdate then
- List.app (tell_file_outdated true) (ThyInfo.loaded_files name)
- else if action = ThyInfo.Remove then
- List.app (tell_file_retracted true) (ThyInfo.loaded_files name)
+ if action = Thy_Info.Update then
+ List.app (tell_file_loaded true) (Thy_Info.loaded_files name)
+ else if action = Thy_Info.Outdate then
+ List.app (tell_file_outdated true) (Thy_Info.loaded_files name)
+ else if action = Thy_Info.Remove then
+ List.app (tell_file_retracted true) (Thy_Info.loaded_files name)
else ()
in
- fun setup_thy_loader () = ThyInfo.add_hook trace_action;
- fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
+ fun setup_thy_loader () = Thy_Info.add_hook trace_action;
+ fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
end;
@@ -217,14 +217,14 @@
val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
-val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
-val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
+val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
+val inform_file_processed = Thy_Info.if_known_thy Thy_Info.touch_child_thys o thy_name;
fun proper_inform_file_processed path state =
let val name = thy_name path in
- if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
- (ThyInfo.touch_child_thys name;
- ThyInfo.register_thy name handle ERROR msg =>
+ if Toplevel.is_toplevel state andalso Thy_Info.known_thy name then
+ (Thy_Info.touch_child_thys name;
+ Thy_Info.register_thy name handle ERROR msg =>
(warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
tell_file_retracted true (Path.base path)))
else raise Toplevel.UNDEF
@@ -522,7 +522,7 @@
local
fun theory_facts name =
- let val thy = ThyInfo.get_theory name
+ let val thy = Thy_Info.get_theory name
in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
@@ -556,13 +556,13 @@
in
case (thyname,objtype) of
(NONE, NONE) =>
- setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
+ setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*)
| (NONE, SOME ObjFile) =>
- setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
+ setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*)
| (SOME fi, SOME ObjFile) =>
setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *)
| (NONE, SOME ObjTheory) =>
- setids (idtable ObjTheory NONE (ThyInfo.get_names()))
+ setids (idtable ObjTheory NONE (Thy_Info.get_names()))
| (SOME thy, SOME ObjTheory) =>
setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
| (SOME thy, SOME ObjTheorem) =>
@@ -571,9 +571,9 @@
(* A large query, but not unreasonable. ~5000 results for HOL.*)
(* Several setids should be allowed, but Eclipse code is currently broken:
List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
- (ThyInfo.get_names()) *)
+ (Thy_Info.get_names()) *)
setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
- (maps qualified_thms_of_thy (ThyInfo.get_names())))
+ (maps qualified_thms_of_thy (Thy_Info.get_names())))
| _ => warning ("askids: ignored argument combination")
end
@@ -592,14 +592,14 @@
fun filerefs f =
let val thy = thy_name f
- val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
+ val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy)
in
issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
name=NONE, idtables=[], fileurls=filerefs})
end
fun thyrefs thy =
- let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
+ let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy)
in
issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
@@ -642,7 +642,7 @@
fun splitthy id =
let val comps = Long_Name.explode id
in case comps of
- (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
+ (thy::(rest as _::_)) => (Thy_Info.get_theory thy, space_implode "." rest)
| [plainid] => (topthy(),plainid)
| _ => raise Toplevel.UNDEF (* assert false *)
end
@@ -659,8 +659,8 @@
val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
in
case (thyname, objtype) of
- (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
- | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
+ (_, ObjTheory) => idvalue [string_of_thy (Thy_Info.get_theory name)]
+ | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (Thy_Info.get_theory thy, name))
| (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
| (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
end
@@ -785,8 +785,8 @@
in
(case (!current_working_dir) of
NONE => ()
- | SOME dir => ThyLoad.del_path dir;
- ThyLoad.add_path newdir;
+ | SOME dir => Thy_Load.del_path dir;
+ Thy_Load.add_path newdir;
current_working_dir := SOME newdir)
end
end
@@ -806,7 +806,7 @@
val filedir = Path.dir filepath
val thy_name = Path.implode o #1 o Path.split_ext o Path.base
val openfile_retract = Output.no_warnings_CRITICAL
- (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
+ (Thy_Info.if_known_thy Thy_Info.remove_thy) o thy_name;
in
case !currently_open_file of
SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
@@ -856,7 +856,7 @@
(* TODO: next should be in thy loader, here just for testing *)
let
val name = thy_name url
- in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
+ in List.app (tell_file_retracted false) (Thy_Info.loaded_files name) end;
inform_file_retracted url)
end
--- a/src/Pure/ROOT.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/ROOT.ML Tue Jun 01 17:52:19 2010 +0200
@@ -299,18 +299,17 @@
struct
structure OuterKeyword = Keyword;
-
-structure OuterLex =
-struct
- open Token;
- type token = T;
-end;
-
+structure OuterLex = struct open Token type token = T end;
structure OuterParse = Parse;
structure OuterSyntax = Outer_Syntax;
+structure PrintMode = Print_Mode;
structure SpecParse = Parse_Spec;
+structure ThyInfo = Thy_Info;
+structure ThyOutput = Thy_Output;
structure TypeInfer = Type_Infer;
-structure PrintMode = Print_Mode;
end;
+structure ThyLoad = Thy_Load; (*Proof General legacy*)
+
+
--- a/src/Pure/Syntax/mixfix.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Syntax/mixfix.ML Tue Jun 01 17:52:19 2010 +0200
@@ -31,8 +31,8 @@
signature MIXFIX =
sig
include MIXFIX1
- val syn_ext_types: (string * typ * mixfix) list -> SynExt.syn_ext
- val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
+ val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext
+ val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext
end;
structure Mixfix: MIXFIX =
@@ -83,11 +83,11 @@
(* syntax specifications *)
fun mixfix_args NoSyn = 0
- | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
- | mixfix_args (Delimfix sy) = SynExt.mfix_args sy
- | mixfix_args (Infix (sy, _)) = 2 + SynExt.mfix_args sy
- | mixfix_args (Infixl (sy, _)) = 2 + SynExt.mfix_args sy
- | mixfix_args (Infixr (sy, _)) = 2 + SynExt.mfix_args sy
+ | mixfix_args (Mixfix (sy, _, _)) = Syn_Ext.mfix_args sy
+ | mixfix_args (Delimfix sy) = Syn_Ext.mfix_args sy
+ | mixfix_args (Infix (sy, _)) = 2 + Syn_Ext.mfix_args sy
+ | mixfix_args (Infixl (sy, _)) = 2 + Syn_Ext.mfix_args sy
+ | mixfix_args (Infixr (sy, _)) = 2 + Syn_Ext.mfix_args sy
| mixfix_args (Binder _) = 1
| mixfix_args Structure = 0;
@@ -97,29 +97,29 @@
(* syn_ext_types *)
-fun make_type n = replicate n SynExt.typeT ---> SynExt.typeT;
+fun make_type n = replicate n Syn_Ext.typeT ---> Syn_Ext.typeT;
fun syn_ext_types type_decls =
let
- fun mk_infix sy ty t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
+ fun mk_infix sy ty t p1 p2 p3 = Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
fun mfix_of (_, _, NoSyn) = NONE
- | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, ty, t, ps, p))
- | mfix_of (t, ty, Delimfix sy) = SOME (SynExt.Mfix (sy, ty, t, [], SynExt.max_pri))
+ | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syn_Ext.Mfix (sy, ty, t, ps, p))
+ | mfix_of (t, ty, Delimfix sy) = SOME (Syn_Ext.Mfix (sy, ty, t, [], Syn_Ext.max_pri))
| mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
| mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
| mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
| mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); (* FIXME printable t (!?) *)
- fun check_args (_, ty, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
- if length (Term.binder_types ty) = SynExt.mfix_args sy then ()
- else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix
+ fun check_args (_, ty, _) (SOME (mfix as Syn_Ext.Mfix (sy, _, _, _, _))) =
+ if length (Term.binder_types ty) = Syn_Ext.mfix_args sy then ()
+ else Syn_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
| check_args _ NONE = ();
val mfix = map mfix_of type_decls;
val _ = map2 check_args type_decls mfix;
val xconsts = map #1 type_decls;
- in SynExt.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end;
+ in Syn_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end;
(* syn_ext_consts *)
@@ -130,21 +130,21 @@
fun syn_ext_consts is_logtype const_decls =
let
fun mk_infix sy ty c p1 p2 p3 =
- [SynExt.Mfix ("op " ^ sy, ty, c, [], SynExt.max_pri),
- SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
+ [Syn_Ext.Mfix ("op " ^ sy, ty, c, [], Syn_Ext.max_pri),
+ Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
[Type ("idts", []), ty2] ---> ty3
| binder_typ c _ = error ("Bad type of binder: " ^ quote c);
fun mfix_of (_, _, NoSyn) = []
- | mfix_of (c, ty, Mixfix (sy, ps, p)) = [SynExt.Mfix (sy, ty, c, ps, p)]
- | mfix_of (c, ty, Delimfix sy) = [SynExt.Mfix (sy, ty, c, [], SynExt.max_pri)]
+ | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syn_Ext.Mfix (sy, ty, c, ps, p)]
+ | mfix_of (c, ty, Delimfix sy) = [Syn_Ext.Mfix (sy, ty, c, [], Syn_Ext.max_pri)]
| mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
| mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
| mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
| mfix_of (c, ty, Binder (sy, p, q)) =
- [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
+ [Syn_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
| mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); (* FIXME printable c (!?) *)
fun binder (c, _, Binder _) = SOME (binder_name c, c)
@@ -154,12 +154,12 @@
val xconsts = map #1 const_decls;
val binders = map_filter binder const_decls;
val binder_trs = binders
- |> map (SynExt.stamp_trfun binder_stamp o apsnd K o SynTrans.mk_binder_tr);
+ |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syn_Trans.mk_binder_tr);
val binder_trs' = binders
- |> map (SynExt.stamp_trfun binder_stamp o
- apsnd (K o SynTrans.non_typed_tr') o SynTrans.mk_binder_tr' o swap);
+ |> map (Syn_Ext.stamp_trfun binder_stamp o
+ apsnd (K o Syn_Trans.non_typed_tr') o Syn_Trans.mk_binder_tr' o swap);
in
- SynExt.syn_ext' true is_logtype
+ Syn_Ext.syn_ext' true is_logtype
mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
end;
--- a/src/Pure/Syntax/parser.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Syntax/parser.ML Tue Jun 01 17:52:19 2010 +0200
@@ -8,8 +8,8 @@
sig
type gram
val empty_gram: gram
- val extend_gram: gram -> SynExt.xprod list -> gram
- val make_gram: SynExt.xprod list -> gram
+ val extend_gram: gram -> Syn_Ext.xprod list -> gram
+ val make_gram: Syn_Ext.xprod list -> gram
val merge_grams: gram -> gram -> gram
val pretty_gram: gram -> Pretty.T list
datatype parsetree =
@@ -23,7 +23,7 @@
structure Parser: PARSER =
struct
-open Lexicon SynExt;
+open Lexicon Syn_Ext;
(** datatype gram **)
--- a/src/Pure/Syntax/printer.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Syntax/printer.ML Tue Jun 01 17:52:19 2010 +0200
@@ -26,8 +26,8 @@
(string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
type prtabs
val empty_prtabs: prtabs
- val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
- val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
+ val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
+ val remove_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
val merge_prtabs: prtabs -> prtabs -> prtabs
val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
@@ -101,8 +101,8 @@
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
in ast_of tm end;
-fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (TypeExt.term_of_sort S);
-fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (TypeExt.term_of_typ (! show_sorts) T);
+fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
+fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (Type_Ext.term_of_typ (! show_sorts) T);
@@ -114,7 +114,7 @@
val {structs, fixes} = idents;
fun mark_atoms ((t as Const (c, T)) $ u) =
- if member (op =) SynExt.standard_token_markers c
+ if member (op =) Syn_Ext.standard_token_markers c
then t $ u else mark_atoms t $ mark_atoms u
| mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
| mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
@@ -130,7 +130,7 @@
else Lexicon.const "_free" $ t
end
| mark_atoms (t as Var (xi, T)) =
- if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
+ if xi = Syn_Ext.dddot_indexname then Const ("_DDDOT", T)
else Lexicon.const "_var" $ t
| mark_atoms a = a;
@@ -155,7 +155,7 @@
fun ast_of tm =
(case strip_comb tm of
- (t as Abs _, ts) => Ast.mk_appl (ast_of (SynTrans.abs_tr' t)) (map ast_of ts)
+ (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' t)) (map ast_of ts)
| ((c as Const ("_free", _)), Free (x, T) :: ts) =>
Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
| ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
@@ -176,12 +176,12 @@
and constrain t T =
if show_types andalso T <> dummyT then
- Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
- ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
+ Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of t,
+ ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
else simple_ast_of t;
in
tm
- |> SynTrans.prop_tr'
+ |> Syn_Trans.prop_tr'
|> show_types ? (#1 o prune_typs o rpair [])
|> mark_atoms
|> ast_of
@@ -211,29 +211,29 @@
(* xprod_to_fmt *)
-fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = NONE
- | xprod_to_fmt (SynExt.XProd (_, xsymbs, const, pri)) =
+fun xprod_to_fmt (Syn_Ext.XProd (_, _, "", _)) = NONE
+ | xprod_to_fmt (Syn_Ext.XProd (_, xsymbs, const, pri)) =
let
fun arg (s, p) =
(if s = "type" then TypArg else Arg)
- (if Lexicon.is_terminal s then SynExt.max_pri else p);
+ (if Lexicon.is_terminal s then Syn_Ext.max_pri else p);
- fun xsyms_to_syms (SynExt.Delim s :: xsyms) =
+ fun xsyms_to_syms (Syn_Ext.Delim s :: xsyms) =
apfst (cons (String s)) (xsyms_to_syms xsyms)
- | xsyms_to_syms (SynExt.Argument s_p :: xsyms) =
+ | xsyms_to_syms (Syn_Ext.Argument s_p :: xsyms) =
apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
- | xsyms_to_syms (SynExt.Space s :: xsyms) =
+ | xsyms_to_syms (Syn_Ext.Space s :: xsyms) =
apfst (cons (Space s)) (xsyms_to_syms xsyms)
- | xsyms_to_syms (SynExt.Bg i :: xsyms) =
+ | xsyms_to_syms (Syn_Ext.Bg i :: xsyms) =
let
val (bsyms, xsyms') = xsyms_to_syms xsyms;
val (syms, xsyms'') = xsyms_to_syms xsyms';
in
(Block (i, bsyms) :: syms, xsyms'')
end
- | xsyms_to_syms (SynExt.Brk i :: xsyms) =
+ | xsyms_to_syms (Syn_Ext.Brk i :: xsyms) =
apfst (cons (Break i)) (xsyms_to_syms xsyms)
- | xsyms_to_syms (SynExt.En :: xsyms) = ([], xsyms)
+ | xsyms_to_syms (Syn_Ext.En :: xsyms) = ([], xsyms)
| xsyms_to_syms [] = ([], []);
fun nargs (Arg _ :: syms) = nargs syms + 1
@@ -263,7 +263,7 @@
fun remove_prtabs mode xprods prtabs =
let
val tab = mode_tab prtabs mode;
- val fmts = map_filter (fn xprod as SynExt.XProd (_, _, c, _) =>
+ val fmts = map_filter (fn xprod as Syn_Ext.XProd (_, _, c, _) =>
if null (Symtab.lookup_list tab c) then NONE
else xprod_to_fmt xprod) xprods;
val tab' = fold (Symtab.remove_list (op =)) fmts tab;
@@ -290,15 +290,15 @@
fun token_trans a x =
(case tokentrf a of
NONE =>
- if member (op =) SynExt.standard_token_classes a
+ if member (op =) Syn_Ext.standard_token_classes a
then SOME (Pretty.str x) else NONE
| SOME f => SOME (f ctxt x));
(*default applications: prefix / postfix*)
val appT =
- if type_mode then TypeExt.tappl_ast_tr'
- else if curried then SynTrans.applC_ast_tr'
- else SynTrans.appl_ast_tr';
+ if type_mode then Type_Ext.tappl_ast_tr'
+ else if curried then Syn_Trans.applC_ast_tr'
+ else Syn_Trans.appl_ast_tr';
fun synT _ ([], args) = ([], args)
| synT markup (Arg p :: symbs, t :: args) =
@@ -333,7 +333,7 @@
and parT markup (pr, args, p, p': int) = #1 (synT markup
(if p > p' orelse
- (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr))
+ (! show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
then [Block (1, Space "(" :: pr @ [Space ")"])]
else pr, args))
--- a/src/Pure/Syntax/syn_ext.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Syntax/syn_ext.ML Tue Jun 01 17:52:19 2010 +0200
@@ -41,7 +41,7 @@
val chain_pri: int
val delims_of: xprod list -> string list list
datatype syn_ext =
- SynExt of {
+ Syn_Ext of {
xprods: xprod list,
consts: string list,
prmodes: string list,
@@ -86,7 +86,7 @@
val pure_ext: syn_ext
end;
-structure SynExt: SYN_EXT =
+structure Syn_Ext: SYN_EXT =
struct
@@ -326,7 +326,7 @@
(** datatype syn_ext **)
datatype syn_ext =
- SynExt of {
+ Syn_Ext of {
xprods: xprod list,
consts: string list,
prmodes: string list,
@@ -352,7 +352,7 @@
val mfix_consts =
distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
in
- SynExt {
+ Syn_Ext {
xprods = xprods,
consts = union (op =) consts mfix_consts,
prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
--- a/src/Pure/Syntax/syn_trans.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Tue Jun 01 17:52:19 2010 +0200
@@ -60,7 +60,7 @@
(string -> (Proof.context -> term list -> term) option) -> Ast.ast list -> term list
end;
-structure SynTrans: SYN_TRANS =
+structure Syn_Trans: SYN_TRANS =
struct
@@ -166,7 +166,7 @@
(* dddot *)
-fun dddot_tr (*"_DDDOT"*) ts = Term.list_comb (Lexicon.var SynExt.dddot_indexname, ts);
+fun dddot_tr (*"_DDDOT"*) ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts);
(* quote / antiquote *)
@@ -354,9 +354,9 @@
(* type propositions *)
fun type_prop_tr' _ (*"_type_prop"*) T [Const ("\\<^const>Pure.sort_constraint", _)] =
- Lexicon.const "_sort_constraint" $ TypeExt.term_of_typ true T
+ Lexicon.const "_sort_constraint" $ Type_Ext.term_of_typ true T
| type_prop_tr' show_sorts (*"_type_prop"*) T [t] =
- Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t
+ Lexicon.const "_ofclass" $ Type_Ext.term_of_typ show_sorts T $ t
| type_prop_tr' _ (*"_type_prop"*) T ts = raise TYPE ("type_prop_tr'", [T], ts);
@@ -394,7 +394,7 @@
(* meta implication *)
fun impl_ast_tr' (*"==>"*) asts =
- if TypeExt.no_brackets () then raise Match
+ if Type_Ext.no_brackets () then raise Match
else
(case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
(prems as _ :: _ :: _, concl) =>
@@ -408,14 +408,14 @@
(* type reflection *)
fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
- Term.list_comb (Lexicon.const "_TYPE" $ TypeExt.term_of_typ show_sorts T, ts)
+ Term.list_comb (Lexicon.const "_TYPE" $ Type_Ext.term_of_typ show_sorts T, ts)
| type_tr' _ _ _ = raise Match;
(* type constraints *)
fun type_constraint_tr' show_sorts (*"_type_constraint_"*) (Type ("fun", [T, _])) (t :: ts) =
- Term.list_comb (Lexicon.const SynExt.constrainC $ t $ TypeExt.term_of_typ show_sorts T, ts)
+ Term.list_comb (Lexicon.const Syn_Ext.constrainC $ t $ Type_Ext.term_of_typ show_sorts T, ts)
| type_constraint_tr' _ _ _ = raise Match;
--- a/src/Pure/Syntax/syntax.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Tue Jun 01 17:52:19 2010 +0200
@@ -168,21 +168,21 @@
fun err_dup_trfun name c =
error ("More than one " ^ name ^ " for " ^ quote c);
-fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
+fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns;
fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
handle Symtab.DUP c => err_dup_trfun name c;
-fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
+fun merge_trtabs name tab1 tab2 = Symtab.merge Syn_Ext.eq_trfun (tab1, tab2)
handle Symtab.DUP c => err_dup_trfun name c;
(* print (ast) translations *)
fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
-fun update_tr'tab trfuns = fold_rev (Symtab.update_list SynExt.eq_trfun) trfuns;
-fun remove_tr'tab trfuns = fold (Symtab.remove_list SynExt.eq_trfun) trfuns;
-fun merge_tr'tabs tab1 tab2 = Symtab.merge_list SynExt.eq_trfun (tab1, tab2);
+fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
+fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
+fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
@@ -239,7 +239,7 @@
datatype syntax =
Syntax of {
- input: SynExt.xprod list,
+ input: Syn_Ext.xprod list,
lexicon: Scan.lexicon,
gram: Parser.gram,
consts: string list,
@@ -287,7 +287,7 @@
val {input, lexicon, gram, consts = consts1, prmodes = prmodes1,
parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
print_ast_trtab, tokentrtab, prtabs} = tabs;
- val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2,
+ val Syn_Ext.Syn_Ext {xprods, consts = consts2, prmodes = prmodes2,
parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
print_ast_translation, token_translation} = syn_ext;
val new_xprods =
@@ -296,7 +296,7 @@
in
Syntax
({input = new_xprods @ input,
- lexicon = fold Scan.extend_lexicon (SynExt.delims_of new_xprods) lexicon,
+ lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
gram = Parser.extend_gram gram new_xprods,
consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
@@ -316,7 +316,7 @@
fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
let
- val SynExt.SynExt {xprods, consts = _, prmodes = _,
+ val Syn_Ext.Syn_Ext {xprods, consts = _, prmodes = _,
parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
print_ast_translation, token_translation = _} = syn_ext;
val {input, lexicon, gram, consts, prmodes,
@@ -328,7 +328,7 @@
in
Syntax
({input = input',
- lexicon = if changed then Scan.make_lexicon (SynExt.delims_of input') else lexicon,
+ lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon,
gram = if changed then Parser.make_gram input' else gram,
consts = consts,
prmodes = prmodes,
@@ -381,13 +381,13 @@
val basic_syntax =
empty_syntax
- |> update_syntax mode_default TypeExt.type_ext
- |> update_syntax mode_default SynExt.pure_ext;
+ |> update_syntax mode_default Type_Ext.type_ext
+ |> update_syntax mode_default Syn_Ext.pure_ext;
val basic_nonterms =
- (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
- SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
- "asms", SynExt.any, SynExt.sprop, "num_const", "float_const",
+ (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
+ Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
+ "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
"index", "struct"]);
@@ -481,13 +481,13 @@
val toks = Lexicon.tokenize lexicon xids syms;
val _ = List.app Lexicon.report_token toks;
- val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
+ val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
val len = length pts;
val limit = ! ambiguity_limit;
fun show_pt pt =
- Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
+ Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
in
if len <= ! ambiguity_level then ()
else if ! ambiguity_is_error then error (ambiguity_msg pos)
@@ -497,7 +497,7 @@
"\nproduces " ^ string_of_int len ^ " parse trees" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
map show_pt (take limit pts))));
- SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
+ Syn_Trans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
end;
@@ -506,9 +506,9 @@
fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty inp =
let
val {parse_ruletab, parse_trtab, ...} = tabs;
- val asts = read_asts ctxt is_logtype syn false (SynExt.typ_to_nonterm ty) inp;
+ val asts = read_asts ctxt is_logtype syn false (Syn_Ext.typ_to_nonterm ty) inp;
in
- SynTrans.asts_to_terms ctxt (lookup_tr parse_trtab)
+ Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
(map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
end;
@@ -547,23 +547,23 @@
fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
read ctxt is_logtype syn ty (syms, pos)
- |> map (TypeExt.decode_term get_sort map_const map_free)
+ |> map (Type_Ext.decode_term get_sort map_const map_free)
|> disambig (Printer.pp_show_brackets pp) check;
(* read types *)
fun standard_parse_typ ctxt syn get_sort (syms, pos) =
- (case read ctxt (K false) syn SynExt.typeT (syms, pos) of
- [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts t)) t
+ (case read ctxt (K false) syn Syn_Ext.typeT (syms, pos) of
+ [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
| _ => error (ambiguity_msg pos));
(* read sorts *)
fun standard_parse_sort ctxt syn (syms, pos) =
- (case read ctxt (K false) syn TypeExt.sortT (syms, pos) of
- [t] => TypeExt.sort_of_term t
+ (case read ctxt (K false) syn Type_Ext.sortT (syms, pos) of
+ [t] => Type_Ext.sort_of_term t
| _ => error (ambiguity_msg pos));
@@ -666,9 +666,9 @@
fun ext_syntax f decls = update_syntax mode_default (f decls);
-val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
-val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
-val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
+val update_trfuns = ext_syntax Syn_Ext.syn_ext_trfuns;
+val update_advanced_trfuns = ext_syntax Syn_Ext.syn_ext_advanced_trfuns;
+val extend_tokentrfuns = ext_syntax Syn_Ext.syn_ext_tokentrfuns;
fun update_type_gram add prmode decls =
(if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
@@ -677,13 +677,13 @@
(if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
fun update_trrules ctxt is_logtype syn =
- ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
+ ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
fun remove_trrules ctxt is_logtype syn =
- remove_syntax mode_default o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
+ remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
-val update_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules;
-val remove_trrules_i = remove_syntax mode_default o SynExt.syn_ext_rules o cert_rules;
+val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
+val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
@@ -798,7 +798,7 @@
val check_typs = gen_check fst false;
val check_terms = gen_check snd false;
-fun check_props ctxt = map (TypeExt.type_constraint propT) #> check_terms ctxt;
+fun check_props ctxt = map (Type_Ext.type_constraint propT) #> check_terms ctxt;
val check_typ = singleton o check_typs;
val check_term = singleton o check_terms;
@@ -905,7 +905,7 @@
(*export parts of internal Syntax structures*)
-open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
+open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;
end;
@@ -913,9 +913,9 @@
open Basic_Syntax;
forget_structure "Ast";
-forget_structure "SynExt";
+forget_structure "Syn_Ext";
forget_structure "Parser";
-forget_structure "TypeExt";
-forget_structure "SynTrans";
+forget_structure "Type_Ext";
+forget_structure "Syn_Trans";
forget_structure "Mixfix";
forget_structure "Printer";
--- a/src/Pure/Syntax/type_ext.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Syntax/type_ext.ML Tue Jun 01 17:52:19 2010 +0200
@@ -27,10 +27,10 @@
val term_of_sort: sort -> term
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val sortT: typ
- val type_ext: SynExt.syn_ext
+ val type_ext: Syn_Ext.syn_ext
end;
-structure TypeExt: TYPE_EXT =
+structure Type_Ext: TYPE_EXT =
struct
(** input utils **)
@@ -242,7 +242,7 @@
val classesT = Type ("classes", []);
val typesT = Type ("types", []);
-local open Lexicon SynExt in
+local open Lexicon Syn_Ext in
val type_ext = syn_ext' false (K false)
[Mfix ("_", tidT --> typeT, "", [], max_pri),
@@ -271,7 +271,7 @@
Mfix ("'(_')", typeT --> typeT, "", [0], max_pri),
Mfix ("'_", typeT, "\\<^type>dummy", [], max_pri)]
["_type_prop"]
- ([], [], [], map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
+ ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
[]
([], []);
--- a/src/Pure/System/isabelle_process.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Tue Jun 01 17:52:19 2010 +0200
@@ -67,9 +67,9 @@
val path = File.platform_path (Path.explode out);
val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*)
val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*)
- val _ = SimpleThread.fork false (auto_flush out_stream);
- val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
- val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
+ val _ = Simple_Thread.fork false (auto_flush out_stream);
+ val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
+ val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
in
Output.status_fn := standard_message out_stream "B";
Output.writeln_fn := standard_message out_stream "C";
--- a/src/Pure/System/isar.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/System/isar.ML Tue Jun 01 17:52:19 2010 +0200
@@ -72,7 +72,7 @@
fun find_and_undo _ [] = error "Undo history exhausted"
| find_and_undo which ((prev, tr) :: hist) =
- ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
+ ((case Toplevel.init_of tr of SOME name => Thy_Info.kill_thy name | NONE => ());
if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
in
--- a/src/Pure/System/session.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/System/session.ML Tue Jun 01 17:52:19 2010 +0200
@@ -73,7 +73,7 @@
(* finish *)
fun finish () =
- (ThyInfo.finish ();
+ (Thy_Info.finish ();
Present.finish ();
Future.shutdown ();
session_finished := true);
@@ -97,7 +97,7 @@
((fn () =>
(init reset parent name;
Present.init build info doc doc_graph doc_versions (path ()) name
- (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
+ (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
if timing then
let
val start = start_timing ();
--- a/src/Pure/Thy/present.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Thy/present.ML Tue Jun 01 17:52:19 2010 +0200
@@ -461,7 +461,7 @@
val parent_specs = map (parent_link remote_path path) parents;
fun prep_file (raw_path, loadit) =
- (case ThyLoad.check_ml dir raw_path of
+ (case Thy_Load.check_ml dir raw_path of
SOME (path, _) =>
let
val base = Path.base path;
--- a/src/Pure/Thy/thm_deps.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Thy/thm_deps.ML Tue Jun 01 17:52:19 2010 +0200
@@ -24,7 +24,7 @@
val session =
(case prefix of
a :: _ =>
- (case ThyInfo.lookup_theory a of
+ (case Thy_Info.lookup_theory a of
SOME thy =>
(case Present.session_name thy of
"" => []
--- a/src/Pure/Thy/thy_info.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Jun 01 17:52:19 2010 +0200
@@ -41,7 +41,7 @@
val finish: unit -> unit
end;
-structure ThyInfo: THY_INFO =
+structure Thy_Info: THY_INFO =
struct
(** theory loader actions and hooks **)
@@ -292,12 +292,12 @@
fun run_file path =
(case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of
- NONE => (ThyLoad.load_ml Path.current path; ())
+ NONE => (Thy_Load.load_ml Path.current path; ())
| SOME name =>
(case lookup_deps name of
SOME deps =>
- change_deps name (provide path name (ThyLoad.load_ml (master_dir' deps) path))
- | NONE => (ThyLoad.load_ml Path.current path; ())));
+ change_deps name (provide path name (Thy_Load.load_ml (master_dir' deps) path))
+ | NONE => (Thy_Load.load_ml Path.current path; ())));
in
@@ -306,7 +306,7 @@
val dir = master_directory name;
val _ = check_unfinished error name;
in
- (case ThyLoad.check_file dir path of
+ (case Thy_Load.check_file dir path of
SOME path_info => change_deps name (provide path name path_info)
| NONE => error ("Could not find file " ^ quote (Path.implode path)))
end;
@@ -429,7 +429,7 @@
let val info' =
(case info of NONE => NONE
| SOME (_, id) =>
- (case ThyLoad.check_ml (master_dir master) src_path of NONE => NONE
+ (case Thy_Load.check_ml (master_dir master) src_path of NONE => NONE
| SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
in (src_path, info') end;
@@ -437,16 +437,16 @@
(case lookup_deps name of
SOME NONE => (true, NONE, get_parents name)
| NONE =>
- let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name
+ let val {master, text, imports = parents, uses = files} = Thy_Load.deps_thy dir name
in (false, init_deps (SOME master) text parents files, parents) end
| SOME (SOME {update_time, master, text, parents, files}) =>
let
- val (thy_path, thy_id) = ThyLoad.check_thy dir name;
+ val (thy_path, thy_id) = Thy_Load.check_thy dir name;
val master' = SOME (thy_path, thy_id);
in
if Option.map #2 master <> SOME thy_id then
let val {text = text', imports = parents', uses = files', ...} =
- ThyLoad.deps_thy dir name;
+ Thy_Load.deps_thy dir name;
in (false, init_deps master' text' parents' files', parents') end
else
let
@@ -571,7 +571,7 @@
val _ = map get_theory (get_parents name);
val _ = check_unfinished error name;
val _ = touch_thy name;
- val master = #master (ThyLoad.deps_thy Path.current name);
+ val master = #master (Thy_Load.deps_thy Path.current name);
val upd_time = #2 (Management_Data.get thy);
in
CRITICAL (fn () =>
--- a/src/Pure/Thy/thy_load.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML Tue Jun 01 17:52:19 2010 +0200
@@ -31,10 +31,9 @@
val load_ml: Path.T -> Path.T -> Path.T * File.ident
end;
-structure ThyLoad: THY_LOAD =
+structure Thy_Load: THY_LOAD =
struct
-
(* maintain load path *)
local val load_path = Unsynchronized.ref [Path.current] in
@@ -132,5 +131,5 @@
end;
-structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
+structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load;
open Basic_Thy_Load;
--- a/src/Pure/Thy/thy_output.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Jun 01 17:52:19 2010 +0200
@@ -33,7 +33,7 @@
val output: Pretty.T list -> string
end;
-structure ThyOutput: THY_OUTPUT =
+structure Thy_Output: THY_OUTPUT =
struct
(** global options **)
--- a/src/Pure/Thy/thy_syntax.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Tue Jun 01 17:52:19 2010 +0200
@@ -25,7 +25,7 @@
(span * span list * bool, (span, 'a) Source.source) Source.source
end;
-structure ThySyntax: THY_SYNTAX =
+structure Thy_Syntax: THY_SYNTAX =
struct
(** tokens **)
--- a/src/Pure/axclass.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/axclass.ML Tue Jun 01 17:52:19 2010 +0200
@@ -412,48 +412,60 @@
(* primitive rules *)
-fun add_classrel raw_th thy =
+fun gen_add_classrel store raw_th thy =
let
val th = Thm.strip_shyps (Thm.transfer thy raw_th);
val prop = Thm.plain_prop_of th;
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
val rel = Logic.dest_classrel prop handle TERM _ => err ();
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
- val th' = th
+ val (th', thy') =
+ if store then PureThy.store_thm
+ (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy
+ else (th, thy);
+ val th'' = th'
|> Thm.unconstrainT
- |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] [];
+ |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
in
- thy
+ thy'
|> Sign.primitive_classrel (c1, c2)
- |> (#2 oo put_trancl_classrel) ((c1, c2), th')
+ |> (#2 oo put_trancl_classrel) ((c1, c2), th'')
|> perhaps complete_arities
end;
-fun add_arity raw_th thy =
+fun gen_add_arity store raw_th thy =
let
val th = Thm.strip_shyps (Thm.transfer thy raw_th);
val prop = Thm.plain_prop_of th;
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
- val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
+ val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
+
+ val (th', thy') =
+ if store then PureThy.store_thm
+ (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy
+ else (th, thy);
val args = Name.names Name.context Name.aT Ss;
val T = Type (t, map TFree args);
- val std_vars = map (fn (a, S) => SOME (ctyp_of thy (TVar ((a, 0), [])))) args;
+ val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
- val missing_params = Sign.complete_sort thy [c]
- |> maps (these o Option.map #params o try (get_info thy))
- |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
+ val missing_params = Sign.complete_sort thy' [c]
+ |> maps (these o Option.map #params o try (get_info thy'))
+ |> filter_out (fn (const, _) => can (get_inst_param thy') (const, t))
|> (map o apsnd o map_atyps) (K T);
- val th' = th
+ val th'' = th'
|> Thm.unconstrainT
|> Drule.instantiate' std_vars [];
in
- thy
+ thy'
|> fold (#2 oo declare_overloaded) missing_params
|> Sign.primitive_arity (t, Ss, [c])
- |> put_arity ((t, Ss, c), th')
+ |> put_arity ((t, Ss, c), th'')
end;
+val add_classrel = gen_add_classrel true;
+val add_arity = gen_add_arity true;
+
(* tactical proofs *)
@@ -468,7 +480,7 @@
thy
|> PureThy.add_thms [((Binding.name
(prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
- |-> (fn [th'] => add_classrel th')
+ |-> (fn [th'] => gen_add_classrel false th')
end;
fun prove_arity raw_arity tac thy =
@@ -484,7 +496,7 @@
in
thy
|> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
- |-> fold add_arity
+ |-> fold (gen_add_arity false)
end;
@@ -618,11 +630,11 @@
fun ax_classrel prep =
axiomatize (map o prep) (map Logic.mk_classrel)
- (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
+ (map (prefix classrel_prefix o Logic.name_classrel)) (gen_add_classrel false);
fun ax_arity prep =
axiomatize (prep o ProofContext.init_global) Logic.mk_arities
- (map (prefix arity_prefix) o Logic.name_arities) add_arity;
+ (map (prefix arity_prefix) o Logic.name_arities) (gen_add_arity false);
fun class_const c =
(Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
--- a/src/Pure/context.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/context.ML Tue Jun 01 17:52:19 2010 +0200
@@ -325,7 +325,7 @@
local
val lock = Mutex.mutex ();
in
- fun SYNCHRONIZED e = SimpleThread.synchronized "theory" lock e;
+ fun SYNCHRONIZED e = Simple_Thread.synchronized "theory" lock e;
end;
fun create_thy self draft ids data ancestry history =
--- a/src/Pure/logic.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/logic.ML Tue Jun 01 17:52:19 2010 +0200
@@ -46,7 +46,8 @@
val name_arity: string * sort list * class -> string
val mk_arities: arity -> term list
val dest_arity: term -> string * sort list * class
- val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
+ val unconstrainT: sort list -> term ->
+ ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
val protectC: term
val protect: term -> term
val unprotect: term -> term
@@ -299,11 +300,15 @@
map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
constraints_map;
+ val outer_constraints =
+ maps (fn (T, S) => map (pair T) S)
+ (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
+
val prop' =
prop
|> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
|> curry list_implies (map snd constraints);
- in ((atyp_map, constraints), prop') end;
+ in ((atyp_map, constraints, outer_constraints), prop') end;
--- a/src/Pure/morphism.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/morphism.ML Tue Jun 01 17:52:19 2010 +0200
@@ -79,5 +79,5 @@
end;
-structure BasicMorphism: BASIC_MORPHISM = Morphism;
-open BasicMorphism;
+structure Basic_Morphism: BASIC_MORPHISM = Morphism;
+open Basic_Morphism;
--- a/src/Pure/proofterm.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/proofterm.ML Tue Jun 01 17:52:19 2010 +0200
@@ -58,6 +58,8 @@
val strip_combt: proof -> proof * term option list
val strip_combP: proof -> proof * proof list
val strip_thm: proof_body -> proof_body
+ val map_proof_same: term Same.operation -> typ Same.operation
+ -> (typ * class -> proof) -> proof Same.operation
val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
val map_proof_types_same: typ Same.operation -> proof Same.operation
val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
@@ -80,7 +82,9 @@
(** proof terms for specific inference rules **)
val implies_intr_proof: term -> proof -> proof
+ val implies_intr_proof': term -> proof -> proof
val forall_intr_proof: term -> string -> proof -> proof
+ val forall_intr_proof': term -> proof -> proof
val varify_proof: term -> (string * sort) list -> proof -> proof
val legacy_freezeT: term -> proof -> proof
val rotate_proof: term list -> term -> int -> proof -> proof
@@ -121,13 +125,13 @@
(** rewriting on proof terms **)
val add_prf_rrule: proof * proof -> theory -> theory
- val add_prf_rproc: (typ list -> proof -> (proof * proof) option) -> theory -> theory
+ val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory
val no_skel: proof
val normal_skel: proof
val rewrite_proof: theory -> (proof * proof) list *
- (typ list -> proof -> (proof * proof) option) list -> proof -> proof
+ (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
val rewrite_proof_notypes: (proof * proof) list *
- (typ list -> proof -> (proof * proof) option) list -> proof -> proof
+ (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
val rew_proof: theory -> proof -> proof
val promise_proof: theory -> serial -> term -> proof
@@ -618,7 +622,7 @@
(***** implication introduction *****)
-fun implies_intr_proof h prf =
+fun gen_implies_intr_proof f h prf =
let
fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME
| abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf)
@@ -630,14 +634,21 @@
| abshyp _ _ = raise Same.SAME
and abshyph i prf = (abshyp i prf handle Same.SAME => prf);
in
- AbsP ("H", NONE (*h*), abshyph 0 prf)
+ AbsP ("H", f h, abshyph 0 prf)
end;
+val implies_intr_proof = gen_implies_intr_proof (K NONE);
+val implies_intr_proof' = gen_implies_intr_proof SOME;
+
(***** forall introduction *****)
fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf);
+fun forall_intr_proof' t prf =
+ let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
+ in Abst (a, SOME T, prf_abstract_over t prf) end;
+
(***** varify *****)
@@ -1105,7 +1116,7 @@
fun flt (i: int) = filter (fn n => n < i);
-fun fomatch Ts tymatch j =
+fun fomatch Ts tymatch j instsp p =
let
fun mtch (instsp as (tyinsts, insts)) = fn
(Var (ixn, T), t) =>
@@ -1120,7 +1131,7 @@
| (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u)
| (Bound i, Bound j) => if i=j then instsp else raise PMatch
| _ => raise PMatch
- in mtch end;
+ in mtch instsp (pairself Envir.beta_eta_contract p) end;
fun match_proof Ts tymatch =
let
@@ -1253,72 +1264,72 @@
fun rewrite_prf tymatch (rules, procs) prf =
let
- fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
- | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
- | rew Ts prf =
- (case get_first (fn r => r Ts prf) procs of
+ fun rew _ _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
+ | rew _ _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
+ | rew Ts hs prf =
+ (case get_first (fn r => r Ts hs prf) procs of
NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
(match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
handle PMatch => NONE) (filter (could_unify prf o fst) rules)
| some => some);
- fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) =
- if prf_loose_Pbvar1 prf' 0 then rew Ts prf
+ fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) =
+ if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf
else
let val prf'' = incr_pboundvars (~1) 0 prf'
- in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
- | rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) =
- if prf_loose_bvar1 prf' 0 then rew Ts prf
+ in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
+ | rew0 Ts hs (prf as Abst (_, _, prf' % SOME (Bound 0))) =
+ if prf_loose_bvar1 prf' 0 then rew Ts hs prf
else
let val prf'' = incr_pboundvars 0 (~1) prf'
- in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
- | rew0 Ts prf = rew Ts prf;
+ in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
+ | rew0 Ts hs prf = rew Ts hs prf;
- fun rew1 _ (Hyp (Var _)) _ = NONE
- | rew1 Ts skel prf = (case rew2 Ts skel prf of
- SOME prf1 => (case rew0 Ts prf1 of
- SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts skel' prf2))
+ fun rew1 _ _ (Hyp (Var _)) _ = NONE
+ | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of
+ SOME prf1 => (case rew0 Ts hs prf1 of
+ SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
| NONE => SOME prf1)
- | NONE => (case rew0 Ts prf of
- SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts skel' prf1))
+ | NONE => (case rew0 Ts hs prf of
+ SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
| NONE => NONE))
- and rew2 Ts skel (prf % SOME t) = (case prf of
+ and rew2 Ts hs skel (prf % SOME t) = (case prf of
Abst (_, _, body) =>
let val prf' = prf_subst_bounds [t] body
- in SOME (the_default prf' (rew2 Ts no_skel prf')) end
- | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf of
+ in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
+ | _ => (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
SOME prf' => SOME (prf' % SOME t)
| NONE => NONE))
- | rew2 Ts skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
- (rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf)
- | rew2 Ts skel (prf1 %% prf2) = (case prf1 of
+ | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
+ (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf)
+ | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of
AbsP (_, _, body) =>
let val prf' = prf_subst_pbounds [prf2] body
- in SOME (the_default prf' (rew2 Ts no_skel prf')) end
+ in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
| _ =>
let val (skel1, skel2) = (case skel of
skel1 %% skel2 => (skel1, skel2)
| _ => (no_skel, no_skel))
- in case rew1 Ts skel1 prf1 of
- SOME prf1' => (case rew1 Ts skel2 prf2 of
+ in case rew1 Ts hs skel1 prf1 of
+ SOME prf1' => (case rew1 Ts hs skel2 prf2 of
SOME prf2' => SOME (prf1' %% prf2')
| NONE => SOME (prf1' %% prf2))
- | NONE => (case rew1 Ts skel2 prf2 of
+ | NONE => (case rew1 Ts hs skel2 prf2 of
SOME prf2' => SOME (prf1 %% prf2')
| NONE => NONE)
end)
- | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts)
+ | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs
(case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
SOME prf' => SOME (Abst (s, T, prf'))
| NONE => NONE)
- | rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts
+ | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs)
(case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
SOME prf' => SOME (AbsP (s, t, prf'))
| NONE => NONE)
- | rew2 _ _ _ = NONE;
+ | rew2 _ _ _ _ = NONE;
- in the_default prf (rew1 [] no_skel prf) end;
+ in the_default prf (rew1 [] [] no_skel prf) end;
fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
@@ -1328,11 +1339,11 @@
(**** theory data ****)
-structure ProofData = Theory_Data
+structure Data = Theory_Data
(
type T =
(stamp * (proof * proof)) list *
- (stamp * (typ list -> proof -> (proof * proof) option)) list;
+ (stamp * (typ list -> term option list -> proof -> (proof * proof) option)) list;
val empty = ([], []);
val extend = I;
@@ -1341,11 +1352,11 @@
AList.merge (op =) (K true) (procs1, procs2));
);
-fun get_data thy = let val (rules, procs) = ProofData.get thy in (map #2 rules, map #2 procs) end;
+fun get_data thy = let val (rules, procs) = Data.get thy in (map #2 rules, map #2 procs) end;
fun rew_proof thy = rewrite_prf fst (get_data thy);
-fun add_prf_rrule r = (ProofData.map o apfst) (cons (stamp (), r));
-fun add_prf_rproc p = (ProofData.map o apsnd) (cons (stamp (), p));
+fun add_prf_rrule r = (Data.map o apfst) (cons (stamp (), r));
+fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p));
(***** promises *****)
@@ -1373,7 +1384,7 @@
| SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel))
| fill _ = NONE;
val (rules, procs) = get_data thy;
- val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
+ val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
in PBody {oracles = oracles, thms = thms, proof = proof} end;
fun fulfill_proof_future _ [] postproc body = Future.value (postproc body)
@@ -1421,12 +1432,13 @@
val (postproc, ofclasses, prop1, args1) =
if do_unconstrain then
let
- val ((atyp_map, constraints), prop1) = Logic.unconstrainT shyps prop;
+ val ((atyp_map, constraints, outer_constraints), prop1) =
+ Logic.unconstrainT shyps prop;
val postproc = unconstrainT_body thy (atyp_map, constraints);
val args1 =
(map o Option.map o Term.map_types o Term.map_atyps)
(Type.strip_sorts o atyp_map) args;
- in (postproc, map (OfClass o fst) constraints, prop1, args1) end
+ in (postproc, map OfClass outer_constraints, prop1, args1) end
else (I, [], prop, args);
val argsP = ofclasses @ map Hyp hyps;
@@ -1447,7 +1459,7 @@
val head = PThm (i, ((name, prop1, NONE), body'));
in ((i, (name, prop1, body')), head, args, argsP, args1) end;
-val unconstrain_thm_proofs = Unsynchronized.ref false;
+val unconstrain_thm_proofs = Unsynchronized.ref true;
fun thm_proof thy name shyps hyps concl promises body =
let val (pthm, head, args, argsP, _) =
--- a/src/Pure/pure_setup.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/pure_setup.ML Tue Jun 01 17:52:19 2010 +0200
@@ -6,14 +6,14 @@
(* the Pure theories *)
-val theory = ThyInfo.get_theory;
+val theory = Thy_Info.get_theory;
Context.>> (Context.map_theory
(Outer_Syntax.process_file (Path.explode "Pure.thy") #>
Theory.end_theory));
structure Pure = struct val thy = ML_Context.the_global_context () end;
Context.set_thread_data NONE;
-ThyInfo.register_theory Pure.thy;
+Thy_Info.register_theory Pure.thy;
(* ML toplevel pretty printing *)
@@ -47,11 +47,11 @@
(* ML toplevel use commands *)
-fun use name = Toplevel.program (fn () => ThyInfo.use name);
-fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name);
-fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name);
-fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name);
-fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
+fun use name = Toplevel.program (fn () => Thy_Info.use name);
+fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
+fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
+fun time_use name = Toplevel.program (fn () => Thy_Info.time_use name);
+fun time_use_thy name = Toplevel.program (fn () => Thy_Info.time_use_thy name);
(* misc *)
--- a/src/Pure/pure_thy.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/pure_thy.ML Tue Jun 01 17:52:19 2010 +0200
@@ -52,7 +52,7 @@
(** theory data **)
-structure FactsData = Theory_Data
+structure Global_Facts = Theory_Data
(
type T = Facts.T * thm list;
val empty = (Facts.empty, []);
@@ -63,19 +63,19 @@
(* facts *)
-val facts_of = #1 o FactsData.get;
+val facts_of = #1 o Global_Facts.get;
val intern_fact = Facts.intern o facts_of;
val defined_fact = Facts.defined o facts_of;
-fun hide_fact fully name = FactsData.map (apfst (Facts.hide fully name));
+fun hide_fact fully name = Global_Facts.map (apfst (Facts.hide fully name));
(* proofs *)
-fun register_proofs (thy, thms) = (FactsData.map (apsnd (append thms)) thy, thms);
+fun register_proofs (thy, thms) = (Global_Facts.map (apsnd (append thms)) thy, thms);
-fun join_proofs thy = Thm.join_proofs (rev (#2 (FactsData.get thy)));
+fun join_proofs thy = Thm.join_proofs (rev (#2 (Global_Facts.get thy)));
@@ -143,7 +143,7 @@
val (thy', thms') =
register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
val thms'' = map (Thm.transfer thy') thms';
- val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
+ val thy'' = thy' |> (Global_Facts.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
in (thms'', thy'') end;
@@ -178,7 +178,7 @@
(* add_thms_dynamic *)
fun add_thms_dynamic (b, f) thy = thy
- |> (FactsData.map o apfst)
+ |> (Global_Facts.map o apfst)
(Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
@@ -252,7 +252,7 @@
("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
-structure OldApplSyntax = Theory_Data
+structure Old_Appl_Syntax = Theory_Data
(
type T = bool;
val empty = false;
@@ -262,10 +262,10 @@
else error "Cannot merge theories with different application syntax";
);
-val old_appl_syntax = OldApplSyntax.get;
+val old_appl_syntax = Old_Appl_Syntax.get;
val old_appl_syntax_setup =
- OldApplSyntax.put true #>
+ Old_Appl_Syntax.put true #>
Sign.del_modesyntax_i Syntax.mode_default applC_syntax #>
Sign.add_syntax_i appl_syntax;
@@ -274,7 +274,7 @@
val _ = Context.>> (Context.map_theory
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
- OldApplSyntax.put false #>
+ Old_Appl_Syntax.put false #>
Sign.add_types
[(Binding.name "fun", 2, NoSyn),
(Binding.name "prop", 0, NoSyn),
--- a/src/Pure/simplifier.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/simplifier.ML Tue Jun 01 17:52:19 2010 +0200
@@ -100,7 +100,7 @@
(** simpset data **)
-structure SimpsetData = Generic_Data
+structure Simpset = Generic_Data
(
type T = simpset;
val empty = empty_ss;
@@ -108,8 +108,8 @@
val merge = merge_ss;
);
-val get_ss = SimpsetData.get;
-fun map_ss f context = SimpsetData.map (with_context (Context.proof_of context) f) context;
+val get_ss = Simpset.get;
+fun map_ss f context = Simpset.map (with_context (Context.proof_of context) f) context;
(* attributes *)
--- a/src/Pure/type_infer.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Pure/type_infer.ML Tue Jun 01 17:52:19 2010 +0200
@@ -295,11 +295,11 @@
| occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts
| occurs_check _ _ _ = ();
- fun assign i (T as Param (i', _)) S (tye_idx as (tye, idx)) =
+ fun assign i (T as Param (i', _)) S tye_idx =
if i = i' then tye_idx
- else meet (T, S) (Inttab.update_new (i, T) tye, idx)
- | assign i T S (tye, idx) =
- (occurs_check tye i T; meet (T, S) (Inttab.update_new (i, T) tye, idx));
+ else tye_idx |> meet (T, S) |>> Inttab.update_new (i, T)
+ | assign i T S (tye_idx as (tye, _)) =
+ (occurs_check tye i T; tye_idx |> meet (T, S) |>> Inttab.update_new (i, T));
(* unification *)
--- a/src/Tools/Code/code_eval.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Tue Jun 01 17:52:19 2010 +0200
@@ -173,7 +173,7 @@
end
| process (code_body, _) _ (SOME file_name) thy =
let
- val preamble = "(* Generated from " ^ Path.implode (ThyLoad.thy_path (Context.theory_name thy))
+ val preamble = "(* Generated from " ^ Path.implode (Thy_Load.thy_path (Context.theory_name thy))
^ "; DO NOT EDIT! *)";
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
in
--- a/src/Tools/Code/code_haskell.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Tue Jun 01 17:52:19 2010 +0200
@@ -447,7 +447,7 @@
(ps @| print_term vars' NOBR t'')
end
| NONE => brackify_infix (1, L) fxy
- [print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2]
+ (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
in (2, ([c_bind], pretty)) end;
fun add_monad target' raw_c_bind thy =
@@ -477,11 +477,11 @@
val setup =
Code_Target.add_target (target, (isar_seri_haskell, literals))
#> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
+ brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
print_typ (INFX (1, R)) ty2
- ]))
+ )))
#> fold (Code_Target.add_reserved target) [
"hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
"import", "default", "forall", "let", "in", "class", "qualified", "data",
--- a/src/Tools/Code/code_ml.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Jun 01 17:52:19 2010 +0200
@@ -963,17 +963,17 @@
Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
#> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
+ brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
print_typ (INFX (1, R)) ty2
- ]))
+ )))
#> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
+ brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
print_typ (INFX (1, R)) ty2
- ]))
+ )))
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
#> fold (Code_Target.add_reserved target_SML)
["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]
--- a/src/Tools/Code/code_printer.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Jun 01 17:52:19 2010 +0200
@@ -61,7 +61,7 @@
val INFX: int * lrx -> fixity
val APP: fixity
val brackify: fixity -> Pretty.T list -> Pretty.T
- val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
+ val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
@@ -219,8 +219,9 @@
fun brackify fxy_ctxt =
gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
-fun brackify_infix infx fxy_ctxt =
- gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
+fun brackify_infix infx fxy_ctxt (l, m, r) =
+ (if fixity (INFX infx) fxy_ctxt then enclose "(" ")" else Pretty.block)
+ ([l, str " ", m, Pretty.brk 1, r]);
fun brackify_block fxy_ctxt p1 ps p2 =
let val p = Pretty.block_enclose (p1, p2) ps
@@ -304,7 +305,7 @@
val r = case x of R => INFX (i, R) | _ => INFX (i, X);
in
mk_mixfix prep_arg (INFX (i, x),
- [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
+ [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
end;
fun parse_mixfix prep_arg s =
--- a/src/Tools/Code/code_scala.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Tue Jun 01 17:52:19 2010 +0200
@@ -25,11 +25,12 @@
fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved args_num is_singleton deresolve =
let
val deresolve_base = Long_Name.base_name o deresolve;
+ val lookup_tyvar = first_upper oo lookup_var;
fun print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
of NONE => applify "[" "]" fxy
((str o deresolve) tyco) (map (print_typ tyvars NOBR) tys)
| SOME (i, print) => print (print_typ tyvars) fxy tys)
- | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
+ | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
fun print_typed tyvars p ty =
Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
fun print_var vars NONE = str "_"
@@ -114,19 +115,20 @@
fun implicit_arguments tyvars vs vars =
let
val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
- [(str o deresolve) class, str "[", (str o lookup_var tyvars) v, str "]"]) sort) vs;
- val implicit_names = Name.invents (snd vars) "a" (length implicit_typ_ps);
+ [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
+ val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
+ lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
val vars' = intro_vars implicit_names vars;
val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
implicit_names implicit_typ_ps;
in ((implicit_names, implicit_ps), vars') end;
fun print_defhead tyvars vars p vs params tys implicits ty =
- concat [str "def", print_typed tyvars (applify "(implicit " ")" NOBR
+ Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
(applify "(" ")" NOBR
- (applify "[" "]" NOBR p (map (str o lookup_var tyvars o fst) vs))
+ (applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs))
(map2 (fn param => fn ty => print_typed tyvars
((str o lookup_var vars) param) ty)
- params tys)) implicits) ty, str "="]
+ params tys)) implicits) ty, str " ="]
fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = (case filter (snd o snd) raw_eqs
of [] =>
let
@@ -193,7 +195,7 @@
val fields = Name.names (snd reserved) "a" tys;
val vars = intro_vars (map fst fields) reserved;
fun add_typargs p = applify "[" "]" NOBR p
- (map (str o lookup_var tyvars o fst) vs);
+ (map (str o lookup_tyvar tyvars o fst) vs);
in
concat [
applify "(" ")" NOBR
@@ -206,7 +208,7 @@
in
Pretty.chunks (
applify "[" "]" NOBR ((concat o map str) ["sealed", "class", deresolve_base name])
- (map (str o prefix "+" o lookup_var tyvars o fst) vs)
+ (map (str o prefix "+" o lookup_tyvar tyvars o fst) vs)
:: map print_co cos
)
end
@@ -214,7 +216,7 @@
let
val tyvars = intro_vars [v] reserved;
val vs = [(v, [name])];
- fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_var tyvars) v];
+ fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
fun print_superclasses [] = NONE
| print_superclasses classes = SOME (concat (str "extends"
:: separate (str "with") (map (add_typarg o str o deresolve o fst) classes)));
@@ -255,7 +257,7 @@
val tyvars = intro_vars (map fst vs) reserved;
val insttyp = tyco `%% map (ITyVar o fst) vs;
val p_inst_typ = print_typ tyvars NOBR insttyp;
- fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_var tyvars o fst) vs);
+ fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs);
fun add_inst_typ p = Pretty.block [p, str "[", p_inst_typ, str "]"];
val ((implicit_names, implicit_ps), vars) = implicit_arguments tyvars vs reserved;
fun print_classparam_inst ((classparam, const as (_, (_, tys))), (thm, _)) =
@@ -282,10 +284,10 @@
@ map print_classparam_inst classparam_insts),
concat [str "implicit", str (if null vs then "val" else "def"),
applify "(implicit " ")" NOBR (applify "[" "]" NOBR
- ((str o deresolve_base) name) (map (str o lookup_var tyvars o fst) vs))
+ ((str o deresolve_base) name) (map (str o lookup_tyvar tyvars o fst) vs))
implicit_ps,
str "=", str "new", applify "[" "]" NOBR ((str o deresolve_base) name)
- (map (str o lookup_var tyvars o fst) vs),
+ (map (str o lookup_tyvar tyvars o fst) vs),
Pretty.enum ";" "{ " " }" (map (str o (fn v => "val arg$" ^ v ^ " = " ^ v) o lookup_var vars)
implicit_names)]
]
@@ -400,10 +402,11 @@
end;
val literals = let
- fun char_scala c =
- let
- val s = ML_Syntax.print_char c;
- in if s = "'" then "\\'" else s end;
+ fun char_scala c = if c = "'" then "\\'"
+ else if c = "\"" then "\\\""
+ else if c = "\\" then "\\\\"
+ else let val k = ord c
+ in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
fun numeral_scala k = if k < 0
then if k <= 2147483647 then "- " ^ string_of_int (~ k)
else quote ("- " ^ string_of_int (~ k))
@@ -430,17 +433,17 @@
val setup =
Code_Target.add_target (target, (isar_seri_scala, literals))
#> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
+ brackify_infix (1, R) fxy (
print_typ BR ty1 (*product type vs. tupled arguments!*),
str "=>",
print_typ (INFX (1, R)) ty2
- ]))
+ )))
#> fold (Code_Target.add_reserved target) [
"abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
"final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
"match", "new", "null", "object", "override", "package", "private", "protected",
"requires", "return", "sealed", "super", "this", "throw", "trait", "try",
- "true", "type", "val", "var", "while", "with"
+ "true", "type", "val", "var", "while", "with", "yield"
]
#> fold (Code_Target.add_reserved target) [
"error", "apply", "List", "Nil", "BigInt"
--- a/src/Tools/Code/code_thingol.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Jun 01 17:52:19 2010 +0200
@@ -882,7 +882,7 @@
fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
fun read_const_expr "*" = ([], consts_of thy)
| read_const_expr s = if String.isSuffix ".*" s
- then ([], consts_of_select (ThyInfo.the_theory (unsuffix ".*" s) thy))
+ then ([], consts_of_select (Thy_Info.the_theory (unsuffix ".*" s) thy))
else ([Code.read_const thy s], []);
in pairself flat o split_list o map read_const_expr end;
--- a/src/Tools/Code/lib/Tools/codegen Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Tue Jun 01 17:52:19 2010 +0200
@@ -58,7 +58,7 @@
QND_CMD="reset"
fi
-CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init_global (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
+CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
--- a/src/Tools/WWW_Find/find_theorems.ML Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML Tue Jun 01 17:52:19 2010 +0200
@@ -5,8 +5,9 @@
*)
local
+
val default_limit = 20;
-val thy_names = sort string_ord (ThyInfo.get_names ());
+val thy_names = sort string_ord (Thy_Info.get_names ());
val find_theorems_url = "find_theorems";
@@ -234,7 +235,9 @@
Xhtml.write_close send header
end;
in
+
val () = show_question_marks := false;
val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
+
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/README Tue Jun 01 17:52:19 2010 +0200
@@ -0,0 +1,77 @@
+Isabelle/jEdit based on Isabelle/Scala
+======================================
+
+The Isabelle/Scala layer that is already part of Isabelle/Pure
+provides some general infrastructure for advanced prover interaction
+and integration. The Isabelle/jEdit application serves as an example
+for asynchronous proof checking with support for parallel processing.
+
+See also the paper:
+
+ Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala
+ and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors,
+ User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite
+ Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS.
+ http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf
+
+
+Some limitations of the current implementation (as of Isabelle2009-2):
+
+ * No provisions for editing multiple theory files.
+
+ * No reclaiming of old/unused document versions. Memory will fill
+ up eventually, both on the JVM and ML side.
+
+ * No support for non-local markup, e.g. commands reporting on
+ previous commands (proof end on proof head), or markup produced by
+ loading external files.
+
+ * Some performance bottlenecks for massive amount of markup,
+ e.g. when processing large ML sections.
+
+ * General lack of various conveniences known from Proof General.
+
+Despite these shortcomings, Isabelle/jEdit already demonstrates that
+interactive theorem proving can be much more than command-line
+interaction via TTY or editor front-ends (such as Proof General and
+its many remakes).
+
+
+Known problems with Mac OS
+==========================
+
+- The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
+ e.g. between the editor and the Console plugin, which is a standard
+ swing text box. Similar for search boxes etc.
+
+- Anti-aliasing does not really work as well as for Linux or Windows.
+ (General Apple/Swing problem?)
+
+- Font.createFont mangles the font family of non-regular fonts,
+ e.g. bold. IsabelleText font files need to be installed manually.
+
+- ToggleButton selected state is not rendered if window focus is lost,
+ which is probably a genuine feature of the Apple look-and-feel.
+
+
+Windows/Linux
+=============
+
+- Works best with Sun Java 1.6.x -- avoid OpenJDK for now.
+
+
+Licenses and home sites of contributing systems
+===============================================
+
+* Scala: BSD-style
+ http://www.scala-lang.org
+
+* jEdit: GPL (with special cases)
+ http://www.jedit.org/
+
+* Lobo/Cobra: GPL and LGPL
+ http://lobobrowser.org/
+
+
+ Makarius
+ 31-May-2010
--- a/src/Tools/jEdit/README_BUILD Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Tools/jEdit/README_BUILD Tue Jun 01 17:52:19 2010 +0200
@@ -2,7 +2,7 @@
Requirements to build from sources
==================================
-* Proper Java JRE/JDK from Sun, e.g. 1.6.0_18
+* Proper Java JRE/JDK from Sun, e.g. 1.6.0_20
http://java.sun.com/javase/downloads/index.jsp
* Netbeans 6.8
@@ -13,7 +13,7 @@
http://sourceforge.net/projects/erlybird/files/nb-scala/6.8v1.1.0rc2
http://blogtrader.net/dcaoyuan/category/NetBeans
-* jEdit 4.3.1 or 4.3.2
+* jEdit 4.3.2
http://www.jedit.org/
Netbeans Project "jEdit": install official sources as ./contrib/jEdit/.
@@ -31,7 +31,8 @@
* Isabelle/Pure Scala components
Netbeans Library "Isabelle-Pure" = ~~/lib/classes/Pure.jar
-* Scala Compiler
+* Scala Compiler 2.8
+ http://www.scala-lang.org
Netbeans Library "Scala-compiler" = $SCALA_HOME/lib/scala-compiler.jar
@@ -74,20 +75,3 @@
releases. (See
http://java.sun.com/j2se/1.5.0/docs/guide/jpda/conninv.html)
-----------------------------------------------------------------------
-
-
-Known problems with Mac OS
-==========================
-
-- The MacOSX plugin disrupts regular C-X/C/V operations, e.g. between
- the editor and the Console plugin, which is a standard swing text
- box. Similar for search boxes etc.
-
-- Anti-aliasing does not really work as well as for Linux or Windows.
- (General Apple/Swing problem?)
-
-- Font.createFont mangles the font family of non-regular fonts,
- e.g. bold.
-
-- ToggleButton selected state is not rendered if window focus is lost,
- which is probably a genuine feature of the Apple look-and-feel.
--- a/src/Tools/jEdit/makedist Tue Jun 01 17:52:00 2010 +0200
+++ b/src/Tools/jEdit/makedist Tue Jun 01 17:52:19 2010 +0200
@@ -84,6 +84,7 @@
cp -R jars/. "$JEDIT/jars/."
cp -R "$THIS/dist-template/." "$JEDIT/."
+cp "$THIS/README" "$JEDIT/."
perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;