*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Problems with Logic.mk_implies + compose_tac*From*: Sascha Boehme <boehmes at in.tum.de>*Date*: Mon, 11 Jul 2011 17:06:51 +0200*Cc*: Matej Urbas <mu232 at cam.ac.uk>, Isabelle Users Mailing List <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.1.10.1107111126160.4450@atbroy100.informatik.tu-muenchen.de>*References*: <1310215039.3708.28.camel@toncka.urbas.si> <alpine.LNX.1.10.1107111126160.4450@atbroy100.informatik.tu-muenchen.de>*User-agent*: Mutt/1.5.20 (2009-06-14)

Makarius wrote: > If the "magic" above is by a totally alien tool, you can also apply > Object_Logic.full_atomize_tac first, then work on a close HOL > proposition, then apply the result using plain resolve_tac. (A > common trap is to get types too general in examples, then the > statement cannot be internalized into HOL.) It would be of much help if you further clarified your application, especially what kind of problems you are solving and how you connect the external tool (i.e., how you feed the subgoal to the external tool and what comes of out it afterwards). As Makarius already pointed out, it is likely that your integration can be tuned towards standard operations (which won't be deprecated in the next Isabelle release). In the meantime, here is a somewhat more standard approach to solve your issue, although still using the odd detour via Goal.prove: ML {* fun replace_subgoal_tac ctxt t = Object_Logic.full_atomize_tac THEN' SUBGOAL (fn (u, i) => let val thm = Goal.prove ctxt [] [] (Logic.mk_implies (t, u)) (fn {context, ...} => auto_tac (clasimpset_of context)) in Tactic.rtac thm i end) *} lemma "\<And>s1 s2. \<lbrakk>distinct [s1, s2]; s1 \<in> A; s1 \<in> B; s2 \<in> A; s2 \<notin> B\<rbrakk> \<Longrightarrow> \<exists>s1 s2. distinct [s1, s2] \<and> s1 \<in> A \<and> s2 \<in> B" apply (tactic {* replace_subgoal_tac @{context} @{term "\<And>s1 s2. \<lbrakk>distinct[s1, s2]; s1 \<in> A \<inter> B; s2 \<in> A - B\<rbrakk> \<Longrightarrow> \<exists>s1 s2. distinct[s1, s2] \<and> s1 \<in> A \<and> s2 \<in> B"} 1 *}) Cheers, Sascha

**Follow-Ups**:**Re: [isabelle] Problems with Logic.mk_implies + compose_tac***From:*Makarius

**References**:**[isabelle] Problems with Logic.mk_implies + compose_tac***From:*Matej Urbas

**Re: [isabelle] Problems with Logic.mk_implies + compose_tac***From:*Makarius

- Previous by Date: [isabelle] Fwd: Collections: problems with sets of sets
- Next by Date: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Previous by Thread: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Next by Thread: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Cl-isabelle-users July 2011 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