Re: [isabelle] On Recursion Induction



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





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