(* * Knowledge-based programs. * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com. * License: BSD *) theory List_local imports Extra "HOL-Library.While_Combinator" begin text‹Partition a list with respect to an equivalence relation.› text‹First up: split a list according to a relation.› abbreviation "rel_ext r ≡ { x . r x }" definition partition_split_body :: "('a × 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ 'a list × 'a list ⇒ 'a list × 'a list" where [code]: "partition_split_body r x ≡ λy (X', xc). if r (x, y) then (X', List.insert y xc) else (List.insert y X', xc)" definition partition_split :: "('a × 'a ⇒ bool) ⇒ 'a ⇒ 'a list ⇒ 'a list × 'a list" where [code]: "partition_split r x xs ≡ foldr (partition_split_body r x) xs ([], [])" lemma partition_split: shows "set (fst (partition_split r x xs)) = set xs - (rel_ext r `` {x})" and "set (snd (partition_split r x xs)) = set xs ∩ (rel_ext r `` {x})" proof(induct xs) case Nil { case 1 with Nil show ?case unfolding partition_split_def by simp } { case 2 with Nil show ?case unfolding partition_split_def by simp } next case (Cons x xs) { case 1 with Cons show ?case unfolding partition_split_def apply simp apply (subst partition_split_body_def) apply (split prod.split) apply clarsimp apply rule apply clarsimp apply clarsimp unfolding Image_def apply auto done } { case 2 with Cons show ?case unfolding partition_split_def apply simp apply (subst partition_split_body_def) apply (split prod.split) apply clarsimp apply rule apply clarsimp apply clarsimp done } qed lemma partition_split': assumes "partition_split r x xs = (xxs', xec)" shows "set xxs' = set xs - (rel_ext r `` {x})" and "set xec = set xs ∩ (rel_ext r `` {x})" using assms partition_split[where r=r and x=x and xs=xs] by simp_all text‹Next, split an list on each of its members. For this to be unambiguous @{term "r"} must be an equivalence relation.› definition partition_aux_body :: "('a × 'a ⇒ bool) ⇒ 'a list × 'a list list ⇒ 'a list × 'a list list" where "partition_aux_body ≡ λr (xxs, ecs). case xxs of [] ⇒ ([], []) | x # xs ⇒ let (xxs', xec) = partition_split r x xs in (xxs', (x # xec) # ecs)" definition partition_aux :: "('a × 'a ⇒ bool) ⇒ 'a list ⇒ 'a list × 'a list list" where [code]: "partition_aux r xs ≡ while (Not ∘ List.null ∘ fst) (partition_aux_body r) (xs, [])" (* FIXME move these. *) lemma equiv_subseteq_in_sym: "⟦ r `` X ⊆ X; (x, y) ∈ r; y ∈ X; equiv Y r; X ⊆ Y ⟧ ⟹ x ∈ X" unfolding equiv_def by (auto dest: symD) lemma FIXME_refl_on_insert_absorb[simp]: "⟦ refl_on A r; x ∈ A ⟧ ⟹ insert x (r `` {x}) = r `` {x}" by (auto dest: refl_onD) lemma equiv_subset[intro]: "⟦ equiv A r; B ⊆ A ⟧ ⟹ equiv B (r ∩ B × B)" unfolding equiv_def by (auto intro: refl_onI symI transI dest: refl_onD symD transD) lemma FIXME_fiddle1: "⟦ x ∈ Y; X ⊆ Y; refl_on Y r ⟧ ⟹ insert x (X ∩ r `` {x}) = (insert x X) ∩ r `` {x}" by (auto dest: refl_onD) lemma FIXME_second_fiddle: "⟦ (r ∩ Y × Y) `` X ⊆ X; refl_on Z r; x ∈ X; X ⊆ Y; Y ⊆ Z ⟧ ⟹ (r ∩ (Y - (X - r `` {x})) × (Y - (X - r `` {x}))) `` {x} = (r ∩ X × X) `` {x}" by (blast dest: refl_onD) lemma FIXME_third_fiddle: "⟦ (r ∩ Y × Y) `` X ⊆ X; X ⊆ Y; x ∈ X; y ∈ Y - X ; r `` {y} ∩ X = {} ⟧ ⟹ (r ∩ (Y - (X - r `` {x})) × (Y - (X - r `` {x}))) `` {y} = (r ∩ (Y - X) × (Y - X)) `` {y}" by auto lemma partition_aux: assumes equiv: "equiv X (rel_ext r)" and XZ: "set xs ⊆ X" shows "fst (partition_aux r xs) = [] ∧ set ` set (snd (partition_aux r xs)) = (set xs // (rel_ext r ∩ set xs × set xs))" proof - let ?b = "Not ∘ List.null ∘ fst" let ?c = "partition_aux_body r" let ?r' = "λA. rel_ext r ∩ A × A" let ?P1 = "λ(A, B). set A ⊆ set xs" let ?P2 = "λ(A, B). ?r' (set xs) `` set A ⊆ set A" let ?P3 = "λ(A, B). set ` set B = ((set xs - set A) // ?r' (set xs - set A))" let ?P = "λAB. ?P1 AB ∧ ?P2 AB ∧ ?P3 AB" let ?wfr = "inv_image finite_psubset (set ∘ fst)" show ?thesis unfolding partition_aux_def proof(rule while_rule[where P="?P" and r="?wfr"]) from equiv XZ show "?P (xs, [])" by auto next fix s assume P: "?P s" and b: "?b s" obtain A B where s: "s = (A, B)" by (cases s) blast moreover from XZ P s have "?P1 (?c (A, B))" unfolding partition_aux_body_def by (auto simp add: partition_split' split: list.split prod.split) moreover from equiv XZ P s have "?P2 (?c s)" apply (cases A) unfolding partition_aux_body_def apply simp_all subgoal for a as apply (cases "partition_split r a as") apply (simp add: partition_split') unfolding equiv_def apply (auto dest: symD transD elim: quotientE) done done moreover have "?P3 (?c s)" proof - from b s obtain x where x: "x ∈ set A" by (cases A) (auto iff: null_def) with XZ equiv P b s x show ?thesis unfolding partition_aux_body_def apply clarsimp apply (erule equivE) apply (cases A) apply simp apply simp apply (case_tac "partition_split r a list") apply clarsimp apply (simp add: partition_split') apply (subst FIXME_fiddle1[where Y=X]) apply blast apply auto[1] apply blast apply rule apply clarsimp apply rule apply (rule_tac x=a in quotientI2) apply (blast dest: refl_onD) using XZ apply (auto dest: refl_onD)[1] apply clarsimp apply (erule quotientE) apply clarsimp apply (rule_tac x=xa in quotientI2) apply (blast dest: refl_onD) apply rule apply clarsimp apply clarsimp apply rule apply rule apply clarsimp apply (cut_tac X="insert a (set list)" and Y="set xs" and x=xa and y=a and r="rel_ext r ∩ set xs × set xs" in equiv_subseteq_in_sym) apply simp_all using equiv apply blast apply clarsimp apply (cut_tac X="insert a (set list)" and Y="set xs" and x=xa and y=xb and r="rel_ext r ∩ set xs × set xs" in equiv_subseteq_in_sym) apply simp_all using equiv apply blast apply (rule subsetI) apply (erule quotientE) apply (case_tac "xaa = a") apply auto[1] apply clarsimp apply (case_tac "xa ∈ set list") apply clarsimp apply rule apply (auto dest: transD)[1] apply (auto dest: symD transD)[1] unfolding quotient_def apply clarsimp apply (erule_tac x=xa in ballE) unfolding Image_def apply clarsimp apply (auto dest: symD transD) (* SLOW *) done qed ultimately show "?P (?c s)" by auto next fix s assume P: "?P s" and b: "¬ (?b s)" from b have F: "fst s = []" apply (cases s) apply simp apply (case_tac a) apply (simp_all add: List.null_def) done from equiv P F have S: "set ` set (snd s) = (set xs // ?r' (set xs))" apply (cases s) unfolding Image_def apply simp done from F S show "fst s = [] ∧ set ` set (snd s) = (set xs // ?r' (set xs))" by (simp add: prod_eqI) next show "wf ?wfr" by (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) next fix s assume P: "?P s" and b: "?b s" from equiv XZ P b have "set (fst (?c s)) ⊂ set (fst s)" apply - apply (cases s) apply (simp add: Let_def) unfolding partition_aux_body_def apply clarsimp apply (case_tac a) apply (simp add: List.null_def) apply simp apply (case_tac "partition_split r aa list") apply (simp add: partition_split') unfolding equiv_def apply (auto dest: refl_onD) done thus "(?c s, s) ∈ ?wfr" by auto qed qed definition partition :: "('a × 'a ⇒ bool) ⇒ 'a list ⇒ 'a list list" where [code]: "partition r xs ≡ snd (partition_aux r xs)" lemma partition: assumes equiv: "equiv X (rel_ext r)" and xs: "set xs ⊆ X" shows "set ` set (partition r xs) = set xs // ((rel_ext r) ∩ set xs × set xs)" unfolding partition_def using partition_aux[OF equiv xs] by simp (* **************************************** *) fun odlist_equal :: "'a list ⇒ 'a list ⇒ bool" where "odlist_equal [] [] = True" | "odlist_equal [] ys = False" | "odlist_equal xs [] = False" | "odlist_equal (x # xs) (y # ys) = (x = y ∧ odlist_equal xs ys)" declare odlist_equal.simps [code] lemma equal_odlist_equal[simp]: "⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧ ⟹ odlist_equal xs ys ⟷ (xs = ys)" by (induct xs ys rule: odlist_equal.induct) (auto) fun difference :: "('a :: linorder) list ⇒ 'a list ⇒ 'a list" where "difference [] ys = []" | "difference xs [] = xs" | "difference (x # xs) (y # ys) = (if x = y then difference xs ys else if x < y then x # difference xs (y # ys) else difference (x # xs) ys)" declare difference.simps [code] lemma set_difference[simp]: "⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧ ⟹ set (difference xs ys) = set xs - set ys" by (induct xs ys rule: difference.induct) (auto) lemma distinct_sorted_difference[simp]: "⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧ ⟹ distinct (difference xs ys) ∧ sorted (difference xs ys)" by (induct xs ys rule: difference.induct) (auto) fun intersection :: "('a :: linorder) list ⇒ 'a list ⇒ 'a list" where "intersection [] ys = []" | "intersection xs [] = []" | "intersection (x # xs) (y # ys) = (if x = y then x # intersection xs ys else if x < y then intersection xs (y # ys) else intersection (x # xs) ys)" declare intersection.simps [code] lemma set_intersection[simp]: "⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧ ⟹ set (intersection xs ys) = set xs ∩ set ys" by (induct xs ys rule: intersection.induct) (auto) lemma distinct_sorted_intersection[simp]: "⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧ ⟹ distinct (intersection xs ys) ∧ sorted (intersection xs ys)" by (induct xs ys rule: intersection.induct) (auto) (* This is a variant of zipWith *) fun image :: "('a :: linorder × 'b :: linorder) list ⇒ 'a list ⇒ 'b list" where "image [] xs = []" | "image R [] = []" | "image ((x, y) # rs) (z # zs) = (if x = z then y # image rs (z # zs) else if x < z then image rs (z # zs) else image ((x, y) # rs) zs)" declare image.simps [code] lemma set_image[simp]: "⟦ distinct R; distinct xs; sorted R; sorted xs ⟧ ⟹ set (image R xs) = set R `` set xs" by (induct R xs rule: image.induct) (auto iff: less_eq_prod_def) (* Extra lemmas that really belong in List.thy *) lemma sorted_filter[simp]: "sorted xs ⟹ sorted (filter P xs)" by (induct xs) (auto) lemma map_prod_eq: assumes f: "map fst xs = map fst ys" and s: "map snd xs = map snd ys" shows "xs = ys" using assms by (fact pair_list_eqI) lemma list_choose_hd: assumes "∀x ∈ set xs. P x" and "x ∈ set xs" shows "P (List.hd xs)" using assms by (induct xs arbitrary: x) auto end