Re: [isabelle] apply proof method to all subgoals
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
This performs all so-called safe inferences: those that cannot lead to information loss.
On 10 Apr 2011, at 12:48, Alex Katovsky wrote:
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  conjI)
apply(rule_tac  allI, rule_tac  allI, rule_tac  allI)
apply(rule_tac  impI, rule_tac  impI, rule_tac  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