# HG changeset patch # User blanchet # Date 1275407539 -7200 # Node ID 4a7fe945412da44917f230f672f32a90c3b66497 # Parent b3ff14122645ece1c195c7cd587896359fc6cf79# Parent e0940e692abb1c5320bc353e89a6b4d433563c87 merged diff -r e0940e692abb -r 4a7fe945412d Admin/makedist --- 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 { diff -r e0940e692abb -r 4a7fe945412d NEWS --- 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) diff -r e0940e692abb -r 4a7fe945412d doc-src/Classes/Thy/document/Classes.tex --- 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% % diff -r e0940e692abb -r 4a7fe945412d doc-src/IsarImplementation/Thy/Integration.thy --- 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 \} 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.\ diff -r e0940e692abb -r 4a7fe945412d doc-src/IsarImplementation/Thy/document/Integration.tex --- 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. diff -r e0940e692abb -r 4a7fe945412d doc-src/IsarRef/Thy/ROOT-HOLCF.ML --- 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"; diff -r e0940e692abb -r 4a7fe945412d doc-src/IsarRef/Thy/ROOT-ZF.ML --- 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"; diff -r e0940e692abb -r 4a7fe945412d doc-src/IsarRef/Thy/ROOT.ML --- 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 [ diff -r e0940e692abb -r 4a7fe945412d doc-src/Main/Docs/Main_Doc.thy --- 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{* diff -r e0940e692abb -r 4a7fe945412d doc-src/System/Thy/ROOT.ML --- 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"]; diff -r e0940e692abb -r 4a7fe945412d doc-src/TutorialI/Rules/Primes.thy --- 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! diff -r e0940e692abb -r 4a7fe945412d doc-src/TutorialI/Types/Numbers.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{* diff -r e0940e692abb -r 4a7fe945412d doc-src/TutorialI/Types/document/Numbers.tex --- 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}% % diff -r e0940e692abb -r 4a7fe945412d doc-src/TutorialI/Types/document/Pairs.tex --- 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 diff -r e0940e692abb -r 4a7fe945412d doc-src/TutorialI/settings.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d doc-src/antiquote_setup.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d doc-src/more_antiquote.ML --- 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 diff -r e0940e692abb -r 4a7fe945412d doc-src/rail.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/HOL/Extraction.thy --- 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) \ (\x y. P y x \ Q) \ Q" by (cases p) simp -setup {* - Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"}) -*} - realizers impI (P, Q): "\pq. pq" - "\ P Q pq (h: _). allI \ _ \ (\ x. impI \ _ \ _ \ (h \ x))" + "\ (c: _) (d: _) P Q pq (h: _). allI \ _ \ c \ (\ x. impI \ _ \ _ \ (h \ x))" impI (P): "Null" - "\ P Q (h: _). allI \ _ \ (\ x. impI \ _ \ _ \ (h \ x))" + "\ (c: _) P Q (h: _). allI \ _ \ c \ (\ x. impI \ _ \ _ \ (h \ x))" - impI (Q): "\q. q" "\ P Q q. impI \ _ \ _" + impI (Q): "\q. q" "\ (c: _) P Q q. impI \ _ \ _" impI: "Null" "impI" mp (P, Q): "\pq. pq" - "\ P Q pq (h: _) p. mp \ _ \ _ \ (spec \ _ \ p \ h)" + "\ (c: _) (d: _) P Q pq (h: _) p. mp \ _ \ _ \ (spec \ _ \ p \ c \ h)" mp (P): "Null" - "\ P Q (h: _) p. mp \ _ \ _ \ (spec \ _ \ p \ h)" + "\ (c: _) P Q (h: _) p. mp \ _ \ _ \ (spec \ _ \ p \ c \ h)" - mp (Q): "\q. q" "\ P Q q. mp \ _ \ _" + mp (Q): "\q. q" "\ (c: _) P Q q. mp \ _ \ _" mp: "Null" "mp" - allI (P): "\p. p" "\ P p. allI \ _" + allI (P): "\p. p" "\ (c: _) P (d: _) p. allI \ _ \ d" allI: "Null" "allI" - spec (P): "\x p. p x" "\ P x p. spec \ _ \ x" + spec (P): "\x p. p x" "\ (c: _) P x (d: _) p. spec \ _ \ x \ d" spec: "Null" "spec" - exI (P): "\x p. (x, p)" "\ P x p. exI_realizer \ P \ p \ x" + exI (P): "\x p. (x, p)" "\ (c: _) P x (d: _) p. exI_realizer \ P \ p \ x \ c \ d" - exI: "\x. x" "\ P x (h: _). h" + exI: "\x. x" "\ P x (c: _) (h: _). h" exE (P, Q): "\p pq. let (x, y) = p in pq x y" - "\ P Q p (h: _) pq. exE_realizer \ P \ p \ Q \ pq \ h" + "\ (c: _) (d: _) P Q (e: _) p (h: _) pq. exE_realizer \ P \ p \ Q \ pq \ c \ e \ d \ h" exE (P): "Null" - "\ P Q p. exE_realizer' \ _ \ _ \ _" + "\ (c: _) P Q (d: _) p. exE_realizer' \ _ \ _ \ _ \ c \ d" exE (Q): "\x pq. pq x" - "\ P Q x (h1: _) pq (h2: _). h2 \ x \ h1" + "\ (c: _) P Q (d: _) x (h1: _) pq (h2: _). h2 \ x \ h1" exE: "Null" - "\ P Q x (h1: _) (h2: _). h2 \ x \ h1" + "\ P Q (c: _) x (h1: _) (h2: _). h2 \ x \ h1" conjI (P, Q): "Pair" - "\ P Q p (h: _) q. conjI_realizer \ P \ p \ Q \ q \ h" + "\ (c: _) (d: _) P Q p (h: _) q. conjI_realizer \ P \ p \ Q \ q \ c \ d \ h" conjI (P): "\p. p" - "\ P Q p. conjI \ _ \ _" + "\ (c: _) P Q p. conjI \ _ \ _" conjI (Q): "\q. q" - "\ P Q (h: _) q. conjI \ _ \ _ \ h" + "\ (c: _) P Q (h: _) q. conjI \ _ \ _ \ h" conjI: "Null" "conjI" conjunct1 (P, Q): "fst" - "\ P Q pq. conjunct1 \ _ \ _" + "\ (c: _) (d: _) P Q pq. conjunct1 \ _ \ _" conjunct1 (P): "\p. p" - "\ P Q p. conjunct1 \ _ \ _" + "\ (c: _) P Q p. conjunct1 \ _ \ _" conjunct1 (Q): "Null" - "\ P Q q. conjunct1 \ _ \ _" + "\ (c: _) P Q q. conjunct1 \ _ \ _" conjunct1: "Null" "conjunct1" conjunct2 (P, Q): "snd" - "\ P Q pq. conjunct2 \ _ \ _" + "\ (c: _) (d: _) P Q pq. conjunct2 \ _ \ _" conjunct2 (P): "Null" - "\ P Q p. conjunct2 \ _ \ _" + "\ (c: _) P Q p. conjunct2 \ _ \ _" conjunct2 (Q): "\p. p" - "\ P Q p. conjunct2 \ _ \ _" + "\ (c: _) P Q p. conjunct2 \ _ \ _" conjunct2: "Null" "conjunct2" disjI1 (P, Q): "Inl" - "\ P Q p. iffD2 \ _ \ _ \ (sum.cases_1 \ P \ _ \ p)" + "\ (c: _) (d: _) P Q p. iffD2 \ _ \ _ \ (sum.cases_1 \ P \ _ \ p \ arity_type_bool \ c \ d)" disjI1 (P): "Some" - "\ P Q p. iffD2 \ _ \ _ \ (option.cases_2 \ _ \ P \ p)" + "\ (c: _) P Q p. iffD2 \ _ \ _ \ (option.cases_2 \ _ \ P \ p \ arity_type_bool \ c)" disjI1 (Q): "None" - "\ P Q. iffD2 \ _ \ _ \ (option.cases_1 \ _ \ _)" + "\ (c: _) P Q. iffD2 \ _ \ _ \ (option.cases_1 \ _ \ _ \ arity_type_bool \ c)" disjI1: "Left" - "\ P Q. iffD2 \ _ \ _ \ (sumbool.cases_1 \ _ \ _)" + "\ P Q. iffD2 \ _ \ _ \ (sumbool.cases_1 \ _ \ _ \ arity_type_bool)" disjI2 (P, Q): "Inr" - "\ Q P q. iffD2 \ _ \ _ \ (sum.cases_2 \ _ \ Q \ q)" + "\ (d: _) (c: _) Q P q. iffD2 \ _ \ _ \ (sum.cases_2 \ _ \ Q \ q \ arity_type_bool \ c \ d)" disjI2 (P): "None" - "\ Q P. iffD2 \ _ \ _ \ (option.cases_1 \ _ \ _)" + "\ (c: _) Q P. iffD2 \ _ \ _ \ (option.cases_1 \ _ \ _ \ arity_type_bool \ c)" disjI2 (Q): "Some" - "\ Q P q. iffD2 \ _ \ _ \ (option.cases_2 \ _ \ Q \ q)" + "\ (c: _) Q P q. iffD2 \ _ \ _ \ (option.cases_2 \ _ \ Q \ q \ arity_type_bool \ c)" disjI2: "Right" - "\ Q P. iffD2 \ _ \ _ \ (sumbool.cases_2 \ _ \ _)" + "\ Q P. iffD2 \ _ \ _ \ (sumbool.cases_2 \ _ \ _ \ arity_type_bool)" disjE (P, Q, R): "\pq pr qr. (case pq of Inl p \ pr p | Inr q \ qr q)" - "\ P Q R pq (h1: _) pr (h2: _) qr. - disjE_realizer \ _ \ _ \ pq \ R \ pr \ qr \ h1 \ h2" + "\ (c: _) (d: _) (e: _) P Q R pq (h1: _) pr (h2: _) qr. + disjE_realizer \ _ \ _ \ pq \ R \ pr \ qr \ c \ d \ e \ h1 \ h2" disjE (Q, R): "\pq pr qr. (case pq of None \ pr | Some q \ qr q)" - "\ P Q R pq (h1: _) pr (h2: _) qr. - disjE_realizer2 \ _ \ _ \ pq \ R \ pr \ qr \ h1 \ h2" + "\ (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr. + disjE_realizer2 \ _ \ _ \ pq \ R \ pr \ qr \ c \ d \ h1 \ h2" disjE (P, R): "\pq pr qr. (case pq of None \ qr | Some p \ pr p)" - "\ P Q R pq (h1: _) pr (h2: _) qr (h3: _). - disjE_realizer2 \ _ \ _ \ pq \ R \ qr \ pr \ h1 \ h3 \ h2" + "\ (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr (h3: _). + disjE_realizer2 \ _ \ _ \ pq \ R \ qr \ pr \ c \ d \ h1 \ h3 \ h2" disjE (R): "\pq pr qr. (case pq of Left \ pr | Right \ qr)" - "\ P Q R pq (h1: _) pr (h2: _) qr. - disjE_realizer3 \ _ \ _ \ pq \ R \ pr \ qr \ h1 \ h2" + "\ (c: _) P Q R pq (h1: _) pr (h2: _) qr. + disjE_realizer3 \ _ \ _ \ pq \ R \ pr \ qr \ c \ h1 \ h2" disjE (P, Q): "Null" - "\ P Q R pq. disjE_realizer \ _ \ _ \ pq \ (\x. R) \ _ \ _" + "\ (c: _) (d: _) P Q R pq. disjE_realizer \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ c \ d \ arity_type_bool" disjE (Q): "Null" - "\ P Q R pq. disjE_realizer2 \ _ \ _ \ pq \ (\x. R) \ _ \ _" + "\ (c: _) P Q R pq. disjE_realizer2 \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ c \ arity_type_bool" disjE (P): "Null" - "\ P Q R pq (h1: _) (h2: _) (h3: _). - disjE_realizer2 \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ h1 \ h3 \ h2" + "\ (c: _) P Q R pq (h1: _) (h2: _) (h3: _). + disjE_realizer2 \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ c \ arity_type_bool \ h1 \ h3 \ h2" disjE: "Null" - "\ P Q R pq. disjE_realizer3 \ _ \ _ \ pq \ (\x. R) \ _ \ _" + "\ P Q R pq. disjE_realizer3 \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ arity_type_bool" FalseE (P): "default" - "\ P. FalseE \ _" + "\ (c: _) P. FalseE \ _" FalseE: "Null" "FalseE" notI (P): "Null" - "\ P (h: _). allI \ _ \ (\ x. notI \ _ \ (h \ x))" + "\ (c: _) P (h: _). allI \ _ \ c \ (\ x. notI \ _ \ (h \ x))" notI: "Null" "notI" notE (P, R): "\p. default" - "\ P R (h: _) p. notE \ _ \ _ \ (spec \ _ \ p \ h)" + "\ (c: _) (d: _) P R (h: _) p. notE \ _ \ _ \ (spec \ _ \ p \ c \ h)" notE (P): "Null" - "\ P R (h: _) p. notE \ _ \ _ \ (spec \ _ \ p \ h)" + "\ (c: _) P R (h: _) p. notE \ _ \ _ \ (spec \ _ \ p \ c \ h)" notE (R): "default" - "\ P R. notE \ _ \ _" + "\ (c: _) P R. notE \ _ \ _" notE: "Null" "notE" subst (P): "\s t ps. ps" - "\ s t P (h: _) ps. subst \ s \ t \ P ps \ h" + "\ (c: _) s t P (d: _) (h: _) ps. subst \ s \ t \ P ps \ d \ h" subst: "Null" "subst" iffD1 (P, Q): "fst" - "\ Q P pq (h: _) p. - mp \ _ \ _ \ (spec \ _ \ p \ (conjunct1 \ _ \ _ \ h))" + "\ (d: _) (c: _) Q P pq (h: _) p. + mp \ _ \ _ \ (spec \ _ \ p \ d \ (conjunct1 \ _ \ _ \ h))" iffD1 (P): "\p. p" - "\ Q P p (h: _). mp \ _ \ _ \ (conjunct1 \ _ \ _ \ h)" + "\ (c: _) Q P p (h: _). mp \ _ \ _ \ (conjunct1 \ _ \ _ \ h)" iffD1 (Q): "Null" - "\ Q P q1 (h: _) q2. - mp \ _ \ _ \ (spec \ _ \ q2 \ (conjunct1 \ _ \ _ \ h))" + "\ (c: _) Q P q1 (h: _) q2. + mp \ _ \ _ \ (spec \ _ \ q2 \ c \ (conjunct1 \ _ \ _ \ h))" iffD1: "Null" "iffD1" iffD2 (P, Q): "snd" - "\ P Q pq (h: _) q. - mp \ _ \ _ \ (spec \ _ \ q \ (conjunct2 \ _ \ _ \ h))" + "\ (c: _) (d: _) P Q pq (h: _) q. + mp \ _ \ _ \ (spec \ _ \ q \ d \ (conjunct2 \ _ \ _ \ h))" iffD2 (P): "\p. p" - "\ P Q p (h: _). mp \ _ \ _ \ (conjunct2 \ _ \ _ \ h)" + "\ (c: _) P Q p (h: _). mp \ _ \ _ \ (conjunct2 \ _ \ _ \ h)" iffD2 (Q): "Null" - "\ P Q q1 (h: _) q2. - mp \ _ \ _ \ (spec \ _ \ q2 \ (conjunct2 \ _ \ _ \ h))" + "\ (c: _) P Q q1 (h: _) q2. + mp \ _ \ _ \ (spec \ _ \ q2 \ c \ (conjunct2 \ _ \ _ \ h))" iffD2: "Null" "iffD2" iffI (P, Q): "Pair" - "\ P Q pq (h1 : _) qp (h2 : _). conjI_realizer \ + "\ (c: _) (d: _) P Q pq (h1 : _) qp (h2 : _). conjI_realizer \ (\pq. \x. P x \ Q (pq x)) \ pq \ (\qp. \x. Q x \ P (qp x)) \ qp \ - (allI \ _ \ (\ x. impI \ _ \ _ \ (h1 \ x))) \ - (allI \ _ \ (\ x. impI \ _ \ _ \ (h2 \ x)))" + (arity_type_fun \ c \ d) \ + (arity_type_fun \ d \ c) \ + (allI \ _ \ c \ (\ x. impI \ _ \ _ \ (h1 \ x))) \ + (allI \ _ \ d \ (\ x. impI \ _ \ _ \ (h2 \ x)))" iffI (P): "\p. p" - "\ P Q (h1 : _) p (h2 : _). conjI \ _ \ _ \ - (allI \ _ \ (\ x. impI \ _ \ _ \ (h1 \ x))) \ + "\ (c: _) P Q (h1 : _) p (h2 : _). conjI \ _ \ _ \ + (allI \ _ \ c \ (\ x. impI \ _ \ _ \ (h1 \ x))) \ (impI \ _ \ _ \ h2)" iffI (Q): "\q. q" - "\ P Q q (h1 : _) (h2 : _). conjI \ _ \ _ \ + "\ (c: _) P Q q (h1 : _) (h2 : _). conjI \ _ \ _ \ (impI \ _ \ _ \ h1) \ - (allI \ _ \ (\ x. impI \ _ \ _ \ (h2 \ x)))" + (allI \ _ \ c \ (\ x. impI \ _ \ _ \ (h2 \ x)))" iffI: "Null" "iffI" -(* - classical: "Null" - "\ P. classical \ _" -*) - -setup {* - Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"}) -*} - end diff -r e0940e692abb -r 4a7fe945412d src/HOL/Lambda/WeakNorm.thy --- 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) diff -r e0940e692abb -r 4a7fe945412d src/HOL/Library/Char_nat.thy --- 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 diff -r e0940e692abb -r 4a7fe945412d src/HOL/Library/Code_Char.thy --- 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 \ char \ char \ bool" (SML "!((_ : char) = _)") (OCaml "!((_ : char) = _)") (Haskell infixl 4 "==") + (Scala infixl 5 "==") code_const "Code_Evaluation.term_of \ char \ 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 diff -r e0940e692abb -r 4a7fe945412d src/HOL/Library/Code_Char_chr.thy --- 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\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 diff -r e0940e692abb -r 4a7fe945412d src/HOL/Library/Efficient_Nat.thy --- 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) diff -r e0940e692abb -r 4a7fe945412d src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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 diff -r e0940e692abb -r 4a7fe945412d src/HOL/Tools/Datatype/datatype_data.ML --- 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); diff -r e0940e692abb -r 4a7fe945412d src/HOL/Tools/Datatype/datatype_realizer.ML --- 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 = diff -r e0940e692abb -r 4a7fe945412d src/HOL/Tools/Nitpick/nitpick.ML --- 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" *) diff -r e0940e692abb -r 4a7fe945412d src/HOL/Tools/inductive_realizer.ML --- 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 diff -r e0940e692abb -r 4a7fe945412d src/HOL/Tools/list_code.ML --- 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 diff -r e0940e692abb -r 4a7fe945412d src/HOL/Tools/rewrite_hol_proof.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/HOL/Word/WordDefinition.thy --- 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 \ 'a\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 \ 'a\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\" 60) + +instantiation word :: ("{len0, typerep}") random +begin + +definition + "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) o\ (\k. Pair ( + let j = word_of_int (Code_Numeral.int_of k) :: 'a word + in (j, \_::unit. Code_Evaluation.term_of j)))" + +instance .. + +end + +no_notation fcomp (infixl "o>" 60) +no_notation scomp (infixl "o\" 60) + subsection {* Type conversions and casting *} diff -r e0940e692abb -r 4a7fe945412d src/Pure/Concurrent/future.ML --- 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)); diff -r e0940e692abb -r 4a7fe945412d src/Pure/Concurrent/simple_thread.ML --- 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 = diff -r e0940e692abb -r 4a7fe945412d src/Pure/Concurrent/single_assignment.ML --- 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 => diff -r e0940e692abb -r 4a7fe945412d src/Pure/Concurrent/synchronized.ML --- 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 diff -r e0940e692abb -r 4a7fe945412d src/Pure/Concurrent/task_queue.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/General/scan.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/Isar/class_target.ML --- 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 diff -r e0940e692abb -r 4a7fe945412d src/Pure/Isar/isar_cmd.ML --- 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 diff -r e0940e692abb -r 4a7fe945412d src/Pure/Isar/isar_document.ML --- 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); diff -r e0940e692abb -r 4a7fe945412d src/Pure/Isar/isar_syn.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/Isar/method.ML --- 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); diff -r e0940e692abb -r 4a7fe945412d src/Pure/Isar/object_logic.ML --- 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); diff -r e0940e692abb -r 4a7fe945412d src/Pure/Isar/outer_syntax.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/Isar/proof_context.ML --- 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) => diff -r e0940e692abb -r 4a7fe945412d src/Pure/Isar/specification.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/Isar/toplevel.ML --- 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)); diff -r e0940e692abb -r 4a7fe945412d src/Pure/ML/ml_antiquote.ML --- 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 ()"); diff -r e0940e692abb -r 4a7fe945412d src/Pure/ML/ml_compiler_polyml-5.3.ML --- 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); diff -r e0940e692abb -r 4a7fe945412d src/Pure/ML/ml_lex.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/ML/ml_thms.ML --- 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 = diff -r e0940e692abb -r 4a7fe945412d src/Pure/Proof/extraction.ML --- 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)))))) diff -r e0940e692abb -r 4a7fe945412d src/Pure/Proof/proof_rewrite_rules.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/Proof/proof_syntax.ML --- 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 = diff -r e0940e692abb -r 4a7fe945412d src/Pure/Proof/proofchecker.ML --- 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) diff -r e0940e692abb -r 4a7fe945412d src/Pure/Proof/reconstruct.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/ProofGeneral/pgip_isabelle.ML --- 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); diff -r e0940e692abb -r 4a7fe945412d src/Pure/ProofGeneral/pgip_parser.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/ProofGeneral/proof_general_emacs.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 (" 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 diff -r e0940e692abb -r 4a7fe945412d src/Pure/ROOT.ML --- 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*) + + diff -r e0940e692abb -r 4a7fe945412d src/Pure/Syntax/mixfix.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/Syntax/parser.ML --- 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 **) diff -r e0940e692abb -r 4a7fe945412d src/Pure/Syntax/printer.ML --- 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)) diff -r e0940e692abb -r 4a7fe945412d src/Pure/Syntax/syn_ext.ML --- 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), diff -r e0940e692abb -r 4a7fe945412d src/Pure/Syntax/syn_trans.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/Syntax/syntax.ML --- 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"; diff -r e0940e692abb -r 4a7fe945412d src/Pure/Syntax/type_ext.ML --- 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')]) [] ([], []); diff -r e0940e692abb -r 4a7fe945412d src/Pure/System/isabelle_process.ML --- 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"; diff -r e0940e692abb -r 4a7fe945412d src/Pure/System/isar.ML --- 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 diff -r e0940e692abb -r 4a7fe945412d src/Pure/System/session.ML --- 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 (); diff -r e0940e692abb -r 4a7fe945412d src/Pure/Thy/present.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/Thy/thm_deps.ML --- 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 "" => [] diff -r e0940e692abb -r 4a7fe945412d src/Pure/Thy/thy_info.ML --- 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 () => diff -r e0940e692abb -r 4a7fe945412d src/Pure/Thy/thy_load.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/Thy/thy_output.ML --- 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 **) diff -r e0940e692abb -r 4a7fe945412d src/Pure/Thy/thy_syntax.ML --- 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 **) diff -r e0940e692abb -r 4a7fe945412d src/Pure/axclass.ML --- 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); diff -r e0940e692abb -r 4a7fe945412d src/Pure/context.ML --- 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 = diff -r e0940e692abb -r 4a7fe945412d src/Pure/logic.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/morphism.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Pure/proofterm.ML --- 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, _) = diff -r e0940e692abb -r 4a7fe945412d src/Pure/pure_setup.ML --- 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 *) diff -r e0940e692abb -r 4a7fe945412d src/Pure/pure_thy.ML --- 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), diff -r e0940e692abb -r 4a7fe945412d src/Pure/simplifier.ML --- 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 *) diff -r e0940e692abb -r 4a7fe945412d src/Pure/type_infer.ML --- 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 *) diff -r e0940e692abb -r 4a7fe945412d src/Tools/Code/code_eval.ML --- 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 diff -r e0940e692abb -r 4a7fe945412d src/Tools/Code/code_haskell.ML --- 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", diff -r e0940e692abb -r 4a7fe945412d src/Tools/Code/code_ml.ML --- 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"] diff -r e0940e692abb -r 4a7fe945412d src/Tools/Code/code_printer.ML --- 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 = diff -r e0940e692abb -r 4a7fe945412d src/Tools/Code/code_scala.ML --- 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" diff -r e0940e692abb -r 4a7fe945412d src/Tools/Code/code_thingol.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Tools/Code/lib/Tools/codegen --- 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" diff -r e0940e692abb -r 4a7fe945412d src/Tools/WWW_Find/find_theorems.ML --- 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; diff -r e0940e692abb -r 4a7fe945412d src/Tools/jEdit/README --- /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 diff -r e0940e692abb -r 4a7fe945412d src/Tools/jEdit/README_BUILD --- 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. diff -r e0940e692abb -r 4a7fe945412d src/Tools/jEdit/makedist --- 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,\n\n,;