Re: [isabelle] On Recursion Induction

Dear Christian,

I was a little puzzled by you "atomic" proof below

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

and wanted to see the details myself. But using step-by-step apply commands
this  was the only way I could solve the goal:

lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)"
   apply (rule)
   apply (rule allI)
   apply (assumption)
   apply (rename_tac x0)
   apply (erule allE)
   apply (assumption)

That is to say,  I had to use "allE" instead of "spec". The renaming above
included because I was a little confused by a scope of a specific arbitrary


On Wed, May 9, 2012 at 12:50 AM, Christian Sternagel
<c-sterna at>wrote:

> Dear Alfio,
> On 05/09/2012 04:40 AM, Alfio Martini wrote:
>>  >Your original version results in "ALL b e. valbool b e = valbool (NNF
>>  >b) e" (which is equivalent, but not so nice to use, since you cannot
>>  >directly instantiate it).
>> I think I spoke about this above, but I would like to capture in a
>> precise way (in a theorem) this equivalence. Informally we
>> all know that they are. I often think about it. Do you know how
>> to write (in Isabelle) this "equivalence"?
> Maybe the closest you get to this equivalence is
>  lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)"
>    by (rule) (rule allI, assumption, rule spec)
> which shows that meta-all-quantification is the same as
> HOL-all-quantification. It is not possible to prove that schematic
> variables are equivalent to meta-all-quantified variables inside the logic.
> Also the need for the explicit Trueprop (which turns something of type
> "bool" [the type of HOL formulas] into type "prop" [the type of
> propositions in the general Isabelle framework]) in the above proof hints
> that we are doing something non-standard (for lack of a better expression).
> To convince yourself that the equivalence is not only informal, the
> theorems allI and spec should be enough.
> just my 2 cents
> chris

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

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