Theory Relational_Regression

theory Relational_Regression
  imports "Voblint_Domain.Order_Lattice"
begin

section ‹Relational carrier regressions›

text ‹Build-checked regression assertions on concrete ‹relc› values, moved out of
  ‹Order_Lattice›.  Nothing cites them; the build failing is the signal.›

subsection ‹Rendering›

text ‹‹to_string› renders bottom and top by their symbols and a known pair set as a sorted
  conjunction of ‹≤› facts.›

lemma to_string_relc_regression:
  "to_string RelBot = sym_bottom"
  "to_string (RelC {}) = sym_top"
  "to_string (RelC {(STR ''y'', STR ''z''), (STR ''x'', STR ''y'')}) =
     STR ''{x<le>y <and> y<le>z}''"
  by eval+

end