src/Sequents/ILL.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ILL.thy	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,134 @@
+(*  Title:      ILL.thy
+    ID:         $Id$
+    Author:     Sara Kalvala and Valeria de Paiva
+    Copyright   1995  University of Cambridge
+*)
+
+
+ILL = Sequents +
+
+consts
+
+  
+ Trueprop	:: "two_seqi"
+ "@Trueprop"	:: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
+ 
+ 
+
+"><"    ::"[o, o] => o"        (infixr 35)
+"-o"    ::"[o, o] => o"        (infixr 45)
+"o-o"   ::"[o, o] => o"        (infixr 45)
+FShriek ::"o => o"             ("! _" [100] 1000)
+"&&"    ::"[o, o] => o"        (infixr 35)
+"++"    ::"[o, o] => o"        (infixr 35)
+zero    ::"o"                  ("0")
+top     ::"o"                  ("1")
+eye     ::"o"                  ("I")
+aneg    ::"o=>o"               ("~_")
+
+
+  (* syntax for context manipulation *)
+
+ Context      :: "two_seqi"
+"@Context"    :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
+
+  (* syntax for promotion rule *)
+
+  PromAux :: "three_seqi"
+"@PromAux":: "three_seqe" ("promaux {_||_||_}")
+
+defs
+
+liff_def        "P o-o Q == (P -o Q) >< (Q -o P)"
+
+aneg_def        "~A == A -o 0"
+
+
+
+
+rules
+  
+identity        "P |- P"
+
+zerol           "$G, 0, $H |- A"
+
+  (* RULES THAT DO NOT DIVIDE CONTEXT *)
+
+derelict   "$F, A, $G |- C ==> $F, !A, $G |- C"
+  (* unfortunately, this one removes !A  *)
+
+contract  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
+  
+weaken     "$F, $G |- C ==> $G, !A, $F |- C"
+  (* weak form of weakening, in practice just to clean context *)
+  (* weaken and contract not needed (CHECK)  *)
+
+promote2        "promaux{ || $H || B} ==> $H |- !B"
+promote1        "promaux{!A, $G || $H || B}
+                 ==> promaux {$G || $H, !A || B}"
+promote0        "$G |- A ==> promaux {$G || || A}"
+
+
+  
+tensl     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
+
+impr      "A, $F |- B ==> $F |- A -o B"
+
+conjr           "[| $F |- A ;
+                 $F |- B |]
+                ==> $F |- (A && B)"
+
+conjll          "$G, A, $H |- C ==> $G, A && B, $H |- C"
+
+conjlr          "$G, B, $H |- C ==> $G, A && B, $H |- C"
+
+disjrl          "$G |- A ==> $G |- A ++ B"
+disjrr          "$G |- B ==> $G |- A ++ B"
+disjl           "[| $G, A, $H |- C ;
+                    $G, B, $H |- C |]
+                ==> $G, A ++ B, $H |- C"
+
+
+      (* RULES THAT DIVIDE CONTEXT *)
+
+tensr           "[| $F, $J :=: $G;
+                    $F |- A ;
+                    $J |- B     |]
+                    ==> $G |- A >< B"
+
+impl            "[| $G, $F :=: $J, $H ;
+                    B, $F |- C ;
+                       $G |- A |]
+                    ==> $J, A -o B, $H |- C"
+
+    
+cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
+         $H1, $H2, $H3, $H4 |- A ;
+         $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
+
+
+  (* CONTEXT RULES *)
+
+context1     "$G :=: $G"
+context2     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
+context3     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
+context4a    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
+context4b    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
+context5     "$F, $G :=: $H ==> $G, $F :=: $H"
+
+
+
+ 
+end
+
+ML
+
+val parse_translation = [("@Trueprop",Sequents.single_tr "Trueprop"),
+                         ("@Context",Sequents.two_seq_tr "Context"),
+                         ("@PromAux", Sequents.three_seq_tr "PromAux")];
+
+val print_translation = [("Trueprop",Sequents.single_tr' "@Trueprop"),
+                         ("Context",Sequents.two_seq_tr'"@Context"),
+                         ("PromAux", Sequents.three_seq_tr'"@PromAux")];
+
+