*To*: Mathieu Giorgino <mathieu.giorgino at irit.fr>*Subject*: Re: [isabelle] apply proof method to all subgoals*From*: Alexander Katovsky <apk32 at cam.ac.uk>*Date*: Sun, 17 Apr 2011 12:07:17 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201104101643.38161.mathieu.giorgino@irit.fr>*References*: <4DA19929.4080101@cam.ac.uk> <D5907011-347A-4FA7-8B8A-F597873FEE3A@cam.ac.uk> <4DA1BC66.9090007@cam.ac.uk> <201104101643.38161.mathieu.giorgino@irit.fr>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.13) Gecko/20101209 Fedora/3.1.7-0.35.b3pre.fc14 Thunderbird/3.1.7

How about

proof(induct n, intro allI conjI impI)

On 04/10/2011 03:43 PM, Mathieu Giorgino wrote:

You could use "intro": apply (intro conjI allI impI) which apply all introduction rules you give to it until no more is applicable. Mathieu Giorgino On Sunday 10 April 2011, Alex Katovsky wrote:This works very well in the example I gave, but it appears that sometimes "apply safe" can do more goal splitting than I want it to. For example, if "F" below is "x = y" where x and y are sets then "apply safe" will use set_eqI to generate these goals 1. ⋀x xa. ⟦E; xa ∈ x⟧ ⟹ xa ∈ y 2. ⋀x xa. ⟦E; xa ∈ y⟧ ⟹ xa ∈ x and in some instances it would be preferable to keep equality as the goal. Is there some way that I can limit "apply safe", for example something like "apply (safe only: conjI allI impI)"? On 04/10/2011 01:50 PM, Lawrence Paulson wrote:Probably you should try apply safe This performs all so-called safe inferences: those that cannot lead to information loss. Larry Paulson On 10 Apr 2011, at 12:48, Alex Katovsky wrote:Hi, This is probably a very basic question, so I apologize if I'm not reading the tutorial carefully enough. I have this lemma lemma "(∀ x . A ⟶ B) ∧ (∀ y . C ⟶ D) ∧ (∀ x . E ⟶ F)" and from this I want to generate the three subgoals 1. ⋀x. A ⟹ B 2. ⋀y. C ⟹ D 3. ⋀x. E ⟹ F The only way I know how to do this at the moment is apply(rule conjI, rule_tac [2] conjI) apply(rule_tac [1] allI, rule_tac [2] allI, rule_tac [3] allI) apply(rule_tac [1] impI, rule_tac [2] impI, rule_tac [3] impI) What I would like to do is repeatedly apply "(rule conjI)|(rule allI)|(rule impI)" to all subgoals until no further progress can be made.

**Follow-Ups**:**Re: [isabelle] apply proof method to all subgoals***From:*Makarius

**References**:**[isabelle] apply proof method to all subgoals***From:*Alex Katovsky

**Re: [isabelle] apply proof method to all subgoals***From:*Lawrence Paulson

**Re: [isabelle] apply proof method to all subgoals***From:*Alex Katovsky

**Re: [isabelle] apply proof method to all subgoals***From:*Mathieu Giorgino

- Previous by Date: Re: [isabelle] Interleave in Isabelle
- Next by Date: Re: [isabelle] apply proof method to all subgoals
- Previous by Thread: Re: [isabelle] apply proof method to all subgoals
- Next by Thread: Re: [isabelle] apply proof method to all subgoals
- Cl-isabelle-users April 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