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



If you really need to use it, there is a primitive compose operation
which is available via compose_tac, Thm.bicompose etc in the ML sources.
This avoids some of the normal automation done around the meta-operators.

This can be used in your case, e.g:

ML_val {*
val foo_induct = Thm.assume @{cprop "!! 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"}
val hyp1 = Thm.assume @{cprop "(!! x y. Q1 y x ==> Q2 y x ==> some_P x y)"}
val it = Thm.bicompose {flatten = false, incremented = false, match = false}
    (false, hyp1, 0)
    2
    @{thm foo_induct}
  |> Seq.list_of
*}

(I tried to do this using the structured mechanisms to create
foo_induct, hyp1 etc, and then Isabelle really wanted to export hyp1 as
"Q1 ?y ?x ==> Q2 ?y ?x ==> some_P x y" which won't work with bicompose.)

I'm not sure if the result is exactly what you want, but maybe it helps.

Cheers,
    Thomas.

On 09/12/14 20:39, Dmitriy Traytel wrote:
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





________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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