# Theory PrettyPrinting

```theory PrettyPrinting
imports
ExecutiblePolyProps
PolyAtoms
Polynomials.Show_Polynomials
Polynomials.Power_Products
begin

global_interpretation drlex_pm: linorder drlex_pm drlex_pm_strict
defines Min_drlex_pm = "linorder.Min drlex_pm"
and Max_drlex_pm = "linorder.Max drlex_pm"
and sorted_drlex_pm = "linorder.sorted drlex_pm"
and sorted_list_of_set_drlex_pm = "linorder.sorted_list_of_set drlex_pm"
and sort_key_drlex_pm = "linorder.sort_key drlex_pm"
and insort_key_drlex_pm = "linorder.insort_key drlex_pm"
and part_drlex_pm = "drlex_pm.part"
apply unfold_locales
subgoal using drlex_pm_trans by auto
done

definition "monomials_list mp = drlex_pm.sorted_list_of_set (monomials mp)"

definition shows_monomial_gen::"((nat × nat) ⇒ shows) ⇒ ('a ⇒ shows) ⇒ shows ⇒ (nat ⇒⇩0 nat) ⇒ 'a option ⇒ shows" where
"shows_monomial_gen shows_factor shows_coeff sep mon cff =
shows_sep (λs. case s of
Inl cff ⇒ shows_coeff cff
| Inr factor ⇒ shows_factor factor
) sep ((case cff of None ⇒ [] | Some cff ⇒ [Inl cff]) @ map Inr (Poly_Mapping.items mon))"

definition "shows_factor_compact factor =
(case factor of (k, v) ⇒ shows_string ''x'' +@+ shows k +@+
(if v = 1 then shows_string '''' else shows_string ''^'' +@+ shows v))"

definition "shows_factor_Var factor =
(case factor of (k, v) ⇒ shows_string ''(Var '' +@+ shows k +@+ shows_string '')'' +@+
(if v = 1 then shows_string '''' else shows_string ''^'' +@+ shows v))"

definition shows_monomial_compact::"('a ⇒ shows) ⇒ (nat ⇒⇩0 nat) ⇒ 'a option ⇒ shows" where
"shows_monomial_compact shows_coeff m =
shows_monomial_gen shows_factor_compact shows_coeff (shows_string '' '') m"

definition shows_monomial_Var::"('a ⇒ shows) ⇒ (nat ⇒⇩0 nat) ⇒ 'a option ⇒ shows" where
"shows_monomial_Var shows_coeff m =
shows_monomial_gen shows_factor_Var shows_coeff (shows_string ''*'') m"

fun shows_mpoly :: "bool ⇒ ('a ⇒ shows) ⇒ 'a::{zero,one} mpoly ⇒ shows" where
"shows_mpoly input shows_coeff p = shows_sep (λmon.
(if input then shows_monomial_Var (λx. shows_paren (shows_string ''Const '' +@+ shows_paren (shows_coeff x))) else shows_monomial_compact shows_coeff)
mon
(let cff = MPoly_Type.coeff p mon in if cff = 1 then None else Some cff)
)
(shows_string '' + '')
(monomials_list p)"

definition "rat_of_real (x::real) =
(if (∃r::rat. x = of_rat r) then (THE r. x = of_rat r) else 99999999999.99999999999)"

lemma rat_of_real: "rat_of_real x = r" if "x = of_rat r"
using that
unfolding rat_of_real_def
by simp

lemma rat_of_real_code[code]: "rat_of_real (Ratreal r) = r"

definition "shows_real x = shows (rat_of_real x)"

experiment begin
abbreviation "foo ≡ ((Var 0::real mpoly) + Const (0.5) * Var 1 + Var 2)^3"
value [code] "shows_mpoly True shows_real foo ''''"
(* rhs of foo\\_eq is the output of this ‹value› command *)
lemma foo_eq: "foo = (Var 0)^3 + (Const (3/2))*(Var 0)^2*(Var 1) + (Const (3))*(Var 0)^2*(Var 2) + (Const (3/4))*(Var 0)*(Var 1)^2 + (Const (3))*(Var 0)*(Var 1)*(Var 2) + (Const (3))*(Var 0)*(Var 2)^2 + (Const (1/8))*(Var 1)^3 + (Const (3/4))*(Var 1)^2*(Var 2) + (Const (3/2))*(Var 1)*(Var 2)^2 + (Var 2)^3"
by code_simp
value [code] "shows_mpoly False shows_real foo ''''"
value [code] "shows_mpoly False (shows_paren o shows_mpoly False shows_real) (extract_var foo 0) ''''"
value [code] "shows_list_gen (shows_mpoly False shows_real)
''[]'' ''['' '', '' '']''
(Polynomial.coeffs (mpoly_to_nested_poly foo 0)) ''''"
end

fun shows_atom :: "bool ⇒ atom ⇒ shows" where
"shows_atom c (Eq p) = (shows_string ''('' +@+ shows_mpoly c shows_real p +@+ shows_string ''=0)'')"|
"shows_atom c (Less p) = (shows_string ''('' +@+ shows_mpoly c shows_real p +@+ shows_string ''<0)'')"|
"shows_atom c (Leq p) = (shows_string ''('' +@+ shows_mpoly c shows_real p +@+ shows_string ''<=0)'')"|
"shows_atom c(Neq p) = (shows_string ''('' +@+ shows_mpoly c shows_real p +@+ shows_string ''~=0)'')"

fun depth' :: "'a fm ⇒ nat"where
"depth' TrueF = 1"|
"depth' FalseF = 1"|
"depth' (Atom _) = 1"|
"depth' (And φ ψ) = max (depth' φ) (depth' ψ) + 1"|
"depth' (Or φ ψ) = max (depth' φ) (depth' ψ) + 1"|
"depth' (Neg φ) = depth' φ + 1"|
"depth' (ExQ φ) = depth' φ + 1"|
"depth' (AllQ φ) = depth' φ + 1"|
"depth' (AllN i φ) = depth' φ  + i * 2 + 1"|
"depth' (ExN i φ) = depth' φ  + i * 2 + 1"

function shows_fm :: "bool ⇒ atom fm ⇒ shows" where
"shows_fm c (Atom a) = shows_atom c a"|
"shows_fm c (TrueF) = shows_string ''(T)''"|
"shows_fm c (FalseF) = shows_string ''(F)''"|
"shows_fm c (And φ ψ) = (shows_string ''('' +@+ shows_fm c φ +@+ shows_string '' and '' +@+ shows_fm c ψ +@+ shows_string ('')''))"|
"shows_fm c (Or φ ψ) = (shows_string ''('' +@+ shows_fm c φ +@+ shows_string '' or '' +@+ shows_fm c ψ  +@+ shows_string '')'')"|
"shows_fm c (Neg φ) = (shows_string ''(neg '' +@+ shows_fm c φ +@+ shows_string '')'')"|
"shows_fm c (ExQ φ) = (shows_string ''(exists'' +@+ shows_fm c φ +@+ shows_string '')'')"|
"shows_fm c (AllQ φ) = (shows_string ''(forall'' +@+ shows_fm c φ +@+ shows_string '')'')"|
"shows_fm c (ExN 0 φ) = shows_fm c φ"|
"shows_fm c (ExN (Suc n) φ) = shows_fm c (ExQ(ExN n φ))"|
"shows_fm c (AllN 0 φ) = shows_fm c φ"|
"shows_fm c (AllN (Suc n) φ) = shows_fm c (AllQ(AllN n φ))"
by pat_completeness auto
termination
apply(relation "measures [λ(_,A). depth' A]")
by auto

value "shows_fm False (ExQ (Or (AllQ(And (Neg TrueF) (Neg FalseF))) (Atom(Eq(Const 4))))) []"
value "shows_fm True (ExQ (Or (AllQ(And (Neg TrueF) (Neg FalseF))) (Atom(Eq(Const 4))))) []"

end```