*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Discharging non-atomic assumptions in Isabelle/ML*From*: Joachim Breitner <breitner at kit.edu>*Date*: Tue, 09 Dec 2014 10:26:02 +0100

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**

**Follow-Ups**:**Re: [isabelle] Discharging non-atomic assumptions in Isabelle/ML***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] running bibtex through document preparation
- Next by Date: Re: [isabelle] Discharging non-atomic assumptions in Isabelle/ML
- Previous by Thread: Re: [isabelle] running bibtex through document preparation
- Next by Thread: Re: [isabelle] Discharging non-atomic assumptions in Isabelle/ML
- Cl-isabelle-users December 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list