*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] apply proof method to all subgoals*From*: Alex Katovsky <apk32 at cam.ac.uk>*Date*: Sun, 10 Apr 2011 15:19:18 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <D5907011-347A-4FA7-8B8A-F597873FEE3A@cam.ac.uk>*References*: <4DA19929.4080101@cam.ac.uk> <D5907011-347A-4FA7-8B8A-F597873FEE3A@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.7) Gecko/20100120 Fedora/3.0.1-1.fc12 Thunderbird/3.0.1

1. ⋀x xa. ⟦E; xa ∈ x⟧ ⟹ xa ∈ y 2. ⋀x xa. ⟦E; xa ∈ y⟧ ⟹ xa ∈ x

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:*Joachim Breitner

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

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

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

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