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