src/Sequents/ILL.thy
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 14765 bafb24c150c1
child 21427 7c8f4a331f9b
permissions -rw-r--r--
converted to Isar theory format;
     1 (*  Title:      Sequents/ILL.thy
     2     ID:         $Id$
     3     Author:     Sara Kalvala and Valeria de Paiva
     4     Copyright   1995  University of Cambridge
     5 *)
     6 
     7 theory ILL
     8 imports Sequents
     9 begin
    10 
    11 consts
    12   Trueprop       :: "two_seqi"
    13 
    14 "><"    ::"[o, o] => o"        (infixr 35)
    15 "-o"    ::"[o, o] => o"        (infixr 45)
    16 "o-o"   ::"[o, o] => o"        (infixr 45)
    17 FShriek ::"o => o"             ("! _" [100] 1000)
    18 "&&"    ::"[o, o] => o"        (infixr 35)
    19 "++"    ::"[o, o] => o"        (infixr 35)
    20 zero    ::"o"                  ("0")
    21 top     ::"o"                  ("1")
    22 eye     ::"o"                  ("I")
    23 aneg    ::"o=>o"               ("~_")
    24 
    25 
    26   (* context manipulation *)
    27 
    28  Context      :: "two_seqi"
    29 
    30   (* promotion rule *)
    31 
    32   PromAux :: "three_seqi"
    33 
    34 syntax
    35   "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
    36   "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
    37   "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")
    38 
    39 parse_translation {*
    40   [("@Trueprop", single_tr "Trueprop"),
    41    ("@Context", two_seq_tr "Context"),
    42    ("@PromAux", three_seq_tr "PromAux")] *}
    43 
    44 print_translation {*
    45   [("Trueprop", single_tr' "@Trueprop"),
    46    ("Context", two_seq_tr'"@Context"),
    47    ("PromAux", three_seq_tr'"@PromAux")] *}
    48 
    49 defs
    50 
    51 liff_def:        "P o-o Q == (P -o Q) >< (Q -o P)"
    52 
    53 aneg_def:        "~A == A -o 0"
    54 
    55 
    56 axioms
    57 
    58 identity:        "P |- P"
    59 
    60 zerol:           "$G, 0, $H |- A"
    61 
    62   (* RULES THAT DO NOT DIVIDE CONTEXT *)
    63 
    64 derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C"
    65   (* unfortunately, this one removes !A  *)
    66 
    67 contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
    68 
    69 weaken:     "$F, $G |- C ==> $G, !A, $F |- C"
    70   (* weak form of weakening, in practice just to clean context *)
    71   (* weaken and contract not needed (CHECK)  *)
    72 
    73 promote2:        "promaux{ || $H || B} ==> $H |- !B"
    74 promote1:        "promaux{!A, $G || $H || B}
    75                   ==> promaux {$G || $H, !A || B}"
    76 promote0:        "$G |- A ==> promaux {$G || || A}"
    77 
    78 
    79 
    80 tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
    81 
    82 impr:      "A, $F |- B ==> $F |- A -o B"
    83 
    84 conjr:           "[| $F |- A ;
    85                  $F |- B |]
    86                 ==> $F |- (A && B)"
    87 
    88 conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C"
    89 
    90 conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C"
    91 
    92 disjrl:          "$G |- A ==> $G |- A ++ B"
    93 disjrr:          "$G |- B ==> $G |- A ++ B"
    94 disjl:           "[| $G, A, $H |- C ;
    95                      $G, B, $H |- C |]
    96                  ==> $G, A ++ B, $H |- C"
    97 
    98 
    99       (* RULES THAT DIVIDE CONTEXT *)
   100 
   101 tensr:           "[| $F, $J :=: $G;
   102                      $F |- A ;
   103                      $J |- B     |]
   104                      ==> $G |- A >< B"
   105 
   106 impl:            "[| $G, $F :=: $J, $H ;
   107                      B, $F |- C ;
   108                         $G |- A |]
   109                      ==> $J, A -o B, $H |- C"
   110 
   111 
   112 cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
   113           $H1, $H2, $H3, $H4 |- A ;
   114           $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
   115 
   116 
   117   (* CONTEXT RULES *)
   118 
   119 context1:     "$G :=: $G"
   120 context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
   121 context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
   122 context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
   123 context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
   124 context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
   125 
   126 ML {* use_legacy_bindings (the_context ()) *}
   127 
   128 end