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