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

```Hi Joachim,

On 09.12.2014 10:26, Joachim Breitner wrote:
```
```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.
```
```
```
in my experience, a backwards proof (your apply script) is usually less fragile than a forward proof (meta_OF if existed).
```
```
Finding out "How many assumptions?" is easy (or even not necessary): rtac hyp1 THEN_ALL_NEW atac
```
```
To avoid HO problems, you will probably find the need to instantiate P from foo.induct with some_P (look for usages of Drule.instantiate' and friends in src/HOL/Tools to see some examples).
```
Hope that helps,
Dmitriy

```

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