Search code examples
isabellehol

How to introduce forall in Isabelle

I am trying to prove the following inference rule in Isabelle (2021) from a previous question:

enter image description here

In particular, I tried to prove this in a forward manner, by first using the two assumptions to get A(y) and B(y), and therefore A(y) /\ B(y), for an arbitrarily chosen y. However, I cannot figure out what the right way is to introduce the ∀ back in the last step as shown in the problem line below.

theorem "∀x. A(x) ⟹ ∀x. B(x) ⟹ ∀x. A(x) ∧ B(x)"
proof (rule allI) ―‹forward›
  fix y
  assume "∀x. A(x)"
  from this have 1:"A(y)" by (rule allE)
  assume " ∀x. B(x)"
  from this have 2:"B(y)" by (rule allE)
  from 1 2 have "A(y) ∧ B(y)" by (rule conjI)
  ―‹problem line: applying allI›
  from this have "∀x. A(x) ∧ B(x)" by (rule allI)

Can someone help explain what is the right way to assume and then abstract away the arbitrary variable y here?

Solution

  • Can someone help explain what is the right way to assume and then abstract away the arbitrary variable y here?

    I would not say that there is a single "right way" to do this. The "right way" will depend on the context of the problem that you are trying to solve.

    In general, the theorem that you are trying to prove can be proved by simp:

    theorem 0: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
  by simp

    In most cases, when trying to prove such results, simp is the best approach.

    However, if you are, for example, writing an expository article/tutorial and wish to show how individual steps of the proof can be executed, then, of course, the explicit rule application becomes a necessity. However, in this case, there are still many possibilities.

    Firstly, you may use explicit blocks, as the examples below showcase:

    (*naive variant*)
theorem 1: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
proof-
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  {
    fix y 
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By have "A y ∧ B y" by (rule conjI)
  }
  then have "∀y. A y ∧ B y" by (rule allI)
  then have "∀x. B x ⟹ ∀y. A y ∧ B y" by (rule asm_rl)
  then show "∀x. A(x) ⟹ ∀x. B(x) ⟹ ∀x. A(x) ∧ B(x)" by (rule asm_rl)
qed

(*more natural variant*)
theorem 2: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
proof-
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  {
    fix y 
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By have "A y ∧ B y" by (rule conjI)
  }
  then show "∀y. A y ∧ B y" by (rule allI)
qed

(*HOL-style*)
theorem 3: "(∀x. A x) ⟶ (∀x. B x) ⟶ (∀x. A x ∧ B x)"
proof(intro impI)
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  {
    fix y 
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By have "A y ∧ B y" by (rule conjI)
  }
  then show "∀y. A y ∧ B y" by (rule allI)
qed

    However, proof- ... qed is usually a better alternative and more consistent with the conventional style of exposition in Isabelle, e.g.

    theorem alt_1: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
proof-
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  have "∀y. A y ∧ B y"
  proof(rule allI)
    fix y
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By show "A y ∧ B y" by (rule conjI)
  qed
  then have "∀x. B x ⟹ ∀y. A y ∧ B y" by (rule asm_rl)
  then show "∀x. A(x) ⟹ ∀x. B(x) ⟹ ∀x. A(x) ∧ B(x)" by (rule asm_rl)
qed

    As a general reference, I suggest section 2.2 in The Isabelle/Isar Reference Manual.