0

1 
(* Title: LK/lk.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Classical FirstOrder Sequent Calculus


7 
*)


8 


9 
LK = Pure +

283

10 

0

11 
classes term < logic

283

12 

0

13 
default term

283

14 


15 
types


16 
o sequence seqobj seqcont sequ sobj


17 


18 
arities


19 
o :: logic


20 

0

21 
consts


22 
True,False :: "o"


23 
"=" :: "['a,'a] => o" (infixl 50)


24 
"Not" :: "o => o" ("~ _" [40] 40)


25 
"&" :: "[o,o] => o" (infixr 35)


26 
"" :: "[o,o] => o" (infixr 30)


27 
">","<>" :: "[o,o] => o" (infixr 25)


28 
The :: "('a => o) => 'a" (binder "THE " 10)


29 
All :: "('a => o) => o" (binder "ALL " 10)


30 
Ex :: "('a => o) => o" (binder "EX " 10)


31 


32 
(*Representation of sequents*)


33 
Trueprop :: "[sobj=>sobj,sobj=>sobj] => prop"


34 
Seqof :: "o => sobj=>sobj"


35 
"@Trueprop" :: "[sequence,sequence] => prop" ("((_)/  (_))" [6,6] 5)


36 
"@MtSeq" :: "sequence" ("" [] 1000)


37 
"@NmtSeq" :: "[seqobj,seqcont] => sequence" ("__" [] 1000)


38 
"@MtSeqCont" :: "seqcont" ("" [] 1000)


39 
"@SeqCont" :: "[seqobj,seqcont] => seqcont" (",/ __" [] 1000)


40 
"" :: "o => seqobj" ("_" [] 1000)


41 
"@SeqId" :: "id => seqobj" ("$_" [] 1000)


42 
"@SeqVar" :: "var => seqobj" ("$_")


43 


44 
rules


45 
(*Structural rules*)


46 


47 
basic "$H, P, $G  $E, P, $F"


48 


49 
thinR "$H  $E, $F ==> $H  $E, P, $F"


50 
thinL "$H, $G  $E ==> $H, P, $G  $E"


51 


52 
cut "[ $H  $E, P; $H, P  $E ] ==> $H  $E"


53 


54 
(*Propositional rules*)


55 


56 
conjR "[ $H $E, P, $F; $H $E, Q, $F ] ==> $H $E, P&Q, $F"


57 
conjL "$H, P, Q, $G  $E ==> $H, P & Q, $G  $E"


58 


59 
disjR "$H  $E, P, Q, $F ==> $H  $E, PQ, $F"


60 
disjL "[ $H, P, $G  $E; $H, Q, $G  $E ] ==> $H, PQ, $G  $E"


61 


62 
impR "$H, P  $E, Q, $F ==> $H  $E, P>Q, $F"


63 
impL "[ $H,$G  $E,P; $H, Q, $G  $E ] ==> $H, P>Q, $G  $E"


64 


65 
notR "$H, P  $E, $F ==> $H  $E, ~P, $F"


66 
notL "$H, $G  $E, P ==> $H, ~P, $G  $E"


67 


68 
FalseL "$H, False, $G  $E"


69 


70 
True_def "True == False>False"


71 
iff_def "P<>Q == (P>Q) & (Q>P)"


72 


73 
(*Quantifiers*)


74 


75 
allR "(!!x.$H  $E, P(x), $F) ==> $H  $E, ALL x.P(x), $F"


76 
allL "$H, P(x), $G, ALL x.P(x)  $E ==> $H, ALL x.P(x), $G  $E"


77 


78 
exR "$H  $E, P(x), $F, EX x.P(x) ==> $H  $E, EX x.P(x), $F"


79 
exL "(!!x.$H, P(x), $G  $E) ==> $H, EX x.P(x), $G  $E"


80 


81 
(*Equality*)


82 


83 
refl "$H  $E, a=a, $F"


84 
sym "$H  $E, a=b, $F ==> $H  $E, b=a, $F"


85 
trans "[ $H $E, a=b, $F; $H $E, b=c, $F ] ==> $H $E, a=c, $F"


86 


87 


88 
(*Descriptions*)


89 


90 
The "[ $H  $E, P(a), $F; !!x.$H, P(x)  $E, x=a, $F ] ==> \


91 
\ $H  $E, P(THE x.P(x)), $F"


92 
end


93 


94 
ML


95 


96 
(*Abstract over "sobj"  representation of a sequence of formulae *)


97 
fun abs_sobj t = Abs("sobj", Type("sobj",[]), t);


98 


99 
(*Representation of empty sequence*)


100 
val Sempty = abs_sobj (Bound 0);


101 


102 
fun seq_obj_tr(Const("@SeqId",_)$id) = id 


103 
seq_obj_tr(Const("@SeqVar",_)$id) = id 


104 
seq_obj_tr(fm) = Const("Seqof",dummyT)$fm;


105 


106 
fun seq_tr(_$obj$seq) = seq_obj_tr(obj)$seq_tr(seq) 


107 
seq_tr(_) = Bound 0;


108 


109 
fun seq_tr1(Const("@MtSeq",_)) = Sempty 


110 
seq_tr1(seq) = abs_sobj(seq_tr seq);


111 


112 
fun true_tr[s1,s2] = Const("Trueprop",dummyT)$seq_tr1 s1$seq_tr1 s2;


113 


114 
fun seq_obj_tr'(Const("Seqof",_)$fm) = fm 


115 
seq_obj_tr'(id) = Const("@SeqId",dummyT)$id;


116 


117 
fun seq_tr'(obj$sq,C) =


118 
let val sq' = case sq of


119 
Bound 0 => Const("@MtSeqCont",dummyT) 


120 
_ => seq_tr'(sq,Const("@SeqCont",dummyT))


121 
in C $ seq_obj_tr' obj $ sq' end;


122 


123 
fun seq_tr1'(Bound 0) = Const("@MtSeq",dummyT) 


124 
seq_tr1' s = seq_tr'(s,Const("@NmtSeq",dummyT));


125 


126 
fun true_tr'[Abs(_,_,s1),Abs(_,_,s2)] =


127 
Const("@Trueprop",dummyT)$seq_tr1' s1$seq_tr1' s2;


128 


129 
val parse_translation = [("@Trueprop",true_tr)];


130 
val print_translation = [("Trueprop",true_tr')];
