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
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").
This archive was generated by a fusion of
Pipermail (Mailman edition) and