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



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





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