directory fdeep contains files using the definition of structures and formulae
as datatypes, whose constructors are the various connectives, as in GDC.thy ;
note that the fdeep development uses some files in common with ../gdeep,
these files are in ../cdeep
note that there are further changes, in cut-elimination proofs done for
FILL - see directory ../fill, eg
types 'a pstructr (so structr = string pstructr)
sFind_def in terms of findf instead of previous,
with some consequential changes (eg thms "sFind.simps")
Changes in fdeep from deep :
in fdeep a rule is a datatype with a single constructor,
and Bidi is a defined function (Bidi_def in RA_Rls.thy)
use of seqrep(s) and strrep instead of seqRep(s) and strRep
Hierarchy of theory files
Embedding to allow IsProvable
HOL_DL = List +
sequent structure formula rule
stuff relating to provability
HOL_RS = HOL_DL +
dRA structural operators
Full Deep Embedding, independent of actual calculus
stringSyntax = String
to support parse and print translations for Structure and Formula variables
GDC = String + stringSyntax +
formula, structr, sequent, rule as datatypes
GSub = GDC +
stuff relating to substitution
GDT = GSub +
derivation tree as datatype, stuff relating to derivation trees,
defines IsDerivableR as existence of a derivation tree ;
inductive definition of derivableR using dtrel.thy,
by "derivableR ?rules == derrec (PC ` rulefs ?rules)" ;
shows equivalence as IsDer_derR =
"IsDerivableR ?rules ?prems ?concl = (?concl : derivableR ?rules ?prems)"
Then IsDerivableR_trans follows easily from derrec_trans (see DT1.ML)
GRep = GSub +
the replacement relation, used in cut-elimination
GCut = GRep + GDT +
stuff for cut-elimination, turning cuts into principal cuts
makeCut = GCut + GRep
GElim = makeCut +
stuff for cut-elimination, turns results in other forms
into results using canElim and canElimAll
culminates in general cut-elimination theorem,
cutElim = "[| C345 ?rules; C8 ?rules; IsDerivableR ?rules {} ?concl |]
==> IsDerivableR (?rules - {cutr}) {} ?concl" : thm
stuff for relation algebras
RA_Syn = GDC +
syntax for relation algebras
RA_Ind = RA_Syn + GSub +
listing of rules - inductive style (RArls) ;
proof of noNewSVs_rls_Ind - related to C4 - based on RArls
IDT = GDT + RA_Ind
RA_Rls = RA_Syn + GSub +
to do with rules (rls) and their properties, proves
seqNoSSF_rls, noDupSVs_rls
RA_IR = RA_Rls + RA_Ind
relationship between rules and inductive-style rules
RArls_fs = "RArls = PC ` rulefs rls" : thm
proves noNewSVs_rls, noSVsAS_rls
C345_rls = "C345 rls" : thm
RA_DT = RA_IR + GDT
relating derivability using rls and RArls, IsDer_RArls =
"IsDerivableR rls ?prems ?concl = (?concl : derrec RArls ?prems)" : thm
IDT = GDT + RA_Ind
version of C8 using inductive-style rules RArls
ICut = GCut + IDT + RA_DT
proves C8_rls = "C8 rls" : thm
IElim = GElim + ICut - culminates in cut-elimination theorem, RA_cutElim =
"IsDerivableR rls {} ?concl ==> IsDerivableR (rls - {cutr}) {} ?concl" : thm
HOL_C8 = GCut + RA_Rls
stuff for cut-elimination, procedures to prove Belnap C8 results,
using deep-embedded rules (rls)
C8cases = HOL_C8
RA_C8 = C8cases
alternative proof of C8_rls
RA_ElimC8 = GElim + RA_C8 + RA_IR
stuff for cut-elimination, putting HOL_C8 and GElim together
meta_proofs = GDT + RA_Rls
ML code for construction of proof trees
HOL_Disp = meta_proofs + RA_Rls +
to do with displaying substructures
fdeep also contains extra definitions, needed for interpolation work,
in ../interp, which are not found in ../gdeep