src/FOL/FOL.thy
changeset 11678 6aa3e2d26683
parent 11096 bedfd42db838
child 11771 b7b100a2de1d
equal deleted inserted replaced
11677:ee12f18599e5 11678:6aa3e2d26683
     1 (*  Title:      FOL/FOL.thy
     1 (*  Title:      FOL/FOL.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     3     Author:     Lawrence C Paulson and Markus Wenzel
       
     4 *)
     4 
     5 
     5 Classical first-order logic.
     6 header {* Classical first-order logic *}
     6 
       
     7 This may serve as a good example of initializing all the tools and
       
     8 packages required for a reasonable working environment.  Please go
       
     9 elsewhere to see actual applications!
       
    10 *)
       
    11 
     7 
    12 theory FOL = IFOL
     8 theory FOL = IFOL
    13 files
     9 files
    14   ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML")
    10   ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML")
    15   ("simpdata.ML") ("FOL_lemmas2.ML"):
    11   ("simpdata.ML") ("FOL_lemmas2.ML"):
    19 
    15 
    20 axioms
    16 axioms
    21   classical: "(~P ==> P) ==> P"
    17   classical: "(~P ==> P) ==> P"
    22 
    18 
    23 
    19 
    24 subsection {* Setup of several proof tools *}
    20 subsection {* Lemmas and proof tools *}
    25 
    21 
    26 use "FOL_lemmas1.ML"
    22 use "FOL_lemmas1.ML"
    27 
    23 theorems case_split = case_split_thm [case_names True False]
    28 lemma atomize_all: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
       
    29 proof (rule equal_intr_rule)
       
    30   assume "!!x. P(x)"
       
    31   show "ALL x. P(x)" by (rule allI)
       
    32 next
       
    33   assume "ALL x. P(x)"
       
    34   thus "!!x. P(x)" by (rule allE)
       
    35 qed
       
    36 
       
    37 lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)"
       
    38 proof (rule equal_intr_rule)
       
    39   assume r: "A ==> B"
       
    40   show "A --> B" by (rule impI) (rule r)
       
    41 next
       
    42   assume "A --> B" and A
       
    43   thus B by (rule mp)
       
    44 qed
       
    45 
       
    46 lemma atomize_eq: "(x == y) == Trueprop (x = y)"
       
    47 proof (rule equal_intr_rule)
       
    48   assume "x == y"
       
    49   show "x = y" by (unfold prems) (rule refl)
       
    50 next
       
    51   assume "x = y"
       
    52   thus "x == y" by (rule eq_reflection)
       
    53 qed
       
    54 
       
    55 lemmas atomize = atomize_all atomize_imp
       
    56 lemmas atomize' = atomize atomize_eq
       
    57 
    24 
    58 use "cladata.ML"
    25 use "cladata.ML"
    59 setup Cla.setup
    26 setup Cla.setup
    60 setup clasetup
    27 setup clasetup
    61 
    28 
    67 setup simpsetup
    34 setup simpsetup
    68 setup "Simplifier.method_setup Splitter.split_modifiers"
    35 setup "Simplifier.method_setup Splitter.split_modifiers"
    69 setup Splitter.setup
    36 setup Splitter.setup
    70 setup Clasimp.setup
    37 setup Clasimp.setup
    71 setup Rulify.setup
    38 setup Rulify.setup
       
    39 
       
    40 
       
    41 
       
    42 subsection {* Proof by cases and induction *}
       
    43 
       
    44 text {* Proper handling of non-atomic rule statements. *}
       
    45 
       
    46 constdefs
       
    47   induct_forall :: "('a => o) => o"
       
    48   "induct_forall(P) == \<forall>x. P(x)"
       
    49   induct_implies :: "o => o => o"
       
    50   "induct_implies(A, B) == A --> B"
       
    51   induct_equal :: "'a => 'a => o"
       
    52   "induct_equal(x, y) == x = y"
       
    53 
       
    54 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
       
    55   by (simp only: atomize_all induct_forall_def)
       
    56 
       
    57 lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))"
       
    58   by (simp only: atomize_imp induct_implies_def)
       
    59 
       
    60 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
       
    61   by (simp only: atomize_eq induct_equal_def)
       
    62 
       
    63 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq
       
    64 lemmas induct_rulify1 = induct_atomize [symmetric, standard]
       
    65 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def
       
    66 
       
    67 hide const induct_forall induct_implies induct_equal
       
    68 
       
    69 
       
    70 text {* Method setup. *}
       
    71 
       
    72 ML {*
       
    73   structure InductMethod = InductMethodFun
       
    74   (struct
       
    75     val dest_concls = FOLogic.dest_concls;
       
    76     val cases_default = thm "case_split";
       
    77     val conjI = thm "conjI";
       
    78     val atomize = thms "induct_atomize";
       
    79     val rulify1 = thms "induct_rulify1";
       
    80     val rulify2 = thms "induct_rulify2";
       
    81   end);
       
    82 *}
       
    83 
       
    84 setup InductMethod.setup
    72 
    85 
    73 
    86 
    74 subsection {* Calculational rules *}
    87 subsection {* Calculational rules *}
    75 
    88 
    76 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
    89 lemma forw_subst: "a = b ==> P(b) ==> P(a)"