# 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
```