Re: [isabelle] Theorem-proving for a Bayesian model compiler
On Thu, 17 Mar 2011, Timothy McKenzie wrote:
On Wed, 16 Mar 2011 04:11:54 Kevin Van Horn wrote:
* Ability to do derivational proofs where I know the form of
what I want to prove but don't know exactly what I'm proving
until I reach the end. For example, I'm doing a chain of A1 =
A2 = ... An, and only when I reach an An that has the form I
want do I know I'm done and know that A1 = An is what I'm
proving. Likewise, I might be trying to find a usable upper
bound: B1 <= B2 <= ... Bn.
I'm a little surprised that no-one has yet mentioned the "also ...
also ... finally ..." constructions in Isabelle/Isar. There's an
example in isar-overview in the documentation provided with
Isabelle, and more technical documentation in isar-ref. It can be
used with both = and <= (and, I think, even mixing the two), but
it behaves unusually with >=, because this is an abbreviation for
<=, and the abbreviation seems to be expanded before Isabelle
decides which is the left-hand side and which is the right-hand
side for the purposes of the next step.
Isar calculations are parameterized by a collection of rules that are
declared as "trans" and can be inspected via print_trans_rules. This is a
very general mechanism to combine relations in a forward manner. It also
works with substitution of equalities or inequalities (with some care
about higher-order unification).
The >= abbreviations indeed do not fit in here. There were added as adhoc
feature when I was not looking, and still await to be integrated properly.
This archive was generated by a fusion of
Pipermail (Mailman edition) and