src/FOL/FOL.thy
author wenzelm
Fri, 04 Aug 2000 22:54:49 +0200
changeset 9525 46fb9ccae463
parent 9487 7e377f912629
child 9713 2c5b42311eb0
permissions -rw-r--r--
lemmas atomize = all_eq imp_eq;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     1
(*  Title:      FOL/FOL.thy
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     2
    ID:         $Id$
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     3
    Author:     Lawrence C Paulson and Markus Wenzel
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     4
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     5
Classical first-order logic.
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     6
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     7
This may serve as a good example of initializing all the tools and
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     8
packages required for a reasonable working environment.  Please go
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     9
elsewhere to see actual applications!
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    10
*)
4093
5e8f3d57dee7 added claset thy_data;
wenzelm
parents: 0
diff changeset
    11
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 5887
diff changeset
    12
theory FOL = IFOL
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    13
files
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    14
  ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML")
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    15
  ("simpdata.ML") ("FOL_lemmas2.ML"):
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    16
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    17
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    18
subsection {* The classical axiom *}
4093
5e8f3d57dee7 added claset thy_data;
wenzelm
parents: 0
diff changeset
    19
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 5887
diff changeset
    20
axioms
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 5887
diff changeset
    21
  classical: "(~P ==> P) ==> P"
4093
5e8f3d57dee7 added claset thy_data;
wenzelm
parents: 0
diff changeset
    22
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    23
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    24
subsection {* Setup of several proof tools *}
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    25
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 5887
diff changeset
    26
use "FOL_lemmas1.ML"
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    27
use "cladata.ML"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    28
setup Cla.setup
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    29
setup clasetup
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    30
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    31
lemma all_eq: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    32
proof (rule equal_intr_rule)
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    33
  assume "!!x. P(x)"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    34
  show "ALL x. P(x)" ..
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    35
next
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    36
  assume "ALL x. P(x)"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    37
  thus "!!x. P(x)" ..
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    38
qed
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    39
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    40
lemma imp_eq: "(A ==> B) == Trueprop (A --> B)"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    41
proof (rule equal_intr_rule)
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    42
  assume r: "A ==> B"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    43
  show "A --> B"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    44
    by (rule) (rule r)
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    45
next
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    46
  assume "A --> B" and A
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    47
  thus B ..
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    48
qed
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    49
9525
46fb9ccae463 lemmas atomize = all_eq imp_eq;
wenzelm
parents: 9487
diff changeset
    50
lemmas atomize = all_eq imp_eq
46fb9ccae463 lemmas atomize = all_eq imp_eq;
wenzelm
parents: 9487
diff changeset
    51
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    52
use "blastdata.ML"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    53
setup Blast.setup
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 5887
diff changeset
    54
use "FOL_lemmas2.ML"
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    55
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    56
use "simpdata.ML"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    57
setup simpsetup
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    58
setup cong_attrib_setup
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    59
setup "Simplifier.method_setup Splitter.split_modifiers"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    60
setup Splitter.setup
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    61
setup Clasimp.setup
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    62
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    63
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    64
subsection {* Calculational rules *}
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    65
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    66
lemma forw_subst: "a = b ==> P(b) ==> P(a)"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    67
  by (rule ssubst)
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    68
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    69
lemma back_subst: "P(a) ==> a = b ==> P(b)"
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    70
  by (rule subst)
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    71
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    72
text {*
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    73
  Note that this list of rules is in reverse order of priorities.
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    74
*}
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    75
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    76
lemmas trans_rules [trans] =
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    77
  forw_subst
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    78
  back_subst
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    79
  rev_mp
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    80
  mp
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    81
  trans
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    82
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    83
lemmas [elim?] = sym
4093
5e8f3d57dee7 added claset thy_data;
wenzelm
parents: 0
diff changeset
    84
4854
d1850e0964f2 tuned setup;
wenzelm
parents: 4793
diff changeset
    85
end