src/FOL/IFOL.thy
author wenzelm
Mon, 16 Nov 1998 11:33:42 +0100
changeset 5896 4a75d89e2818
parent 4854 d1850e0964f2
child 6027 9dd06eeda95c
permissions -rw-r--r--
thm, thms;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1268
f6ef556b3ede corrected title
clasohm
parents: 928
diff changeset
     1
(*  Title:      FOL/IFOL.thy
35
d71f96f1780e ifol.thy: added ~= for "not equals"
lcp
parents: 0
diff changeset
     2
    ID:         $Id$
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
35
d71f96f1780e ifol.thy: added ~= for "not equals"
lcp
parents: 0
diff changeset
     4
    Copyright   1993  University of Cambridge
d71f96f1780e ifol.thy: added ~= for "not equals"
lcp
parents: 0
diff changeset
     5
2205
c5a7c72746ac added symbolfont syntax;
wenzelm
parents: 1322
diff changeset
     6
Intuitionistic first-order logic.
35
d71f96f1780e ifol.thy: added ~= for "not equals"
lcp
parents: 0
diff changeset
     7
*)
d71f96f1780e ifol.thy: added ~= for "not equals"
lcp
parents: 0
diff changeset
     8
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
     9
IFOL = Pure +
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
3906
5ae0e1324c56 global;
wenzelm
parents: 3835
diff changeset
    11
global
5ae0e1324c56 global;
wenzelm
parents: 3835
diff changeset
    12
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    13
classes
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    14
  term < logic
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    15
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    16
default
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    17
  term
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    19
types
278
523518f44286 adapted type definition to new syntax
clasohm
parents: 79
diff changeset
    20
  o
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    22
arities
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    23
  o :: logic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    25
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    26
consts
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
1322
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    28
  Trueprop      :: o => prop                    ("(_)" 5)
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    29
  True, False   :: o
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    30
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    31
  (* Connectives *)
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    32
1322
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    33
  "="           :: ['a, 'a] => o                (infixl 50)
35
d71f96f1780e ifol.thy: added ~= for "not equals"
lcp
parents: 0
diff changeset
    34
1322
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    35
  Not           :: o => o                       ("~ _" [40] 40)
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    36
  "&"           :: [o, o] => o                  (infixr 35)
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    37
  "|"           :: [o, o] => o                  (infixr 30)
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    38
  "-->"         :: [o, o] => o                  (infixr 25)
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    39
  "<->"         :: [o, o] => o                  (infixr 25)
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    40
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    41
  (* Quantifiers *)
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    42
1322
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    43
  All           :: ('a => o) => o               (binder "ALL " 10)
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    44
  Ex            :: ('a => o) => o               (binder "EX " 10)
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    45
  Ex1           :: ('a => o) => o               (binder "EX! " 10)
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    46
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
2257
c8154379738c symbol names changes;
wenzelm
parents: 2205
diff changeset
    48
928
cb31a4e97f75 Moved declaration of ~= to a syntax section
lcp
parents: 278
diff changeset
    49
syntax
1322
9b3d3362a048 removed quotes from types in consts section
clasohm
parents: 1268
diff changeset
    50
  "~="          :: ['a, 'a] => o                (infixl 50)
928
cb31a4e97f75 Moved declaration of ~= to a syntax section
lcp
parents: 278
diff changeset
    51
35
d71f96f1780e ifol.thy: added ~= for "not equals"
lcp
parents: 0
diff changeset
    52
translations
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    53
  "x ~= y"      == "~ (x = y)"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    54
2257
c8154379738c symbol names changes;
wenzelm
parents: 2205
diff changeset
    55
syntax (symbols)
c8154379738c symbol names changes;
wenzelm
parents: 2205
diff changeset
    56
  Not           :: o => o                       ("\\<not> _" [40] 40)
c8154379738c symbol names changes;
wenzelm
parents: 2205
diff changeset
    57
  "op &"        :: [o, o] => o                  (infixr "\\<and>" 35)
c8154379738c symbol names changes;
wenzelm
parents: 2205
diff changeset
    58
  "op |"        :: [o, o] => o                  (infixr "\\<or>" 30)
c8154379738c symbol names changes;
wenzelm
parents: 2205
diff changeset
    59
  "op -->"      :: [o, o] => o                  (infixr "\\<midarrow>\\<rightarrow>" 25)
c8154379738c symbol names changes;
wenzelm
parents: 2205
diff changeset
    60
  "op <->"      :: [o, o] => o                  (infixr "\\<leftarrow>\\<rightarrow>" 25)
2367
eba760ebe315 fixed pris of binder syntax;
wenzelm
parents: 2257
diff changeset
    61
  "ALL "        :: [idts, o] => o               ("(3\\<forall>_./ _)" [0, 10] 10)
eba760ebe315 fixed pris of binder syntax;
wenzelm
parents: 2257
diff changeset
    62
  "EX "         :: [idts, o] => o               ("(3\\<exists>_./ _)" [0, 10] 10)
eba760ebe315 fixed pris of binder syntax;
wenzelm
parents: 2257
diff changeset
    63
  "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" [0, 10] 10)
2257
c8154379738c symbol names changes;
wenzelm
parents: 2205
diff changeset
    64
  "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
2205
c5a7c72746ac added symbolfont syntax;
wenzelm
parents: 1322
diff changeset
    65
35
d71f96f1780e ifol.thy: added ~= for "not equals"
lcp
parents: 0
diff changeset
    66
3932
wenzelm
parents: 3906
diff changeset
    67
local
3906
5ae0e1324c56 global;
wenzelm
parents: 3835
diff changeset
    68
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    71
  (* Equality *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    73
  refl          "a=a"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    74
  subst         "[| a=b;  P(a) |] ==> P(b)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    76
  (* Propositional logic *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    78
  conjI         "[| P;  Q |] ==> P&Q"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    79
  conjunct1     "P&Q ==> P"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    80
  conjunct2     "P&Q ==> Q"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    82
  disjI1        "P ==> P|Q"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    83
  disjI2        "Q ==> P|Q"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    84
  disjE         "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    86
  impI          "(P ==> Q) ==> P-->Q"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    87
  mp            "[| P-->Q;  P |] ==> Q"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    89
  FalseE        "False ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    91
  (* Definitions *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    93
  True_def      "True  == False-->False"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    94
  not_def       "~P    == P-->False"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    95
  iff_def       "P<->Q == (P-->Q) & (Q-->P)"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    96
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    97
  (* Unique existence *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
    99
  ex1_def       "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
   101
  (* Quantifiers *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
3835
9a5a4e123859 fixed dots;
wenzelm
parents: 2367
diff changeset
   103
  allI          "(!!x. P(x)) ==> (ALL x. P(x))"
9a5a4e123859 fixed dots;
wenzelm
parents: 2367
diff changeset
   104
  spec          "(ALL x. P(x)) ==> P(x)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
3835
9a5a4e123859 fixed dots;
wenzelm
parents: 2367
diff changeset
   106
  exI           "P(x) ==> (EX x. P(x))"
9a5a4e123859 fixed dots;
wenzelm
parents: 2367
diff changeset
   107
  exE           "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
  (* Reflection *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
79
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
   111
  eq_reflection   "(x=y)   ==> (x==y)"
74e68ed3b4fd added white-space;
wenzelm
parents: 35
diff changeset
   112
  iff_reflection  "(P<->Q) ==> (P==Q)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
4092
9faf228771dc added simpset thy_data;
wenzelm
parents: 3932
diff changeset
   114
4854
d1850e0964f2 tuned setup;
wenzelm
parents: 4793
diff changeset
   115
setup
d1850e0964f2 tuned setup;
wenzelm
parents: 4793
diff changeset
   116
  Simplifier.setup
4092
9faf228771dc added simpset thy_data;
wenzelm
parents: 3932
diff changeset
   117
4854
d1850e0964f2 tuned setup;
wenzelm
parents: 4793
diff changeset
   118
end