# Theory Inversion

theory Inversion
imports List_Index
```section "List Inversion"

theory Inversion
imports "List-Index.List_Index"
begin

abbreviation "dist_perm xs ys ≡ distinct xs ∧ distinct ys ∧ set xs = set ys"

definition before_in :: "'a ⇒ 'a ⇒ 'a list ⇒ bool"
("(_ </ _/ in _)" [55,55,55] 55) where
"x < y in xs = (index xs x < index xs y ∧ y ∈ set xs)"

definition Inv :: "'a list ⇒ 'a list ⇒ ('a * 'a) set" where
"Inv xs ys = {(x,y). x < y in xs ∧ y < x in ys}"

lemma before_in_setD1: "x < y in xs ⟹ x : set xs"
by (metis index_conv_size_if_notin index_less before_in_def less_asym order_refl)

lemma before_in_setD2: "x < y in xs ⟹ y : set xs"

lemma not_before_in:
"x : set xs ⟹ y : set xs ⟹ ¬ x < y in xs ⟷ y < x in xs ∨ x=y"
by (metis index_eq_index_conv before_in_def less_asym linorder_neqE_nat)

lemma before_in_irefl: "x < x in xs = False"
by (meson before_in_setD2 not_before_in)

lemma no_before_inI[simp]: "x < y in xs ⟹ (¬ y < x in xs) = True"
by (metis before_in_setD1 not_before_in)

lemma finite_Invs[simp]:  "finite(Inv xs ys)"
apply(rule finite_subset[where B = "set xs × set ys"])
apply(metis index_conv_size_if_notin index_less_size_conv less_asym)+
done

lemma Inv_id[simp]: "Inv xs xs = {}"

lemma card_Inv_sym: "card(Inv xs ys) = card(Inv ys xs)"
proof -
have "Inv xs ys = (λ(x,y). (y,x)) ` Inv ys xs" by(auto simp: Inv_def)
thus ?thesis by (metis card_image swap_inj_on)
qed

lemma Inv_tri_ineq:
"dist_perm xs ys ⟹ dist_perm ys zs ⟹
Inv xs zs ⊆ Inv xs ys Un Inv ys zs"
by(auto simp: Inv_def) (metis before_in_setD1 not_before_in)

lemma card_Inv_tri_ineq:
"dist_perm xs ys ⟹ dist_perm ys zs ⟹
card (Inv xs zs) ≤ card(Inv xs ys) + card (Inv ys zs)"
using card_mono[OF _ Inv_tri_ineq[of xs ys zs]]
by auto (metis card_Un_Int finite_Invs trans_le_add1)

end
```