(* Title: HOL/Isar_examples/BasicLogic.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
Basic propositional and quantifier reasoning.
*)
theory BasicLogic = Main:;
text {* Just a few tiny examples to get an idea of how Isabelle/Isar
proof documents may look like. *};
lemma I: "A --> A";
proof;
assume A;
show A; .;
qed;
lemma K: "A --> B --> A";
proof;
assume A;
show "B --> A";
proof;
show A; .;
qed;
qed;
lemma K': "A --> B --> A";
proof;
assume A;
thus "B --> A"; ..;
qed;
lemma K'': "A --> B --> A";
proof intro;
assume A;
show A; .;
qed;
lemma K''': "A --> B --> A";
by intro;
lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
proof;
assume "A --> B --> C";
show "(A --> B) --> A --> C";
proof;
assume "A --> B";
show "A --> C";
proof;
assume A;
show C;
proof (rule mp);
show "B --> C"; by (rule mp);
show B; by (rule mp);
qed;
qed;
qed;
qed;
text {* Variations of backward vs.\ forward reasonong \dots *};
lemma "A & B --> B & A";
proof;
assume "A & B";
show "B & A";
proof;
show B; by (rule conjunct2);
show A; by (rule conjunct1);
qed;
qed;
lemma "A & B --> B & A";
proof;
assume "A & B";
then; show "B & A";
proof;
assume A B;
show ?thesis; ..;
qed;
qed;
lemma "A & B --> B & A";
proof;
assume ab: "A & B";
from ab; have a: A; ..;
from ab; have b: B; ..;
from b a; show "B & A"; ..;
qed;
section {* Examples from 'Introduction to Isabelle' *};
text {* 'Propositional proof' *};
lemma "P | P --> P";
proof;
assume "P | P";
then; show P;
proof;
assume P;
show P; .;
show P; .;
qed;
qed;
lemma "P | P --> P";
proof;
assume "P | P";
then; show P; ..;
qed;
text {* 'Quantifier proof' *};
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
proof;
assume "EX x. P(f(x))";
then; show "EX x. P(x)";
proof (rule exE);
fix a;
assume "P(f(a))" (is "P(?witness)");
show ?thesis; by (rule exI [of P ?witness]);
qed;
qed;
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
proof;
assume "EX x. P(f(x))";
then; show "EX x. P(x)";
proof;
fix a;
assume "P(f(a))";
show ?thesis; ..;
qed;
qed;
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
by blast;
subsection {* 'Deriving rules in Isabelle' *};
text {* We derive the conjunction elimination rule from the
projections. The proof below follows the basic reasoning of the
script given in the Isabelle Intro Manual closely. Although, the
actual underlying operations on rules and proof states are quite
different: Isabelle/Isar supports non-atomic goals and assumptions
fully transparently, while the original Isabelle classic script
depends on the primitive goal command to decompose the rule into
premises and conclusion, with the result emerging by discharging the
context again later. *};
theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
proof -;
assume ab: "A & B";
assume ab_c: "A ==> B ==> C";
show C;
proof (rule ab_c);
from ab; show A; ..;
from ab; show B; ..;
qed;
qed;
end;