(* RS.thy Display logic - structural rules for relational algebras *) RS = Pure + classes term < logic default term types structure formula struct arities structure :: term formula :: term consts I :: "structure" E :: "structure" (* Structural Connectives *) "Sequent" :: "[structure, structure] => prop" "*" :: "structure => structure" "," :: "[structure, structure] => structure" "@" :: "structure => structure" ";" :: "[structure, structure] => structure" (* Coercing formula to structure *) Structform :: "formula => structure" syntax "@Bracket" :: "struct => struct" ("'(_')" [0] 1000) "@Semicolon" :: "[struct, struct] => struct" ("_; _" [21, 21] 20) "@Comma" :: "[struct, struct] => struct" ("_, _" [21, 21] 20) "@Blob" :: "struct => struct" ("@ _" [30] 30) "@Star" :: "struct => struct" ("* _" [30] 30) "@Sequent" :: "[struct, struct] => prop" ("((_)/ |- (_))" [6,6] 5) StructId :: id => struct ("$_") StructVar :: var => struct ("$_") "" :: "formula => struct" ("_") rules (* Display equivalences *) sA "(*$X) |- $Y == *$Y |- $X" (* () *) sS "$X |- *$Y == $Y |- *$X" rssA "(**$X) |- $Y == $X |- $Y" (* () *) mblob "(@$X) |- $Y == $X |- @$Y" (* () *) rbbA "(@@$X |- $Y) == $X |- $Y" (* () *) ca2 "$X, $Y |- $Z == $Y |- *$X, $Z" cs2 "$X |- $Y, $Z == $X, *$Z |- $Y" sa1 "$X; $Y |- $Z == $X |- $Z; *@$Y" ss1 "$X |- $Y; $Z == *@$Y; $X |- $Z" sa2 "$X; $Y |- $Z == $Y |- *@$X; $Z" ss2 "$X |- $Y; $Z == $X; *@$Z |- $Y" (* Basic structural rules *) taga "$X; $Y |- $Z ==> @$Y; @$X |- @$Z" mra "$X |- $Z ==> $X, $Y |- $Z" pA "$X, $Y |- $Z ==> $Y, $X |- $Z" cA "$X, $X |- $Z ==> $X |- $Z" aA "$X, ($Y, $Z) |- $W == ($X, $Y), $Z |- $W" ila "$I, $X |- $Z ==> $X |- $Z" ils "$X |- $I, $Z ==> $X |- $Z" arA "$X; ($Y; $Z) |- $W == ($X; $Y); $Z |- $W" ela "$E; $X |- $Z == $X |- $Z" els "$X |- $E; $Z == $X |- $Z" era "$X; $E |- $Z == $X |- $Z" ers "$X |- $Z; $E == $X |- $Z" (* Identity rule for formulae *) idf "A |- A" (* Cut rule *) cut "[| $X |- A ; A |- $Y |] ==> $X |- $Y" end ML fun str_tr (Const("StructId",_)$id) = id | str_tr (Const("StructVar",_)$id) = id | str_tr (Const("@Blob",_)$U) = (Const("@",dummyT)$str_tr U) | str_tr (Const("@Star",_)$U) = (Const("*",dummyT)$str_tr U) | str_tr (Const("@Bracket",_)$U) = str_tr U | str_tr (Const("@Comma",_)$L$R) = (Const(",",dummyT)$str_tr L$str_tr R) | str_tr (Const("@Semicolon",_)$L$R) = (Const(";",dummyT)$str_tr L$str_tr R) | str_tr (fm) = Const("Structform",dummyT)$fm; fun true_tr[s1,s2] = Const("Sequent",dummyT)$str_tr s1$str_tr s2; fun str_tr' (Const("Structform",_)$fm) = fm | str_tr' (Const("@",_)$U) = (Const("@Blob",dummyT)$str_tr' U) | str_tr' (Const("*",_)$U) = (Const("@Star",dummyT)$str_tr' U) | str_tr' (Const(",",_)$L$R) = (Const("@Comma",dummyT)$str_tr' L$str_tr' R) | str_tr' (Const(";",_)$L$R) = (Const("@Semicolon",dummyT)$str_tr' L$str_tr' R) | str_tr' (id) = Const("StructId",dummyT)$id; fun true_tr' [s1,s2] = Const("@Sequent",dummyT)$str_tr' s1$str_tr' s2; val parse_translation = [("@Sequent",true_tr)]; val print_translation = [("Sequent",true_tr')];