src/HOL/Isar_examples/BasicLogic.thy
 author wenzelm Wed, 14 Jul 1999 13:07:09 +0200 changeset 7005 cc778d613217 parent 7001 8121e11ed765 child 7133 64c9f2364dae permissions -rw-r--r--
```
(*  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 single+   -- {* better use sufficient-to-show here \dots *};
assume A;
show A; .;
qed;

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 same;
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;
```