# HG changeset patch # User wenzelm # Date 1346149330 -7200 # Node ID d54a3d39ba85f4cd95e9944dadf8d0ab814b804a # Parent a0aca6d0498ef00f47d159cd421f9623582337bb prefer doc-src/pdfsetup.sty; moved IsarRef/Thy/ZF_Specific.thy to ZF/ZF_Isar.thy to avoid dependence of IsarRef on another object-logic; diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/Classes/document/build --- a/doc-src/Classes/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/Classes/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -15,6 +15,8 @@ cp "$ISABELLE_HOME/doc-src/manual.bib" . "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/Codegen/document/build --- a/doc-src/Codegen/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/Codegen/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -22,6 +22,8 @@ done "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/Functions/document/build --- a/doc-src/Functions/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/Functions/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -11,6 +11,8 @@ cp "$ISABELLE_HOME/doc-src/manual.bib" . "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/HOL/document/build --- a/doc-src/HOL/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/HOL/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -16,6 +16,8 @@ cp "$ISABELLE_HOME/doc-src/Logics/document/syntax.tex" . "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/Intro/document/build --- a/doc-src/Intro/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/Intro/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -15,6 +15,8 @@ cp "$ISABELLE_HOME/doc-src/manual.bib" . "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/IsarImplementation/document/build --- a/doc-src/IsarImplementation/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/IsarImplementation/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -17,6 +17,8 @@ cp "$ISABELLE_HOME/doc-src/manual.bib" . "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/IsarRef/Makefile --- a/doc-src/IsarRef/Makefile Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/IsarRef/Makefile Tue Aug 28 12:22:10 2012 +0200 @@ -14,7 +14,7 @@ Thy/document/HOL_Specific.tex Thy/document/ML_Tactic.tex \ Thy/document/Proof.tex Thy/document/Quick_Reference.tex \ Thy/document/Spec.tex Thy/document/Synopsis.tex \ - Thy/document/ZF_Specific.tex Thy/document/Inner_Syntax.tex \ + Thy/document/Inner_Syntax.tex \ Thy/document/Preface.tex Thy/document/Document_Preparation.tex \ Thy/document/Misc.tex Thy/document/Outer_Syntax.tex \ Thy/document/Symbols.tex ../isar.sty ../proof.sty ../iman.sty \ diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/IsarRef/Thy/Base.thy --- a/doc-src/IsarRef/Thy/Base.thy Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/IsarRef/Thy/Base.thy Tue Aug 28 12:22:10 2012 +0200 @@ -3,12 +3,6 @@ begin ML_file "../../antiquote_setup.ML" - -setup {* - Antiquote_Setup.setup #> - member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup -*} - -declare [[thy_output_source]] +setup Antiquote_Setup.setup end diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/IsarRef/Thy/ZF_Specific.thy --- a/doc-src/IsarRef/Thy/ZF_Specific.thy Mon Aug 27 23:37:16 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,135 +0,0 @@ -theory ZF_Specific -imports Base Main -begin - -chapter {* Isabelle/ZF \label{ch:zf} *} - -section {* Type checking *} - -text {* - The ZF logic is essentially untyped, so the concept of ``type - checking'' is performed as logical reasoning about set-membership - statements. A special method assists users in this task; a version - of this is already declared as a ``solver'' in the standard - Simplifier setup. - - \begin{matharray}{rcl} - @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{method_def (ZF) typecheck} & : & @{text method} \\ - @{attribute_def (ZF) TC} & : & @{text attribute} \\ - \end{matharray} - - @{rail " - @@{attribute (ZF) TC} (() | 'add' | 'del') - "} - - \begin{description} - - \item @{command (ZF) "print_tcset"} prints the collection of - typechecking rules of the current context. - - \item @{method (ZF) typecheck} attempts to solve any pending - type-checking problems in subgoals. - - \item @{attribute (ZF) TC} adds or deletes type-checking rules from - the context. - - \end{description} -*} - - -section {* (Co)Inductive sets and datatypes *} - -subsection {* Set definitions *} - -text {* - In ZF everything is a set. The generic inductive package also - provides a specific view for ``datatype'' specifications. - Coinductive definitions are available in both cases, too. - - \begin{matharray}{rcl} - @{command_def (ZF) "inductive"} & : & @{text "theory \ theory"} \\ - @{command_def (ZF) "coinductive"} & : & @{text "theory \ theory"} \\ - @{command_def (ZF) "datatype"} & : & @{text "theory \ theory"} \\ - @{command_def (ZF) "codatatype"} & : & @{text "theory \ theory"} \\ - \end{matharray} - - @{rail " - (@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints - ; - - domains: @'domains' (@{syntax term} + '+') ('<=' | '\') @{syntax term} - ; - intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +) - ; - hints: @{syntax (ZF) \"monos\"}? condefs? \\ - @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? - ; - @{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs} - ; - condefs: @'con_defs' @{syntax thmrefs} - ; - @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs} - ; - @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs} - "} - - In the following syntax specification @{text "monos"}, @{text - typeintros}, and @{text typeelims} are the same as above. - - @{rail " - (@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints - ; - - domain: ('<=' | '\') @{syntax term} - ; - dtspec: @{syntax term} '=' (con + '|') - ; - con: @{syntax name} ('(' (@{syntax term} ',' +) ')')? - ; - hints: @{syntax (ZF) \"monos\"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? - "} - - See \cite{isabelle-ZF} for further information on inductive - definitions in ZF, but note that this covers the old-style theory - format. -*} - - -subsection {* Primitive recursive functions *} - -text {* - \begin{matharray}{rcl} - @{command_def (ZF) "primrec"} & : & @{text "theory \ theory"} \\ - \end{matharray} - - @{rail " - @@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +) - "} -*} - - -subsection {* Cases and induction: emulating tactic scripts *} - -text {* - The following important tactical tools of Isabelle/ZF have been - ported to Isar. These should not be used in proper proof texts. - - \begin{matharray}{rcl} - @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & @{text method} \\ - @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\ - @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\ - @{command_def (ZF) "inductive_cases"} & : & @{text "theory \ theory"} \\ - \end{matharray} - - @{rail " - (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name} - ; - @@{method (ZF) ind_cases} (@{syntax prop} +) - ; - @@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and') - ; - "} -*} - -end diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/IsarRef/Thy/document/ZF_Specific.tex --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Mon Aug 27 23:37:16 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,334 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{ZF{\isaliteral{5F}{\isacharunderscore}}Specific}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{theory}\isamarkupfalse% -\ ZF{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline -\isakeyword{imports}\ Base\ Main\isanewline -\isakeyword{begin}% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isamarkupchapter{Isabelle/ZF \label{ch:zf}% -} -\isamarkuptrue% -% -\isamarkupsection{Type checking% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -The ZF logic is essentially untyped, so the concept of ``type - checking'' is performed as logical reasoning about set-membership - statements. A special method assists users in this task; a version - of this is already declared as a ``solver'' in the standard - Simplifier setup. - - \begin{matharray}{rcl} - \indexdef{ZF}{command}{print\_tcset}\hypertarget{command.ZF.print-tcset}{\hyperlink{command.ZF.print-tcset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}tcset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ - \indexdef{ZF}{method}{typecheck}\hypertarget{method.ZF.typecheck}{\hyperlink{method.ZF.typecheck}{\mbox{\isa{typecheck}}}} & : & \isa{method} \\ - \indexdef{ZF}{attribute}{TC}\hypertarget{attribute.ZF.TC}{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}} & : & \isa{attribute} \\ - \end{matharray} - - \begin{railoutput} -\rail@begin{3}{} -\rail@term{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}}[] -\rail@bar -\rail@nextbar{1} -\rail@term{\isa{add}}[] -\rail@nextbar{2} -\rail@term{\isa{del}}[] -\rail@endbar -\rail@end -\end{railoutput} - - - \begin{description} - - \item \hyperlink{command.ZF.print-tcset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}tcset}}}} prints the collection of - typechecking rules of the current context. - - \item \hyperlink{method.ZF.typecheck}{\mbox{\isa{typecheck}}} attempts to solve any pending - type-checking problems in subgoals. - - \item \hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}} adds or deletes type-checking rules from - the context. - - \end{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsection{(Co)Inductive sets and datatypes% -} -\isamarkuptrue% -% -\isamarkupsubsection{Set definitions% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -In ZF everything is a set. The generic inductive package also - provides a specific view for ``datatype'' specifications. - Coinductive definitions are available in both cases, too. - - \begin{matharray}{rcl} - \indexdef{ZF}{command}{inductive}\hypertarget{command.ZF.inductive}{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ - \indexdef{ZF}{command}{coinductive}\hypertarget{command.ZF.coinductive}{\hyperlink{command.ZF.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ - \indexdef{ZF}{command}{datatype}\hypertarget{command.ZF.datatype}{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ - \indexdef{ZF}{command}{codatatype}\hypertarget{command.ZF.codatatype}{\hyperlink{command.ZF.codatatype}{\mbox{\isa{\isacommand{codatatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ - \end{matharray} - - \begin{railoutput} -\rail@begin{2}{} -\rail@bar -\rail@term{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[] -\rail@nextbar{1} -\rail@term{\hyperlink{command.ZF.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[] -\rail@endbar -\rail@nont{\isa{domains}}[] -\rail@nont{\isa{intros}}[] -\rail@nont{\isa{hints}}[] -\rail@end -\rail@begin{2}{\isa{domains}} -\rail@term{\isa{\isakeyword{domains}}}[] -\rail@plus -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] -\rail@nextplus{1} -\rail@cterm{\isa{{\isaliteral{2B}{\isacharplus}}}}[] -\rail@endplus -\rail@bar -\rail@term{\isa{{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}}}[] -\rail@nextbar{1} -\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[] -\rail@endbar -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] -\rail@end -\rail@begin{3}{\isa{intros}} -\rail@term{\isa{\isakeyword{intros}}}[] -\rail@plus -\rail@bar -\rail@nextbar{1} -\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[] -\rail@endbar -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] -\rail@nextplus{2} -\rail@endplus -\rail@end -\rail@begin{5}{\isa{hints}} -\rail@bar -\rail@nextbar{1} -\rail@nont{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}[] -\rail@endbar -\rail@bar -\rail@nextbar{1} -\rail@nont{\isa{condefs}}[] -\rail@endbar -\rail@cr{3} -\rail@bar -\rail@nextbar{4} -\rail@nont{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}[] -\rail@endbar -\rail@bar -\rail@nextbar{4} -\rail@nont{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}[] -\rail@endbar -\rail@end -\rail@begin{1}{\indexdef{ZF}{syntax}{monos}\hypertarget{syntax.ZF.monos}{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}} -\rail@term{\isa{\isakeyword{monos}}}[] -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] -\rail@end -\rail@begin{1}{\isa{condefs}} -\rail@term{\isa{\isakeyword{con{\isaliteral{5F}{\isacharunderscore}}defs}}}[] -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] -\rail@end -\rail@begin{1}{\indexdef{ZF}{syntax}{typeintros}\hypertarget{syntax.ZF.typeintros}{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}} -\rail@term{\isa{\isakeyword{type{\isaliteral{5F}{\isacharunderscore}}intros}}}[] -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] -\rail@end -\rail@begin{1}{\indexdef{ZF}{syntax}{typeelims}\hypertarget{syntax.ZF.typeelims}{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}} -\rail@term{\isa{\isakeyword{type{\isaliteral{5F}{\isacharunderscore}}elims}}}[] -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] -\rail@end -\end{railoutput} - - - In the following syntax specification \isa{{\isaliteral{22}{\isachardoublequote}}monos{\isaliteral{22}{\isachardoublequote}}}, \isa{typeintros}, and \isa{typeelims} are the same as above. - - \begin{railoutput} -\rail@begin{2}{} -\rail@bar -\rail@term{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[] -\rail@nextbar{1} -\rail@term{\hyperlink{command.ZF.codatatype}{\mbox{\isa{\isacommand{codatatype}}}}}[] -\rail@endbar -\rail@bar -\rail@nextbar{1} -\rail@nont{\isa{domain}}[] -\rail@endbar -\rail@plus -\rail@nont{\isa{dtspec}}[] -\rail@nextplus{1} -\rail@cterm{\isa{\isakeyword{and}}}[] -\rail@endplus -\rail@nont{\isa{hints}}[] -\rail@end -\rail@begin{2}{\isa{domain}} -\rail@bar -\rail@term{\isa{{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}}}[] -\rail@nextbar{1} -\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[] -\rail@endbar -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] -\rail@end -\rail@begin{2}{\isa{dtspec}} -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] -\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[] -\rail@plus -\rail@nont{\isa{con}}[] -\rail@nextplus{1} -\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[] -\rail@endplus -\rail@end -\rail@begin{3}{\isa{con}} -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] -\rail@bar -\rail@nextbar{1} -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] -\rail@plus -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] -\rail@term{\isa{{\isaliteral{2C}{\isacharcomma}}}}[] -\rail@nextplus{2} -\rail@endplus -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] -\rail@endbar -\rail@end -\rail@begin{2}{\isa{hints}} -\rail@bar -\rail@nextbar{1} -\rail@nont{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}[] -\rail@endbar -\rail@bar -\rail@nextbar{1} -\rail@nont{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}[] -\rail@endbar -\rail@bar -\rail@nextbar{1} -\rail@nont{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}[] -\rail@endbar -\rail@end -\end{railoutput} - - - See \cite{isabelle-ZF} for further information on inductive - definitions in ZF, but note that this covers the old-style theory - format.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Primitive recursive functions% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -\begin{matharray}{rcl} - \indexdef{ZF}{command}{primrec}\hypertarget{command.ZF.primrec}{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ - \end{matharray} - - \begin{railoutput} -\rail@begin{3}{} -\rail@term{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[] -\rail@plus -\rail@bar -\rail@nextbar{1} -\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[] -\rail@endbar -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] -\rail@nextplus{2} -\rail@endplus -\rail@end -\end{railoutput}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Cases and induction: emulating tactic scripts% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -The following important tactical tools of Isabelle/ZF have been - ported to Isar. These should not be used in proper proof texts. - - \begin{matharray}{rcl} - \indexdef{ZF}{method}{case\_tac}\hypertarget{method.ZF.case-tac}{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\ - \indexdef{ZF}{method}{induct\_tac}\hypertarget{method.ZF.induct-tac}{\hyperlink{method.ZF.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\ - \indexdef{ZF}{method}{ind\_cases}\hypertarget{method.ZF.ind-cases}{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\ - \indexdef{ZF}{command}{inductive\_cases}\hypertarget{command.ZF.inductive-cases}{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ - \end{matharray} - - \begin{railoutput} -\rail@begin{2}{} -\rail@bar -\rail@term{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[] -\rail@nextbar{1} -\rail@term{\hyperlink{method.ZF.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[] -\rail@endbar -\rail@bar -\rail@nextbar{1} -\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[] -\rail@endbar -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] -\rail@end -\rail@begin{2}{} -\rail@term{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[] -\rail@plus -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] -\rail@nextplus{1} -\rail@endplus -\rail@end -\rail@begin{3}{} -\rail@term{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[] -\rail@plus -\rail@bar -\rail@nextbar{1} -\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[] -\rail@endbar -\rail@plus -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] -\rail@nextplus{1} -\rail@endplus -\rail@nextplus{2} -\rail@cterm{\isa{\isakeyword{and}}}[] -\rail@endplus -\rail@end -\end{railoutput}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{end}\isamarkupfalse% -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\isanewline -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/IsarRef/isar-ref.tex Tue Aug 28 12:22:10 2012 +0200 @@ -72,7 +72,6 @@ \part{Object-Logics} \input{Thy/document/HOL_Specific.tex} \input{Thy/document/HOLCF_Specific.tex} -\input{Thy/document/ZF_Specific.tex} \part{Appendix} \appendix diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/LaTeXsugar/document/build --- a/doc-src/LaTeXsugar/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/LaTeXsugar/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -6,6 +6,8 @@ VARIANT="$2" "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/Locales/document/build --- a/doc-src/Locales/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/Locales/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -6,6 +6,8 @@ VARIANT="$2" "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/Logics/document/build --- a/doc-src/Logics/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/Logics/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -15,6 +15,8 @@ cp "$ISABELLE_HOME/doc-src/manual.bib" . "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/Main/document/build --- a/doc-src/Main/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/Main/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -6,6 +6,8 @@ VARIANT="$2" "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/ProgProve/document/build --- a/doc-src/ProgProve/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/ProgProve/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -11,6 +11,8 @@ cp "$ISABELLE_HOME/doc-src/ProgProve/MyList.thy" . "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/ROOT --- a/doc-src/ROOT Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/ROOT Tue Aug 28 12:22:10 2012 +0200 @@ -3,6 +3,7 @@ theories [document = false] Setup theories Classes files + "../pdfsetup.sty" "document/build" "document/root.tex" "document/style.sty" @@ -19,6 +20,7 @@ Adaptation Further files + "../pdfsetup.sty" "document/adapt.tex" "document/architecture.tex" "document/build" @@ -29,6 +31,7 @@ options [document_variants = "functions"] theories Functions files + "../pdfsetup.sty" "../iman.sty" "../extra.sty" "../isar.sty" @@ -54,6 +57,7 @@ Syntax Tactic files + "../pdfsetup.sty" "../iman.sty" "../extra.sty" "../isar.sty" @@ -69,6 +73,7 @@ options [document_variants = "intro"] theories files + "../pdfsetup.sty" "../iman.sty" "../extra.sty" "../ttbox.sty" @@ -80,7 +85,7 @@ session "HOL-IsarRef" (doc) in "IsarRef/Thy" = HOL + options [browser_info = false, document = false, document_dump = document, document_dump_mode = "tex", - quick_and_dirty] + quick_and_dirty, thy_output_source] theories Preface Synopsis @@ -101,15 +106,9 @@ session "HOLCF-IsarRef" (doc) in "IsarRef/Thy" = HOLCF + options [browser_info = false, document = false, document_dump = document, document_dump_mode = "tex", - quick_and_dirty] + quick_and_dirty, thy_output_source] theories HOLCF_Specific -session "ZF-IsarRef" (doc) in "IsarRef/Thy" = ZF + - options [browser_info = false, document = false, - document_dump = document, document_dump_mode = "tex", - quick_and_dirty] - theories ZF_Specific - session LaTeXsugar (doc) in "LaTeXsugar" = HOL + options [document_variants = "sugar"] theories [document = ""] @@ -117,6 +116,7 @@ "~~/src/HOL/Library/OptionalSugar" theories Sugar files + "../pdfsetup.sty" "document/build" "document/mathpartir.sty" "document/root.bib" @@ -129,6 +129,7 @@ Examples2 Examples3 files + "../pdfsetup.sty" "document/build" "document/root.tex" @@ -136,6 +137,7 @@ options [document_variants = "logics"] theories files + "../pdfsetup.sty" "../iman.sty" "../extra.sty" "../ttbox.sty" @@ -148,6 +150,7 @@ options [document_variants = "logics-HOL"] theories files + "../pdfsetup.sty" "../iman.sty" "../extra.sty" "../ttbox.sty" @@ -158,13 +161,17 @@ "document/root.tex" session "Logics-ZF" (doc) in "ZF" = ZF + - options [document_variants = "logics-ZF", print_mode = "brackets"] + options [document_variants = "logics-ZF", print_mode = "brackets", + thy_output_source] theories IFOL_examples FOL_examples ZF_examples If + ZF_Isar files + "../pdfsetup.sty" + "../isar.sty" "../ttbox.sty" "../proof.sty" "../manual.bib" @@ -176,6 +183,7 @@ options [document_variants = "main"] theories Main_Doc files + "../pdfsetup.sty" "document/build" "document/root.tex" @@ -189,6 +197,7 @@ Logic Isar files + "../pdfsetup.sty" "document/bang.eps" "document/bang.pdf" "document/build" @@ -203,6 +212,7 @@ options [document_variants = "ref"] theories files + "../pdfsetup.sty" "../iman.sty" "../extra.sty" "../ttbox.sty" @@ -228,6 +238,7 @@ Misc files "../IsarRef/style.sty" + "../pdfsetup.sty" "../iman.sty" "../extra.sty" "../ttbox.sty" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/Ref/document/build --- a/doc-src/Ref/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/Ref/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -15,6 +15,8 @@ cp "$ISABELLE_HOME/doc-src/manual.bib" . "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/System/document/build --- a/doc-src/System/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/System/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -17,6 +17,8 @@ cp "$ISABELLE_HOME/doc-src/manual.bib" . "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/ZF/ZF_Isar.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/ZF/ZF_Isar.thy Tue Aug 28 12:22:10 2012 +0200 @@ -0,0 +1,140 @@ +theory ZF_Isar +imports Main +begin + +(*<*) +ML_file "../antiquote_setup.ML" +setup Antiquote_Setup.setup +(*>*) + +chapter {* Some Isar language elements *} + +section {* Type checking *} + +text {* + The ZF logic is essentially untyped, so the concept of ``type + checking'' is performed as logical reasoning about set-membership + statements. A special method assists users in this task; a version + of this is already declared as a ``solver'' in the standard + Simplifier setup. + + \begin{matharray}{rcl} + @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{method_def (ZF) typecheck} & : & @{text method} \\ + @{attribute_def (ZF) TC} & : & @{text attribute} \\ + \end{matharray} + + @{rail " + @@{attribute (ZF) TC} (() | 'add' | 'del') + "} + + \begin{description} + + \item @{command (ZF) "print_tcset"} prints the collection of + typechecking rules of the current context. + + \item @{method (ZF) typecheck} attempts to solve any pending + type-checking problems in subgoals. + + \item @{attribute (ZF) TC} adds or deletes type-checking rules from + the context. + + \end{description} +*} + + +section {* (Co)Inductive sets and datatypes *} + +subsection {* Set definitions *} + +text {* + In ZF everything is a set. The generic inductive package also + provides a specific view for ``datatype'' specifications. + Coinductive definitions are available in both cases, too. + + \begin{matharray}{rcl} + @{command_def (ZF) "inductive"} & : & @{text "theory \ theory"} \\ + @{command_def (ZF) "coinductive"} & : & @{text "theory \ theory"} \\ + @{command_def (ZF) "datatype"} & : & @{text "theory \ theory"} \\ + @{command_def (ZF) "codatatype"} & : & @{text "theory \ theory"} \\ + \end{matharray} + + @{rail " + (@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints + ; + + domains: @'domains' (@{syntax term} + '+') ('<=' | '\') @{syntax term} + ; + intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +) + ; + hints: @{syntax (ZF) \"monos\"}? condefs? \\ + @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? + ; + @{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs} + ; + condefs: @'con_defs' @{syntax thmrefs} + ; + @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs} + ; + @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs} + "} + + In the following syntax specification @{text "monos"}, @{text + typeintros}, and @{text typeelims} are the same as above. + + @{rail " + (@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints + ; + + domain: ('<=' | '\') @{syntax term} + ; + dtspec: @{syntax term} '=' (con + '|') + ; + con: @{syntax name} ('(' (@{syntax term} ',' +) ')')? + ; + hints: @{syntax (ZF) \"monos\"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}? + "} + + See \cite{isabelle-ZF} for further information on inductive + definitions in ZF, but note that this covers the old-style theory + format. +*} + + +subsection {* Primitive recursive functions *} + +text {* + \begin{matharray}{rcl} + @{command_def (ZF) "primrec"} & : & @{text "theory \ theory"} \\ + \end{matharray} + + @{rail " + @@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +) + "} +*} + + +subsection {* Cases and induction: emulating tactic scripts *} + +text {* + The following important tactical tools of Isabelle/ZF have been + ported to Isar. These should not be used in proper proof texts. + + \begin{matharray}{rcl} + @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & @{text method} \\ + @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\ + @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\ + @{command_def (ZF) "inductive_cases"} & : & @{text "theory \ theory"} \\ + \end{matharray} + + @{rail " + (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name} + ; + @@{method (ZF) ind_cases} (@{syntax prop} +) + ; + @@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and') + ; + "} +*} + +end diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/ZF/document/build --- a/doc-src/ZF/document/build Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/ZF/document/build Tue Aug 28 12:22:10 2012 +0200 @@ -8,12 +8,15 @@ "$ISABELLE_TOOL" logo -o isabelle_zf.pdf "ZF" "$ISABELLE_TOOL" logo -o isabelle_zf.eps "ZF" +cp "$ISABELLE_HOME/doc-src/isar.sty" . cp "$ISABELLE_HOME/doc-src/ttbox.sty" . cp "$ISABELLE_HOME/doc-src/proof.sty" . cp "$ISABELLE_HOME/doc-src/manual.bib" . cp "$ISABELLE_HOME/doc-src/Logics/document/syntax.tex" . "$ISABELLE_TOOL" latex -o sty +cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" . + "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r a0aca6d0498e -r d54a3d39ba85 doc-src/ZF/document/root.tex --- a/doc-src/ZF/document/root.tex Mon Aug 27 23:37:16 2012 +0200 +++ b/doc-src/ZF/document/root.tex Tue Aug 28 12:22:10 2012 +0200 @@ -1,6 +1,7 @@ \documentclass[11pt,a4paper]{report} -\usepackage{isabelle,isabellesym} +\usepackage{isabelle,isabellesym,railsetup} \usepackage{graphicx,logics,ttbox,proof,latexsym} +\usepackage{isar} \usepackage{pdfsetup} %last package! @@ -36,6 +37,14 @@ \sloppy \binperiod %%%treat . like a binary operator + +\isadroptag{theory} + +\railtermfont{\isabellestyle{tt}} +\railnontermfont{\isabellestyle{literal}} +\railnamefont{\isabellestyle{literal}} + + \begin{document} \maketitle @@ -71,6 +80,11 @@ \input{syntax} \include{FOL} \include{ZF} + +\isabellestyle{literal} +\include{ZF_Isar} +\isabellestyle{tt} + \bibliographystyle{plain} \bibliography{manual} \printindex