Theory Solvers

theory Solvers
  imports
    (* TD0 *)
    TD0
    (* TD_plain *)
    TD_plain
    TD_plain_s
    TD_plain_s_warrow
    TD_plain_widen
    (* TD *)
    TD
    (* TD with widening *)
    TD_widen
    (* TD with warrowing *)
    TD_warrow
    (* TD with widening/narrowing in phases*)
    TD_wn_phases
    TD_wn_post
    TD_wn_wo_opt
    TD_wn_post_wo_opt
    (* TD with side-effects *)
    TD_side
    TD_side_upd_rule
    (* Worklist *)
    Worklist
    (* Examples *)
    Example
begin

thm TD0.correctness_trace

thm TD_plain.partial_correctness
thm TD_plain_mono.exactness
thm TD_plain_term.terminating
thm TD_plain_s.partial_correctness
thm TD_plain_s_warrow.partial_correctness
thm TD_plain_widen.partial_correctness

thm TD.TD_plain_TD_equivalence
thm TD.TD_TD_plain_equivalence
thm TD.partial_correctness
thm TD_mono.exactness
thm TD_term.terminating

thm TD_widen.partial_correctness
thm TD_widen_term.terminating

thm TD_wn_phases.TD_wn_phases_term.solve_termination
thm TD_warrow.partial_correctness
thm TD_warrow_mono_term.TD_warrow_terminating
thm TD_warrow_mono_term.TD_wn_phases_partial_correctness

thm TD_wn_wo_opt.TD_wn_post_TD_wn_equivalence
thm TD_wn_wo_opt.TD_wn_TD_wn_post_equivalence
thm TD_wn_wo_opt.solve_termination
thm TD_wn_wo_opt.partial_correctness

thm TD_wn_post.TD_wn_post.partial_correctness
thm TD_wn_post.solve_termination

thm TD_wn_post_wo_opt.partial_correctness
thm TD_wn_post_wo_opt.solve_termination

end