--- 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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 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: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
+ by (metis option.exhaust) (* TODO: move to Option.thy *)
+
+lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
+ by (metis option.exhaust) (* TODO: move to Option.thy *)
+
lemma option_reflp:
"reflp R \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> right_unique (option_rel R)"
+ unfolding right_unique_def split_option_all by simp
+
+lemma bi_total_option_rel [transfer_rule]:
+ "bi_total R \<Longrightarrow> 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 \<Longrightarrow> 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"
--- 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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> 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"
--- 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 \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> 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: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
+ by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
+
+lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
+ by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
+
lemma sum_reflp:
"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> 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 \<Longrightarrow> symp R2 \<Longrightarrow> 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 \<Longrightarrow> transp R2 \<Longrightarrow> 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 \<Longrightarrow> equivp R2 \<Longrightarrow> 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 \<Longrightarrow> right_total R2 \<Longrightarrow> 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 \<Longrightarrow> right_unique R2 \<Longrightarrow> 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 \<Longrightarrow> bi_total R2 \<Longrightarrow> 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 \<Longrightarrow> bi_unique R2 \<Longrightarrow> 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"