*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Discharging non-atomic assumptions in Isabelle/ML*From*: Thomas Sewell <thomas.sewell at nicta.com.au>*Date*: Wed, 10 Dec 2014 11:45:48 +1100*In-reply-to*: <5486C35C.7000307@in.tum.de>*References*: <1418117162.3339.13.camel@kit.edu> <5486C35C.7000307@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.3.0

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.

**Follow-Ups**:

**References**:**[isabelle] Discharging non-atomic assumptions in Isabelle/ML***From:*Joachim Breitner

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

- Previous by Date: [isabelle] export_code ... checking
- Next by Date: [isabelle] Shadowing constants in obtains clause
- Previous by Thread: Re: [isabelle] Discharging non-atomic assumptions in Isabelle/ML
- 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