wenzelm@47455: (* Title: HOL/Library/Quotient_Sum.thy huffman@47624: Author: Cezary Kaliszyk, Christian Urban and Brian Huffman kaliszyk@35222: *) wenzelm@35788: wenzelm@35788: header {* Quotient infrastructure for the sum type *} wenzelm@35788: kaliszyk@35222: theory Quotient_Sum kaliszyk@35222: imports Main Quotient_Syntax kaliszyk@35222: begin kaliszyk@35222: huffman@47624: subsection {* Relator for sum type *} huffman@47624: kaliszyk@35222: fun haftmann@40542: sum_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ 'a + 'b \ 'c + 'd \ bool" kaliszyk@35222: where kaliszyk@35222: "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" kaliszyk@35222: | "sum_rel R1 R2 (Inl a1) (Inr b2) = False" kaliszyk@35222: | "sum_rel R1 R2 (Inr a2) (Inl b1) = False" kaliszyk@35222: | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" kaliszyk@35222: haftmann@40820: lemma sum_rel_unfold: haftmann@40820: "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \ R1 x y haftmann@40820: | (Inr x, Inr y) \ R2 x y haftmann@40820: | _ \ False)" haftmann@40820: by (cases x) (cases y, simp_all)+ kaliszyk@35222: haftmann@40820: lemma sum_rel_map1: haftmann@40820: "sum_rel R1 R2 (sum_map f1 f2 x) y \ sum_rel (\x. R1 (f1 x)) (\x. R2 (f2 x)) x y" haftmann@40820: by (simp add: sum_rel_unfold split: sum.split) haftmann@40820: haftmann@40820: lemma sum_rel_map2: haftmann@40820: "sum_rel R1 R2 x (sum_map f1 f2 y) \ sum_rel (\x y. R1 x (f1 y)) (\x y. R2 x (f2 y)) x y" haftmann@40820: by (simp add: sum_rel_unfold split: sum.split) haftmann@40820: haftmann@40820: lemma sum_map_id [id_simps]: haftmann@40820: "sum_map id id = id" haftmann@40820: by (simp add: id_def sum_map.identity fun_eq_iff) kaliszyk@35222: huffman@47624: lemma sum_rel_eq [id_simps, relator_eq]: haftmann@40820: "sum_rel (op =) (op =) = (op =)" haftmann@40820: by (simp add: sum_rel_unfold fun_eq_iff split: sum.split) haftmann@40820: huffman@47624: lemma split_sum_all: "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" huffman@47624: by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) huffman@47624: huffman@47624: lemma split_sum_ex: "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" huffman@47624: by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) huffman@47624: kuncar@47982: lemma sum_reflp[reflexivity_rule]: haftmann@40820: "reflp R1 \ reflp R2 \ reflp (sum_rel R1 R2)" huffman@47624: unfolding reflp_def split_sum_all sum_rel.simps by fast kaliszyk@35222: kuncar@47982: lemma sum_left_total[reflexivity_rule]: kuncar@47982: "left_total R1 \ left_total R2 \ left_total (sum_rel R1 R2)" kuncar@47982: apply (intro left_totalI) kuncar@47982: unfolding split_sum_ex kuncar@47982: by (case_tac x) (auto elim: left_totalE) kuncar@47982: haftmann@40820: lemma sum_symp: haftmann@40820: "symp R1 \ symp R2 \ symp (sum_rel R1 R2)" huffman@47624: unfolding symp_def split_sum_all sum_rel.simps by fast haftmann@40820: haftmann@40820: lemma sum_transp: haftmann@40820: "transp R1 \ transp R2 \ transp (sum_rel R1 R2)" huffman@47624: unfolding transp_def split_sum_all sum_rel.simps by fast haftmann@40820: haftmann@40820: lemma sum_equivp [quot_equiv]: haftmann@40820: "equivp R1 \ equivp R2 \ equivp (sum_rel R1 R2)" haftmann@40820: by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE) huffman@47624: huffman@47624: lemma right_total_sum_rel [transfer_rule]: huffman@47624: "right_total R1 \ right_total R2 \ right_total (sum_rel R1 R2)" huffman@47624: unfolding right_total_def split_sum_all split_sum_ex by simp huffman@47624: huffman@47624: lemma right_unique_sum_rel [transfer_rule]: huffman@47624: "right_unique R1 \ right_unique R2 \ right_unique (sum_rel R1 R2)" huffman@47624: unfolding right_unique_def split_sum_all by simp huffman@47624: huffman@47624: lemma bi_total_sum_rel [transfer_rule]: huffman@47624: "bi_total R1 \ bi_total R2 \ bi_total (sum_rel R1 R2)" huffman@47624: using assms unfolding bi_total_def split_sum_all split_sum_ex by simp huffman@47624: huffman@47624: lemma bi_unique_sum_rel [transfer_rule]: huffman@47624: "bi_unique R1 \ bi_unique R2 \ bi_unique (sum_rel R1 R2)" huffman@47624: using assms unfolding bi_unique_def split_sum_all by simp huffman@47624: huffman@47635: subsection {* Transfer rules for transfer package *} huffman@47624: huffman@47624: lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl" huffman@47624: unfolding fun_rel_def by simp huffman@47624: huffman@47624: lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr" huffman@47624: unfolding fun_rel_def by simp huffman@47624: huffman@47624: lemma sum_case_transfer [transfer_rule]: huffman@47624: "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case" huffman@47624: unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split) huffman@47624: huffman@47624: subsection {* Setup for lifting package *} huffman@47624: kuncar@47777: lemma Quotient_sum[quot_map]: huffman@47624: assumes "Quotient R1 Abs1 Rep1 T1" huffman@47624: assumes "Quotient R2 Abs2 Rep2 T2" huffman@47624: shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) huffman@47624: (sum_map Rep1 Rep2) (sum_rel T1 T2)" huffman@47624: using assms unfolding Quotient_alt_def huffman@47624: by (simp add: split_sum_all) huffman@47624: kuncar@47634: fun sum_pred :: "('a \ bool) \ ('b \ bool) \ 'a + 'b \ bool" kuncar@47634: where kuncar@47634: "sum_pred R1 R2 (Inl a) = R1 a" kuncar@47634: | "sum_pred R1 R2 (Inr a) = R2 a" kuncar@47634: kuncar@47634: lemma sum_invariant_commute [invariant_commute]: kuncar@47634: "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)" kuncar@47634: apply (simp add: fun_eq_iff Lifting.invariant_def) kuncar@47634: apply (intro allI) kuncar@47634: apply (case_tac x rule: sum.exhaust) kuncar@47634: apply (case_tac xa rule: sum.exhaust) kuncar@47634: apply auto[2] kuncar@47634: apply (case_tac xa rule: sum.exhaust) kuncar@47634: apply auto kuncar@47634: done kuncar@47634: huffman@47624: subsection {* Rules for quotient package *} huffman@47624: haftmann@40820: lemma sum_quotient [quot_thm]: kuncar@47308: assumes q1: "Quotient3 R1 Abs1 Rep1" kuncar@47308: assumes q2: "Quotient3 R2 Abs2 Rep2" kuncar@47308: shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" kuncar@47308: apply (rule Quotient3I) haftmann@41372: apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2 kuncar@47308: Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2]) kuncar@47308: using Quotient3_rel [OF q1] Quotient3_rel [OF q2] haftmann@41372: apply (simp add: sum_rel_unfold comp_def split: sum.split) kaliszyk@35222: done kaliszyk@35222: kuncar@47308: declare [[mapQ3 sum = (sum_rel, sum_quotient)]] kuncar@47094: haftmann@40820: lemma sum_Inl_rsp [quot_respect]: kuncar@47308: assumes q1: "Quotient3 R1 Abs1 Rep1" kuncar@47308: assumes q2: "Quotient3 R2 Abs2 Rep2" kaliszyk@35222: shows "(R1 ===> sum_rel R1 R2) Inl Inl" haftmann@40465: by auto kaliszyk@35222: haftmann@40820: lemma sum_Inr_rsp [quot_respect]: kuncar@47308: assumes q1: "Quotient3 R1 Abs1 Rep1" kuncar@47308: assumes q2: "Quotient3 R2 Abs2 Rep2" kaliszyk@35222: shows "(R2 ===> sum_rel R1 R2) Inr Inr" haftmann@40465: by auto kaliszyk@35222: haftmann@40820: lemma sum_Inl_prs [quot_preserve]: kuncar@47308: assumes q1: "Quotient3 R1 Abs1 Rep1" kuncar@47308: assumes q2: "Quotient3 R2 Abs2 Rep2" kaliszyk@35222: shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" nipkow@39302: apply(simp add: fun_eq_iff) kuncar@47308: apply(simp add: Quotient3_abs_rep[OF q1]) kaliszyk@35222: done kaliszyk@35222: haftmann@40820: lemma sum_Inr_prs [quot_preserve]: kuncar@47308: assumes q1: "Quotient3 R1 Abs1 Rep1" kuncar@47308: assumes q2: "Quotient3 R2 Abs2 Rep2" kaliszyk@35222: shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" nipkow@39302: apply(simp add: fun_eq_iff) kuncar@47308: apply(simp add: Quotient3_abs_rep[OF q2]) kaliszyk@35222: done kaliszyk@35222: kaliszyk@35222: end