[isabelle] how to eliminate ALL



I have this lemma in the format "[| A; B |] ==> ALL x. C x". I want to
apply allI to the rule to get rid of the ALL before applying it with
apply (rule ...), which ought to be a simple task. I was thinking it
would be something like apply (rule myLemma[THEN/OF allI]). However,
that doesn't work, and nothing else I've tried has either. You'd think
there would be a way, but as far as I can tell, there's no
attribute-based analogue of RS or (rule ...). So I have to state the
lemma sans ALL as a new lemma and prove it.

Note, I'm sure there's plenty of nice ways to do it in Isar, but I've
given up on Isar for now because my goals are quite large and I can't
figure out how to get around stating them over and over in full, even
with higher-order-unification-based abbreviation.

Chris Capel
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)





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