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.