kuncar@47308: (* Title: HOL/Library/Quotient3_List.thy kaliszyk@35222: Author: Cezary Kaliszyk and Christian Urban kaliszyk@35222: *) wenzelm@35788: wenzelm@35788: header {* Quotient infrastructure for the list type *} wenzelm@35788: kaliszyk@35222: theory Quotient_List kaliszyk@35222: imports Main Quotient_Syntax kaliszyk@35222: begin kaliszyk@35222: haftmann@40820: lemma map_id [id_simps]: haftmann@40820: "map id = id" haftmann@46663: by (fact List.map.id) kaliszyk@35222: haftmann@40820: lemma list_all2_eq [id_simps]: haftmann@40820: "list_all2 (op =) = (op =)" haftmann@40820: proof (rule ext)+ haftmann@40820: fix xs ys haftmann@40820: show "list_all2 (op =) xs ys \ xs = ys" haftmann@40820: by (induct xs ys rule: list_induct2') simp_all haftmann@40820: qed kaliszyk@35222: haftmann@40820: lemma list_reflp: haftmann@40820: assumes "reflp R" haftmann@40820: shows "reflp (list_all2 R)" haftmann@40820: proof (rule reflpI) haftmann@40820: from assms have *: "\xs. R xs xs" by (rule reflpE) haftmann@40820: fix xs haftmann@40820: show "list_all2 R xs xs" haftmann@40820: by (induct xs) (simp_all add: *) haftmann@40820: qed kaliszyk@35222: haftmann@40820: lemma list_symp: haftmann@40820: assumes "symp R" haftmann@40820: shows "symp (list_all2 R)" haftmann@40820: proof (rule sympI) haftmann@40820: from assms have *: "\xs ys. R xs ys \ R ys xs" by (rule sympE) haftmann@40820: fix xs ys haftmann@40820: assume "list_all2 R xs ys" haftmann@40820: then show "list_all2 R ys xs" haftmann@40820: by (induct xs ys rule: list_induct2') (simp_all add: *) haftmann@40820: qed kaliszyk@35222: haftmann@40820: lemma list_transp: haftmann@40820: assumes "transp R" haftmann@40820: shows "transp (list_all2 R)" haftmann@40820: proof (rule transpI) haftmann@40820: from assms have *: "\xs ys zs. R xs ys \ R ys zs \ R xs zs" by (rule transpE) haftmann@40820: fix xs ys zs huffman@45803: assume "list_all2 R xs ys" and "list_all2 R ys zs" huffman@45803: then show "list_all2 R xs zs" huffman@45803: by (induct arbitrary: zs) (auto simp: list_all2_Cons1 intro: *) haftmann@40820: qed kaliszyk@35222: haftmann@40820: lemma list_equivp [quot_equiv]: haftmann@40820: "equivp R \ equivp (list_all2 R)" haftmann@40820: by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE) kaliszyk@35222: kuncar@47308: lemma list_quotient3 [quot_thm]: kuncar@47308: assumes "Quotient3 R Abs Rep" kuncar@47308: shows "Quotient3 (list_all2 R) (map Abs) (map Rep)" kuncar@47308: proof (rule Quotient3I) kuncar@47308: from assms have "\x. Abs (Rep x) = x" by (rule Quotient3_abs_rep) haftmann@40820: then show "\xs. map Abs (map Rep xs) = xs" by (simp add: comp_def) haftmann@40820: next kuncar@47308: from assms have "\x y. R (Rep x) (Rep y) \ x = y" by (rule Quotient3_rel_rep) haftmann@40820: then show "\xs. list_all2 R (map Rep xs) (map Rep xs)" haftmann@40820: by (simp add: list_all2_map1 list_all2_map2 list_all2_eq) haftmann@40820: next haftmann@40820: fix xs ys kuncar@47308: from assms have "\x y. R x x \ R y y \ Abs x = Abs y \ R x y" by (rule Quotient3_rel) haftmann@40820: then show "list_all2 R xs ys \ list_all2 R xs xs \ list_all2 R ys ys \ map Abs xs = map Abs ys" haftmann@40820: by (induct xs ys rule: list_induct2') auto haftmann@40820: qed kaliszyk@35222: kuncar@47308: declare [[mapQ3 list = (list_all2, list_quotient3)]] kuncar@47094: haftmann@40820: lemma cons_prs [quot_preserve]: kuncar@47308: assumes q: "Quotient3 R Abs Rep" kaliszyk@35222: shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" kuncar@47308: by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q]) kaliszyk@35222: haftmann@40820: lemma cons_rsp [quot_respect]: kuncar@47308: assumes q: "Quotient3 R Abs Rep" kaliszyk@37492: shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)" haftmann@40463: by auto kaliszyk@35222: haftmann@40820: lemma nil_prs [quot_preserve]: kuncar@47308: assumes q: "Quotient3 R Abs Rep" kaliszyk@35222: shows "map Abs [] = []" kaliszyk@35222: by simp kaliszyk@35222: haftmann@40820: lemma nil_rsp [quot_respect]: kuncar@47308: assumes q: "Quotient3 R Abs Rep" kaliszyk@37492: shows "list_all2 R [] []" kaliszyk@35222: by simp kaliszyk@35222: kaliszyk@35222: lemma map_prs_aux: kuncar@47308: assumes a: "Quotient3 R1 abs1 rep1" kuncar@47308: and b: "Quotient3 R2 abs2 rep2" kaliszyk@35222: shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" kaliszyk@35222: by (induct l) kuncar@47308: (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) kaliszyk@35222: haftmann@40820: lemma map_prs [quot_preserve]: kuncar@47308: assumes a: "Quotient3 R1 abs1 rep1" kuncar@47308: and b: "Quotient3 R2 abs2 rep2" kaliszyk@35222: shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" kaliszyk@36216: and "((abs1 ---> id) ---> map rep1 ---> id) map = map" haftmann@40463: by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def) kuncar@47308: (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) haftmann@40463: haftmann@40820: lemma map_rsp [quot_respect]: kuncar@47308: assumes q1: "Quotient3 R1 Abs1 Rep1" kuncar@47308: and q2: "Quotient3 R2 Abs2 Rep2" kaliszyk@37492: shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map" kaliszyk@37492: and "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map" haftmann@40463: apply (simp_all add: fun_rel_def) kaliszyk@36216: apply(rule_tac [!] allI)+ kaliszyk@36216: apply(rule_tac [!] impI) kaliszyk@36216: apply(rule_tac [!] allI)+ kaliszyk@36216: apply (induct_tac [!] xa ya rule: list_induct2') kaliszyk@35222: apply simp_all kaliszyk@35222: done kaliszyk@35222: kaliszyk@35222: lemma foldr_prs_aux: kuncar@47308: assumes a: "Quotient3 R1 abs1 rep1" kuncar@47308: and b: "Quotient3 R2 abs2 rep2" kaliszyk@35222: shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" kuncar@47308: by (induct l) (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) kaliszyk@35222: haftmann@40820: lemma foldr_prs [quot_preserve]: kuncar@47308: assumes a: "Quotient3 R1 abs1 rep1" kuncar@47308: and b: "Quotient3 R2 abs2 rep2" kaliszyk@35222: shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" haftmann@40463: apply (simp add: fun_eq_iff) haftmann@40463: by (simp only: fun_eq_iff foldr_prs_aux[OF a b]) kaliszyk@35222: (simp) kaliszyk@35222: kaliszyk@35222: lemma foldl_prs_aux: kuncar@47308: assumes a: "Quotient3 R1 abs1 rep1" kuncar@47308: and b: "Quotient3 R2 abs2 rep2" kaliszyk@35222: shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" kuncar@47308: by (induct l arbitrary:e) (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) kaliszyk@35222: haftmann@40820: lemma foldl_prs [quot_preserve]: kuncar@47308: assumes a: "Quotient3 R1 abs1 rep1" kuncar@47308: and b: "Quotient3 R2 abs2 rep2" kaliszyk@35222: shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" haftmann@40463: by (simp add: fun_eq_iff foldl_prs_aux [OF a b]) kaliszyk@35222: kaliszyk@35222: (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) kaliszyk@35222: lemma foldl_rsp[quot_respect]: kuncar@47308: assumes q1: "Quotient3 R1 Abs1 Rep1" kuncar@47308: and q2: "Quotient3 R2 Abs2 Rep2" kaliszyk@37492: shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_all2 R2 ===> R1) foldl foldl" haftmann@40463: apply(auto simp add: fun_rel_def) huffman@45803: apply (erule_tac P="R1 xa ya" in rev_mp) kaliszyk@35222: apply (rule_tac x="xa" in spec) kaliszyk@35222: apply (rule_tac x="ya" in spec) huffman@45803: apply (erule list_all2_induct, simp_all) kaliszyk@35222: done kaliszyk@35222: kaliszyk@35222: lemma foldr_rsp[quot_respect]: kuncar@47308: assumes q1: "Quotient3 R1 Abs1 Rep1" kuncar@47308: and q2: "Quotient3 R2 Abs2 Rep2" kaliszyk@37492: shows "((R1 ===> R2 ===> R2) ===> list_all2 R1 ===> R2 ===> R2) foldr foldr" haftmann@40463: apply (auto simp add: fun_rel_def) huffman@45803: apply (erule list_all2_induct, simp_all) kaliszyk@35222: done kaliszyk@35222: kaliszyk@37492: lemma list_all2_rsp: kaliszyk@36154: assumes r: "\x y. R x y \ (\a b. R a b \ S x a = T y b)" kaliszyk@37492: and l1: "list_all2 R x y" kaliszyk@37492: and l2: "list_all2 R a b" kaliszyk@37492: shows "list_all2 S x a = list_all2 T y b" huffman@45803: using l1 l2 huffman@45803: by (induct arbitrary: a b rule: list_all2_induct, huffman@45803: auto simp: list_all2_Cons1 list_all2_Cons2 r) kaliszyk@36154: haftmann@40820: lemma [quot_respect]: kaliszyk@37492: "((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2" haftmann@40463: by (simp add: list_all2_rsp fun_rel_def) kaliszyk@36154: haftmann@40820: lemma [quot_preserve]: kuncar@47308: assumes a: "Quotient3 R abs1 rep1" kaliszyk@37492: shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2" nipkow@39302: apply (simp add: fun_eq_iff) kaliszyk@36154: apply clarify kaliszyk@36154: apply (induct_tac xa xb rule: list_induct2') kuncar@47308: apply (simp_all add: Quotient3_abs_rep[OF a]) kaliszyk@36154: done kaliszyk@36154: haftmann@40820: lemma [quot_preserve]: kuncar@47308: assumes a: "Quotient3 R abs1 rep1" kaliszyk@37492: shows "(list_all2 ((rep1 ---> rep1 ---> id) R) l m) = (l = m)" kuncar@47308: by (induct l m rule: list_induct2') (simp_all add: Quotient3_rel_rep[OF a]) kaliszyk@36154: kaliszyk@37492: lemma list_all2_find_element: kaliszyk@36276: assumes a: "x \ set a" kaliszyk@37492: and b: "list_all2 R a b" kaliszyk@36276: shows "\y. (y \ set b \ R x y)" huffman@45803: using b a by induct auto kaliszyk@36276: kaliszyk@37492: lemma list_all2_refl: kaliszyk@35222: assumes a: "\x y. R x y = (R x = R y)" kaliszyk@37492: shows "list_all2 R x x" kaliszyk@35222: by (induct x) (auto simp add: a) kaliszyk@35222: kuncar@47308: lemma list_quotient: kuncar@47308: assumes "Quotient R Abs Rep T" kuncar@47308: shows "Quotient (list_all2 R) (List.map Abs) (List.map Rep) (list_all2 T)" kuncar@47308: proof (rule QuotientI) kuncar@47308: from assms have "\x. Abs (Rep x) = x" by (rule Quotient_abs_rep) kuncar@47308: then show "\xs. List.map Abs (List.map Rep xs) = xs" by (simp add: comp_def) kuncar@47308: next kuncar@47308: from assms have "\x y. R (Rep x) (Rep y) \ x = y" by (rule Quotient_rel_rep) kuncar@47308: then show "\xs. list_all2 R (List.map Rep xs) (List.map Rep xs)" kuncar@47308: by (simp add: list_all2_map1 list_all2_map2 list_all2_eq) kuncar@47308: next kuncar@47308: fix xs ys kuncar@47308: from assms have "\x y. R x x \ R y y \ Abs x = Abs y \ R x y" by (rule Quotient_rel) kuncar@47308: then show "list_all2 R xs ys \ list_all2 R xs xs \ list_all2 R ys ys \ List.map Abs xs = List.map Abs ys" kuncar@47308: by (induct xs ys rule: list_induct2') auto kuncar@47308: next kuncar@47308: { kuncar@47308: fix l1 l2 kuncar@47308: have "List.length l1 = List.length l2 \ kuncar@47308: (\(x, y)\set (zip l1 l1). R x y) = (\(x, y)\set (zip l1 l2). R x x)" kuncar@47308: by (induction rule: list_induct2) auto kuncar@47308: } note x = this kuncar@47308: { kuncar@47308: fix f g kuncar@47308: have "list_all2 (\x y. f x y \ g x y) = (\ x y. list_all2 f x y \ list_all2 g x y)" kuncar@47308: by (intro ext) (auto simp add: list_all2_def) kuncar@47308: } note list_all2_conj = this kuncar@47308: from assms have t: "T = (\x y. R x x \ Abs x = y)" by (rule Quotient_cr_rel) kuncar@47308: show "list_all2 T = (\x y. list_all2 R x x \ List.map Abs x = y)" kuncar@47308: apply (simp add: t list_all2_conj[symmetric]) kuncar@47308: apply (rule sym) kuncar@47308: apply (simp add: list_all2_conj) kuncar@47308: apply(intro ext) kuncar@47308: apply (intro rev_conj_cong) kuncar@47308: unfolding list_all2_def apply (metis List.list_all2_eq list_all2_def list_all2_map1) kuncar@47308: apply (drule conjunct1) kuncar@47308: apply (intro conj_cong) kuncar@47308: apply simp kuncar@47308: apply(simp add: x) kuncar@47308: done kuncar@47308: qed kuncar@47308: kuncar@47308: declare [[map list = (list_all2, list_quotient)]] kuncar@47308: kaliszyk@35222: end