Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



On 03.05.2012 06:29, Bill Richter wrote:
    The induct/induction/induct_tac methods just set up an induction
    proof (i.e., base cases + inductive cases) according to the
    variable you want to induct over. It's the same with pen'n'paper
    actually. What you do to solve the base case and inductive case is
    not induction, but mostly different techniques like equational
    reasoning etc.

I need to understand what you mean in order to understand how to write
Isabelle or HOL Light proofs, but what I did is certainly what
mathematicians call an inductive proof.  I showed the results were
true for lists of length 0 (just []), and then assumed the results
were true for all lists of length n, and used that to prove the
results were true for all lists length n+1.  I've heard Schemers call
that tree induction.

There are two steps in an inductive proof: In a first step the original goal ("property holds for all lists") is transformed with an induction rule in a number of new goals ("property holds for lists of length 0" and "assuming property holds for all lists of length n, it holds for all lists of length n + 1"). In a second step these new goals have to be proven.

Isabelle's "induct" and "induct_tac" methods only perform the first step. This transformation is done purely schematic -- even if e.g. the base case is trivial, it will not be solved automatically. The second step needs to be performed explicitly (here "auto").

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.