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 MHonArc.