isabelleproofisarhol

Is it possible to write non-automatic formalizations in Isar?

I have the following:

lemma 
  assumes p: "P"
  assumes pimpq: "P⟶Q"
  shows "P∧Q"
proof -
  from pimpq p have q: "Q" by (rule impE)
  from p q show ?thesis by (rule conjI)
qed

I have thought that this is down to basic inference rules but reading the documentation for rule in section 9.4.3 Structured Methods of the Isar Reference Manual it turned out that it uses the Classical Reasoner with various rules. And, replacing the by clauses by .. also solves the goals, so mentioning implication elimination and conjunction introduction is not essential.

Is it possible to write a strict formalization here in Isar, i.e. not to use any automation and extra rules that are not explicit in the program text? Something like a forward proof in HOL4.

Solution

  • You could use Pure.rule if you don't want to use the classical module.

    lemma 
  assumes p: "P"
  assumes pimpq: "P⟶Q"
  shows "P∧Q"
proof -
  from pimpq p have q: "Q" by (Pure.rule impE)
  from p q show ?thesis by (Pure.rule conjI)
qed

    If you write .. Isabelle will automatically select a rule based on lemmas that are marked with the [intro] or [elim] attribute.

    Maybe you can also share your HOL4 proof that you want to reproduce in Isabelle, so that we can suggest the equivalent in Isabelle/HOL.