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