Re: [isabelle] Discharging non-atomic assumptions in Isabelle/ML
On 09.12.2014 10:26, Joachim Breitner wrote:
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.
"!! 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"
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 (rule hyp1)
apply (rule hyp2)
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and