# HG changeset patch # User wenzelm # Date 924277469 -7200 # Node ID 2ebe9e630cab50e55dd52a35bdd5af7d0b359ae8 # Parent 6d5d3ecedf50fb2003d8008047c86d7d3478b3c4 Miscellaneous Isabelle/Isar examples for Higher-Order Logic. diff -r 6d5d3ecedf50 -r 2ebe9e630cab src/HOL/Isar_examples/BasicLogic.thy --- /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; diff -r 6d5d3ecedf50 -r 2ebe9e630cab src/HOL/Isar_examples/Cantor.thy --- /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; diff -r 6d5d3ecedf50 -r 2ebe9e630cab src/HOL/Isar_examples/ExprCompiler.thy --- /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; diff -r 6d5d3ecedf50 -r 2ebe9e630cab src/HOL/Isar_examples/Peirce.thy --- /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; diff -r 6d5d3ecedf50 -r 2ebe9e630cab src/HOL/Isar_examples/ROOT.ML --- /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";