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" by (simp add: before_in_def) 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(auto simp add: Inv_def before_in_def) apply(metis index_conv_size_if_notin index_less_size_conv less_asym)+ done lemma Inv_id[simp]: "Inv xs xs = {}" by(auto simp add: Inv_def before_in_def) 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