# HG changeset patch
# User wenzelm
# Date 965123894 -7200
# Node ID 7e377f912629cfa30ea1e82e10ec5c1dc5903770
# Parent  2df511ebb95676d4a7ef6e728ba5d3a4ea286618
improved comments;
added all_eq, imp_eq (for blast);
basic calculational rules;

diff -r 2df511ebb956 -r 7e377f912629 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Tue Aug 01 11:57:09 2000 +0200
+++ b/src/FOL/FOL.thy	Tue Aug 01 11:58:14 2000 +0200
@@ -1,16 +1,83 @@
+(*  Title:      FOL/FOL.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson and Markus Wenzel
+
+Classical first-order logic.
+
+This may serve as a good example of initializing all the tools and
+packages required for a reasonable working environment.  Please go
+elsewhere to see actual applications!
+*)
 
 theory FOL = IFOL
-files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"):
+files
+  ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML")
+  ("simpdata.ML") ("FOL_lemmas2.ML"):
+
+
+subsection {* The classical axiom *}
 
 axioms
   classical: "(~P ==> P) ==> P"
 
+
+subsection {* Setup of several proof tools *}
+
 use "FOL_lemmas1.ML"
-use "cladata.ML"        setup Cla.setup setup clasetup
-use "blastdata.ML"      setup Blast.setup
+use "cladata.ML"
+setup Cla.setup
+setup clasetup
+
+lemma all_eq: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
+proof (rule equal_intr_rule)
+  assume "!!x. P(x)"
+  show "ALL x. P(x)" ..
+next
+  assume "ALL x. P(x)"
+  thus "!!x. P(x)" ..
+qed
+
+lemma imp_eq: "(A ==> B) == Trueprop (A --> B)"
+proof (rule equal_intr_rule)
+  assume r: "A ==> B"
+  show "A --> B"
+    by (rule) (rule r)
+next
+  assume "A --> B" and A
+  thus B ..
+qed
+
+use "blastdata.ML"
+setup Blast.setup
 use "FOL_lemmas2.ML"
-use "simpdata.ML"       setup simpsetup setup cong_attrib_setup
-                        setup "Simplifier.method_setup Splitter.split_modifiers"
-                        setup Splitter.setup setup Clasimp.setup
+
+use "simpdata.ML"
+setup simpsetup
+setup cong_attrib_setup
+setup "Simplifier.method_setup Splitter.split_modifiers"
+setup Splitter.setup
+setup Clasimp.setup
+
+
+subsection {* Calculational rules *}
+
+lemma forw_subst: "a = b ==> P(b) ==> P(a)"
+  by (rule ssubst)
+
+lemma back_subst: "P(a) ==> a = b ==> P(b)"
+  by (rule subst)
+
+text {*
+  Note that this list of rules is in reverse order of priorities.
+*}
+
+lemmas trans_rules [trans] =
+  forw_subst
+  back_subst
+  rev_mp
+  mp
+  trans
+
+lemmas [elim?] = sym
 
 end