src/FOL/.ifol.thy.ML
author clasohm
Fri, 13 Oct 1995 11:48:40 +0100
changeset 1280 909079af97b7
parent 0 a5a9c433f639
permissions -rw-r--r--
corrected spelling of title
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
structure IFOL =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
 val parse_ast_translation = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
 val parse_preproc = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
 val parse_postproc = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
 val parse_translation = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
 val print_translation = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
 val print_preproc = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
 val print_postproc = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
 val print_ast_translation = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
(**** begin of user section ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
(**** end of user section ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
val thy = extend_theory (Pure.thy)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
 "IFOL"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
 ([("term", ["logic"])],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  ["term"],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  [(["o"], 0)],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  [(["o"], ([], "logic"))],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  [(["True", "False"], "o")],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  Some (NewSext {
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
   mixfix =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
    [Mixfix("(_)", "o => prop", "Trueprop", [0], 5),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
     Infixl("=", "['a,'a] => o", 50),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
     Mixfix("~ _", "o => o", "Not", [40], 40),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
     Infixr("&", "[o,o] => o", 35),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
     Infixr("|", "[o,o] => o", 30),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
     Infixr("-->", "[o,o] => o", 25),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
     Infixr("<->", "[o,o] => o", 25),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
     Binder("ALL ", "('a => o) => o", "All", 0, 10),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
     Binder("EX ", "('a => o) => o", "Ex", 0, 10),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
     Binder("EX! ", "('a => o) => o", "Ex1", 0, 10)],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
   xrules =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
    [],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
   parse_ast_translation = parse_ast_translation,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
   parse_preproc = parse_preproc,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
   parse_postproc = parse_postproc,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
   parse_translation = parse_translation,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
   print_translation = print_translation,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
   print_preproc = print_preproc,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
   print_postproc = print_postproc,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
   print_ast_translation = print_ast_translation}))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
 [("refl", "a=a"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
  ("subst", "[| a=b;  P(a) |] ==> P(b)"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
  ("conjI", "[| P;  Q |] ==> P&Q"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
  ("conjunct1", "P&Q ==> P"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  ("conjunct2", "P&Q ==> Q"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
  ("disjI1", "P ==> P|Q"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
  ("disjI2", "Q ==> P|Q"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
  ("disjE", "[| P|Q;  P ==> R;  Q ==> R |] ==> R"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
  ("impI", "(P ==> Q) ==> P-->Q"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  ("mp", "[| P-->Q;  P |] ==> Q"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
  ("FalseE", "False ==> P"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  ("True_def", "True == False-->False"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
  ("not_def", "~P == P-->False"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
  ("iff_def", "P<->Q == (P-->Q) & (Q-->P)"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
  ("ex1_def", "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  ("allI", "(!!x. P(x)) ==> (ALL x.P(x))"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
  ("spec", "(ALL x.P(x)) ==> P(x)"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
  ("exI", "P(x) ==> (EX x.P(x))"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
  ("exE", "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
  ("eq_reflection", "(x=y)   ==> (x==y)"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  ("iff_reflection", "(P<->Q) ==> (P==Q)")]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
val ax = get_axiom thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
val refl = ax "refl"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val subst = ax "subst"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
val conjI = ax "conjI"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val conjunct1 = ax "conjunct1"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
val conjunct2 = ax "conjunct2"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
val disjI1 = ax "disjI1"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
val disjI2 = ax "disjI2"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
val disjE = ax "disjE"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
val impI = ax "impI"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
val mp = ax "mp"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
val FalseE = ax "FalseE"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
val True_def = ax "True_def"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
val not_def = ax "not_def"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
val iff_def = ax "iff_def"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
val ex1_def = ax "ex1_def"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val allI = ax "allI"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val spec = ax "spec"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
val exI = ax "exI"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
val exE = ax "exE"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
val eq_reflection = ax "eq_reflection"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
val iff_reflection = ax "iff_reflection"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
end