Theory PAC_Polynomials_Term

(*
  File:         PAC_Polynomials_Term.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory PAC_Polynomials_Term
  imports PAC_Polynomials
    Refine_Imperative_HOL.IICF
begin


section ‹Terms›

text ‹We define some helper functions.›

subsection ‹Ordering›

(*Taken from WB_More_Refinement*)
lemma fref_to_Down_curry_left:
  fixes f:: ‹'a ⇒ 'b ⇒ 'c nres› and
    A::‹(('a × 'b) × 'd) set›
  shows
    ‹(uncurry f, g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
      (⋀a b x'. P x' ⟹ ((a, b), x') ∈ A ⟹ f a b ≤ ⇓ B (g x'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry_right:
  fixes g :: ‹'a ⇒ 'b ⇒ 'c nres› and f :: ‹'d ⇒ _ nres› and
    A::‹('d × ('a × 'b)) set›
  shows
    ‹(f, uncurry g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
      (⋀a b x'. P (a,b) ⟹ (x', (a, b)) ∈ A ⟹ f x' ≤ ⇓ B (g a b))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

type_synonym term_poly_list = ‹string list›
type_synonym llist_polynomial = ‹(term_poly_list × int) list›


text ‹We instantiate the characters with typeclass linorder to be able to talk abourt sorted and
  so on.›

definition less_eq_char :: ‹char ⇒ char ⇒ bool› where
  ‹less_eq_char c d = (((of_char c) :: nat) ≤ of_char d)›

definition less_char :: ‹char ⇒ char ⇒ bool› where
  ‹less_char c d = (((of_char c) :: nat) < of_char d)›

global_interpretation char: linorder less_eq_char less_char
  using linorder_char
  unfolding linorder_class_def class.linorder_def
    less_eq_char_def[symmetric] less_char_def[symmetric]
    class.order_def order_class_def
    class.preorder_def preorder_class_def
    ord_class_def
  apply auto
  done

abbreviation less_than_char :: ‹(char × char) set› where
  ‹less_than_char ≡ p2rel less_char›

lemma less_than_char_def:
  ‹(x,y) ∈ less_than_char ⟷ less_char x y›
  by (auto simp: p2rel_def)

lemma trans_less_than_char[simp]:
    ‹trans less_than_char› and
  irrefl_less_than_char:
    ‹irrefl less_than_char› and
  antisym_less_than_char:
    ‹antisym less_than_char›
  by (auto simp: less_than_char_def trans_def irrefl_def antisym_def)


subsection ‹Polynomials›

definition var_order_rel :: ‹(string × string) set› where
  ‹var_order_rel ≡ lexord less_than_char›

abbreviation var_order :: ‹string ⇒ string ⇒ bool› where
  ‹var_order ≡ rel2p var_order_rel›

abbreviation term_order_rel :: ‹(term_poly_list × term_poly_list) set› where
  ‹term_order_rel ≡ lexord var_order_rel›

abbreviation term_order :: ‹term_poly_list ⇒ term_poly_list ⇒ bool› where
  ‹term_order ≡ rel2p term_order_rel›

definition term_poly_list_rel :: ‹(term_poly_list × term_poly) set› where
  ‹term_poly_list_rel = {(xs, ys).
     ys = mset xs ∧
     distinct xs ∧
     sorted_wrt (rel2p var_order_rel) xs}›

definition unsorted_term_poly_list_rel :: ‹(term_poly_list × term_poly) set› where
  ‹unsorted_term_poly_list_rel = {(xs, ys).
     ys = mset xs ∧ distinct xs}›

definition poly_list_rel :: ‹_ ⇒ (('a × int) list × mset_polynomial) set› where
  ‹poly_list_rel R = {(xs, ys).
     (xs, ys) ∈ ⟨R ×r int_rel⟩list_rel O list_mset_rel ∧
     0 ∉# snd `# ys}›

definition sorted_poly_list_rel_wrt :: ‹('a ⇒ 'a ⇒ bool)
     ⇒ ('a × string multiset) set ⇒ (('a × int) list × mset_polynomial) set› where
  ‹sorted_poly_list_rel_wrt S R = {(xs, ys).
     (xs, ys) ∈ ⟨R ×r int_rel⟩list_rel O list_mset_rel ∧
     sorted_wrt S (map fst xs) ∧
     distinct (map fst xs) ∧
     0 ∉# snd `# ys}›

abbreviation sorted_poly_list_rel where
  ‹sorted_poly_list_rel R ≡ sorted_poly_list_rel_wrt R term_poly_list_rel›

abbreviation sorted_poly_rel where
  ‹sorted_poly_rel ≡ sorted_poly_list_rel term_order›


definition sorted_repeat_poly_list_rel_wrt :: ‹('a ⇒ 'a ⇒ bool)
     ⇒ ('a × string multiset) set ⇒ (('a × int) list × mset_polynomial) set› where
  ‹sorted_repeat_poly_list_rel_wrt S R = {(xs, ys).
     (xs, ys) ∈ ⟨R ×r int_rel⟩list_rel O list_mset_rel ∧
     sorted_wrt S (map fst xs) ∧
     0 ∉# snd `# ys}›

abbreviation sorted_repeat_poly_list_rel where
  ‹sorted_repeat_poly_list_rel R ≡ sorted_repeat_poly_list_rel_wrt R term_poly_list_rel›

abbreviation sorted_repeat_poly_rel where
  ‹sorted_repeat_poly_rel ≡ sorted_repeat_poly_list_rel (rel2p (Id ∪ lexord var_order_rel))›


abbreviation unsorted_poly_rel where
  ‹unsorted_poly_rel ≡ poly_list_rel term_poly_list_rel›

lemma sorted_poly_list_rel_empty_l[simp]:
  ‹([], s') ∈ sorted_poly_list_rel_wrt S T ⟷ s' = {#}›
  by (cases s')
    (auto simp: sorted_poly_list_rel_wrt_def list_mset_rel_def br_def)


definition fully_unsorted_poly_list_rel :: ‹_ ⇒ (('a × int) list × mset_polynomial) set› where
  ‹fully_unsorted_poly_list_rel R = {(xs, ys).
     (xs, ys) ∈ ⟨R ×r int_rel⟩list_rel O list_mset_rel}›

abbreviation fully_unsorted_poly_rel where
  ‹fully_unsorted_poly_rel ≡ fully_unsorted_poly_list_rel unsorted_term_poly_list_rel›


lemma fully_unsorted_poly_list_rel_empty_iff[simp]:
  ‹(p, {#}) ∈ fully_unsorted_poly_list_rel R ⟷ p = []›
  ‹([], p') ∈ fully_unsorted_poly_list_rel R ⟷ p' = {#}›
  by (auto simp: fully_unsorted_poly_list_rel_def list_mset_rel_def br_def)

definition poly_list_rel_with0 :: ‹_ ⇒ (('a × int) list × mset_polynomial) set› where
  ‹poly_list_rel_with0 R = {(xs, ys).
     (xs, ys) ∈ ⟨R ×r int_rel⟩list_rel O list_mset_rel}›

abbreviation unsorted_poly_rel_with0 where
  ‹unsorted_poly_rel_with0 ≡ fully_unsorted_poly_list_rel term_poly_list_rel›

lemma poly_list_rel_with0_empty_iff[simp]:
  ‹(p, {#}) ∈ poly_list_rel_with0 R ⟷ p = []›
  ‹([], p') ∈ poly_list_rel_with0 R ⟷ p' = {#}›
  by (auto simp: poly_list_rel_with0_def list_mset_rel_def br_def)


definition sorted_repeat_poly_list_rel_with0_wrt :: ‹('a ⇒ 'a ⇒ bool)
     ⇒ ('a × string multiset) set ⇒ (('a × int) list × mset_polynomial) set› where
  ‹sorted_repeat_poly_list_rel_with0_wrt S R = {(xs, ys).
     (xs, ys) ∈ ⟨R ×r int_rel⟩list_rel O list_mset_rel ∧
     sorted_wrt S (map fst xs)}›

abbreviation sorted_repeat_poly_list_rel_with0 where
  ‹sorted_repeat_poly_list_rel_with0 R ≡ sorted_repeat_poly_list_rel_with0_wrt R term_poly_list_rel›

abbreviation sorted_repeat_poly_rel_with0 where
  ‹sorted_repeat_poly_rel_with0 ≡ sorted_repeat_poly_list_rel_with0 (rel2p (Id ∪ lexord var_order_rel))›

lemma term_poly_list_relD:
  ‹(xs, ys) ∈ term_poly_list_rel ⟹ distinct xs›
  ‹(xs, ys) ∈ term_poly_list_rel ⟹ ys = mset xs›
  ‹(xs, ys) ∈ term_poly_list_rel ⟹ sorted_wrt (rel2p var_order_rel) xs›
  ‹(xs, ys) ∈ term_poly_list_rel ⟹ sorted_wrt (rel2p (Id ∪ var_order_rel)) xs›
  apply (auto simp: term_poly_list_rel_def; fail)+
  by (metis (mono_tags, lifting) CollectD UnI2 rel2p_def sorted_wrt_mono_rel split_conv
    term_poly_list_rel_def)

end