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