(* SSer.thy Display logic - rules for exponentially restricted structures *) SSer = SSS + rules (* rules for exponentials, s10.3, Fig 9 *) comeA "[| $Y; $X |- $Z ; iser $Y |] ==> $X; $Y |- $Z" comdS "[| $Z |- $Y; $X ; isder $Y |] ==> $Z |- $X; $Y" ctreA "[| $Y |- $Z ; iser $Y |] ==> $Y; $Y |- $Z" ctrdS "[| $Z |- $Y ; isder $Y |] ==> $Z |- $Y; $Y" wkeAr "[| $X |- $Z ; iser $Y |] ==> $X; $Y |- $Z" wkeAl "[| $X |- $Z ; iser $Y |] ==> $Y; $X |- $Z" wkdSr "[| $Z |- $X ; isder $Y |] ==> $Z |- $X; $Y" wkdSl "[| $Z |- $X ; isder $Y |] ==> $Z |- $Y; $X" (* rules for exponentially restricted *) ersc "[| iser $X ; iser $Y |] ==> iser ($X ; $Y)" erlt "[| iser $X ; isder $Y |] ==> iser ($X < $Y)" ergt "[| isder $X ; iser $Y |] ==> iser ($X > $Y)" dersc "[| isder $X ; isder $Y |] ==> isder ($X ; $Y)" derlt "[| isder $X ; iser $Y |] ==> isder ($X < $Y)" dergt "[| iser $X ; isder $Y |] ==> isder ($X > $Y)" erblob "iser $X ==> iser (@ $X)" ercirc "iser $X ==> iser (o $X)" ersh "isder $X ==> iser (# $X)" erfl "isder $X ==> iser (b $X)" derblob "isder $X ==> isder (@ $X)" dercirc "isder $X ==> isder (o $X)" dersh "iser $X ==> isder (# $X)" derfl "iser $X ==> isder (b $X)" erI "iser $I" derI "isder $I" erphi "iser $phi" end