1

This is an continuation of the question proof (rule disjE) for nested disjunction

There we learned that

assume "(A ∨ B) ∧ C"
hence "thesis"
proof (elim conjE disjE)

is a nice idiom to resolve such conjunctions.

But what if I, before being able to use elim ..., need to also apply an introduction rule – say, some induction, or equalityI. If i try

have "(A ∨ B) ∧ C ⟷ (A' ∨ B') ∧ C'"
proof (rule iffI, elim conjE disjE)

then the elim only acts on the first goal, the other goal is still noisy with unwanted and easily eliminated operators.

So how do I apply it on all goals introduced by the rule?

Community
  • 1
  • 1
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
  • For example, is there a method like intro` and `elim` that takes both intro and elim rules? – Joachim Breitner Jul 23 '14 at 15:19
  • Sorry to be nitpicky, but your second example is not proper Isar. First in the assumption you need more parentheses (or use `<-->`). Then `equalityI` is a theorem for set equality, I guess you meant `iffI`. Moreover, if your assumption is an equality I don't see the point of applying an *introduction* rule, wouldn't there rather be need for an elimination rule? I'm just noting all this, because it might be confusing for those to read your question much later. – chris Aug 06 '14 at 08:30
  • That’s what I get for believing I can writer proper Isar without Isabelle. Thanks, fixed. – Joachim Breitner Aug 06 '14 at 09:24

1 Answers1

2

The methods intro and elim essentially behave like rule_tac and erule_tac. So you can use these with explicit goal addressing in square brackets. A [!] tells such tactic emulation methods to work on all subgoals. For example:

have "(A ∨ B) ∧ C ⟷ (A' ∨ B') ∧ C'"
proof(rule_tac [!] iffI | erule_tac [!] disjE conjE)+
Andreas Lochbihler
  • 4,998
  • 12
  • 10
  • An important difference between `intro`/`elim` and `rule_tac`/`erule_tac` is that the former never instantiate schematic variables. – Lars Noschinski Aug 22 '14 at 08:38