# Re: [isabelle] On Recursion Induction

```Dear Christian,

Thanks for your reply. The proposition below is simple and
precise enough for me. The use of allI was clear, but I was
not so sure about spec, to be honest.

Many thanks!

On Wed, May 9, 2012 at 12:50 AM, Christian Sternagel
<c-sterna at jaist.ac.jp>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.