add new transfer rules and setup for lifting package
authorhuffman
Fri Apr 20 14:57:19 2012 +0200 (2012-04-20)
changeset 4762416d433895d2e
parent 47623 01e4fdf9d748
child 47625 10cfaf771687
add new transfer rules and setup for lifting package
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Sum.thy
     1.1 --- a/src/HOL/Library/Quotient_Option.thy	Fri Apr 20 10:37:00 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Option.thy	Fri Apr 20 14:57:19 2012 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  (*  Title:      HOL/Library/Quotient_Option.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 option type *}
    1.10 @@ -8,6 +8,8 @@
    1.11  imports Main Quotient_Syntax
    1.12  begin
    1.13  
    1.14 +subsection {* Relator for option type *}
    1.15 +
    1.16  fun
    1.17    option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
    1.18  where
    1.19 @@ -34,26 +36,82 @@
    1.20    "Option.map id = id"
    1.21    by (simp add: id_def Option.map.identity fun_eq_iff)
    1.22  
    1.23 -lemma option_rel_eq [id_simps]:
    1.24 +lemma option_rel_eq [id_simps, relator_eq]:
    1.25    "option_rel (op =) = (op =)"
    1.26    by (simp add: option_rel_unfold fun_eq_iff split: option.split)
    1.27  
    1.28 +lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
    1.29 +  by (metis option.exhaust) (* TODO: move to Option.thy *)
    1.30 +
    1.31 +lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
    1.32 +  by (metis option.exhaust) (* TODO: move to Option.thy *)
    1.33 +
    1.34  lemma option_reflp:
    1.35    "reflp R \<Longrightarrow> reflp (option_rel R)"
    1.36 -  by (auto simp add: option_rel_unfold split: option.splits intro!: reflpI elim: reflpE)
    1.37 +  unfolding reflp_def split_option_all by simp
    1.38  
    1.39  lemma option_symp:
    1.40    "symp R \<Longrightarrow> symp (option_rel R)"
    1.41 -  by (auto simp add: option_rel_unfold split: option.splits intro!: sympI elim: sympE)
    1.42 +  unfolding symp_def split_option_all option_rel.simps by fast
    1.43  
    1.44  lemma option_transp:
    1.45    "transp R \<Longrightarrow> transp (option_rel R)"
    1.46 -  by (auto simp add: option_rel_unfold split: option.splits intro!: transpI elim: transpE)
    1.47 +  unfolding transp_def split_option_all option_rel.simps by fast
    1.48  
    1.49  lemma option_equivp [quot_equiv]:
    1.50    "equivp R \<Longrightarrow> equivp (option_rel R)"
    1.51    by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
    1.52  
    1.53 +lemma right_total_option_rel [transfer_rule]:
    1.54 +  "right_total R \<Longrightarrow> right_total (option_rel R)"
    1.55 +  unfolding right_total_def split_option_all split_option_ex by simp
    1.56 +
    1.57 +lemma right_unique_option_rel [transfer_rule]:
    1.58 +  "right_unique R \<Longrightarrow> right_unique (option_rel R)"
    1.59 +  unfolding right_unique_def split_option_all by simp
    1.60 +
    1.61 +lemma bi_total_option_rel [transfer_rule]:
    1.62 +  "bi_total R \<Longrightarrow> bi_total (option_rel R)"
    1.63 +  unfolding bi_total_def split_option_all split_option_ex by simp
    1.64 +
    1.65 +lemma bi_unique_option_rel [transfer_rule]:
    1.66 +  "bi_unique R \<Longrightarrow> bi_unique (option_rel R)"
    1.67 +  unfolding bi_unique_def split_option_all by simp
    1.68 +
    1.69 +subsection {* Correspondence rules for transfer package *}
    1.70 +
    1.71 +lemma None_transfer [transfer_rule]: "(option_rel A) None None"
    1.72 +  by simp
    1.73 +
    1.74 +lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some"
    1.75 +  unfolding fun_rel_def by simp
    1.76 +
    1.77 +lemma option_case_transfer [transfer_rule]:
    1.78 +  "(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case"
    1.79 +  unfolding fun_rel_def split_option_all by simp
    1.80 +
    1.81 +lemma option_map_transfer [transfer_rule]:
    1.82 +  "((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map"
    1.83 +  unfolding Option.map_def by correspondence
    1.84 +
    1.85 +lemma option_bind_transfer [transfer_rule]:
    1.86 +  "(option_rel A ===> (A ===> option_rel B) ===> option_rel B)
    1.87 +    Option.bind Option.bind"
    1.88 +  unfolding fun_rel_def split_option_all by simp
    1.89 +
    1.90 +subsection {* Setup for lifting package *}
    1.91 +
    1.92 +lemma Quotient_option:
    1.93 +  assumes "Quotient R Abs Rep T"
    1.94 +  shows "Quotient (option_rel R) (Option.map Abs)
    1.95 +    (Option.map Rep) (option_rel T)"
    1.96 +  using assms unfolding Quotient_alt_def option_rel_unfold
    1.97 +  by (simp split: option.split)
    1.98 +
    1.99 +declare [[map option = (option_rel, Quotient_option)]]
   1.100 +
   1.101 +subsection {* Rules for quotient package *}
   1.102 +
   1.103  lemma option_quotient [quot_thm]:
   1.104    assumes "Quotient3 R Abs Rep"
   1.105    shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)"
   1.106 @@ -68,12 +126,12 @@
   1.107  lemma option_None_rsp [quot_respect]:
   1.108    assumes q: "Quotient3 R Abs Rep"
   1.109    shows "option_rel R None None"
   1.110 -  by simp
   1.111 +  by (rule None_transfer)
   1.112  
   1.113  lemma option_Some_rsp [quot_respect]:
   1.114    assumes q: "Quotient3 R Abs Rep"
   1.115    shows "(R ===> option_rel R) Some Some"
   1.116 -  by auto
   1.117 +  by (rule Some_transfer)
   1.118  
   1.119  lemma option_None_prs [quot_preserve]:
   1.120    assumes q: "Quotient3 R Abs Rep"
     2.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Apr 20 10:37:00 2012 +0200
     2.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Apr 20 14:57:19 2012 +0200
     2.3 @@ -1,5 +1,5 @@
     2.4  (*  Title:      HOL/Library/Quotient_Product.thy
     2.5 -    Author:     Cezary Kaliszyk and Christian Urban
     2.6 +    Author:     Cezary Kaliszyk, Christian Urban and Brian Huffman
     2.7  *)
     2.8  
     2.9  header {* Quotient infrastructure for the product type *}
    2.10 @@ -8,6 +8,8 @@
    2.11  imports Main Quotient_Syntax
    2.12  begin
    2.13  
    2.14 +subsection {* Relator for product type *}
    2.15 +
    2.16  definition
    2.17    prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
    2.18  where
    2.19 @@ -21,7 +23,7 @@
    2.20    shows "map_pair id id = id"
    2.21    by (simp add: fun_eq_iff)
    2.22  
    2.23 -lemma prod_rel_eq [id_simps]:
    2.24 +lemma prod_rel_eq [id_simps, relator_eq]:
    2.25    shows "prod_rel (op =) (op =) = (op =)"
    2.26    by (simp add: fun_eq_iff)
    2.27  
    2.28 @@ -31,6 +33,68 @@
    2.29    shows "equivp (prod_rel R1 R2)"
    2.30    using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
    2.31  
    2.32 +lemma right_total_prod_rel [transfer_rule]:
    2.33 +  assumes "right_total R1" and "right_total R2"
    2.34 +  shows "right_total (prod_rel R1 R2)"
    2.35 +  using assms unfolding right_total_def prod_rel_def by auto
    2.36 +
    2.37 +lemma right_unique_prod_rel [transfer_rule]:
    2.38 +  assumes "right_unique R1" and "right_unique R2"
    2.39 +  shows "right_unique (prod_rel R1 R2)"
    2.40 +  using assms unfolding right_unique_def prod_rel_def by auto
    2.41 +
    2.42 +lemma bi_total_prod_rel [transfer_rule]:
    2.43 +  assumes "bi_total R1" and "bi_total R2"
    2.44 +  shows "bi_total (prod_rel R1 R2)"
    2.45 +  using assms unfolding bi_total_def prod_rel_def by auto
    2.46 +
    2.47 +lemma bi_unique_prod_rel [transfer_rule]:
    2.48 +  assumes "bi_unique R1" and "bi_unique R2"
    2.49 +  shows "bi_unique (prod_rel R1 R2)"
    2.50 +  using assms unfolding bi_unique_def prod_rel_def by auto
    2.51 +
    2.52 +subsection {* Correspondence rules for transfer package *}
    2.53 +
    2.54 +lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
    2.55 +  unfolding fun_rel_def prod_rel_def by simp
    2.56 +
    2.57 +lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst"
    2.58 +  unfolding fun_rel_def prod_rel_def by simp
    2.59 +
    2.60 +lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
    2.61 +  unfolding fun_rel_def prod_rel_def by simp
    2.62 +
    2.63 +lemma prod_case_transfer [transfer_rule]:
    2.64 +  "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case"
    2.65 +  unfolding fun_rel_def prod_rel_def by simp
    2.66 +
    2.67 +lemma curry_transfer [transfer_rule]:
    2.68 +  "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
    2.69 +  unfolding curry_def by correspondence
    2.70 +
    2.71 +lemma map_pair_transfer [transfer_rule]:
    2.72 +  "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
    2.73 +    map_pair map_pair"
    2.74 +  unfolding map_pair_def [abs_def] by correspondence
    2.75 +
    2.76 +lemma prod_rel_transfer [transfer_rule]:
    2.77 +  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
    2.78 +    prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel"
    2.79 +  unfolding fun_rel_def by auto
    2.80 +
    2.81 +subsection {* Setup for lifting package *}
    2.82 +
    2.83 +lemma Quotient_prod:
    2.84 +  assumes "Quotient R1 Abs1 Rep1 T1"
    2.85 +  assumes "Quotient R2 Abs2 Rep2 T2"
    2.86 +  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2)
    2.87 +    (map_pair Rep1 Rep2) (prod_rel T1 T2)"
    2.88 +  using assms unfolding Quotient_alt_def by auto
    2.89 +
    2.90 +declare [[map prod = (prod_rel, Quotient_prod)]]
    2.91 +
    2.92 +subsection {* Rules for quotient package *}
    2.93 +
    2.94  lemma prod_quotient [quot_thm]:
    2.95    assumes "Quotient3 R1 Abs1 Rep1"
    2.96    assumes "Quotient3 R2 Abs2 Rep2"
    2.97 @@ -49,7 +113,7 @@
    2.98    assumes q1: "Quotient3 R1 Abs1 Rep1"
    2.99    assumes q2: "Quotient3 R2 Abs2 Rep2"
   2.100    shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
   2.101 -  by (auto simp add: prod_rel_def)
   2.102 +  by (rule Pair_transfer)
   2.103  
   2.104  lemma Pair_prs [quot_preserve]:
   2.105    assumes q1: "Quotient3 R1 Abs1 Rep1"
   2.106 @@ -85,8 +149,7 @@
   2.107  
   2.108  lemma split_rsp [quot_respect]:
   2.109    shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
   2.110 -  unfolding prod_rel_def fun_rel_def
   2.111 -  by auto
   2.112 +  by (rule prod_case_transfer)
   2.113  
   2.114  lemma split_prs [quot_preserve]:
   2.115    assumes q1: "Quotient3 R1 Abs1 Rep1"
   2.116 @@ -97,7 +160,7 @@
   2.117  lemma [quot_respect]:
   2.118    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
   2.119    prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
   2.120 -  by (auto simp add: fun_rel_def)
   2.121 +  by (rule prod_rel_transfer)
   2.122  
   2.123  lemma [quot_preserve]:
   2.124    assumes q1: "Quotient3 R1 abs1 rep1"
     3.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 10:37:00 2012 +0200
     3.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 14:57:19 2012 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4  (*  Title:      HOL/Library/Quotient_Sum.thy
     3.5 -    Author:     Cezary Kaliszyk and Christian Urban
     3.6 +    Author:     Cezary Kaliszyk, Christian Urban and Brian Huffman
     3.7  *)
     3.8  
     3.9  header {* Quotient infrastructure for the sum type *}
    3.10 @@ -8,6 +8,8 @@
    3.11  imports Main Quotient_Syntax
    3.12  begin
    3.13  
    3.14 +subsection {* Relator for sum type *}
    3.15 +
    3.16  fun
    3.17    sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
    3.18  where
    3.19 @@ -34,26 +36,74 @@
    3.20    "sum_map id id = id"
    3.21    by (simp add: id_def sum_map.identity fun_eq_iff)
    3.22  
    3.23 -lemma sum_rel_eq [id_simps]:
    3.24 +lemma sum_rel_eq [id_simps, relator_eq]:
    3.25    "sum_rel (op =) (op =) = (op =)"
    3.26    by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
    3.27  
    3.28 +lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
    3.29 +  by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
    3.30 +
    3.31 +lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
    3.32 +  by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
    3.33 +
    3.34  lemma sum_reflp:
    3.35    "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    3.36 -  by (auto simp add: sum_rel_unfold split: sum.splits intro!: reflpI elim: reflpE)
    3.37 +  unfolding reflp_def split_sum_all sum_rel.simps by fast
    3.38  
    3.39  lemma sum_symp:
    3.40    "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    3.41 -  by (auto simp add: sum_rel_unfold split: sum.splits intro!: sympI elim: sympE)
    3.42 +  unfolding symp_def split_sum_all sum_rel.simps by fast
    3.43  
    3.44  lemma sum_transp:
    3.45    "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
    3.46 -  by (auto simp add: sum_rel_unfold split: sum.splits intro!: transpI elim: transpE)
    3.47 +  unfolding transp_def split_sum_all sum_rel.simps by fast
    3.48  
    3.49  lemma sum_equivp [quot_equiv]:
    3.50    "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    3.51    by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
    3.52 -  
    3.53 +
    3.54 +lemma right_total_sum_rel [transfer_rule]:
    3.55 +  "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
    3.56 +  unfolding right_total_def split_sum_all split_sum_ex by simp
    3.57 +
    3.58 +lemma right_unique_sum_rel [transfer_rule]:
    3.59 +  "right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (sum_rel R1 R2)"
    3.60 +  unfolding right_unique_def split_sum_all by simp
    3.61 +
    3.62 +lemma bi_total_sum_rel [transfer_rule]:
    3.63 +  "bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (sum_rel R1 R2)"
    3.64 +  using assms unfolding bi_total_def split_sum_all split_sum_ex by simp
    3.65 +
    3.66 +lemma bi_unique_sum_rel [transfer_rule]:
    3.67 +  "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
    3.68 +  using assms unfolding bi_unique_def split_sum_all by simp
    3.69 +
    3.70 +subsection {* Correspondence rules for transfer package *}
    3.71 +
    3.72 +lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
    3.73 +  unfolding fun_rel_def by simp
    3.74 +
    3.75 +lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr"
    3.76 +  unfolding fun_rel_def by simp
    3.77 +
    3.78 +lemma sum_case_transfer [transfer_rule]:
    3.79 +  "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case"
    3.80 +  unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split)
    3.81 +
    3.82 +subsection {* Setup for lifting package *}
    3.83 +
    3.84 +lemma Quotient_sum:
    3.85 +  assumes "Quotient R1 Abs1 Rep1 T1"
    3.86 +  assumes "Quotient R2 Abs2 Rep2 T2"
    3.87 +  shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2)
    3.88 +    (sum_map Rep1 Rep2) (sum_rel T1 T2)"
    3.89 +  using assms unfolding Quotient_alt_def
    3.90 +  by (simp add: split_sum_all)
    3.91 +
    3.92 +declare [[map sum = (sum_rel, Quotient_sum)]]
    3.93 +
    3.94 +subsection {* Rules for quotient package *}
    3.95 +
    3.96  lemma sum_quotient [quot_thm]:
    3.97    assumes q1: "Quotient3 R1 Abs1 Rep1"
    3.98    assumes q2: "Quotient3 R2 Abs2 Rep2"