Theory MLSS_Proc_All

theory MLSS_Proc_All
  imports MLSS_Proc MLSS_Proc_Code
begin

section ‹Outline of the Formalisation›

text ‹
  We reference the most important aspects of the formalisation here
  and highlight the (mostly syntactic) differences between the paper
  and the formalisation.
  The sections roughly correspond to the sections in the paper.
›

subsection ‹Syntax and Semantics›

subsubsection ‹Syntax›
text ‹
  Datatypes:
    ▪ Propositional formulae: @{datatype fm}. The formalisation uses constructors like @{term And}
      instead of ‹∧›.
    ▪ Set terms: @{datatype pset_term}
    ▪ Set atoms: @{datatype pset_atom}
›
text ‹
  Important constants:
    ▪ @{const vars}
    ▪ @{const atoms}
    ▪ @{const subterms}
    ▪ @{const subfms}
    ▪ @{const is_literal}
›

subsubsection ‹Semantics›

text ‹
  Interpretation functions:
    ▪ @{const Ist}
    ▪ @{const Isa}
    ▪ ‹⊨› corresponds to @{term ‹interp Isa›}
›

thm Ist.simps Isa.simps interp.simps

subsection ‹Tableau Calculus›

text ‹
  Type of branches @{typ ‹'a branch›}.
  Closedness @{const bclosed} and Openness @{const bopen}.
›

thm bclosed.intros

text ‹
  Instead of triangles such as ‹▹›, we use the constant names
  @{const lexpands}, @{const bexpands}, and @{const expandss} for
  linear expansion, branching expansion, and expansion closure, respectively.
  Note that the term-for-term substitution that is denoted by ‹l{s/t}› in the paper
  corresponds to @{const subst_tlvl}.
  
  Further important constants:
    ▪ @{const lin_sat}
    ▪ @{const sat}
    ▪ @{const wits}
    ▪ @{const wf_branch}
›

thm lin_sat_def sat_def wits_def wf_branch_def
thm subst_tlvl.simps

subsection ‹Abstract Specification of the Decision Procedure›

text ‹
  Since Hilbert choice (such as @{term ‹SOME x. P›}) does not allow for refinement,
  we parametrise the abstract specification @{const mlss_proc.mlss_proc_branch} of the
  decision procedure by two choice functions ‹lexpand› and ‹bexpand›.
  This parametrisation is realised by the locale @{locale mlss_proc}.
  We then refine the abstract to a naive executable specification @{const ‹mlss_proc_branch_partial›}.
  
  See also: @{const mlss_proc.mlss_proc} and @{const mlss_proc_partial}.
›

subsection ‹Completeness›

text ‹
  Constants needed for the realisation function:
    ▪ The terms defined by @{const base_vars} receive special treatment from the realisation function.
      Without typing @{const base_vars} is equal to the pure witnesses @{const pwits}.
      With typing we also add the urelems @{const urelems} to it.
    ▪ Rest of the subterms @{const subterms'}
    ▪ Realisation graph @{const bgraph}
  In contrast to the paper, we put the the realisation function @{const realisation.realise} into
  a locale @{locale realisation} and prove its properties abstractly.
  Then, we instantiate the locale with the above constants. Since this takes place in the context,
  we put this into the locale @{locale open_branch}.
›

thm base_vars_def pwits_def subterms'_def
thm realisation.realise.simps

subsubsection ‹Characterisation of the Pure Witnesses›

thm lemma_2

subsubsection ‹Realisation of an Open Branch›
text ‹
  The assumption that the branch is open is captured by the locale @{locale open_branch}.
  Important theorems:
›
context open_branch
begin
thm realise.simps

thm realisation_if_AT_mem realisation_if_AT_eq
    realisation_if_AF_eq realisation_if_AF_mem
thm realisation_simps
thm Ist_realisation_eq_realisation coherence
end


subsection ‹Soundness of the Calculus›

thm bclosed_sound lexpands_sound bexpands_sound


subsection ‹Total Correctness of the Procedure›

subsubsection ‹Abstract Specification›
thm card_wf_branch_ub

context mlss_proc
begin
thm mlss_proc_branch_dom_if_wf_branch

thm mlss_proc_branch_complete mlss_proc_branch_sound

thm mlss_proc_complete mlss_proc_sound
end

subsubsection ‹Executable Specification›

thm mlss_proc_partial_eq_None
thm mlss_proc_partial_complete mlss_proc_partial_sound

subsection ‹Urelements›
text ‹
  Typing for set terms, atoms, and formulae:
    ▪ @{const types_pset_term}
    ▪ @{const types_pset_atom}
    ▪ @{const types_pset_fm}
›
thm types_pset_term.intros types_pset_atom.intros types_pset_fm_def

text ‹Typing judgement is invariant under branch expansion.›
thm types_lexpands types_bexpands_nowit types_bexpands_wit types_expandss

text ‹Definition of urelements›
thm urelems_def

text ‹Constraint generation›
thm constrs_term.simps
thm constrs_atom.simps
thm constrs_fm.simps

text ‹Solving of constraints›
thm MLSS_Suc_Theory.solve.simps
thm MLSS_Suc_Theory.assign.simps

text ‹Urelems are those terms that receive an assignment of 0 after solving the constraints.›
thm urelem_iff_assign_eq_0


end