src/HOL/Library/Quotient_Sum.thy
changeset 47624 16d433895d2e
parent 47455 26315a545e26
child 47634 091bcd569441
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 10:37:00 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 14:57:19 2012 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  (*  Title:      HOL/Library/Quotient_Sum.thy
     1.5 -    Author:     Cezary Kaliszyk and Christian Urban
     1.6 +    Author:     Cezary Kaliszyk, Christian Urban and Brian Huffman
     1.7  *)
     1.8  
     1.9  header {* Quotient infrastructure for the sum type *}
    1.10 @@ -8,6 +8,8 @@
    1.11  imports Main Quotient_Syntax
    1.12  begin
    1.13  
    1.14 +subsection {* Relator for sum type *}
    1.15 +
    1.16  fun
    1.17    sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
    1.18  where
    1.19 @@ -34,26 +36,74 @@
    1.20    "sum_map id id = id"
    1.21    by (simp add: id_def sum_map.identity fun_eq_iff)
    1.22  
    1.23 -lemma sum_rel_eq [id_simps]:
    1.24 +lemma sum_rel_eq [id_simps, relator_eq]:
    1.25    "sum_rel (op =) (op =) = (op =)"
    1.26    by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
    1.27  
    1.28 +lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
    1.29 +  by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
    1.30 +
    1.31 +lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
    1.32 +  by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
    1.33 +
    1.34  lemma sum_reflp:
    1.35    "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    1.36 -  by (auto simp add: sum_rel_unfold split: sum.splits intro!: reflpI elim: reflpE)
    1.37 +  unfolding reflp_def split_sum_all sum_rel.simps by fast
    1.38  
    1.39  lemma sum_symp:
    1.40    "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    1.41 -  by (auto simp add: sum_rel_unfold split: sum.splits intro!: sympI elim: sympE)
    1.42 +  unfolding symp_def split_sum_all sum_rel.simps by fast
    1.43  
    1.44  lemma sum_transp:
    1.45    "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
    1.46 -  by (auto simp add: sum_rel_unfold split: sum.splits intro!: transpI elim: transpE)
    1.47 +  unfolding transp_def split_sum_all sum_rel.simps by fast
    1.48  
    1.49  lemma sum_equivp [quot_equiv]:
    1.50    "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    1.51    by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
    1.52 -  
    1.53 +
    1.54 +lemma right_total_sum_rel [transfer_rule]:
    1.55 +  "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
    1.56 +  unfolding right_total_def split_sum_all split_sum_ex by simp
    1.57 +
    1.58 +lemma right_unique_sum_rel [transfer_rule]:
    1.59 +  "right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (sum_rel R1 R2)"
    1.60 +  unfolding right_unique_def split_sum_all by simp
    1.61 +
    1.62 +lemma bi_total_sum_rel [transfer_rule]:
    1.63 +  "bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (sum_rel R1 R2)"
    1.64 +  using assms unfolding bi_total_def split_sum_all split_sum_ex by simp
    1.65 +
    1.66 +lemma bi_unique_sum_rel [transfer_rule]:
    1.67 +  "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
    1.68 +  using assms unfolding bi_unique_def split_sum_all by simp
    1.69 +
    1.70 +subsection {* Correspondence rules for transfer package *}
    1.71 +
    1.72 +lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
    1.73 +  unfolding fun_rel_def by simp
    1.74 +
    1.75 +lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr"
    1.76 +  unfolding fun_rel_def by simp
    1.77 +
    1.78 +lemma sum_case_transfer [transfer_rule]:
    1.79 +  "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case"
    1.80 +  unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split)
    1.81 +
    1.82 +subsection {* Setup for lifting package *}
    1.83 +
    1.84 +lemma Quotient_sum:
    1.85 +  assumes "Quotient R1 Abs1 Rep1 T1"
    1.86 +  assumes "Quotient R2 Abs2 Rep2 T2"
    1.87 +  shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2)
    1.88 +    (sum_map Rep1 Rep2) (sum_rel T1 T2)"
    1.89 +  using assms unfolding Quotient_alt_def
    1.90 +  by (simp add: split_sum_all)
    1.91 +
    1.92 +declare [[map sum = (sum_rel, Quotient_sum)]]
    1.93 +
    1.94 +subsection {* Rules for quotient package *}
    1.95 +
    1.96  lemma sum_quotient [quot_thm]:
    1.97    assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.98    assumes q2: "Quotient3 R2 Abs2 Rep2"