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