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