src/HOL/Lifting_Sum.thy
changeset 53012 cb82606b8215
child 53026 e1a548c11845
equal deleted inserted replaced
53011:aeee0a4be6cf 53012:cb82606b8215
       
     1 (*  Title:      HOL/Lifting_Sum.thy
       
     2     Author:     Brian Huffman and Ondrej Kuncar
       
     3 *)
       
     4 
       
     5 header {* Setup for Lifting/Transfer for the sum type *}
       
     6 
       
     7 theory Lifting_Sum
       
     8 imports Lifting FunDef
       
     9 begin
       
    10 
       
    11 subsection {* Relator and predicator properties *}
       
    12 
       
    13 fun
       
    14   sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
       
    15 where
       
    16   "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
       
    17 | "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
       
    18 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
       
    19 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
       
    20 
       
    21 lemma sum_rel_unfold:
       
    22   "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
       
    23     | (Inr x, Inr y) \<Rightarrow> R2 x y
       
    24     | _ \<Rightarrow> False)"
       
    25   by (cases x) (cases y, simp_all)+
       
    26 
       
    27 fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
       
    28 where
       
    29   "sum_pred P1 P2 (Inl a) = P1 a"
       
    30 | "sum_pred P1 P2 (Inr a) = P2 a"
       
    31 
       
    32 lemma sum_pred_unfold:
       
    33   "sum_pred P1 P2 x = (case x of Inl x \<Rightarrow> P1 x
       
    34     | Inr x \<Rightarrow> P2 x)"
       
    35 by (cases x) simp_all
       
    36 
       
    37 lemma sum_rel_eq [relator_eq]:
       
    38   "sum_rel (op =) (op =) = (op =)"
       
    39   by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
       
    40 
       
    41 lemma sum_rel_mono[relator_mono]:
       
    42   assumes "A \<le> C"
       
    43   assumes "B \<le> D"
       
    44   shows "(sum_rel A B) \<le> (sum_rel C D)"
       
    45 using assms by (auto simp: sum_rel_unfold split: sum.splits)
       
    46 
       
    47 lemma sum_rel_OO[relator_distr]:
       
    48   "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
       
    49 by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
       
    50 
       
    51 lemma Domainp_sum[relator_domain]:
       
    52   assumes "Domainp R1 = P1"
       
    53   assumes "Domainp R2 = P2"
       
    54   shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
       
    55 using assms
       
    56 by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
       
    57 
       
    58 lemma reflp_sum_rel[reflexivity_rule]:
       
    59   "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
       
    60   unfolding reflp_def split_sum_all sum_rel.simps by fast
       
    61 
       
    62 lemma left_total_sum_rel[reflexivity_rule]:
       
    63   "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
       
    64   using assms unfolding left_total_def split_sum_all split_sum_ex by simp
       
    65 
       
    66 lemma left_unique_sum_rel [reflexivity_rule]:
       
    67   "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)"
       
    68   using assms unfolding left_unique_def split_sum_all by simp
       
    69 
       
    70 lemma right_total_sum_rel [transfer_rule]:
       
    71   "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
       
    72   unfolding right_total_def split_sum_all split_sum_ex by simp
       
    73 
       
    74 lemma right_unique_sum_rel [transfer_rule]:
       
    75   "right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (sum_rel R1 R2)"
       
    76   unfolding right_unique_def split_sum_all by simp
       
    77 
       
    78 lemma bi_total_sum_rel [transfer_rule]:
       
    79   "bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (sum_rel R1 R2)"
       
    80   using assms unfolding bi_total_def split_sum_all split_sum_ex by simp
       
    81 
       
    82 lemma bi_unique_sum_rel [transfer_rule]:
       
    83   "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
       
    84   using assms unfolding bi_unique_def split_sum_all by simp
       
    85 
       
    86 lemma sum_invariant_commute [invariant_commute]: 
       
    87   "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
       
    88   by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split)
       
    89 
       
    90 subsection {* Quotient theorem for the Lifting package *}
       
    91 
       
    92 lemma Quotient_sum[quot_map]:
       
    93   assumes "Quotient R1 Abs1 Rep1 T1"
       
    94   assumes "Quotient R2 Abs2 Rep2 T2"
       
    95   shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2)
       
    96     (sum_map Rep1 Rep2) (sum_rel T1 T2)"
       
    97   using assms unfolding Quotient_alt_def
       
    98   by (simp add: split_sum_all)
       
    99 
       
   100 subsection {* Transfer rules for the Transfer package *}
       
   101 
       
   102 context
       
   103 begin
       
   104 interpretation lifting_syntax .
       
   105 
       
   106 lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
       
   107   unfolding fun_rel_def by simp
       
   108 
       
   109 lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr"
       
   110   unfolding fun_rel_def by simp
       
   111 
       
   112 lemma sum_case_transfer [transfer_rule]:
       
   113   "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case"
       
   114   unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split)
       
   115 
       
   116 end
       
   117 
       
   118 end
       
   119