Page 353 of 800
| Page 353 of 800 | Search internet |
Now consider the following proof:
After tactic expansion, the proof resembles this proof:
Each conclusion has the form that a hypothesis conjunction implies a consequence. The hypothesis conjunction starts out being the dummy hypothesis 
. One can then add conjuncts to the hypothesis conjunction by stating hypotheses as is done in Line L01 and L02. And one can subtract from the hypothesis conjunction by leaving a block.
Nothing particular happens when entering a block. But when leaving a block, the hypothesis conjunction is reset to the value it had when entering the block. Additional hypotheses made inside the block are moved from the hypothesis conjunction to the consequence. An example of this can be seen in Line L05 where two hypotheses are moved from hypothesis conjunction to consequence.
Furthermore, when leaving a block, the lines inside the block become inaccessible so that one cannot refer e.g. to Line L04 from Line L06 in the proof above. Nothing prevents lines inside a block from referencing lines that occur before the beginning of the block.
A mentioned earlier, the conclusions of proof lines are accumulated in ![s [[ !"pre" ]]](../../renderings/840CDCAC46099D723C97DD063811AEA329EE7250.png "s [[ !\"pre\" ]]")
of the tactic state 
. The value of is a list of entries of form 
where 
is the line number, 
is the conclusion of the line, and 
is an argumentation in the form of a sequent term to include in proofs whenever a the given line is referenced.
When leaving a block, is reset to the value it had before entering the block and then the conclusion of the block is added.
Each hypothesis line modifies all entries in by adding the hypothesis to each entry. As an example, Line L01 adds 
to but Line L02 modifies the conclusion of Line L01 to 
in . Line L02 also modifies the argumentation such that the argumentation proves the new conclusion.
Now consider Line L04 in the proof above. The argumentation refers to Line L01 and L03. Due to the modifications to made by Line L02, both 
and 
have hypothesis when seen from Line L04.
The modifications done by Line L02 disappear when leaving the block because is reset to the value it had before entering the block. The conclusion of the block is added after resetting so that one can use the result of the block.
| Page 353 of 800 | Search logiweb.eu |