Hi,
I have another Isabelle/ML beginner’s question, and hope to get some
help with a tricky point.
My goal is to program some automation around inductive predicate and
inductive proofs. At some point, I have theorems which match precisely
the assumption of the induct theorem of an inductive predicate. I.e.

`
`` foo.induct:
` "!! P a b.
foo a b ==>
(!! x y. Q1 y x ==> Q2 y x ==> P x y) ==>
(!! x y z. foo x y ==> P x z ==> P y z) ==>
P a b"
hyp1: "(!! x y. Q1 y x ==> Q2 y x ==> some_P x y)"
hyp2: "(!! x y z. foo x y ==> some_P x z ==> some_P y z)"

`
``what is the proper way to obtain
`
some_P: "!! a b . foo a b ==> some_P a b"
from this?
Naively, I would expect something like foo.induct[meta_OF _ hyp1 hyp2]
to exist, but could not find such a thing.
It would of course work with the equivalent of
lemma some_P: "!! a b . foo a b ==> some_P a b"
apply (rule foo.induct)
apply assumption
apply (rule hyp1)
apply assumption
apply assumption
apply (rule hyp2)
apply assumption
apply assumption
done

`
``but that seems far too fragile (i.e. how many assumptions? What if the
`there are multiple unifiers along the way, before the next assumption
determines the choice?) when a direct unification of the non-atomic
terms appears to be so much more reliable and predictable.