Miscellaneous Isabelle/Isar examples for Higher-Order Logic.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Fri Apr 16 17:44:29 1999 +0200
@@ -0,0 +1,128 @@
+(*  Title:      HOL/Isar_examples/BasicLogic.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Basic propositional and quantifier reasoning.
+*)
+
+theory BasicLogic = Main:;
+
+
+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*;
+  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;
+
+
+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;
+
+
+(* propositional proof (from 'Introduction to Isabelle') *)
+
+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;
+
+
+(* quantifier proof (from 'Introduction to Isabelle') *)
+
+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 [with 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;
+
+
+end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Cantor.thy	Fri Apr 16 17:44:29 1999 +0200
@@ -0,0 +1,13 @@
+(*  Title:      HOL/Isar_examples/Cantor.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Cantor's theorem (see also 'Isabelle's Object-Logics').
+*)
+
+theory Cantor = Main:;
+
+theorem cantor: "EX S. S ~: range(f :: 'a => 'a set)";
+by (best elim: equalityCE);
+
+end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Fri Apr 16 17:44:29 1999 +0200
@@ -0,0 +1,143 @@
+(*  Title:      HOL/Isar_examples/ExprCompiler.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Correctness of a simple expression/stack-machine compiler.
+*)
+
+theory ExprCompiler = Main:;
+
+title
+  "Correctness of a simple expression/stack-machine compiler --- an Isabelle/Isar demonstration"
+  "Markus Wenzel";
+
+
+section "Basics";
+
+text {|
+  First we define a type abbreviation for binary operations over some
+  type @type "'val" of values.
+|};
+
+types
+  'val binop = "'val => 'val => 'val";
+
+
+section "Machine";
+
+text {|
+  Next we model a simple stack machine, with three instructions.
+|};
+
+datatype ('adr, 'val) instr =
+  Const 'val |
+  Load 'adr |
+  Apply "'val binop";
+
+text {|
+  Execution of a list of stack machine instructions is
+  straight-forward.
+|};
+
+consts
+  exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list";
+
+primrec
+  "exec [] stack env = stack"
+  "exec (instr # instrs) stack env =
+    (case instr of
+      Const c => exec instrs (c # stack) env
+    | Load x => exec instrs (env x # stack) env
+    | Apply f => exec instrs (f (hd stack) (hd (tl stack)) # (tl (tl stack))) env)";
+
+constdefs
+  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
+  "execute instrs env == hd (exec instrs [] env)";
+
+
+section "Expressions";
+
+text {|
+  We introduce a simple language of expressions: variables ---
+  constants --- binary operations.
+|};
+
+datatype ('adr, 'val) expr =
+  Variable 'adr |
+  Constant 'val |
+  Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr";
+
+text {|
+  Evaluation of expressions does not do any unexpected things.
+|};
+
+consts
+  eval :: "('adr, 'val) expr => ('adr => 'val) => 'val";
+
+primrec
+  "eval (Variable x) env = env x"
+  "eval (Constant c) env = c"
+  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)";
+
+
+section "Compiler";
+
+text {|
+  So we are ready to define the compilation function of expressions to
+  lists of stack machine instructions.
+|};
+
+consts
+  comp :: "('adr, 'val) expr => (('adr, 'val) instr) list";
+
+primrec
+  "comp (Variable x) = [Load x]"
+  "comp (Constant c) = [Const c]"
+  "comp (Binop f e1 e2) = comp e2 @ comp e1 @ [Apply f]";
+
+
+text {|
+  The main result of this developement is the correctness theorem for
+  @term "comp".  We first establish some lemmas.
+|};
+
+ML "reset HOL_quantifiers";
+
+lemma exec_append:
+  "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");
+proof ("induct" ??P xs type: list);
+  show "??P []"; by simp;
+
+  fix x xs;
+  assume "??P xs";
+  show "??P (x # xs)" (is "??Q x");
+  proof ("induct" ??Q x type: instr);
+    fix val; show "??Q (Const val)"; by brute_force;
+    next;
+    fix adr; show "??Q (Load adr)"; by brute_force;
+    next;
+    fix fun; show "??Q (Apply fun)"; by brute_force;
+  qed;
+qed;
+
+
+lemma exec_comp:
+  "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e");
+proof ("induct" ??P e type: expr);
+
+  fix adr; show "??P (Variable adr)"; by brute_force;
+  next;
+  fix val; show "??P (Constant val)"; by brute_force;
+  next;
+  fix fun e1 e2; assume "??P e1" "??P e2"; show "??P (Binop fun e1 e2)";
+    by (brute_force simp add: exec_append);
+qed;
+
+
+text "Main theorem ahead.";
+
+theorem correctness: "execute (comp e) env = eval e env";
+  by (simp add: execute_def exec_comp);
+
+
+end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Peirce.thy	Fri Apr 16 17:44:29 1999 +0200
@@ -0,0 +1,51 @@
+(*  Title:      HOL/Isar_examples/Peirce.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Peirce's law: some examples of classical proof.
+*)
+
+theory Peirce = Main:;
+
+lemmas it[elim!] = mp notE;	(* FIXME elim!! *)
+
+
+lemma Peirce's_law: "((A --> B) --> A) --> A";
+proof;
+  assume ABA: "(A --> B) --> A";
+  show A;
+  proof (rule classical);
+    assume notA: "~ A";
+
+    have AB: "A --> B";
+    proof;
+      assume A: A;
+      from notA A; show B; ..;
+    qed;
+
+    from ABA AB; show A; ..;
+  qed;
+qed;
+
+
+lemma Peirce's_law: "((A --> B) --> A) --> A";
+proof;
+  assume ABA: "(A --> B) --> A";
+  show A;
+  proof (rule classical);
+
+    assume AB: "A --> B";
+    from ABA AB; show A; ..;
+
+    next;
+    assume notA: "~ A";
+    show "A --> B";
+    proof;
+      assume A: A;
+      from notA A; show B; ..;
+    qed;
+  qed;
+qed;
+
+
+end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/ROOT.ML	Fri Apr 16 17:44:29 1999 +0200
@@ -0,0 +1,11 @@
+(*  Title:      HOL/Isar_examples/ROOT.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
+*)
+
+use_thy "BasicLogic";
+use_thy "Peirce";
+use_thy "Cantor";
+use_thy "ExprCompiler";