(*
listing of rules
*)
HOL_Rls = HOL_Sub +
consts
sA, sS, rstars, rssA, mblob, rblobs, rbbA :: "rule"
ca1, cs1, ca2, cs2, sa1, ss1, sa2, ss2 :: "rule"
taga, mra, pA, cA, aA, arA, ela, els, era, ers, ila, ils :: "rule"
tA, tS, fA, fS, nota, nots, anda, ands, ora, ors :: "rule"
r0A, r0S, r1A, r1S, conva, convs, compa, comps, rsa, rss :: "rule"
rls, dps, bsrs, lirs :: "rule set"
defs
(* Display Postulates *)
sA "sA == Bidi ( * $''X'' |- $''Y'') ( * $''Y'' |- $''X'')"
sS "sS == Bidi ($''X'' |- *$''Y'') ($''Y'' |- *$''X'')"
rstars"rstars == Bidi (( *$''X'') |- *$''Y'') ($''Y'' |- $''X'')" (* () *)
rssA "rssA == Bidi (( * *$''X'') |- $''Y'') ($''X'' |- $''Y'')" (* () *)
mblob "mblob == Bidi ((@$''X'') |- $''Y'') ($''X'' |- @$''Y'')" (* () *)
rblobs"rblobs == Bidi ((@$''X'') |- @$''Y'') ($''X'' |- $''Y'')" (* () *)
rbbA "rbbA == Bidi ((@@$''X'' |- $''Y'')) ($''X'' |- $''Y'')" (* () *)
ca1 "ca1 == Bidi ($''X'',, $''Y'' |- $''Z'') ($''X'' |- $''Z'',, *$''Y'')"
cs1 "cs1 == Bidi ($''X'' |- $''Y'',, $''Z'') ( *$''Y'',, $''X'' |- $''Z'')"
ca2 "ca2 == Bidi ($''X'',, $''Y'' |- $''Z'') ($''Y'' |- *$''X'',, $''Z'')"
cs2 "cs2 == Bidi ($''X'' |- $''Y'',, $''Z'') ($''X'',, *$''Z'' |- $''Y'')"
sa1 "sa1 == Bidi ($''X'';; $''Y'' |- $''Z'') ($''X'' |- $''Z'';; *@$''Y'')"
ss1 "ss1 == Bidi ($''X'' |- $''Y'';; $''Z'') ( *@$''Y'';; $''X'' |- $''Z'')"
sa2 "sa2 == Bidi ($''X'';; $''Y'' |- $''Z'') ($''Y'' |- *@$''X'';; $''Z'')"
ss2 "ss2 == Bidi ($''X'' |- $''Y'';; $''Z'') ($''X'';; *@$''Z'' |- $''Y'')"
dps "dps == {sA, sS, rstars, rssA, mblob, rblobs, rbbA,
ca1, cs1, ca2, cs2, sa1, ss1, sa2, ss2}"
(* Basic structural rules *)
taga "taga == Rule [($''X'';; $''Y'' |- $''Z'')]
(@$''Y'';; @$''X'' |- @$''Z'')"
mra "mra == Rule [($''X'' |- $''Z'')] ($''X'',, $''Y'' |- $''Z'')"
pA "pA == Rule [($''X'',, $''Y'' |- $''Z'')] ($''Y'',, $''X'' |- $''Z'')"
cA "cA == Rule [($''X'',, $''X'' |- $''Z'')] ($''X'' |- $''Z'')"
aA "aA == Bidi ($''X'',, ($''Y'',, $''Z'') |- $''W'')
(($''X'',, $''Y''),, $''Z'' |- $''W'')"
ila "ila == Rule [($I,, $''X'' |- $''Z'')] ($''X'' |- $''Z'')"
ils "ils == Rule [($''X'' |- $I,, $''Z'')] ($''X'' |- $''Z'')"
arA "arA == Bidi ($''X'';; ($''Y'';; $''Z'') |- $''W'')
(($''X'';; $''Y'');; $''Z'' |- $''W'')"
ela "ela == Bidi ($E;; $''X'' |- $''Z'') ($''X'' |- $''Z'')"
els "els == Bidi ($''X'' |- $E;; $''Z'') ($''X'' |- $''Z'')"
era "era == Bidi ($''X'';; $E |- $''Z'') ($''X'' |- $''Z'')"
ers "ers == Bidi ($''X'' |- $''Z'';; $E) ($''X'' |- $''Z'')"
bsrs "bsrs == {taga, mra, pA, cA, aA, arA, ela, els, era, ers, ila, ils}"
(* Logical Introduction rules *)
tA "tA == Rule [$I |- $''X''] (T |- $''X'')"
tS "tS == Rule [] ($I |- T)"
fA "fA == Rule [] (F |- $I)"
fS "fS == Rule [$''X'' |- $I] ($''X'' |- F)"
r1A "r1A == Rule [$E |- $''X''] (r1 |- $''X'')"
r1S "r1S == Rule [] ($E |- r1)"
r0A "r0A == Rule [] (r0 |- $E)"
r0S "r0S == Rule [$''X'' |- $E] ($''X'' |- r0)"
(*
nega "nega == Rule [( * @ ''A'' |- $''X'')] (~''A'' |- $''X'')" (* () *)
negs "negs == Rule [$''X'' |- * @ ''A''] ($''X'' |- ~ ''A'')"
*)
nota "nota == Rule [( * ''A'' |- $''X'')] (--''A'' |- $''X'')" (* () *)
nots "nots == Rule [$''X'' |- * ''A''] ($''X'' |- -- ''A'')"
conva "conva == Rule [( @ ''A'' |- $''X'')] (''A''^ |- $''X'')" (* () *)
convs "convs == Rule [$''X'' |- @ ''A''] ($''X'' |- ''A''^)"
anda "anda == Rule [''A'',, ''B'' |- $''X''] (''A'' && ''B'' |- $''X'')"
ands "ands == Rule [($''X'' |- ''A''), ($''Y'' |- ''B'')]
($''X'',, $''Y'' |- ''A'' && ''B'')"
ora "ora == Rule [(''A'' |- $''X''), (''B'' |- $''Y'')]
(''A'' v ''B'' |- $''X'',, $''Y'')"
ors "ors == Rule [$''X'' |- ''A'',, ''B''] ($''X'' |- ''A'' v ''B'')"
compa "compa == Rule [''A'';; ''B'' |- $''X''] (''A'' oo ''B'' |- $''X'')"
comps "comps == Rule [($''X'' |- ''A''), ($''Y'' |- ''B'')]
($''X'';; $''Y'' |- ''A'' oo ''B'')"
rsa "rsa == Rule [(''A'' |- $''X''), (''B'' |- $''Y'')]
(''A'' +++ ''B'' |- $''X'';; $''Y'')"
rss "rss == Rule [$''X'' |- ''A'';; ''B''] ($''X'' |- ''A'' +++ ''B'')"
(*
bimpa "bimpa == Rule [($''X'' |- ''A''), (''B'' |- $''Y'')]
(''A'' => ''B'' |- *$''X'',, $''Y'')"
bimps "bimps == Rule [$''X'',, ''A'' |- ''B''] ($''X'' |- ''A'' => ''B'')"
*)
lirs "lirs == {tA, tS, fA, fS, nota, nots, anda, ands, ora, ors,
r0A, r0S, r1A, r1S, conva, convs, compa, comps, rsa, rss}"
rls "rls == dps Un bsrs Un lirs Un {cutr, idf}"
end