proving Predicate logic with Isabelle

Question

I'm trying to prove the following lemma:

lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"

I'm trying to start by eliminating the forall quantifiers, so here's what I tried:

lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"
  apply(rule iffI)
  apply ( erule_tac x="x" in allE)
  apply (rule allE)
  (*goal now: get rid of conj on both sides and the quantifiers on right*)
  apply (erule conjE) (*isn't conjE supposed to be used with elim/erule?*)
  apply (rule allI)
  apply (assumption)
  
  
  apply ( rule conjI) (*at this point, the following starts to make no sense... *)
    
   apply (rule conjE) (*should be erule?*)
   apply ( rule conjI)
   apply ( rule conjI)

  ...

At the end I just started to act depending on the outcome of the previous apply, but it seems wrong to me, probably because there's some mistake in the beginning... Could someone please explain to me my error and how to finish this proof correctly?

Thanks in advance

Answer 1

Eliminating the universal quantifier at this early stage is not a good idea because you don't even have any value that you could plug in at that point (the x that you give is not in scope at that point, which is why it is printed with that orange background in Isabelle/jEdit).

After you do iffI you have two goals:

goal (2 subgoals):
 1. ∀x. A x ∧ B x ⟹ (∀x. A x) ∧ (∀x. B x)
 2. (∀x. A x) ∧ (∀x. B x) ⟹ ∀x. A x ∧ B x

Let's focus on the first one for now. You should first apply the introduction rules on the right-hand side, namely conjI and allI. That leaves you with

goal (3 subgoals):
 1. ⋀x. ∀x. A x ∧ B x ⟹ A x
 2. ⋀x. ∀x. A x ∧ B x ⟹ B x
 3. (∀x. A x) ∧ (∀x. B x) ⟹ ∀x. A x ∧ B x

Now you can apply allE instantiated with x and the first goal becomes ⋀x. A x ∧ B x ⟹ A x, which you can then solve with erule conjE and assumption. The second goal works similarly.

For the last goal, it is similar again: apply the introduction rules first, then apply the elimination rules and assumption and you're done.

Of course, all the standard provers for Isabelle such as auto, force, blast and even the simple ones like metis, meson, iprover can easily solve this automatically, but that's probably not what you were going for here.