src/Sequents/LK0.thy
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 16019 0e1405402d53
child 21426 87ac12bed1ab
permissions -rw-r--r--
converted to Isar theory format;
     1 (*  Title:      LK/LK0.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 There may be printing problems if a seqent is in expanded normal form
     7         (eta-expanded, beta-contracted)
     8 *)
     9 
    10 header {* Classical First-Order Sequent Calculus *}
    11 
    12 theory LK0
    13 imports Sequents
    14 begin
    15 
    16 global
    17 
    18 classes "term"
    19 defaultsort "term"
    20 
    21 consts
    22 
    23  Trueprop       :: "two_seqi"
    24 
    25   True         :: o
    26   False        :: o
    27   "="          :: "['a,'a] => o"     (infixl 50)
    28   Not          :: "o => o"           ("~ _" [40] 40)
    29   "&"          :: "[o,o] => o"       (infixr 35)
    30   "|"          :: "[o,o] => o"       (infixr 30)
    31   "-->"        :: "[o,o] => o"       (infixr 25)
    32   "<->"        :: "[o,o] => o"       (infixr 25)
    33   The          :: "('a => o) => 'a"  (binder "THE " 10)
    34   All          :: "('a => o) => o"   (binder "ALL " 10)
    35   Ex           :: "('a => o) => o"   (binder "EX " 10)
    36 
    37 syntax
    38  "@Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
    39   "_not_equal" :: "['a, 'a] => o"              (infixl "~=" 50)
    40 
    41 parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
    42 print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
    43 
    44 translations
    45   "x ~= y"      == "~ (x = y)"
    46 
    47 syntax (xsymbols)
    48   Not           :: "o => o"               ("\<not> _" [40] 40)
    49   "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
    50   "op |"        :: "[o, o] => o"          (infixr "\<or>" 30)
    51   "op -->"      :: "[o, o] => o"          (infixr "\<longrightarrow>" 25)
    52   "op <->"      :: "[o, o] => o"          (infixr "\<longleftrightarrow>" 25)
    53   "ALL "        :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
    54   "EX "         :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
    55   "EX! "        :: "[idts, o] => o"       ("(3\<exists>!_./ _)" [0, 10] 10)
    56   "_not_equal"  :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
    57 
    58 syntax (HTML output)
    59   Not           :: "o => o"               ("\<not> _" [40] 40)
    60   "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
    61   "op |"        :: "[o, o] => o"          (infixr "\<or>" 30)
    62   "ALL "        :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
    63   "EX "         :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
    64   "EX! "        :: "[idts, o] => o"       ("(3\<exists>!_./ _)" [0, 10] 10)
    65   "_not_equal"  :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
    66 
    67 local
    68 
    69 axioms
    70 
    71   (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
    72 
    73   contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F"
    74   contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
    75 
    76   thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F"
    77   thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E"
    78 
    79   exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F"
    80   exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
    81 
    82   cut:   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
    83 
    84   (*Propositional rules*)
    85 
    86   basic: "$H, P, $G |- $E, P, $F"
    87 
    88   conjR: "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
    89   conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
    90 
    91   disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
    92   disjL: "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
    93 
    94   impR:  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
    95   impL:  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
    96 
    97   notR:  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
    98   notL:  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
    99 
   100   FalseL: "$H, False, $G |- $E"
   101 
   102   True_def: "True == False-->False"
   103   iff_def:  "P<->Q == (P-->Q) & (Q-->P)"
   104 
   105   (*Quantifiers*)
   106 
   107   allR:  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
   108   allL:  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
   109 
   110   exR:   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
   111   exL:   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
   112 
   113   (*Equality*)
   114 
   115   refl:  "$H |- $E, a=a, $F"
   116   subst: "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
   117 
   118   (* Reflection *)
   119 
   120   eq_reflection:  "|- x=y ==> (x==y)"
   121   iff_reflection: "|- P<->Q ==> (P==Q)"
   122 
   123   (*Descriptions*)
   124 
   125   The: "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
   126           $H |- $E, P(THE x. P(x)), $F"
   127 
   128 constdefs
   129   If :: "[o, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
   130    "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
   131 
   132 setup
   133   prover_setup
   134 
   135 ML {* use_legacy_bindings (the_context ()) *}
   136 
   137 end
   138 
   139