Re: [isabelle] On Recursion Induction



On Fri, 11 May 2012, Christian Sternagel wrote:

Dear Alfio,

it works like this

lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)"
 apply (rule)
 apply (rule allI)
 apply (assumption)
 apply (rule spec, assumption)
done

But I agree that there are some "strange" steps.

BTW, src/HOL/HOL.thy subsubsection {* Atomizing meta-level connectives *} has proper Isar proofs for these Pure-vs-HOL theorems. This reduces the magic to some extent.

When showing such things in public I usually make the Trueprop explicit like this:

  notation Trueprop  ("Tr")

or even:

  notation Trueprop  ("\<^bold>T\<^bold>r")


	Makarius


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