364 text {* |
364 text {* |
365 \begin{matharray}{rcl} |
365 \begin{matharray}{rcl} |
366 @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ |
366 @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ |
367 @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ |
367 @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ |
368 @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ |
368 @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ |
|
369 @{command_def "schematic_lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ |
|
370 @{command_def "schematic_theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ |
|
371 @{command_def "schematic_corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ |
369 @{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\ |
372 @{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\ |
370 @{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\ |
373 @{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\ |
371 @{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\ |
374 @{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\ |
372 @{command_def "thus"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\ |
375 @{command_def "thus"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\ |
373 @{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
376 @{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
404 @{element_def "obtains"} claims several simultaneous simultaneous |
407 @{element_def "obtains"} claims several simultaneous simultaneous |
405 contexts of (essentially a big disjunction of eliminated parameters |
408 contexts of (essentially a big disjunction of eliminated parameters |
406 and assumptions, cf.\ \secref{sec:obtain}). |
409 and assumptions, cf.\ \secref{sec:obtain}). |
407 |
410 |
408 \begin{rail} |
411 \begin{rail} |
409 ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal) |
412 ('lemma' | 'theorem' | 'corollary' | |
|
413 'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal) |
410 ; |
414 ; |
411 ('have' | 'show' | 'hence' | 'thus') goal |
415 ('have' | 'show' | 'hence' | 'thus') goal |
412 ; |
416 ; |
413 'print\_statement' modes? thmrefs |
417 'print\_statement' modes? thmrefs |
414 ; |
418 ; |
436 \item @{command "theorem"}~@{text "a: \<phi>"} and @{command |
440 \item @{command "theorem"}~@{text "a: \<phi>"} and @{command |
437 "corollary"}~@{text "a: \<phi>"} are essentially the same as @{command |
441 "corollary"}~@{text "a: \<phi>"} are essentially the same as @{command |
438 "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as |
442 "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as |
439 being of a different kind. This discrimination acts like a formal |
443 being of a different kind. This discrimination acts like a formal |
440 comment. |
444 comment. |
|
445 |
|
446 \item @{command "schematic_lemma"}, @{command "schematic_theorem"}, |
|
447 @{command "schematic_corollary"} are similar to @{command "lemma"}, |
|
448 @{command "theorem"}, @{command "corollary"}, respectively but allow |
|
449 the statement to contain unbound schematic variables. |
|
450 |
|
451 Under normal circumstances, an Isar proof text needs to specify |
|
452 claims explicitly. Schematic goals are more like goals in Prolog, |
|
453 where certain results are synthesized in the course of reasoning. |
|
454 With schematic statements, the inherent compositionality of Isar |
|
455 proofs is lost, which also impacts performance, because proof |
|
456 checking is forced into sequential mode. |
441 |
457 |
442 \item @{command "have"}~@{text "a: \<phi>"} claims a local goal, |
458 \item @{command "have"}~@{text "a: \<phi>"} claims a local goal, |
443 eventually resulting in a fact within the current logical context. |
459 eventually resulting in a fact within the current logical context. |
444 This operation is completely independent of any pending sub-goals of |
460 This operation is completely independent of any pending sub-goals of |
445 an enclosing goal statements, so @{command "have"} may be freely |
461 an enclosing goal statements, so @{command "have"} may be freely |
485 The optional case names of @{element_ref "obtains"} have a twofold |
501 The optional case names of @{element_ref "obtains"} have a twofold |
486 meaning: (1) during the of this claim they refer to the the local |
502 meaning: (1) during the of this claim they refer to the the local |
487 context introductions, (2) the resulting rule is annotated |
503 context introductions, (2) the resulting rule is annotated |
488 accordingly to support symbolic case splits when used with the |
504 accordingly to support symbolic case splits when used with the |
489 @{method_ref cases} method (cf.\ \secref{sec:cases-induct}). |
505 @{method_ref cases} method (cf.\ \secref{sec:cases-induct}). |
490 |
|
491 \medskip |
|
492 |
|
493 \begin{warn} |
|
494 Isabelle/Isar suffers theory-level goal statements to contain |
|
495 \emph{unbound schematic variables}, although this does not conform |
|
496 to the aim of human-readable proof documents! The main problem |
|
497 with schematic goals is that the actual outcome is usually hard to |
|
498 predict, depending on the behavior of the proof methods applied |
|
499 during the course of reasoning. Note that most semi-automated |
|
500 methods heavily depend on several kinds of implicit rule |
|
501 declarations within the current theory context. As this would |
|
502 also result in non-compositional checking of sub-proofs, |
|
503 \emph{local goals} are not allowed to be schematic at all. |
|
504 Nevertheless, schematic goals do have their use in Prolog-style |
|
505 interactive synthesis of proven results, usually by stepwise |
|
506 refinement via emulation of traditional Isabelle tactic scripts |
|
507 (see also \secref{sec:tactic-commands}). In any case, users |
|
508 should know what they are doing. |
|
509 \end{warn} |
|
510 *} |
506 *} |
511 |
507 |
512 |
508 |
513 section {* Refinement steps *} |
509 section {* Refinement steps *} |
514 |
510 |