src/Pure/Isar/isar_syn.ML
changeset 6727 c8dba1da73cc
parent 6723 f342449d73ca
child 6735 e5138b3dbd3b
equal deleted inserted replaced
6726:ac968ce542a8 6727:c8dba1da73cc
    47 
    47 
    48 val textP = OuterSyntax.command "text" "formal comments" K.thy_decl
    48 val textP = OuterSyntax.command "text" "formal comments" K.thy_decl
    49   (P.comment >> (Toplevel.theory o IsarThy.add_text));
    49   (P.comment >> (Toplevel.theory o IsarThy.add_text));
    50 
    50 
    51 val titleP = OuterSyntax.command "title" "document title" K.thy_heading
    51 val titleP = OuterSyntax.command "title" "document title" K.thy_heading
    52   ((P.comment -- Scan.optional P.comment Comment.empty -- Scan.optional P.comment Comment.empty)
    52   ((P.comment -- Scan.optional P.comment Comment.none -- Scan.optional P.comment Comment.none)
    53     >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
    53     >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
    54 
    54 
    55 val chapterP = OuterSyntax.command "chapter" "chapter heading" K.thy_heading
    55 val chapterP = OuterSyntax.command "chapter" "chapter heading" K.thy_heading
    56   (P.comment >> (Toplevel.theory o IsarThy.add_chapter));
    56   (P.comment >> (Toplevel.theory o IsarThy.add_chapter));
    57 
    57 
    68 (* classes and sorts *)
    68 (* classes and sorts *)
    69 
    69 
    70 val classesP =
    70 val classesP =
    71   OuterSyntax.command "classes" "declare type classes" K.thy_decl
    71   OuterSyntax.command "classes" "declare type classes" K.thy_decl
    72     (Scan.repeat1 (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [])
    72     (Scan.repeat1 (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [])
    73       >> (Toplevel.theory o Theory.add_classes));
    73       -- P.marg_comment >> (Toplevel.theory o IsarThy.add_classes));
    74 
    74 
    75 val classrelP =
    75 val classrelP =
    76   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
    76   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
    77     (P.xname -- (P.$$$ "<" |-- P.!!! P.xname) >> (Toplevel.theory o Theory.add_classrel o single));
    77     (P.xname -- (P.$$$ "<" |-- P.!!! P.xname) -- P.marg_comment
       
    78       >> (Toplevel.theory o IsarThy.add_classrel));
    78 
    79 
    79 val defaultsortP =
    80 val defaultsortP =
    80   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
    81   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
    81     (P.sort >> (Toplevel.theory o Theory.add_defsort));
    82     (P.sort -- P.marg_comment >> (Toplevel.theory o IsarThy.add_defsort));
    82 
    83 
    83 
    84 
    84 (* types *)
    85 (* types *)
    85 
    86 
    86 val typedeclP =
    87 val typedeclP =
    87   OuterSyntax.command "typedecl" "Pure type declaration" K.thy_decl
    88   OuterSyntax.command "typedecl" "Pure type declaration" K.thy_decl
    88     (P.type_args -- P.name -- P.opt_infix
    89     (P.type_args -- P.name -- P.opt_infix -- P.marg_comment >> (fn (((args, a), mx), cmt) =>
    89       >> (fn ((args, a), mx) => Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
    90       Toplevel.theory (IsarThy.add_typedecl ((a, args, mx), cmt))));
    90 
    91 
    91 val typeabbrP =
    92 val typeabbrP =
    92   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    93   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    93     (Scan.repeat1 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix)))
    94     (Scan.repeat1
    94       >> (Toplevel.theory o Theory.add_tyabbrs o
    95       (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix)) -- P.marg_comment)
    95         map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
    96       >> (Toplevel.theory o IsarThy.add_tyabbrs o
       
    97         map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt))));
    96 
    98 
    97 val nontermP =
    99 val nontermP =
    98   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   100   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
    99     K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals));
   101     K.thy_decl (Scan.repeat1 (P.name -- P.marg_comment)
       
   102       >> (Toplevel.theory o IsarThy.add_nonterminals));
   100 
   103 
   101 val aritiesP =
   104 val aritiesP =
   102   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   105   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   103     (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2)
   106     (Scan.repeat1 ((P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2) -- P.marg_comment)
   104       >> (Toplevel.theory o Theory.add_arities));
   107       >> (Toplevel.theory o IsarThy.add_arities));
   105 
   108 
   106 
   109 
   107 (* consts and syntax *)
   110 (* consts and syntax *)
   108 
   111 
   109 val constsP =
   112 val constsP =
   110   OuterSyntax.command "consts" "declare constants" K.thy_decl
   113   OuterSyntax.command "consts" "declare constants" K.thy_decl
   111     (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
   114     (Scan.repeat1 (P.const -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_consts));
   112 
   115 
   113 val opt_mode =
   116 val opt_mode =
   114   Scan.optional
   117   Scan.optional
   115     (P.$$$ "(" |-- P.!!! (P.name -- Scan.optional (P.$$$ "output" >> K false) true --| P.$$$ ")"))
   118     (P.$$$ "(" |-- P.!!! (P.name -- Scan.optional (P.$$$ "output" >> K false) true --| P.$$$ ")"))
   116     ("", true);
   119     ("", true);
   117 
   120 
   118 val syntaxP =
   121 val syntaxP =
   119   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   122   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   120     (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
   123     (opt_mode -- Scan.repeat1 (P.const -- P.marg_comment)
       
   124       >> (Toplevel.theory o uncurry IsarThy.add_modesyntax));
   121 
   125 
   122 
   126 
   123 (* translations *)
   127 (* translations *)
   124 
   128 
   125 val trans_pat =
   129 val trans_pat =
   134   trans_pat -- P.!!! (trans_arrow -- trans_pat)
   138   trans_pat -- P.!!! (trans_arrow -- trans_pat)
   135     >> (fn (left, (arr, right)) => arr (left, right));
   139     >> (fn (left, (arr, right)) => arr (left, right));
   136 
   140 
   137 val translationsP =
   141 val translationsP =
   138   OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   142   OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   139     (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
   143     (Scan.repeat1 (trans_line -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_trrules));
   140 
   144 
   141 
   145 
   142 (* axioms and definitions *)
   146 (* axioms and definitions *)
   143 
   147 
   144 val axiomsP =
   148 val axiomsP =
   145   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   149   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   146     (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
   150     (Scan.repeat1 (P.spec_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_axioms));
   147 
   151 
   148 val defsP =
   152 val defsP =
   149   OuterSyntax.command "defs" "define constants" K.thy_decl
   153   OuterSyntax.command "defs" "define constants" K.thy_decl
   150     (Scan.repeat1 P.spec_opt_name >> (Toplevel.theory o IsarThy.add_defs));
   154     (Scan.repeat1 (P.spec_opt_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_defs));
   151 
   155 
   152 val constdefsP =
   156 val constdefsP =
   153   OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl
   157   OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl
   154     (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o IsarThy.add_constdefs));
   158     (Scan.repeat1 ((P.const -- P.marg_comment) -- (P.term -- P.marg_comment))
       
   159       >> (Toplevel.theory o IsarThy.add_constdefs));
   155 
   160 
   156 
   161 
   157 (* theorems *)
   162 (* theorems *)
   158 
   163 
   159 val facts = P.opt_thm_name "=" -- P.xthms1;
   164 val facts = P.opt_thm_name "=" -- P.xthms1;
   160 
   165 
   161 val theoremsP =
   166 val theoremsP =
   162   OuterSyntax.command "theorems" "define theorems" K.thy_decl
   167   OuterSyntax.command "theorems" "define theorems" K.thy_decl
   163     (facts >> (Toplevel.theory o IsarThy.have_theorems));
   168     (facts -- P.marg_comment >> (Toplevel.theory o IsarThy.have_theorems));
   164 
   169 
   165 val lemmasP =
   170 val lemmasP =
   166   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
   171   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
   167     (facts >> (Toplevel.theory o IsarThy.have_lemmas));
   172     (facts -- P.marg_comment >> (Toplevel.theory o IsarThy.have_lemmas));
   168 
   173 
   169 
   174 
   170 (* name space entry path *)
   175 (* name space entry path *)
   171 
   176 
   172 val globalP =
   177 val globalP =
   226 
   231 
   227 (* oracles *)
   232 (* oracles *)
   228 
   233 
   229 val oracleP =
   234 val oracleP =
   230   OuterSyntax.command "oracle" "install oracle" K.thy_decl
   235   OuterSyntax.command "oracle" "install oracle" K.thy_decl
   231     (P.name -- P.text >> (Toplevel.theory o IsarThy.add_oracle));
   236     (P.name -- P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.add_oracle));
   232 
   237 
   233 
   238 
   234 
   239 
   235 (** proof commands **)
   240 (** proof commands **)
   236 
   241 
   237 (* statements *)
   242 (* statements *)
   238 
   243 
   239 val is_props = P.$$$ "(" |-- P.!!! (Scan.repeat1 (P.$$$ "is" |-- P.prop) --| P.$$$ ")");
   244 val is_props = P.$$$ "(" |-- P.!!! (Scan.repeat1 (P.$$$ "is" |-- P.prop) --| P.$$$ ")");
   240 val propp = P.prop -- Scan.optional is_props [];
   245 val propp = P.prop -- Scan.optional is_props [];
   241 fun statement f = P.opt_thm_name ":" -- propp >> (fn ((x, y), z) => f x y z);
   246 fun statement f = (P.opt_thm_name ":" -- propp >> P.triple1) -- P.marg_comment >> f;
   242 
   247 
   243 val theoremP =
   248 val theoremP =
   244   OuterSyntax.command "theorem" "state theorem" K.thy_goal
   249   OuterSyntax.command "theorem" "state theorem" K.thy_goal
   245     (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   250     (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   246 
   251 
   267 
   272 
   268 (* facts *)
   273 (* facts *)
   269 
   274 
   270 val thenP =
   275 val thenP =
   271   OuterSyntax.command "then" "forward chaining" K.prf_chain
   276   OuterSyntax.command "then" "forward chaining" K.prf_chain
   272     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.chain));
   277     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
   273 
   278 
   274 val fromP =
   279 val fromP =
   275   OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
   280   OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
   276     (P.xthms1 >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));
   281     (P.xthms1 -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.from_facts)));
   277 
   282 
   278 val factsP =
   283 val factsP =
   279   OuterSyntax.command "note" "define facts" K.prf_decl
   284   OuterSyntax.command "note" "define facts" K.prf_decl
   280     (facts >> (Toplevel.proof o IsarThy.have_facts));
   285     (facts -- P.marg_comment >> (Toplevel.proof o IsarThy.have_facts));
   281 
   286 
   282 
   287 
   283 (* proof context *)
   288 (* proof context *)
   284 
   289 
   285 val assumeP =
   290 val assumeP =
   286   OuterSyntax.command "assume" "assume propositions" K.prf_decl
   291   OuterSyntax.command "assume" "assume propositions" K.prf_decl
   287     (P.opt_thm_name ":" -- Scan.repeat1 propp >>
   292     ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
   288       (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
   293       >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
   289 
   294 
   290 val fixP =
   295 val fixP =
   291   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_decl
   296   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_decl
   292     (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
   297     (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
   293       >> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
   298       >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
   294 
   299 
   295 val letP =
   300 val letP =
   296   OuterSyntax.command "let" "bind text variables" K.prf_decl
   301   OuterSyntax.command "let" "bind text variables" K.prf_decl
   297     (P.and_list1 (P.enum1 "as" P.term -- (P.$$$ "=" |-- P.term))
   302     (P.and_list1 (P.enum1 "as" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
   298       >> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
   303       >> (Toplevel.print oo (Toplevel.proof o IsarThy.match_bind)));
   299 
   304 
   300 
   305 
   301 (* proof structure *)
   306 (* proof structure *)
   302 
   307 
   303 val beginP =
   308 val beginP =
   319   OuterSyntax.improper_command "kill_proof" "abort current proof" K.control
   324   OuterSyntax.improper_command "kill_proof" "abort current proof" K.control
   320     (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
   325     (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
   321 
   326 
   322 val qed_withP =
   327 val qed_withP =
   323   OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes" K.qed
   328   OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes" K.qed
   324     (Scan.option P.name -- Scan.option P.attribs -- Scan.option P.method
   329     (Scan.option P.name -- Scan.option P.attribs -- Scan.option (P.method -- P.interest)
   325       >> (uncurry IsarThy.global_qed_with));
   330       >> (uncurry IsarThy.global_qed_with));
   326 
   331 
   327 val qedP =
   332 val qedP =
   328   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed
   333   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed
   329     (Scan.option P.method >> IsarThy.qed);
   334     (Scan.option (P.method -- P.interest) >> IsarThy.qed);
   330 
   335 
   331 val terminal_proofP =
   336 val terminal_proofP =
   332   OuterSyntax.command "by" "terminal backward proof" K.qed
   337   OuterSyntax.command "by" "terminal backward proof" K.qed
   333     (P.method >> IsarThy.terminal_proof)
   338     (P.method -- P.interest >> IsarThy.terminal_proof);
   334 
   339 
   335 val immediate_proofP =
   340 val immediate_proofP =
   336   OuterSyntax.command "." "immediate proof" K.qed
   341   OuterSyntax.command "." "immediate proof" K.qed
   337     (Scan.succeed IsarThy.immediate_proof);
   342     (Scan.succeed IsarThy.immediate_proof);
   338 
   343 
   351   OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
   356   OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
   352     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   357     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   353 
   358 
   354 val proofP =
   359 val proofP =
   355   OuterSyntax.command "proof" "backward proof" K.prf_block
   360   OuterSyntax.command "proof" "backward proof" K.prf_block
   356     (Scan.option P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   361     (P.interest -- Scan.option (P.method -- P.interest)
       
   362       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   357 
   363 
   358 
   364 
   359 (* proof history *)
   365 (* proof history *)
   360 
   366 
   361 val clear_undoP =
   367 val clear_undoP =