# 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