*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] apply proof method to all subgoals*From*: Mathieu Giorgino <mathieu.giorgino at irit.fr>*Date*: Sun, 10 Apr 2011 16:43:37 +0200*Cc*: Alex Katovsky <apk32 at cam.ac.uk>*In-reply-to*: <4DA1BC66.9090007@cam.ac.uk>*References*: <4DA19929.4080101@cam.ac.uk> <D5907011-347A-4FA7-8B8A-F597873FEE3A@cam.ac.uk> <4DA1BC66.9090007@cam.ac.uk>*User-agent*: KMail/1.13.6 (Linux/2.6.37-ARCH; KDE/4.6.1; x86_64; ; )

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:*Alexander Katovsky

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

- Previous by Date: Re: [isabelle] apply proof method to all subgoals
- Next by Date: Re: [isabelle] Pairs/tuples
- 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