src/HOL/Lifting_Product.thy
changeset 53012 cb82606b8215
child 55083 0a689157e3ce
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Lifting_Product.thy	Tue Aug 13 15:59:22 2013 +0200
     1.3 @@ -0,0 +1,135 @@
     1.4 +(*  Title:      HOL/Lifting_Product.thy
     1.5 +    Author:     Brian Huffman and Ondrej Kuncar
     1.6 +*)
     1.7 +
     1.8 +header {* Setup for Lifting/Transfer for the product type *}
     1.9 +
    1.10 +theory Lifting_Product
    1.11 +imports Lifting
    1.12 +begin
    1.13 +
    1.14 +subsection {* Relator and predicator properties *}
    1.15 +
    1.16 +definition
    1.17 +  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
    1.18 +where
    1.19 +  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    1.20 +
    1.21 +definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.22 +where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
    1.23 +
    1.24 +lemma prod_rel_apply [simp]:
    1.25 +  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.26 +  by (simp add: prod_rel_def)
    1.27 +
    1.28 +lemma prod_pred_apply [simp]:
    1.29 +  "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
    1.30 +  by (simp add: prod_pred_def)
    1.31 +
    1.32 +lemma prod_rel_eq [relator_eq]:
    1.33 +  shows "prod_rel (op =) (op =) = (op =)"
    1.34 +  by (simp add: fun_eq_iff)
    1.35 +
    1.36 +lemma prod_rel_mono[relator_mono]:
    1.37 +  assumes "A \<le> C"
    1.38 +  assumes "B \<le> D"
    1.39 +  shows "(prod_rel A B) \<le> (prod_rel C D)"
    1.40 +using assms by (auto simp: prod_rel_def)
    1.41 +
    1.42 +lemma prod_rel_OO[relator_distr]:
    1.43 +  "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
    1.44 +by (rule ext)+ (auto simp: prod_rel_def OO_def)
    1.45 +
    1.46 +lemma Domainp_prod[relator_domain]:
    1.47 +  assumes "Domainp T1 = P1"
    1.48 +  assumes "Domainp T2 = P2"
    1.49 +  shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
    1.50 +using assms unfolding prod_rel_def prod_pred_def by blast
    1.51 +
    1.52 +lemma reflp_prod_rel [reflexivity_rule]:
    1.53 +  assumes "reflp R1"
    1.54 +  assumes "reflp R2"
    1.55 +  shows "reflp (prod_rel R1 R2)"
    1.56 +using assms by (auto intro!: reflpI elim: reflpE)
    1.57 +
    1.58 +lemma left_total_prod_rel [reflexivity_rule]:
    1.59 +  assumes "left_total R1"
    1.60 +  assumes "left_total R2"
    1.61 +  shows "left_total (prod_rel R1 R2)"
    1.62 +  using assms unfolding left_total_def prod_rel_def by auto
    1.63 +
    1.64 +lemma left_unique_prod_rel [reflexivity_rule]:
    1.65 +  assumes "left_unique R1" and "left_unique R2"
    1.66 +  shows "left_unique (prod_rel R1 R2)"
    1.67 +  using assms unfolding left_unique_def prod_rel_def by auto
    1.68 +
    1.69 +lemma right_total_prod_rel [transfer_rule]:
    1.70 +  assumes "right_total R1" and "right_total R2"
    1.71 +  shows "right_total (prod_rel R1 R2)"
    1.72 +  using assms unfolding right_total_def prod_rel_def by auto
    1.73 +
    1.74 +lemma right_unique_prod_rel [transfer_rule]:
    1.75 +  assumes "right_unique R1" and "right_unique R2"
    1.76 +  shows "right_unique (prod_rel R1 R2)"
    1.77 +  using assms unfolding right_unique_def prod_rel_def by auto
    1.78 +
    1.79 +lemma bi_total_prod_rel [transfer_rule]:
    1.80 +  assumes "bi_total R1" and "bi_total R2"
    1.81 +  shows "bi_total (prod_rel R1 R2)"
    1.82 +  using assms unfolding bi_total_def prod_rel_def by auto
    1.83 +
    1.84 +lemma bi_unique_prod_rel [transfer_rule]:
    1.85 +  assumes "bi_unique R1" and "bi_unique R2"
    1.86 +  shows "bi_unique (prod_rel R1 R2)"
    1.87 +  using assms unfolding bi_unique_def prod_rel_def by auto
    1.88 +
    1.89 +lemma prod_invariant_commute [invariant_commute]: 
    1.90 +  "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
    1.91 +  by (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) blast
    1.92 +
    1.93 +subsection {* Quotient theorem for the Lifting package *}
    1.94 +
    1.95 +lemma Quotient_prod[quot_map]:
    1.96 +  assumes "Quotient R1 Abs1 Rep1 T1"
    1.97 +  assumes "Quotient R2 Abs2 Rep2 T2"
    1.98 +  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2)
    1.99 +    (map_pair Rep1 Rep2) (prod_rel T1 T2)"
   1.100 +  using assms unfolding Quotient_alt_def by auto
   1.101 +
   1.102 +subsection {* Transfer rules for the Transfer package *}
   1.103 +
   1.104 +context
   1.105 +begin
   1.106 +interpretation lifting_syntax .
   1.107 +
   1.108 +lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
   1.109 +  unfolding fun_rel_def prod_rel_def by simp
   1.110 +
   1.111 +lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst"
   1.112 +  unfolding fun_rel_def prod_rel_def by simp
   1.113 +
   1.114 +lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
   1.115 +  unfolding fun_rel_def prod_rel_def by simp
   1.116 +
   1.117 +lemma prod_case_transfer [transfer_rule]:
   1.118 +  "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case"
   1.119 +  unfolding fun_rel_def prod_rel_def by simp
   1.120 +
   1.121 +lemma curry_transfer [transfer_rule]:
   1.122 +  "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
   1.123 +  unfolding curry_def by transfer_prover
   1.124 +
   1.125 +lemma map_pair_transfer [transfer_rule]:
   1.126 +  "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
   1.127 +    map_pair map_pair"
   1.128 +  unfolding map_pair_def [abs_def] by transfer_prover
   1.129 +
   1.130 +lemma prod_rel_transfer [transfer_rule]:
   1.131 +  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
   1.132 +    prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel"
   1.133 +  unfolding fun_rel_def by auto
   1.134 +
   1.135 +end
   1.136 +
   1.137 +end
   1.138 +