59 facts, using ``missing'' premises from the goal state; this allows |
59 facts, using ``missing'' premises from the goal state; this allows |
60 rules stemming from inductive sets to be applied in unstructured |
60 rules stemming from inductive sets to be applied in unstructured |
61 scripts, while still benefitting from proper handling of non-atomic |
61 scripts, while still benefitting from proper handling of non-atomic |
62 statements; NB: major inductive premises need to be put first, all the |
62 statements; NB: major inductive premises need to be put first, all the |
63 rest of the goal is passed through the induction; |
63 rest of the goal is passed through the induction; |
|
64 |
|
65 - 'induct' proper support for mutual induction involving non-atomic |
|
66 rule statements (uses the new concept of simultaneous goals, see |
|
67 below); |
|
68 |
|
69 * Pure: support multiple simultaneous goal statements, for example |
|
70 "have a: A and b: B" (same for 'theorem' etc.); being a pure |
|
71 meta-level mechanism, this acts as if several individual goals had |
|
72 been stated separately; in particular common proof methods need to be |
|
73 repeated in order to cover all claims; note that a single elimination |
|
74 step is *not* sufficient to establish the two conjunctions, so this |
|
75 fails: |
|
76 |
|
77 assume "A & B" then have A and B .. (*".." fails*) |
|
78 |
|
79 better use "obtain" in situations as above; alternative refer to |
|
80 multi-step methods like 'auto', 'simp_all', 'blast+' etc.; |
64 |
81 |
65 * Pure: proper integration with ``locales''; unlike the original |
82 * Pure: proper integration with ``locales''; unlike the original |
66 version by Florian Kammueller, Isar locales package high-level proof |
83 version by Florian Kammueller, Isar locales package high-level proof |
67 contexts rather than raw logical ones (e.g. we admit to include |
84 contexts rather than raw logical ones (e.g. we admit to include |
68 attributes everywhere); |
85 attributes everywhere); |