src/Sequents/ILL.thy
changeset 17481 75166ebb619b
parent 14765 bafb24c150c1
child 21427 7c8f4a331f9b
     1.1 --- a/src/Sequents/ILL.thy	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/ILL.thy	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -1,11 +1,12 @@
     1.4 -(*  Title:      ILL.thy
     1.5 +(*  Title:      Sequents/ILL.thy
     1.6      ID:         $Id$
     1.7      Author:     Sara Kalvala and Valeria de Paiva
     1.8      Copyright   1995  University of Cambridge
     1.9  *)
    1.10  
    1.11 -
    1.12 -ILL = Sequents +
    1.13 +theory ILL
    1.14 +imports Sequents
    1.15 +begin
    1.16  
    1.17  consts
    1.18    Trueprop       :: "two_seqi"
    1.19 @@ -35,98 +36,93 @@
    1.20    "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
    1.21    "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")
    1.22  
    1.23 +parse_translation {*
    1.24 +  [("@Trueprop", single_tr "Trueprop"),
    1.25 +   ("@Context", two_seq_tr "Context"),
    1.26 +   ("@PromAux", three_seq_tr "PromAux")] *}
    1.27 +
    1.28 +print_translation {*
    1.29 +  [("Trueprop", single_tr' "@Trueprop"),
    1.30 +   ("Context", two_seq_tr'"@Context"),
    1.31 +   ("PromAux", three_seq_tr'"@PromAux")] *}
    1.32 +
    1.33  defs
    1.34  
    1.35 -liff_def        "P o-o Q == (P -o Q) >< (Q -o P)"
    1.36 +liff_def:        "P o-o Q == (P -o Q) >< (Q -o P)"
    1.37  
    1.38 -aneg_def        "~A == A -o 0"
    1.39 +aneg_def:        "~A == A -o 0"
    1.40  
    1.41  
    1.42 -
    1.43 -
    1.44 -rules
    1.45 +axioms
    1.46  
    1.47 -identity        "P |- P"
    1.48 +identity:        "P |- P"
    1.49  
    1.50 -zerol           "$G, 0, $H |- A"
    1.51 +zerol:           "$G, 0, $H |- A"
    1.52  
    1.53    (* RULES THAT DO NOT DIVIDE CONTEXT *)
    1.54  
    1.55 -derelict   "$F, A, $G |- C ==> $F, !A, $G |- C"
    1.56 +derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C"
    1.57    (* unfortunately, this one removes !A  *)
    1.58  
    1.59 -contract  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
    1.60 +contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
    1.61  
    1.62 -weaken     "$F, $G |- C ==> $G, !A, $F |- C"
    1.63 +weaken:     "$F, $G |- C ==> $G, !A, $F |- C"
    1.64    (* weak form of weakening, in practice just to clean context *)
    1.65    (* weaken and contract not needed (CHECK)  *)
    1.66  
    1.67 -promote2        "promaux{ || $H || B} ==> $H |- !B"
    1.68 -promote1        "promaux{!A, $G || $H || B}
    1.69 -                 ==> promaux {$G || $H, !A || B}"
    1.70 -promote0        "$G |- A ==> promaux {$G || || A}"
    1.71 +promote2:        "promaux{ || $H || B} ==> $H |- !B"
    1.72 +promote1:        "promaux{!A, $G || $H || B}
    1.73 +                  ==> promaux {$G || $H, !A || B}"
    1.74 +promote0:        "$G |- A ==> promaux {$G || || A}"
    1.75  
    1.76  
    1.77  
    1.78 -tensl     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
    1.79 +tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
    1.80  
    1.81 -impr      "A, $F |- B ==> $F |- A -o B"
    1.82 +impr:      "A, $F |- B ==> $F |- A -o B"
    1.83  
    1.84 -conjr           "[| $F |- A ;
    1.85 +conjr:           "[| $F |- A ;
    1.86                   $F |- B |]
    1.87                  ==> $F |- (A && B)"
    1.88  
    1.89 -conjll          "$G, A, $H |- C ==> $G, A && B, $H |- C"
    1.90 +conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C"
    1.91  
    1.92 -conjlr          "$G, B, $H |- C ==> $G, A && B, $H |- C"
    1.93 +conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C"
    1.94  
    1.95 -disjrl          "$G |- A ==> $G |- A ++ B"
    1.96 -disjrr          "$G |- B ==> $G |- A ++ B"
    1.97 -disjl           "[| $G, A, $H |- C ;
    1.98 -                    $G, B, $H |- C |]
    1.99 -                ==> $G, A ++ B, $H |- C"
   1.100 +disjrl:          "$G |- A ==> $G |- A ++ B"
   1.101 +disjrr:          "$G |- B ==> $G |- A ++ B"
   1.102 +disjl:           "[| $G, A, $H |- C ;
   1.103 +                     $G, B, $H |- C |]
   1.104 +                 ==> $G, A ++ B, $H |- C"
   1.105  
   1.106  
   1.107        (* RULES THAT DIVIDE CONTEXT *)
   1.108  
   1.109 -tensr           "[| $F, $J :=: $G;
   1.110 -                    $F |- A ;
   1.111 -                    $J |- B     |]
   1.112 -                    ==> $G |- A >< B"
   1.113 +tensr:           "[| $F, $J :=: $G;
   1.114 +                     $F |- A ;
   1.115 +                     $J |- B     |]
   1.116 +                     ==> $G |- A >< B"
   1.117  
   1.118 -impl            "[| $G, $F :=: $J, $H ;
   1.119 -                    B, $F |- C ;
   1.120 -                       $G |- A |]
   1.121 -                    ==> $J, A -o B, $H |- C"
   1.122 +impl:            "[| $G, $F :=: $J, $H ;
   1.123 +                     B, $F |- C ;
   1.124 +                        $G |- A |]
   1.125 +                     ==> $J, A -o B, $H |- C"
   1.126  
   1.127  
   1.128 -cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
   1.129 -         $H1, $H2, $H3, $H4 |- A ;
   1.130 -         $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
   1.131 +cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
   1.132 +          $H1, $H2, $H3, $H4 |- A ;
   1.133 +          $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
   1.134  
   1.135  
   1.136    (* CONTEXT RULES *)
   1.137  
   1.138 -context1     "$G :=: $G"
   1.139 -context2     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
   1.140 -context3     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
   1.141 -context4a    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
   1.142 -context4b    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
   1.143 -context5     "$F, $G :=: $H ==> $G, $F :=: $H"
   1.144 +context1:     "$G :=: $G"
   1.145 +context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
   1.146 +context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
   1.147 +context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
   1.148 +context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
   1.149 +context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
   1.150  
   1.151 -
   1.152 -
   1.153 +ML {* use_legacy_bindings (the_context ()) *}
   1.154  
   1.155  end
   1.156 -
   1.157 -ML
   1.158 -
   1.159 -val parse_translation = [("@Trueprop",Sequents.single_tr "Trueprop"),
   1.160 -                         ("@Context",Sequents.two_seq_tr "Context"),
   1.161 -                         ("@PromAux", Sequents.three_seq_tr "PromAux")];
   1.162 -
   1.163 -val print_translation = [("Trueprop",Sequents.single_tr' "@Trueprop"),
   1.164 -                         ("Context",Sequents.two_seq_tr'"@Context"),
   1.165 -                         ("PromAux", Sequents.three_seq_tr'"@PromAux")];
   1.166 -
   1.167 -