# HG changeset patch # User wenzelm # Date 1210789877 -7200 # Node ID 1120f6cc10b011006bdcf59e0794cd64594851c4 # Parent 44d9960d358756b6e6d3b709a1cf1dfd53506156 proper checking of various Isar elements; diff -r 44d9960d3587 -r 1120f6cc10b0 doc-src/IsarRef/Thy/Generic.thy --- a/doc-src/IsarRef/Thy/Generic.thy Wed May 14 20:30:53 2008 +0200 +++ b/doc-src/IsarRef/Thy/Generic.thy Wed May 14 20:31:17 2008 +0200 @@ -1,7 +1,7 @@ (* $Id$ *) theory Generic -imports CPure +imports Main begin chapter {* Generic tools and packages \label{ch:gen-tools} *} diff -r 44d9960d3587 -r 1120f6cc10b0 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 14 20:30:53 2008 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 14 20:31:17 2008 +0200 @@ -53,10 +53,10 @@ corresponding injection/surjection pair (in both directions). Rules @{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly more convenient view on the injectivity part, suitable for automated - proof tools (e.g.\ in @{method simp} or @{method iff} declarations). - Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and @{text - Abs_t_cases}/@{text Abs_t_induct} provide alternative views on - surjectivity; these are already declared as set or type rules for + proof tools (e.g.\ in @{attribute simp} or @{attribute iff} + declarations). Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and + @{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views + on surjectivity; these are already declared as set or type rules for the generic @{method cases} and @{method induct} methods. An alternative name may be specified in parentheses; the default is @@ -89,7 +89,7 @@ \begin{descr} - \item [@{method (HOL) split_format}~@{text "p\<^sub>1 \ p\<^sub>m + \item [@{attribute (HOL) split_format}~@{text "p\<^sub>1 \ p\<^sub>m \ \ \ q\<^sub>1 \ q\<^sub>n"}] puts expressions of low-level tuple types into canonical form as specified by the arguments given; the @{text i}-th collection of arguments refers to @@ -813,15 +813,15 @@ text {* \begin{matharray}{rcl} @{method_def (HOL) arith} & : & \isarmeth \\ - @{method_def (HOL) arith_split} & : & \isaratt \\ + @{attribute_def (HOL) arith_split} & : & \isaratt \\ \end{matharray} The @{method (HOL) arith} method decides linear arithmetic problems (on types @{text nat}, @{text int}, @{text real}). Any current facts are inserted into the goal before running the procedure. - The @{method (HOL) arith_split} attribute declares case split rules - to be expanded before the arithmetic procedure is invoked. + The @{attribute (HOL) arith_split} attribute declares case split + rules to be expanded before the arithmetic procedure is invoked. Note that a simpler (but faster) version of arithmetic reasoning is already performed by the Simplifier. diff -r 44d9960d3587 -r 1120f6cc10b0 doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Wed May 14 20:30:53 2008 +0200 +++ b/doc-src/IsarRef/Thy/Proof.thy Wed May 14 20:31:17 2008 +0200 @@ -784,7 +784,7 @@ multi-step tactic script for @{command "qed"}, but may be given anywhere within the proof body. - No facts are passed to @{method m} here. Furthermore, the static + No facts are passed to @{text m} here. Furthermore, the static context is that of the enclosing goal (as for actual @{command "qed"}). Thus the proof method may not refer to any assumptions introduced in the current body, for example. @@ -1020,7 +1020,7 @@ \item [@{attribute trans}] declares theorems as transitivity rules. \item [@{attribute sym}] declares symmetry rules, as well as - @{attribute "Pure.elim?"} rules. + @{attribute "Pure.elim"}@{text "?"} rules. \item [@{attribute symmetric}] resolves a theorem with some rule declared as @{attribute sym} in the current context. For example, diff -r 44d9960d3587 -r 1120f6cc10b0 doc-src/IsarRef/Thy/ZF_Specific.thy --- a/doc-src/IsarRef/Thy/ZF_Specific.thy Wed May 14 20:30:53 2008 +0200 +++ b/doc-src/IsarRef/Thy/ZF_Specific.thy Wed May 14 20:31:17 2008 +0200 @@ -1,7 +1,7 @@ (* $Id$ *) theory ZF_Specific -imports ZF +imports Main begin chapter {* Isabelle/ZF \label{ch:zf} *} diff -r 44d9960d3587 -r 1120f6cc10b0 doc-src/IsarRef/Thy/pure.thy --- a/doc-src/IsarRef/Thy/pure.thy Wed May 14 20:30:53 2008 +0200 +++ b/doc-src/IsarRef/Thy/pure.thy Wed May 14 20:31:17 2008 +0200 @@ -731,7 +731,7 @@ @{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ @{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ @{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "thms_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "thm_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ \end{matharray} @@ -795,7 +795,7 @@ yields \emph{all} currently known facts. An optional limit for the number of printed facts may be given; the default is 40. By default, duplicates are removed from the search result. Use - @{keyword "with_dups"} to display duplicates. + @{text with_dups} to display duplicates. \item [@{command "thm_deps"}~@{text "a\<^sub>1 \ a\<^sub>n"}] visualizes dependencies of facts, using Isabelle's graph browser diff -r 44d9960d3587 -r 1120f6cc10b0 doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Wed May 14 20:30:53 2008 +0200 +++ b/doc-src/antiquote_setup.ML Wed May 14 20:31:17 2008 +0200 @@ -138,42 +138,50 @@ local +fun no_check _ _ = true; + +fun thy_check intern defined ctxt = + let val thy = ProofContext.theory_of ctxt + in defined thy o intern thy end; + val arg = enclose "{" "}" o clean_string; -fun output_entity markup index kind ctxt (logic, name) = - (case index of - NONE => "" - | SOME is_def => - "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name) - ^ - (Output.output name - |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") - |> (if ! O.quotes then quote else I) - |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" - else enclose "\\mbox{\\isa{" "}}")); +fun output_entity check markup index kind ctxt (logic, name) = + if check ctxt name then + (case index of + NONE => "" + | SOME is_def => + "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name) + ^ + (Output.output name + |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") + |> (if ! O.quotes then quote else I) + |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" + else enclose "\\mbox{\\isa{" "}}")) + else error ("Undefined " ^ kind ^ " " ^ quote name); -fun entity markup index kind = +fun entity check markup index kind = O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name)) - (K (output_entity markup index kind)); + (K (output_entity check markup index kind)); -fun entity_antiqs markup kind = - [(kind, entity markup NONE kind), - (kind ^ "_def", entity markup (SOME true) kind), - (kind ^ "_ref", entity markup (SOME false) kind)]; +fun entity_antiqs check markup kind = + [(kind, entity check markup NONE kind), + (kind ^ "_def", entity check markup (SOME true) kind), + (kind ^ "_ref", entity check markup (SOME false) kind)]; in val _ = O.add_commands - (entity_antiqs "" "syntax" @ - entity_antiqs "isacommand" "command" @ - entity_antiqs "isakeyword" "keyword" @ - entity_antiqs "isakeyword" "element" @ - entity_antiqs "" "method" @ - entity_antiqs "" "attribute" @ - entity_antiqs "" "fact" @ - entity_antiqs "" "variable" @ - entity_antiqs "" "case" @ - entity_antiqs "" "antiquotation"); + (entity_antiqs no_check "" "syntax" @ + entity_antiqs (K (is_some o OuterSyntax.command_keyword)) "isacommand" "command" @ + entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "keyword" @ + entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "element" @ + entity_antiqs (thy_check Method.intern Method.defined) "" "method" @ + entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @ + entity_antiqs no_check "" "fact" @ + entity_antiqs no_check "" "variable" @ + entity_antiqs no_check "" "case" @ + entity_antiqs (K ThyOutput.defined_command) "" "antiquotation"); end;