Re: [isabelle] apply proof method to all subgoals



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.






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