[isabelle-dev] Reviving an old thread: [isabelle] structured induction: mutual definitions and "arbitrary" in inductions?

[Makarius]

On Wed, 12 Oct 2011, Randy Pollack wrote:

> Second, how do we know the Isar behavior is logically sound?  When a 
> user erroneously makes arbitrary a variable that is bound by an 
> induction, Isar returns a goal that is logically different from the 
> original goal.  "arbitrary" is somewhat of a user-level transformation; 
> is it checked by the Isabelle kernel that the new goal implies the 
> original goal?

It is all based on regular inferences and tactics of Isabelle/Pure.  So it 
is sound by construction according to the "LCF approach".  There are also 
explicit checks in the proof state management that ensure that the 
theorems produced in the end have the same statement than the initial 
claim.  (With schematic goals it could be an instance.)

This means Isar proof methods might lead to confusion, but not to wrong 
results.


 	Makarius