# [isabelle] Discharging non-atomic assumptions in Isabelle/ML

```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.

Thanks,
Joachim

--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
```

Attachment: signature.asc
Description: This is a digitally signed message part

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