Theory Set_Proc_All

theory Set_Proc_All
  imports Set_Proc
begin

chapter ‹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.
›

section ‹Syntax and Semantics›

subsection ‹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}
›

subsection ‹Semantics›

text ‹
  Interpretation functions:
    ▪ @{const I⇩s⇩t}
    ▪ @{const I⇩s⇩a}
    ▪ ‹⊨› corresponds to @{term ‹interp I⇩s⇩a›}
›

thm I⇩s⇩t.simps I⇩s⇩a.simps interp.simps

section ‹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

section ‹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}.
  
  See also: @{const mlss_proc.mlss_proc}.
›

section ‹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}.
    ▪ 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

subsection ‹Characterisation of the Pure Witnesses›

thm lemma_2

subsection ‹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 I⇩s⇩t_realisation_eq_realisation coherence
end


section ‹Soundness of the Calculus›

thm bclosed_sound lexpands_sound bexpands_sound


section ‹Total Correctness of the Procedure›

subsection ‹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

end