--- /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")];
+
+