# HG changeset patch # User huffman # Date 1334926639 -7200 # Node ID 16d433895d2e4cf842bcf7e7c4e2d274bcf441dc # Parent 01e4fdf9d7484a5b858042148d1b9f1138caa79c add new transfer rules and setup for lifting package diff -r 01e4fdf9d748 -r 16d433895d2e src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Fri Apr 20 10:37:00 2012 +0200 +++ b/src/HOL/Library/Quotient_Option.thy Fri Apr 20 14:57:19 2012 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Library/Quotient_Option.thy - Author: Cezary Kaliszyk and Christian Urban + Author: Cezary Kaliszyk, Christian Urban and Brian Huffman *) header {* Quotient infrastructure for the option type *} @@ -8,6 +8,8 @@ imports Main Quotient_Syntax begin +subsection {* Relator for option type *} + fun option_rel :: "('a \ 'b \ bool) \ 'a option \ 'b option \ bool" where @@ -34,26 +36,82 @@ "Option.map id = id" by (simp add: id_def Option.map.identity fun_eq_iff) -lemma option_rel_eq [id_simps]: +lemma option_rel_eq [id_simps, relator_eq]: "option_rel (op =) = (op =)" by (simp add: option_rel_unfold fun_eq_iff split: option.split) +lemma split_option_all: "(\x. P x) \ P None \ (\x. P (Some x))" + by (metis option.exhaust) (* TODO: move to Option.thy *) + +lemma split_option_ex: "(\x. P x) \ P None \ (\x. P (Some x))" + by (metis option.exhaust) (* TODO: move to Option.thy *) + lemma option_reflp: "reflp R \ reflp (option_rel R)" - by (auto simp add: option_rel_unfold split: option.splits intro!: reflpI elim: reflpE) + unfolding reflp_def split_option_all by simp lemma option_symp: "symp R \ symp (option_rel R)" - by (auto simp add: option_rel_unfold split: option.splits intro!: sympI elim: sympE) + unfolding symp_def split_option_all option_rel.simps by fast lemma option_transp: "transp R \ transp (option_rel R)" - by (auto simp add: option_rel_unfold split: option.splits intro!: transpI elim: transpE) + unfolding transp_def split_option_all option_rel.simps by fast lemma option_equivp [quot_equiv]: "equivp R \ equivp (option_rel R)" by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE) +lemma right_total_option_rel [transfer_rule]: + "right_total R \ right_total (option_rel R)" + unfolding right_total_def split_option_all split_option_ex by simp + +lemma right_unique_option_rel [transfer_rule]: + "right_unique R \ right_unique (option_rel R)" + unfolding right_unique_def split_option_all by simp + +lemma bi_total_option_rel [transfer_rule]: + "bi_total R \ bi_total (option_rel R)" + unfolding bi_total_def split_option_all split_option_ex by simp + +lemma bi_unique_option_rel [transfer_rule]: + "bi_unique R \ bi_unique (option_rel R)" + unfolding bi_unique_def split_option_all by simp + +subsection {* Correspondence rules for transfer package *} + +lemma None_transfer [transfer_rule]: "(option_rel A) None None" + by simp + +lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some" + unfolding fun_rel_def by simp + +lemma option_case_transfer [transfer_rule]: + "(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case" + unfolding fun_rel_def split_option_all by simp + +lemma option_map_transfer [transfer_rule]: + "((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map" + unfolding Option.map_def by correspondence + +lemma option_bind_transfer [transfer_rule]: + "(option_rel A ===> (A ===> option_rel B) ===> option_rel B) + Option.bind Option.bind" + unfolding fun_rel_def split_option_all by simp + +subsection {* Setup for lifting package *} + +lemma Quotient_option: + assumes "Quotient R Abs Rep T" + shows "Quotient (option_rel R) (Option.map Abs) + (Option.map Rep) (option_rel T)" + using assms unfolding Quotient_alt_def option_rel_unfold + by (simp split: option.split) + +declare [[map option = (option_rel, Quotient_option)]] + +subsection {* Rules for quotient package *} + lemma option_quotient [quot_thm]: assumes "Quotient3 R Abs Rep" shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)" @@ -68,12 +126,12 @@ lemma option_None_rsp [quot_respect]: assumes q: "Quotient3 R Abs Rep" shows "option_rel R None None" - by simp + by (rule None_transfer) lemma option_Some_rsp [quot_respect]: assumes q: "Quotient3 R Abs Rep" shows "(R ===> option_rel R) Some Some" - by auto + by (rule Some_transfer) lemma option_None_prs [quot_preserve]: assumes q: "Quotient3 R Abs Rep" diff -r 01e4fdf9d748 -r 16d433895d2e src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Fri Apr 20 10:37:00 2012 +0200 +++ b/src/HOL/Library/Quotient_Product.thy Fri Apr 20 14:57:19 2012 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Library/Quotient_Product.thy - Author: Cezary Kaliszyk and Christian Urban + Author: Cezary Kaliszyk, Christian Urban and Brian Huffman *) header {* Quotient infrastructure for the product type *} @@ -8,6 +8,8 @@ imports Main Quotient_Syntax begin +subsection {* Relator for product type *} + definition prod_rel :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" where @@ -21,7 +23,7 @@ shows "map_pair id id = id" by (simp add: fun_eq_iff) -lemma prod_rel_eq [id_simps]: +lemma prod_rel_eq [id_simps, relator_eq]: shows "prod_rel (op =) (op =) = (op =)" by (simp add: fun_eq_iff) @@ -31,6 +33,68 @@ shows "equivp (prod_rel R1 R2)" using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE) +lemma right_total_prod_rel [transfer_rule]: + assumes "right_total R1" and "right_total R2" + shows "right_total (prod_rel R1 R2)" + using assms unfolding right_total_def prod_rel_def by auto + +lemma right_unique_prod_rel [transfer_rule]: + assumes "right_unique R1" and "right_unique R2" + shows "right_unique (prod_rel R1 R2)" + using assms unfolding right_unique_def prod_rel_def by auto + +lemma bi_total_prod_rel [transfer_rule]: + assumes "bi_total R1" and "bi_total R2" + shows "bi_total (prod_rel R1 R2)" + using assms unfolding bi_total_def prod_rel_def by auto + +lemma bi_unique_prod_rel [transfer_rule]: + assumes "bi_unique R1" and "bi_unique R2" + shows "bi_unique (prod_rel R1 R2)" + using assms unfolding bi_unique_def prod_rel_def by auto + +subsection {* Correspondence rules for transfer package *} + +lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair" + unfolding fun_rel_def prod_rel_def by simp + +lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst" + unfolding fun_rel_def prod_rel_def by simp + +lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd" + unfolding fun_rel_def prod_rel_def by simp + +lemma prod_case_transfer [transfer_rule]: + "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case" + unfolding fun_rel_def prod_rel_def by simp + +lemma curry_transfer [transfer_rule]: + "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry" + unfolding curry_def by correspondence + +lemma map_pair_transfer [transfer_rule]: + "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D) + map_pair map_pair" + unfolding map_pair_def [abs_def] by correspondence + +lemma prod_rel_transfer [transfer_rule]: + "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> + prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel" + unfolding fun_rel_def by auto + +subsection {* Setup for lifting package *} + +lemma Quotient_prod: + assumes "Quotient R1 Abs1 Rep1 T1" + assumes "Quotient R2 Abs2 Rep2 T2" + shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) + (map_pair Rep1 Rep2) (prod_rel T1 T2)" + using assms unfolding Quotient_alt_def by auto + +declare [[map prod = (prod_rel, Quotient_prod)]] + +subsection {* Rules for quotient package *} + lemma prod_quotient [quot_thm]: assumes "Quotient3 R1 Abs1 Rep1" assumes "Quotient3 R2 Abs2 Rep2" @@ -49,7 +113,7 @@ assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" - by (auto simp add: prod_rel_def) + by (rule Pair_transfer) lemma Pair_prs [quot_preserve]: assumes q1: "Quotient3 R1 Abs1 Rep1" @@ -85,8 +149,7 @@ lemma split_rsp [quot_respect]: shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" - unfolding prod_rel_def fun_rel_def - by auto + by (rule prod_case_transfer) lemma split_prs [quot_preserve]: assumes q1: "Quotient3 R1 Abs1 Rep1" @@ -97,7 +160,7 @@ lemma [quot_respect]: shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel" - by (auto simp add: fun_rel_def) + by (rule prod_rel_transfer) lemma [quot_preserve]: assumes q1: "Quotient3 R1 abs1 rep1" diff -r 01e4fdf9d748 -r 16d433895d2e src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Fri Apr 20 10:37:00 2012 +0200 +++ b/src/HOL/Library/Quotient_Sum.thy Fri Apr 20 14:57:19 2012 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Library/Quotient_Sum.thy - Author: Cezary Kaliszyk and Christian Urban + Author: Cezary Kaliszyk, Christian Urban and Brian Huffman *) header {* Quotient infrastructure for the sum type *} @@ -8,6 +8,8 @@ imports Main Quotient_Syntax begin +subsection {* Relator for sum type *} + fun sum_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ 'a + 'b \ 'c + 'd \ bool" where @@ -34,26 +36,74 @@ "sum_map id id = id" by (simp add: id_def sum_map.identity fun_eq_iff) -lemma sum_rel_eq [id_simps]: +lemma sum_rel_eq [id_simps, relator_eq]: "sum_rel (op =) (op =) = (op =)" by (simp add: sum_rel_unfold fun_eq_iff split: sum.split) +lemma split_sum_all: "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" + by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) + +lemma split_sum_ex: "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" + by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) + lemma sum_reflp: "reflp R1 \ reflp R2 \ reflp (sum_rel R1 R2)" - by (auto simp add: sum_rel_unfold split: sum.splits intro!: reflpI elim: reflpE) + unfolding reflp_def split_sum_all sum_rel.simps by fast lemma sum_symp: "symp R1 \ symp R2 \ symp (sum_rel R1 R2)" - by (auto simp add: sum_rel_unfold split: sum.splits intro!: sympI elim: sympE) + unfolding symp_def split_sum_all sum_rel.simps by fast lemma sum_transp: "transp R1 \ transp R2 \ transp (sum_rel R1 R2)" - by (auto simp add: sum_rel_unfold split: sum.splits intro!: transpI elim: transpE) + unfolding transp_def split_sum_all sum_rel.simps by fast lemma sum_equivp [quot_equiv]: "equivp R1 \ equivp R2 \ equivp (sum_rel R1 R2)" by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE) - + +lemma right_total_sum_rel [transfer_rule]: + "right_total R1 \ right_total R2 \ right_total (sum_rel R1 R2)" + unfolding right_total_def split_sum_all split_sum_ex by simp + +lemma right_unique_sum_rel [transfer_rule]: + "right_unique R1 \ right_unique R2 \ right_unique (sum_rel R1 R2)" + unfolding right_unique_def split_sum_all by simp + +lemma bi_total_sum_rel [transfer_rule]: + "bi_total R1 \ bi_total R2 \ bi_total (sum_rel R1 R2)" + using assms unfolding bi_total_def split_sum_all split_sum_ex by simp + +lemma bi_unique_sum_rel [transfer_rule]: + "bi_unique R1 \ bi_unique R2 \ bi_unique (sum_rel R1 R2)" + using assms unfolding bi_unique_def split_sum_all by simp + +subsection {* Correspondence rules for transfer package *} + +lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl" + unfolding fun_rel_def by simp + +lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr" + unfolding fun_rel_def by simp + +lemma sum_case_transfer [transfer_rule]: + "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case" + unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split) + +subsection {* Setup for lifting package *} + +lemma Quotient_sum: + assumes "Quotient R1 Abs1 Rep1 T1" + assumes "Quotient R2 Abs2 Rep2 T2" + shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) + (sum_map Rep1 Rep2) (sum_rel T1 T2)" + using assms unfolding Quotient_alt_def + by (simp add: split_sum_all) + +declare [[map sum = (sum_rel, Quotient_sum)]] + +subsection {* Rules for quotient package *} + lemma sum_quotient [quot_thm]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2"