Re: [isabelle] On Recursion Induction
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
To convince yourself that the equivalence is not only informal, the
theorems allI and spec should be enough.
just my 2 cents
This archive was generated by a fusion of
Pipermail (Mailman edition) and