move Lifting/Transfer relevant parts of Library/Quotient_* to Main
authorkuncar
Tue Aug 13 15:59:22 2013 +0200 (2013-08-13)
changeset 53012cb82606b8215
parent 53011 aeee0a4be6cf
child 53013 3fbcfa911863
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Lifting_Option.thy
src/HOL/Lifting_Product.thy
src/HOL/Lifting_Set.thy
src/HOL/Lifting_Sum.thy
src/HOL/List.thy
src/HOL/Main.thy
src/HOL/Rat.thy
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Tue Aug 13 15:59:22 2013 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Tue Aug 13 15:59:22 2013 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  (*  Title:      HOL/Library/Quotient_List.thy
     1.5 -    Author:     Cezary Kaliszyk, Christian Urban and Brian Huffman
     1.6 +    Author:     Cezary Kaliszyk and Christian Urban
     1.7  *)
     1.8  
     1.9  header {* Quotient infrastructure for the list type *}
    1.10 @@ -8,13 +8,13 @@
    1.11  imports Main Quotient_Set Quotient_Product Quotient_Option
    1.12  begin
    1.13  
    1.14 -subsection {* Relator for list type *}
    1.15 +subsection {* Rules for the Quotient package *}
    1.16  
    1.17  lemma map_id [id_simps]:
    1.18    "map id = id"
    1.19    by (fact List.map.id)
    1.20  
    1.21 -lemma list_all2_eq [id_simps, relator_eq]:
    1.22 +lemma list_all2_eq [id_simps]:
    1.23    "list_all2 (op =) = (op =)"
    1.24  proof (rule ext)+
    1.25    fix xs ys
    1.26 @@ -22,66 +22,6 @@
    1.27      by (induct xs ys rule: list_induct2') simp_all
    1.28  qed
    1.29  
    1.30 -lemma list_all2_mono[relator_mono]:
    1.31 -  assumes "A \<le> B"
    1.32 -  shows "(list_all2 A) \<le> (list_all2 B)"
    1.33 -using assms by (auto intro: list_all2_mono)
    1.34 -
    1.35 -lemma list_all2_OO[relator_distr]: "list_all2 A OO list_all2 B = list_all2 (A OO B)"
    1.36 -proof (intro ext iffI)
    1.37 -  fix xs ys
    1.38 -  assume "list_all2 (A OO B) xs ys"
    1.39 -  thus "(list_all2 A OO list_all2 B) xs ys"
    1.40 -    unfolding OO_def
    1.41 -    by (induct, simp, simp add: list_all2_Cons1 list_all2_Cons2, fast)
    1.42 -next
    1.43 -  fix xs ys
    1.44 -  assume "(list_all2 A OO list_all2 B) xs ys"
    1.45 -  then obtain zs where "list_all2 A xs zs" and "list_all2 B zs ys" ..
    1.46 -  thus "list_all2 (A OO B) xs ys"
    1.47 -    by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
    1.48 -qed
    1.49 -
    1.50 -lemma Domainp_list[relator_domain]:
    1.51 -  assumes "Domainp A = P"
    1.52 -  shows "Domainp (list_all2 A) = (list_all P)"
    1.53 -proof -
    1.54 -  {
    1.55 -    fix x
    1.56 -    have *: "\<And>x. (\<exists>y. A x y) = P x" using assms unfolding Domainp_iff by blast
    1.57 -    have "(\<exists>y. (list_all2 A x y)) = list_all P x"
    1.58 -    by (induction x) (simp_all add: * list_all2_Cons1)
    1.59 -  }
    1.60 -  then show ?thesis
    1.61 -  unfolding Domainp_iff[abs_def]
    1.62 -  by (auto iff: fun_eq_iff)
    1.63 -qed 
    1.64 -
    1.65 -lemma reflp_list_all2[reflexivity_rule]:
    1.66 -  assumes "reflp R"
    1.67 -  shows "reflp (list_all2 R)"
    1.68 -proof (rule reflpI)
    1.69 -  from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
    1.70 -  fix xs
    1.71 -  show "list_all2 R xs xs"
    1.72 -    by (induct xs) (simp_all add: *)
    1.73 -qed
    1.74 -
    1.75 -lemma left_total_list_all2[reflexivity_rule]:
    1.76 -  "left_total R \<Longrightarrow> left_total (list_all2 R)"
    1.77 -  unfolding left_total_def
    1.78 -  apply safe
    1.79 -  apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
    1.80 -done
    1.81 -
    1.82 -lemma left_unique_list_all2 [reflexivity_rule]:
    1.83 -  "left_unique R \<Longrightarrow> left_unique (list_all2 R)"
    1.84 -  unfolding left_unique_def
    1.85 -  apply (subst (2) all_comm, subst (1) all_comm)
    1.86 -  apply (rule allI, rename_tac zs, induct_tac zs)
    1.87 -  apply (auto simp add: list_all2_Cons2)
    1.88 -  done
    1.89 -
    1.90  lemma list_symp:
    1.91    assumes "symp R"
    1.92    shows "symp (list_all2 R)"
    1.93 @@ -108,272 +48,6 @@
    1.94    "equivp R \<Longrightarrow> equivp (list_all2 R)"
    1.95    by (blast intro: equivpI reflp_list_all2 list_symp list_transp elim: equivpE)
    1.96  
    1.97 -lemma right_total_list_all2 [transfer_rule]:
    1.98 -  "right_total R \<Longrightarrow> right_total (list_all2 R)"
    1.99 -  unfolding right_total_def
   1.100 -  by (rule allI, induct_tac y, simp, simp add: list_all2_Cons2)
   1.101 -
   1.102 -lemma right_unique_list_all2 [transfer_rule]:
   1.103 -  "right_unique R \<Longrightarrow> right_unique (list_all2 R)"
   1.104 -  unfolding right_unique_def
   1.105 -  apply (rule allI, rename_tac xs, induct_tac xs)
   1.106 -  apply (auto simp add: list_all2_Cons1)
   1.107 -  done
   1.108 -
   1.109 -lemma bi_total_list_all2 [transfer_rule]:
   1.110 -  "bi_total A \<Longrightarrow> bi_total (list_all2 A)"
   1.111 -  unfolding bi_total_def
   1.112 -  apply safe
   1.113 -  apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
   1.114 -  apply (rename_tac ys, induct_tac ys, simp, simp add: list_all2_Cons2)
   1.115 -  done
   1.116 -
   1.117 -lemma bi_unique_list_all2 [transfer_rule]:
   1.118 -  "bi_unique A \<Longrightarrow> bi_unique (list_all2 A)"
   1.119 -  unfolding bi_unique_def
   1.120 -  apply (rule conjI)
   1.121 -  apply (rule allI, rename_tac xs, induct_tac xs)
   1.122 -  apply (simp, force simp add: list_all2_Cons1)
   1.123 -  apply (subst (2) all_comm, subst (1) all_comm)
   1.124 -  apply (rule allI, rename_tac xs, induct_tac xs)
   1.125 -  apply (simp, force simp add: list_all2_Cons2)
   1.126 -  done
   1.127 -
   1.128 -subsection {* Transfer rules for transfer package *}
   1.129 -
   1.130 -lemma Nil_transfer [transfer_rule]: "(list_all2 A) [] []"
   1.131 -  by simp
   1.132 -
   1.133 -lemma Cons_transfer [transfer_rule]:
   1.134 -  "(A ===> list_all2 A ===> list_all2 A) Cons Cons"
   1.135 -  unfolding fun_rel_def by simp
   1.136 -
   1.137 -lemma list_case_transfer [transfer_rule]:
   1.138 -  "(B ===> (A ===> list_all2 A ===> B) ===> list_all2 A ===> B)
   1.139 -    list_case list_case"
   1.140 -  unfolding fun_rel_def by (simp split: list.split)
   1.141 -
   1.142 -lemma list_rec_transfer [transfer_rule]:
   1.143 -  "(B ===> (A ===> list_all2 A ===> B ===> B) ===> list_all2 A ===> B)
   1.144 -    list_rec list_rec"
   1.145 -  unfolding fun_rel_def by (clarify, erule list_all2_induct, simp_all)
   1.146 -
   1.147 -lemma tl_transfer [transfer_rule]:
   1.148 -  "(list_all2 A ===> list_all2 A) tl tl"
   1.149 -  unfolding tl_def by transfer_prover
   1.150 -
   1.151 -lemma butlast_transfer [transfer_rule]:
   1.152 -  "(list_all2 A ===> list_all2 A) butlast butlast"
   1.153 -  by (rule fun_relI, erule list_all2_induct, auto)
   1.154 -
   1.155 -lemma set_transfer [transfer_rule]:
   1.156 -  "(list_all2 A ===> set_rel A) set set"
   1.157 -  unfolding set_def by transfer_prover
   1.158 -
   1.159 -lemma map_transfer [transfer_rule]:
   1.160 -  "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"
   1.161 -  unfolding List.map_def by transfer_prover
   1.162 -
   1.163 -lemma append_transfer [transfer_rule]:
   1.164 -  "(list_all2 A ===> list_all2 A ===> list_all2 A) append append"
   1.165 -  unfolding List.append_def by transfer_prover
   1.166 -
   1.167 -lemma rev_transfer [transfer_rule]:
   1.168 -  "(list_all2 A ===> list_all2 A) rev rev"
   1.169 -  unfolding List.rev_def by transfer_prover
   1.170 -
   1.171 -lemma filter_transfer [transfer_rule]:
   1.172 -  "((A ===> op =) ===> list_all2 A ===> list_all2 A) filter filter"
   1.173 -  unfolding List.filter_def by transfer_prover
   1.174 -
   1.175 -lemma fold_transfer [transfer_rule]:
   1.176 -  "((A ===> B ===> B) ===> list_all2 A ===> B ===> B) fold fold"
   1.177 -  unfolding List.fold_def by transfer_prover
   1.178 -
   1.179 -lemma foldr_transfer [transfer_rule]:
   1.180 -  "((A ===> B ===> B) ===> list_all2 A ===> B ===> B) foldr foldr"
   1.181 -  unfolding List.foldr_def by transfer_prover
   1.182 -
   1.183 -lemma foldl_transfer [transfer_rule]:
   1.184 -  "((B ===> A ===> B) ===> B ===> list_all2 A ===> B) foldl foldl"
   1.185 -  unfolding List.foldl_def by transfer_prover
   1.186 -
   1.187 -lemma concat_transfer [transfer_rule]:
   1.188 -  "(list_all2 (list_all2 A) ===> list_all2 A) concat concat"
   1.189 -  unfolding List.concat_def by transfer_prover
   1.190 -
   1.191 -lemma drop_transfer [transfer_rule]:
   1.192 -  "(op = ===> list_all2 A ===> list_all2 A) drop drop"
   1.193 -  unfolding List.drop_def by transfer_prover
   1.194 -
   1.195 -lemma take_transfer [transfer_rule]:
   1.196 -  "(op = ===> list_all2 A ===> list_all2 A) take take"
   1.197 -  unfolding List.take_def by transfer_prover
   1.198 -
   1.199 -lemma list_update_transfer [transfer_rule]:
   1.200 -  "(list_all2 A ===> op = ===> A ===> list_all2 A) list_update list_update"
   1.201 -  unfolding list_update_def by transfer_prover
   1.202 -
   1.203 -lemma takeWhile_transfer [transfer_rule]:
   1.204 -  "((A ===> op =) ===> list_all2 A ===> list_all2 A) takeWhile takeWhile"
   1.205 -  unfolding takeWhile_def by transfer_prover
   1.206 -
   1.207 -lemma dropWhile_transfer [transfer_rule]:
   1.208 -  "((A ===> op =) ===> list_all2 A ===> list_all2 A) dropWhile dropWhile"
   1.209 -  unfolding dropWhile_def by transfer_prover
   1.210 -
   1.211 -lemma zip_transfer [transfer_rule]:
   1.212 -  "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) zip zip"
   1.213 -  unfolding zip_def by transfer_prover
   1.214 -
   1.215 -lemma insert_transfer [transfer_rule]:
   1.216 -  assumes [transfer_rule]: "bi_unique A"
   1.217 -  shows "(A ===> list_all2 A ===> list_all2 A) List.insert List.insert"
   1.218 -  unfolding List.insert_def [abs_def] by transfer_prover
   1.219 -
   1.220 -lemma find_transfer [transfer_rule]:
   1.221 -  "((A ===> op =) ===> list_all2 A ===> option_rel A) List.find List.find"
   1.222 -  unfolding List.find_def by transfer_prover
   1.223 -
   1.224 -lemma remove1_transfer [transfer_rule]:
   1.225 -  assumes [transfer_rule]: "bi_unique A"
   1.226 -  shows "(A ===> list_all2 A ===> list_all2 A) remove1 remove1"
   1.227 -  unfolding remove1_def by transfer_prover
   1.228 -
   1.229 -lemma removeAll_transfer [transfer_rule]:
   1.230 -  assumes [transfer_rule]: "bi_unique A"
   1.231 -  shows "(A ===> list_all2 A ===> list_all2 A) removeAll removeAll"
   1.232 -  unfolding removeAll_def by transfer_prover
   1.233 -
   1.234 -lemma distinct_transfer [transfer_rule]:
   1.235 -  assumes [transfer_rule]: "bi_unique A"
   1.236 -  shows "(list_all2 A ===> op =) distinct distinct"
   1.237 -  unfolding distinct_def by transfer_prover
   1.238 -
   1.239 -lemma remdups_transfer [transfer_rule]:
   1.240 -  assumes [transfer_rule]: "bi_unique A"
   1.241 -  shows "(list_all2 A ===> list_all2 A) remdups remdups"
   1.242 -  unfolding remdups_def by transfer_prover
   1.243 -
   1.244 -lemma replicate_transfer [transfer_rule]:
   1.245 -  "(op = ===> A ===> list_all2 A) replicate replicate"
   1.246 -  unfolding replicate_def by transfer_prover
   1.247 -
   1.248 -lemma length_transfer [transfer_rule]:
   1.249 -  "(list_all2 A ===> op =) length length"
   1.250 -  unfolding list_size_overloaded_def by transfer_prover
   1.251 -
   1.252 -lemma rotate1_transfer [transfer_rule]:
   1.253 -  "(list_all2 A ===> list_all2 A) rotate1 rotate1"
   1.254 -  unfolding rotate1_def by transfer_prover
   1.255 -
   1.256 -lemma funpow_transfer [transfer_rule]: (* FIXME: move to Transfer.thy *)
   1.257 -  "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
   1.258 -  unfolding funpow_def by transfer_prover
   1.259 -
   1.260 -lemma rotate_transfer [transfer_rule]:
   1.261 -  "(op = ===> list_all2 A ===> list_all2 A) rotate rotate"
   1.262 -  unfolding rotate_def [abs_def] by transfer_prover
   1.263 -
   1.264 -lemma list_all2_transfer [transfer_rule]:
   1.265 -  "((A ===> B ===> op =) ===> list_all2 A ===> list_all2 B ===> op =)
   1.266 -    list_all2 list_all2"
   1.267 -  apply (subst (4) list_all2_def [abs_def])
   1.268 -  apply (subst (3) list_all2_def [abs_def])
   1.269 -  apply transfer_prover
   1.270 -  done
   1.271 -
   1.272 -lemma sublist_transfer [transfer_rule]:
   1.273 -  "(list_all2 A ===> set_rel (op =) ===> list_all2 A) sublist sublist"
   1.274 -  unfolding sublist_def [abs_def] by transfer_prover
   1.275 -
   1.276 -lemma partition_transfer [transfer_rule]:
   1.277 -  "((A ===> op =) ===> list_all2 A ===> prod_rel (list_all2 A) (list_all2 A))
   1.278 -    partition partition"
   1.279 -  unfolding partition_def by transfer_prover
   1.280 -
   1.281 -lemma lists_transfer [transfer_rule]:
   1.282 -  "(set_rel A ===> set_rel (list_all2 A)) lists lists"
   1.283 -  apply (rule fun_relI, rule set_relI)
   1.284 -  apply (erule lists.induct, simp)
   1.285 -  apply (simp only: set_rel_def list_all2_Cons1, metis lists.Cons)
   1.286 -  apply (erule lists.induct, simp)
   1.287 -  apply (simp only: set_rel_def list_all2_Cons2, metis lists.Cons)
   1.288 -  done
   1.289 -
   1.290 -lemma set_Cons_transfer [transfer_rule]:
   1.291 -  "(set_rel A ===> set_rel (list_all2 A) ===> set_rel (list_all2 A))
   1.292 -    set_Cons set_Cons"
   1.293 -  unfolding fun_rel_def set_rel_def set_Cons_def
   1.294 -  apply safe
   1.295 -  apply (simp add: list_all2_Cons1, fast)
   1.296 -  apply (simp add: list_all2_Cons2, fast)
   1.297 -  done
   1.298 -
   1.299 -lemma listset_transfer [transfer_rule]:
   1.300 -  "(list_all2 (set_rel A) ===> set_rel (list_all2 A)) listset listset"
   1.301 -  unfolding listset_def by transfer_prover
   1.302 -
   1.303 -lemma null_transfer [transfer_rule]:
   1.304 -  "(list_all2 A ===> op =) List.null List.null"
   1.305 -  unfolding fun_rel_def List.null_def by auto
   1.306 -
   1.307 -lemma list_all_transfer [transfer_rule]:
   1.308 -  "((A ===> op =) ===> list_all2 A ===> op =) list_all list_all"
   1.309 -  unfolding list_all_iff [abs_def] by transfer_prover
   1.310 -
   1.311 -lemma list_ex_transfer [transfer_rule]:
   1.312 -  "((A ===> op =) ===> list_all2 A ===> op =) list_ex list_ex"
   1.313 -  unfolding list_ex_iff [abs_def] by transfer_prover
   1.314 -
   1.315 -lemma splice_transfer [transfer_rule]:
   1.316 -  "(list_all2 A ===> list_all2 A ===> list_all2 A) splice splice"
   1.317 -  apply (rule fun_relI, erule list_all2_induct, simp add: fun_rel_def, simp)
   1.318 -  apply (rule fun_relI)
   1.319 -  apply (erule_tac xs=x in list_all2_induct, simp, simp add: fun_rel_def)
   1.320 -  done
   1.321 -
   1.322 -lemma listsum_transfer[transfer_rule]:
   1.323 -  assumes [transfer_rule]: "A 0 0"
   1.324 -  assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
   1.325 -  shows "(list_all2 A ===> A) listsum listsum"
   1.326 -  unfolding listsum_def[abs_def]
   1.327 -  by transfer_prover
   1.328 -
   1.329 -subsection {* Setup for lifting package *}
   1.330 -
   1.331 -lemma Quotient_list[quot_map]:
   1.332 -  assumes "Quotient R Abs Rep T"
   1.333 -  shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"
   1.334 -proof (unfold Quotient_alt_def, intro conjI allI impI)
   1.335 -  from assms have 1: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
   1.336 -    unfolding Quotient_alt_def by simp
   1.337 -  fix xs ys assume "list_all2 T xs ys" thus "map Abs xs = ys"
   1.338 -    by (induct, simp, simp add: 1)
   1.339 -next
   1.340 -  from assms have 2: "\<And>x. T (Rep x) x"
   1.341 -    unfolding Quotient_alt_def by simp
   1.342 -  fix xs show "list_all2 T (map Rep xs) xs"
   1.343 -    by (induct xs, simp, simp add: 2)
   1.344 -next
   1.345 -  from assms have 3: "\<And>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y"
   1.346 -    unfolding Quotient_alt_def by simp
   1.347 -  fix xs ys show "list_all2 R xs ys \<longleftrightarrow> list_all2 T xs (map Abs xs) \<and>
   1.348 -    list_all2 T ys (map Abs ys) \<and> map Abs xs = map Abs ys"
   1.349 -    by (induct xs ys rule: list_induct2', simp_all, metis 3)
   1.350 -qed
   1.351 -
   1.352 -lemma list_invariant_commute [invariant_commute]:
   1.353 -  "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
   1.354 -  apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def) 
   1.355 -  apply (intro allI) 
   1.356 -  apply (induct_tac rule: list_induct2') 
   1.357 -  apply simp_all 
   1.358 -  apply metis
   1.359 -done
   1.360 -
   1.361 -subsection {* Rules for quotient package *}
   1.362 -
   1.363  lemma list_quotient3 [quot_thm]:
   1.364    assumes "Quotient3 R Abs Rep"
   1.365    shows "Quotient3 (list_all2 R) (map Abs) (map Rep)"
     2.1 --- a/src/HOL/Library/Quotient_Option.thy	Tue Aug 13 15:59:22 2013 +0200
     2.2 +++ b/src/HOL/Library/Quotient_Option.thy	Tue Aug 13 15:59:22 2013 +0200
     2.3 @@ -1,5 +1,5 @@
     2.4  (*  Title:      HOL/Library/Quotient_Option.thy
     2.5 -    Author:     Cezary Kaliszyk, Christian Urban and Brian Huffman
     2.6 +    Author:     Cezary Kaliszyk and Christian Urban
     2.7  *)
     2.8  
     2.9  header {* Quotient infrastructure for the option type *}
    2.10 @@ -8,31 +8,7 @@
    2.11  imports Main Quotient_Syntax
    2.12  begin
    2.13  
    2.14 -subsection {* Relator for option type *}
    2.15 -
    2.16 -fun
    2.17 -  option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
    2.18 -where
    2.19 -  "option_rel R None None = True"
    2.20 -| "option_rel R (Some x) None = False"
    2.21 -| "option_rel R None (Some x) = False"
    2.22 -| "option_rel R (Some x) (Some y) = R x y"
    2.23 -
    2.24 -lemma option_rel_unfold:
    2.25 -  "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
    2.26 -    | (Some x, Some y) \<Rightarrow> R x y
    2.27 -    | _ \<Rightarrow> False)"
    2.28 -  by (cases x) (cases y, simp_all)+
    2.29 -
    2.30 -fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
    2.31 -where
    2.32 -  "option_pred R None = True"
    2.33 -| "option_pred R (Some x) = R x"
    2.34 -
    2.35 -lemma option_pred_unfold:
    2.36 -  "option_pred P x = (case x of None \<Rightarrow> True
    2.37 -    | Some x \<Rightarrow> P x)"
    2.38 -by (cases x) simp_all
    2.39 +subsection {* Rules for the Quotient package *}
    2.40  
    2.41  lemma option_rel_map1:
    2.42    "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
    2.43 @@ -46,37 +22,10 @@
    2.44    "Option.map id = id"
    2.45    by (simp add: id_def Option.map.identity fun_eq_iff)
    2.46  
    2.47 -lemma option_rel_eq [id_simps, relator_eq]:
    2.48 +lemma option_rel_eq [id_simps]:
    2.49    "option_rel (op =) = (op =)"
    2.50    by (simp add: option_rel_unfold fun_eq_iff split: option.split)
    2.51  
    2.52 -lemma option_rel_mono[relator_mono]:
    2.53 -  assumes "A \<le> B"
    2.54 -  shows "(option_rel A) \<le> (option_rel B)"
    2.55 -using assms by (auto simp: option_rel_unfold split: option.splits)
    2.56 -
    2.57 -lemma option_rel_OO[relator_distr]:
    2.58 -  "(option_rel A) OO (option_rel B) = option_rel (A OO B)"
    2.59 -by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split)
    2.60 -
    2.61 -lemma Domainp_option[relator_domain]:
    2.62 -  assumes "Domainp A = P"
    2.63 -  shows "Domainp (option_rel A) = (option_pred P)"
    2.64 -using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def]
    2.65 -by (auto iff: fun_eq_iff split: option.split)
    2.66 -
    2.67 -lemma reflp_option_rel[reflexivity_rule]:
    2.68 -  "reflp R \<Longrightarrow> reflp (option_rel R)"
    2.69 -  unfolding reflp_def split_option_all by simp
    2.70 -
    2.71 -lemma left_total_option_rel[reflexivity_rule]:
    2.72 -  "left_total R \<Longrightarrow> left_total (option_rel R)"
    2.73 -  unfolding left_total_def split_option_all split_option_ex by simp
    2.74 -
    2.75 -lemma left_unique_option_rel [reflexivity_rule]:
    2.76 -  "left_unique R \<Longrightarrow> left_unique (option_rel R)"
    2.77 -  unfolding left_unique_def split_option_all by simp
    2.78 -
    2.79  lemma option_symp:
    2.80    "symp R \<Longrightarrow> symp (option_rel R)"
    2.81    unfolding symp_def split_option_all option_rel.simps by fast
    2.82 @@ -89,65 +38,6 @@
    2.83    "equivp R \<Longrightarrow> equivp (option_rel R)"
    2.84    by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE)
    2.85  
    2.86 -lemma right_total_option_rel [transfer_rule]:
    2.87 -  "right_total R \<Longrightarrow> right_total (option_rel R)"
    2.88 -  unfolding right_total_def split_option_all split_option_ex by simp
    2.89 -
    2.90 -lemma right_unique_option_rel [transfer_rule]:
    2.91 -  "right_unique R \<Longrightarrow> right_unique (option_rel R)"
    2.92 -  unfolding right_unique_def split_option_all by simp
    2.93 -
    2.94 -lemma bi_total_option_rel [transfer_rule]:
    2.95 -  "bi_total R \<Longrightarrow> bi_total (option_rel R)"
    2.96 -  unfolding bi_total_def split_option_all split_option_ex by simp
    2.97 -
    2.98 -lemma bi_unique_option_rel [transfer_rule]:
    2.99 -  "bi_unique R \<Longrightarrow> bi_unique (option_rel R)"
   2.100 -  unfolding bi_unique_def split_option_all by simp
   2.101 -
   2.102 -subsection {* Transfer rules for transfer package *}
   2.103 -
   2.104 -lemma None_transfer [transfer_rule]: "(option_rel A) None None"
   2.105 -  by simp
   2.106 -
   2.107 -lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some"
   2.108 -  unfolding fun_rel_def by simp
   2.109 -
   2.110 -lemma option_case_transfer [transfer_rule]:
   2.111 -  "(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case"
   2.112 -  unfolding fun_rel_def split_option_all by simp
   2.113 -
   2.114 -lemma option_map_transfer [transfer_rule]:
   2.115 -  "((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map"
   2.116 -  unfolding Option.map_def by transfer_prover
   2.117 -
   2.118 -lemma option_bind_transfer [transfer_rule]:
   2.119 -  "(option_rel A ===> (A ===> option_rel B) ===> option_rel B)
   2.120 -    Option.bind Option.bind"
   2.121 -  unfolding fun_rel_def split_option_all by simp
   2.122 -
   2.123 -subsection {* Setup for lifting package *}
   2.124 -
   2.125 -lemma Quotient_option[quot_map]:
   2.126 -  assumes "Quotient R Abs Rep T"
   2.127 -  shows "Quotient (option_rel R) (Option.map Abs)
   2.128 -    (Option.map Rep) (option_rel T)"
   2.129 -  using assms unfolding Quotient_alt_def option_rel_unfold
   2.130 -  by (simp split: option.split)
   2.131 -
   2.132 -lemma option_invariant_commute [invariant_commute]:
   2.133 -  "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)"
   2.134 -  apply (simp add: fun_eq_iff Lifting.invariant_def)
   2.135 -  apply (intro allI) 
   2.136 -  apply (case_tac x rule: option.exhaust)
   2.137 -  apply (case_tac xa rule: option.exhaust)
   2.138 -  apply auto[2]
   2.139 -  apply (case_tac xa rule: option.exhaust)
   2.140 -  apply auto
   2.141 -done
   2.142 -
   2.143 -subsection {* Rules for quotient package *}
   2.144 -
   2.145  lemma option_quotient [quot_thm]:
   2.146    assumes "Quotient3 R Abs Rep"
   2.147    shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)"
     3.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Aug 13 15:59:22 2013 +0200
     3.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Aug 13 15:59:22 2013 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4  (*  Title:      HOL/Library/Quotient_Product.thy
     3.5 -    Author:     Cezary Kaliszyk, Christian Urban and Brian Huffman
     3.6 +    Author:     Cezary Kaliszyk and Christian Urban
     3.7  *)
     3.8  
     3.9  header {* Quotient infrastructure for the product type *}
    3.10 @@ -8,137 +8,22 @@
    3.11  imports Main Quotient_Syntax
    3.12  begin
    3.13  
    3.14 -subsection {* Relator for product type *}
    3.15 -
    3.16 -definition
    3.17 -  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
    3.18 -where
    3.19 -  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    3.20 -
    3.21 -definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    3.22 -where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
    3.23 -
    3.24 -lemma prod_rel_apply [simp]:
    3.25 -  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    3.26 -  by (simp add: prod_rel_def)
    3.27 -
    3.28 -lemma prod_pred_apply [simp]:
    3.29 -  "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
    3.30 -  by (simp add: prod_pred_def)
    3.31 +subsection {* Rules for the Quotient package *}
    3.32  
    3.33  lemma map_pair_id [id_simps]:
    3.34    shows "map_pair id id = id"
    3.35    by (simp add: fun_eq_iff)
    3.36  
    3.37 -lemma prod_rel_eq [id_simps, relator_eq]:
    3.38 +lemma prod_rel_eq [id_simps]:
    3.39    shows "prod_rel (op =) (op =) = (op =)"
    3.40    by (simp add: fun_eq_iff)
    3.41  
    3.42 -lemma prod_rel_mono[relator_mono]:
    3.43 -  assumes "A \<le> C"
    3.44 -  assumes "B \<le> D"
    3.45 -  shows "(prod_rel A B) \<le> (prod_rel C D)"
    3.46 -using assms by (auto simp: prod_rel_def)
    3.47 -
    3.48 -lemma prod_rel_OO[relator_distr]:
    3.49 -  "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
    3.50 -by (rule ext)+ (auto simp: prod_rel_def OO_def)
    3.51 -
    3.52 -lemma Domainp_prod[relator_domain]:
    3.53 -  assumes "Domainp T1 = P1"
    3.54 -  assumes "Domainp T2 = P2"
    3.55 -  shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
    3.56 -using assms unfolding prod_rel_def prod_pred_def by blast
    3.57 -
    3.58 -lemma reflp_prod_rel [reflexivity_rule]:
    3.59 -  assumes "reflp R1"
    3.60 -  assumes "reflp R2"
    3.61 -  shows "reflp (prod_rel R1 R2)"
    3.62 -using assms by (auto intro!: reflpI elim: reflpE)
    3.63 -
    3.64 -lemma left_total_prod_rel [reflexivity_rule]:
    3.65 -  assumes "left_total R1"
    3.66 -  assumes "left_total R2"
    3.67 -  shows "left_total (prod_rel R1 R2)"
    3.68 -  using assms unfolding left_total_def prod_rel_def by auto
    3.69 -
    3.70 -lemma left_unique_prod_rel [reflexivity_rule]:
    3.71 -  assumes "left_unique R1" and "left_unique R2"
    3.72 -  shows "left_unique (prod_rel R1 R2)"
    3.73 -  using assms unfolding left_unique_def prod_rel_def by auto
    3.74 -
    3.75  lemma prod_equivp [quot_equiv]:
    3.76    assumes "equivp R1"
    3.77    assumes "equivp R2"
    3.78    shows "equivp (prod_rel R1 R2)"
    3.79    using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
    3.80  
    3.81 -lemma right_total_prod_rel [transfer_rule]:
    3.82 -  assumes "right_total R1" and "right_total R2"
    3.83 -  shows "right_total (prod_rel R1 R2)"
    3.84 -  using assms unfolding right_total_def prod_rel_def by auto
    3.85 -
    3.86 -lemma right_unique_prod_rel [transfer_rule]:
    3.87 -  assumes "right_unique R1" and "right_unique R2"
    3.88 -  shows "right_unique (prod_rel R1 R2)"
    3.89 -  using assms unfolding right_unique_def prod_rel_def by auto
    3.90 -
    3.91 -lemma bi_total_prod_rel [transfer_rule]:
    3.92 -  assumes "bi_total R1" and "bi_total R2"
    3.93 -  shows "bi_total (prod_rel R1 R2)"
    3.94 -  using assms unfolding bi_total_def prod_rel_def by auto
    3.95 -
    3.96 -lemma bi_unique_prod_rel [transfer_rule]:
    3.97 -  assumes "bi_unique R1" and "bi_unique R2"
    3.98 -  shows "bi_unique (prod_rel R1 R2)"
    3.99 -  using assms unfolding bi_unique_def prod_rel_def by auto
   3.100 -
   3.101 -subsection {* Transfer rules for transfer package *}
   3.102 -
   3.103 -lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
   3.104 -  unfolding fun_rel_def prod_rel_def by simp
   3.105 -
   3.106 -lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst"
   3.107 -  unfolding fun_rel_def prod_rel_def by simp
   3.108 -
   3.109 -lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
   3.110 -  unfolding fun_rel_def prod_rel_def by simp
   3.111 -
   3.112 -lemma prod_case_transfer [transfer_rule]:
   3.113 -  "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case"
   3.114 -  unfolding fun_rel_def prod_rel_def by simp
   3.115 -
   3.116 -lemma curry_transfer [transfer_rule]:
   3.117 -  "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
   3.118 -  unfolding curry_def by transfer_prover
   3.119 -
   3.120 -lemma map_pair_transfer [transfer_rule]:
   3.121 -  "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
   3.122 -    map_pair map_pair"
   3.123 -  unfolding map_pair_def [abs_def] by transfer_prover
   3.124 -
   3.125 -lemma prod_rel_transfer [transfer_rule]:
   3.126 -  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
   3.127 -    prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel"
   3.128 -  unfolding fun_rel_def by auto
   3.129 -
   3.130 -subsection {* Setup for lifting package *}
   3.131 -
   3.132 -lemma Quotient_prod[quot_map]:
   3.133 -  assumes "Quotient R1 Abs1 Rep1 T1"
   3.134 -  assumes "Quotient R2 Abs2 Rep2 T2"
   3.135 -  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2)
   3.136 -    (map_pair Rep1 Rep2) (prod_rel T1 T2)"
   3.137 -  using assms unfolding Quotient_alt_def by auto
   3.138 -
   3.139 -lemma prod_invariant_commute [invariant_commute]: 
   3.140 -  "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
   3.141 -  apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) 
   3.142 -  apply blast
   3.143 -done
   3.144 -
   3.145 -subsection {* Rules for quotient package *}
   3.146 -
   3.147  lemma prod_quotient [quot_thm]:
   3.148    assumes "Quotient3 R1 Abs1 Rep1"
   3.149    assumes "Quotient3 R2 Abs2 Rep2"
     4.1 --- a/src/HOL/Library/Quotient_Set.thy	Tue Aug 13 15:59:22 2013 +0200
     4.2 +++ b/src/HOL/Library/Quotient_Set.thy	Tue Aug 13 15:59:22 2013 +0200
     4.3 @@ -8,273 +8,7 @@
     4.4  imports Main Quotient_Syntax
     4.5  begin
     4.6  
     4.7 -subsection {* Relator for set type *}
     4.8 -
     4.9 -definition set_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
    4.10 -  where "set_rel R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))"
    4.11 -
    4.12 -lemma set_relI:
    4.13 -  assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y"
    4.14 -  assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y"
    4.15 -  shows "set_rel R A B"
    4.16 -  using assms unfolding set_rel_def by simp
    4.17 -
    4.18 -lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
    4.19 -  unfolding set_rel_def by auto
    4.20 -
    4.21 -lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
    4.22 -  unfolding set_rel_def fun_eq_iff by auto
    4.23 -
    4.24 -lemma set_rel_mono[relator_mono]:
    4.25 -  assumes "A \<le> B"
    4.26 -  shows "set_rel A \<le> set_rel B"
    4.27 -using assms unfolding set_rel_def by blast
    4.28 -
    4.29 -lemma set_rel_OO[relator_distr]: "set_rel R OO set_rel S = set_rel (R OO S)"
    4.30 -  apply (rule sym)
    4.31 -  apply (intro ext, rename_tac X Z)
    4.32 -  apply (rule iffI)
    4.33 -  apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI)
    4.34 -  apply (simp add: set_rel_def, fast)
    4.35 -  apply (simp add: set_rel_def, fast)
    4.36 -  apply (simp add: set_rel_def, fast)
    4.37 -  done
    4.38 -
    4.39 -lemma Domainp_set[relator_domain]:
    4.40 -  assumes "Domainp T = R"
    4.41 -  shows "Domainp (set_rel T) = (\<lambda>A. Ball A R)"
    4.42 -using assms unfolding set_rel_def Domainp_iff[abs_def]
    4.43 -apply (intro ext)
    4.44 -apply (rule iffI) 
    4.45 -apply blast
    4.46 -apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
    4.47 -done
    4.48 -
    4.49 -lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
    4.50 -  unfolding reflp_def set_rel_def by fast
    4.51 -
    4.52 -lemma left_total_set_rel[reflexivity_rule]: 
    4.53 -  "left_total A \<Longrightarrow> left_total (set_rel A)"
    4.54 -  unfolding left_total_def set_rel_def
    4.55 -  apply safe
    4.56 -  apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
    4.57 -done
    4.58 -
    4.59 -lemma left_unique_set_rel[reflexivity_rule]: 
    4.60 -  "left_unique A \<Longrightarrow> left_unique (set_rel A)"
    4.61 -  unfolding left_unique_def set_rel_def
    4.62 -  by fast
    4.63 -
    4.64 -lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
    4.65 -  unfolding symp_def set_rel_def by fast
    4.66 -
    4.67 -lemma transp_set_rel: "transp R \<Longrightarrow> transp (set_rel R)"
    4.68 -  unfolding transp_def set_rel_def by fast
    4.69 -
    4.70 -lemma equivp_set_rel: "equivp R \<Longrightarrow> equivp (set_rel R)"
    4.71 -  by (blast intro: equivpI reflp_set_rel symp_set_rel transp_set_rel
    4.72 -    elim: equivpE)
    4.73 -
    4.74 -lemma right_total_set_rel [transfer_rule]:
    4.75 -  "right_total A \<Longrightarrow> right_total (set_rel A)"
    4.76 -  unfolding right_total_def set_rel_def
    4.77 -  by (rule allI, rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
    4.78 -
    4.79 -lemma right_unique_set_rel [transfer_rule]:
    4.80 -  "right_unique A \<Longrightarrow> right_unique (set_rel A)"
    4.81 -  unfolding right_unique_def set_rel_def by fast
    4.82 -
    4.83 -lemma bi_total_set_rel [transfer_rule]:
    4.84 -  "bi_total A \<Longrightarrow> bi_total (set_rel A)"
    4.85 -  unfolding bi_total_def set_rel_def
    4.86 -  apply safe
    4.87 -  apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
    4.88 -  apply (rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
    4.89 -  done
    4.90 -
    4.91 -lemma bi_unique_set_rel [transfer_rule]:
    4.92 -  "bi_unique A \<Longrightarrow> bi_unique (set_rel A)"
    4.93 -  unfolding bi_unique_def set_rel_def by fast
    4.94 -
    4.95 -subsection {* Transfer rules for transfer package *}
    4.96 -
    4.97 -subsubsection {* Unconditional transfer rules *}
    4.98 -
    4.99 -lemma empty_transfer [transfer_rule]: "(set_rel A) {} {}"
   4.100 -  unfolding set_rel_def by simp
   4.101 -
   4.102 -lemma insert_transfer [transfer_rule]:
   4.103 -  "(A ===> set_rel A ===> set_rel A) insert insert"
   4.104 -  unfolding fun_rel_def set_rel_def by auto
   4.105 -
   4.106 -lemma union_transfer [transfer_rule]:
   4.107 -  "(set_rel A ===> set_rel A ===> set_rel A) union union"
   4.108 -  unfolding fun_rel_def set_rel_def by auto
   4.109 -
   4.110 -lemma Union_transfer [transfer_rule]:
   4.111 -  "(set_rel (set_rel A) ===> set_rel A) Union Union"
   4.112 -  unfolding fun_rel_def set_rel_def by simp fast
   4.113 -
   4.114 -lemma image_transfer [transfer_rule]:
   4.115 -  "((A ===> B) ===> set_rel A ===> set_rel B) image image"
   4.116 -  unfolding fun_rel_def set_rel_def by simp fast
   4.117 -
   4.118 -lemma UNION_transfer [transfer_rule]:
   4.119 -  "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) UNION UNION"
   4.120 -  unfolding SUP_def [abs_def] by transfer_prover
   4.121 -
   4.122 -lemma Ball_transfer [transfer_rule]:
   4.123 -  "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball"
   4.124 -  unfolding set_rel_def fun_rel_def by fast
   4.125 -
   4.126 -lemma Bex_transfer [transfer_rule]:
   4.127 -  "(set_rel A ===> (A ===> op =) ===> op =) Bex Bex"
   4.128 -  unfolding set_rel_def fun_rel_def by fast
   4.129 -
   4.130 -lemma Pow_transfer [transfer_rule]:
   4.131 -  "(set_rel A ===> set_rel (set_rel A)) Pow Pow"
   4.132 -  apply (rule fun_relI, rename_tac X Y, rule set_relI)
   4.133 -  apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp)
   4.134 -  apply (simp add: set_rel_def, fast)
   4.135 -  apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp)
   4.136 -  apply (simp add: set_rel_def, fast)
   4.137 -  done
   4.138 -
   4.139 -lemma set_rel_transfer [transfer_rule]:
   4.140 -  "((A ===> B ===> op =) ===> set_rel A ===> set_rel B ===> op =)
   4.141 -    set_rel set_rel"
   4.142 -  unfolding fun_rel_def set_rel_def by fast
   4.143 -
   4.144 -
   4.145 -subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
   4.146 -
   4.147 -lemma member_transfer [transfer_rule]:
   4.148 -  assumes "bi_unique A"
   4.149 -  shows "(A ===> set_rel A ===> op =) (op \<in>) (op \<in>)"
   4.150 -  using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
   4.151 -
   4.152 -lemma right_total_Collect_transfer[transfer_rule]:
   4.153 -  assumes "right_total A"
   4.154 -  shows "((A ===> op =) ===> set_rel A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect"
   4.155 -  using assms unfolding right_total_def set_rel_def fun_rel_def Domainp_iff by fast
   4.156 -
   4.157 -lemma Collect_transfer [transfer_rule]:
   4.158 -  assumes "bi_total A"
   4.159 -  shows "((A ===> op =) ===> set_rel A) Collect Collect"
   4.160 -  using assms unfolding fun_rel_def set_rel_def bi_total_def by fast
   4.161 -
   4.162 -lemma inter_transfer [transfer_rule]:
   4.163 -  assumes "bi_unique A"
   4.164 -  shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter"
   4.165 -  using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
   4.166 -
   4.167 -lemma Diff_transfer [transfer_rule]:
   4.168 -  assumes "bi_unique A"
   4.169 -  shows "(set_rel A ===> set_rel A ===> set_rel A) (op -) (op -)"
   4.170 -  using assms unfolding fun_rel_def set_rel_def bi_unique_def
   4.171 -  unfolding Ball_def Bex_def Diff_eq
   4.172 -  by (safe, simp, metis, simp, metis)
   4.173 -
   4.174 -lemma subset_transfer [transfer_rule]:
   4.175 -  assumes [transfer_rule]: "bi_unique A"
   4.176 -  shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)"
   4.177 -  unfolding subset_eq [abs_def] by transfer_prover
   4.178 -
   4.179 -lemma right_total_UNIV_transfer[transfer_rule]: 
   4.180 -  assumes "right_total A"
   4.181 -  shows "(set_rel A) (Collect (Domainp A)) UNIV"
   4.182 -  using assms unfolding right_total_def set_rel_def Domainp_iff by blast
   4.183 -
   4.184 -lemma UNIV_transfer [transfer_rule]:
   4.185 -  assumes "bi_total A"
   4.186 -  shows "(set_rel A) UNIV UNIV"
   4.187 -  using assms unfolding set_rel_def bi_total_def by simp
   4.188 -
   4.189 -lemma right_total_Compl_transfer [transfer_rule]:
   4.190 -  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
   4.191 -  shows "(set_rel A ===> set_rel A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus"
   4.192 -  unfolding Compl_eq [abs_def]
   4.193 -  by (subst Collect_conj_eq[symmetric]) transfer_prover
   4.194 -
   4.195 -lemma Compl_transfer [transfer_rule]:
   4.196 -  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
   4.197 -  shows "(set_rel A ===> set_rel A) uminus uminus"
   4.198 -  unfolding Compl_eq [abs_def] by transfer_prover
   4.199 -
   4.200 -lemma right_total_Inter_transfer [transfer_rule]:
   4.201 -  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
   4.202 -  shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter"
   4.203 -  unfolding Inter_eq[abs_def]
   4.204 -  by (subst Collect_conj_eq[symmetric]) transfer_prover
   4.205 -
   4.206 -lemma Inter_transfer [transfer_rule]:
   4.207 -  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
   4.208 -  shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter"
   4.209 -  unfolding Inter_eq [abs_def] by transfer_prover
   4.210 -
   4.211 -lemma filter_transfer [transfer_rule]:
   4.212 -  assumes [transfer_rule]: "bi_unique A"
   4.213 -  shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter"
   4.214 -  unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast
   4.215 -
   4.216 -lemma bi_unique_set_rel_lemma:
   4.217 -  assumes "bi_unique R" and "set_rel R X Y"
   4.218 -  obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)"
   4.219 -proof
   4.220 -  let ?f = "\<lambda>x. THE y. R x y"
   4.221 -  from assms show f: "\<forall>x\<in>X. R x (?f x)"
   4.222 -    apply (clarsimp simp add: set_rel_def)
   4.223 -    apply (drule (1) bspec, clarify)
   4.224 -    apply (rule theI2, assumption)
   4.225 -    apply (simp add: bi_unique_def)
   4.226 -    apply assumption
   4.227 -    done
   4.228 -  from assms show "Y = image ?f X"
   4.229 -    apply safe
   4.230 -    apply (clarsimp simp add: set_rel_def)
   4.231 -    apply (drule (1) bspec, clarify)
   4.232 -    apply (rule image_eqI)
   4.233 -    apply (rule the_equality [symmetric], assumption)
   4.234 -    apply (simp add: bi_unique_def)
   4.235 -    apply assumption
   4.236 -    apply (clarsimp simp add: set_rel_def)
   4.237 -    apply (frule (1) bspec, clarify)
   4.238 -    apply (rule theI2, assumption)
   4.239 -    apply (clarsimp simp add: bi_unique_def)
   4.240 -    apply (simp add: bi_unique_def, metis)
   4.241 -    done
   4.242 -  show "inj_on ?f X"
   4.243 -    apply (rule inj_onI)
   4.244 -    apply (drule f [rule_format])
   4.245 -    apply (drule f [rule_format])
   4.246 -    apply (simp add: assms(1) [unfolded bi_unique_def])
   4.247 -    done
   4.248 -qed
   4.249 -
   4.250 -lemma finite_transfer [transfer_rule]:
   4.251 -  "bi_unique A \<Longrightarrow> (set_rel A ===> op =) finite finite"
   4.252 -  by (rule fun_relI, erule (1) bi_unique_set_rel_lemma,
   4.253 -    auto dest: finite_imageD)
   4.254 -
   4.255 -lemma card_transfer [transfer_rule]:
   4.256 -  "bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card"
   4.257 -  by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image)
   4.258 -
   4.259 -subsection {* Setup for lifting package *}
   4.260 -
   4.261 -lemma Quotient_set[quot_map]:
   4.262 -  assumes "Quotient R Abs Rep T"
   4.263 -  shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
   4.264 -  using assms unfolding Quotient_alt_def4
   4.265 -  apply (simp add: set_rel_OO[symmetric] set_rel_conversep)
   4.266 -  apply (simp add: set_rel_def, fast)
   4.267 -  done
   4.268 -
   4.269 -lemma set_invariant_commute [invariant_commute]:
   4.270 -  "set_rel (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)"
   4.271 -  unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast
   4.272 -
   4.273 -subsection {* Contravariant set map (vimage) and set relator *}
   4.274 +subsection {* Contravariant set map (vimage) and set relator, rules for the Quotient package *}
   4.275  
   4.276  definition "vset_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
   4.277  
     5.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Aug 13 15:59:22 2013 +0200
     5.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Aug 13 15:59:22 2013 +0200
     5.3 @@ -1,5 +1,5 @@
     5.4  (*  Title:      HOL/Library/Quotient_Sum.thy
     5.5 -    Author:     Cezary Kaliszyk, Christian Urban and Brian Huffman
     5.6 +    Author:     Cezary Kaliszyk and Christian Urban
     5.7  *)
     5.8  
     5.9  header {* Quotient infrastructure for the sum type *}
    5.10 @@ -8,31 +8,7 @@
    5.11  imports Main Quotient_Syntax
    5.12  begin
    5.13  
    5.14 -subsection {* Relator for sum type *}
    5.15 -
    5.16 -fun
    5.17 -  sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
    5.18 -where
    5.19 -  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    5.20 -| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    5.21 -| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    5.22 -| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    5.23 -
    5.24 -lemma sum_rel_unfold:
    5.25 -  "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    5.26 -    | (Inr x, Inr y) \<Rightarrow> R2 x y
    5.27 -    | _ \<Rightarrow> False)"
    5.28 -  by (cases x) (cases y, simp_all)+
    5.29 -
    5.30 -fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
    5.31 -where
    5.32 -  "sum_pred P1 P2 (Inl a) = P1 a"
    5.33 -| "sum_pred P1 P2 (Inr a) = P2 a"
    5.34 -
    5.35 -lemma sum_pred_unfold:
    5.36 -  "sum_pred P1 P2 x = (case x of Inl x \<Rightarrow> P1 x
    5.37 -    | Inr x \<Rightarrow> P2 x)"
    5.38 -by (cases x) simp_all
    5.39 +subsection {* Rules for the Quotient package *}
    5.40  
    5.41  lemma sum_rel_map1:
    5.42    "sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
    5.43 @@ -46,39 +22,10 @@
    5.44    "sum_map id id = id"
    5.45    by (simp add: id_def sum_map.identity fun_eq_iff)
    5.46  
    5.47 -lemma sum_rel_eq [id_simps, relator_eq]:
    5.48 +lemma sum_rel_eq [id_simps]:
    5.49    "sum_rel (op =) (op =) = (op =)"
    5.50    by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
    5.51  
    5.52 -lemma sum_rel_mono[relator_mono]:
    5.53 -  assumes "A \<le> C"
    5.54 -  assumes "B \<le> D"
    5.55 -  shows "(sum_rel A B) \<le> (sum_rel C D)"
    5.56 -using assms by (auto simp: sum_rel_unfold split: sum.splits)
    5.57 -
    5.58 -lemma sum_rel_OO[relator_distr]:
    5.59 -  "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
    5.60 -by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
    5.61 -
    5.62 -lemma Domainp_sum[relator_domain]:
    5.63 -  assumes "Domainp R1 = P1"
    5.64 -  assumes "Domainp R2 = P2"
    5.65 -  shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
    5.66 -using assms
    5.67 -by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
    5.68 -
    5.69 -lemma reflp_sum_rel[reflexivity_rule]:
    5.70 -  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    5.71 -  unfolding reflp_def split_sum_all sum_rel.simps by fast
    5.72 -
    5.73 -lemma left_total_sum_rel[reflexivity_rule]:
    5.74 -  "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
    5.75 -  using assms unfolding left_total_def split_sum_all split_sum_ex by simp
    5.76 -
    5.77 -lemma left_unique_sum_rel [reflexivity_rule]:
    5.78 -  "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)"
    5.79 -  using assms unfolding left_unique_def split_sum_all by simp
    5.80 -
    5.81  lemma sum_symp:
    5.82    "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    5.83    unfolding symp_def split_sum_all sum_rel.simps by fast
    5.84 @@ -91,50 +38,6 @@
    5.85    "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    5.86    by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE)
    5.87  
    5.88 -lemma right_total_sum_rel [transfer_rule]:
    5.89 -  "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
    5.90 -  unfolding right_total_def split_sum_all split_sum_ex by simp
    5.91 -
    5.92 -lemma right_unique_sum_rel [transfer_rule]:
    5.93 -  "right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (sum_rel R1 R2)"
    5.94 -  unfolding right_unique_def split_sum_all by simp
    5.95 -
    5.96 -lemma bi_total_sum_rel [transfer_rule]:
    5.97 -  "bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (sum_rel R1 R2)"
    5.98 -  using assms unfolding bi_total_def split_sum_all split_sum_ex by simp
    5.99 -
   5.100 -lemma bi_unique_sum_rel [transfer_rule]:
   5.101 -  "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
   5.102 -  using assms unfolding bi_unique_def split_sum_all by simp
   5.103 -
   5.104 -subsection {* Transfer rules for transfer package *}
   5.105 -
   5.106 -lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
   5.107 -  unfolding fun_rel_def by simp
   5.108 -
   5.109 -lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr"
   5.110 -  unfolding fun_rel_def by simp
   5.111 -
   5.112 -lemma sum_case_transfer [transfer_rule]:
   5.113 -  "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case"
   5.114 -  unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split)
   5.115 -
   5.116 -subsection {* Setup for lifting package *}
   5.117 -
   5.118 -lemma Quotient_sum[quot_map]:
   5.119 -  assumes "Quotient R1 Abs1 Rep1 T1"
   5.120 -  assumes "Quotient R2 Abs2 Rep2 T2"
   5.121 -  shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2)
   5.122 -    (sum_map Rep1 Rep2) (sum_rel T1 T2)"
   5.123 -  using assms unfolding Quotient_alt_def
   5.124 -  by (simp add: split_sum_all)
   5.125 -
   5.126 -lemma sum_invariant_commute [invariant_commute]: 
   5.127 -  "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
   5.128 -  by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split)
   5.129 -
   5.130 -subsection {* Rules for quotient package *}
   5.131 -
   5.132  lemma sum_quotient [quot_thm]:
   5.133    assumes q1: "Quotient3 R1 Abs1 Rep1"
   5.134    assumes q2: "Quotient3 R2 Abs2 Rep2"
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Lifting_Option.thy	Tue Aug 13 15:59:22 2013 +0200
     6.3 @@ -0,0 +1,125 @@
     6.4 +(*  Title:      HOL/Lifting_Option.thy
     6.5 +    Author:     Brian Huffman and Ondrej Kuncar
     6.6 +*)
     6.7 +
     6.8 +header {* Setup for Lifting/Transfer for the option type *}
     6.9 +
    6.10 +theory Lifting_Option
    6.11 +imports Lifting FunDef
    6.12 +begin
    6.13 +
    6.14 +subsection {* Relator and predicator properties *}
    6.15 +
    6.16 +fun
    6.17 +  option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
    6.18 +where
    6.19 +  "option_rel R None None = True"
    6.20 +| "option_rel R (Some x) None = False"
    6.21 +| "option_rel R None (Some x) = False"
    6.22 +| "option_rel R (Some x) (Some y) = R x y"
    6.23 +
    6.24 +lemma option_rel_unfold:
    6.25 +  "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
    6.26 +    | (Some x, Some y) \<Rightarrow> R x y
    6.27 +    | _ \<Rightarrow> False)"
    6.28 +  by (cases x) (cases y, simp_all)+
    6.29 +
    6.30 +fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
    6.31 +where
    6.32 +  "option_pred R None = True"
    6.33 +| "option_pred R (Some x) = R x"
    6.34 +
    6.35 +lemma option_pred_unfold:
    6.36 +  "option_pred P x = (case x of None \<Rightarrow> True
    6.37 +    | Some x \<Rightarrow> P x)"
    6.38 +by (cases x) simp_all
    6.39 +
    6.40 +lemma option_rel_eq [relator_eq]:
    6.41 +  "option_rel (op =) = (op =)"
    6.42 +  by (simp add: option_rel_unfold fun_eq_iff split: option.split)
    6.43 +
    6.44 +lemma option_rel_mono[relator_mono]:
    6.45 +  assumes "A \<le> B"
    6.46 +  shows "(option_rel A) \<le> (option_rel B)"
    6.47 +using assms by (auto simp: option_rel_unfold split: option.splits)
    6.48 +
    6.49 +lemma option_rel_OO[relator_distr]:
    6.50 +  "(option_rel A) OO (option_rel B) = option_rel (A OO B)"
    6.51 +by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split)
    6.52 +
    6.53 +lemma Domainp_option[relator_domain]:
    6.54 +  assumes "Domainp A = P"
    6.55 +  shows "Domainp (option_rel A) = (option_pred P)"
    6.56 +using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def]
    6.57 +by (auto iff: fun_eq_iff split: option.split)
    6.58 +
    6.59 +lemma reflp_option_rel[reflexivity_rule]:
    6.60 +  "reflp R \<Longrightarrow> reflp (option_rel R)"
    6.61 +  unfolding reflp_def split_option_all by simp
    6.62 +
    6.63 +lemma left_total_option_rel[reflexivity_rule]:
    6.64 +  "left_total R \<Longrightarrow> left_total (option_rel R)"
    6.65 +  unfolding left_total_def split_option_all split_option_ex by simp
    6.66 +
    6.67 +lemma left_unique_option_rel [reflexivity_rule]:
    6.68 +  "left_unique R \<Longrightarrow> left_unique (option_rel R)"
    6.69 +  unfolding left_unique_def split_option_all by simp
    6.70 +
    6.71 +lemma right_total_option_rel [transfer_rule]:
    6.72 +  "right_total R \<Longrightarrow> right_total (option_rel R)"
    6.73 +  unfolding right_total_def split_option_all split_option_ex by simp
    6.74 +
    6.75 +lemma right_unique_option_rel [transfer_rule]:
    6.76 +  "right_unique R \<Longrightarrow> right_unique (option_rel R)"
    6.77 +  unfolding right_unique_def split_option_all by simp
    6.78 +
    6.79 +lemma bi_total_option_rel [transfer_rule]:
    6.80 +  "bi_total R \<Longrightarrow> bi_total (option_rel R)"
    6.81 +  unfolding bi_total_def split_option_all split_option_ex by simp
    6.82 +
    6.83 +lemma bi_unique_option_rel [transfer_rule]:
    6.84 +  "bi_unique R \<Longrightarrow> bi_unique (option_rel R)"
    6.85 +  unfolding bi_unique_def split_option_all by simp
    6.86 +
    6.87 +lemma option_invariant_commute [invariant_commute]:
    6.88 +  "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)"
    6.89 +  by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all)
    6.90 +
    6.91 +subsection {* Quotient theorem for the Lifting package *}
    6.92 +
    6.93 +lemma Quotient_option[quot_map]:
    6.94 +  assumes "Quotient R Abs Rep T"
    6.95 +  shows "Quotient (option_rel R) (Option.map Abs)
    6.96 +    (Option.map Rep) (option_rel T)"
    6.97 +  using assms unfolding Quotient_alt_def option_rel_unfold
    6.98 +  by (simp split: option.split)
    6.99 +
   6.100 +subsection {* Transfer rules for the Transfer package *}
   6.101 +
   6.102 +context
   6.103 +begin
   6.104 +interpretation lifting_syntax .
   6.105 +
   6.106 +lemma None_transfer [transfer_rule]: "(option_rel A) None None"
   6.107 +  by simp
   6.108 +
   6.109 +lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some"
   6.110 +  unfolding fun_rel_def by simp
   6.111 +
   6.112 +lemma option_case_transfer [transfer_rule]:
   6.113 +  "(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case"
   6.114 +  unfolding fun_rel_def split_option_all by simp
   6.115 +
   6.116 +lemma option_map_transfer [transfer_rule]:
   6.117 +  "((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map"
   6.118 +  unfolding Option.map_def by transfer_prover
   6.119 +
   6.120 +lemma option_bind_transfer [transfer_rule]:
   6.121 +  "(option_rel A ===> (A ===> option_rel B) ===> option_rel B)
   6.122 +    Option.bind Option.bind"
   6.123 +  unfolding fun_rel_def split_option_all by simp
   6.124 +
   6.125 +end
   6.126 +
   6.127 +end
   6.128 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Lifting_Product.thy	Tue Aug 13 15:59:22 2013 +0200
     7.3 @@ -0,0 +1,135 @@
     7.4 +(*  Title:      HOL/Lifting_Product.thy
     7.5 +    Author:     Brian Huffman and Ondrej Kuncar
     7.6 +*)
     7.7 +
     7.8 +header {* Setup for Lifting/Transfer for the product type *}
     7.9 +
    7.10 +theory Lifting_Product
    7.11 +imports Lifting
    7.12 +begin
    7.13 +
    7.14 +subsection {* Relator and predicator properties *}
    7.15 +
    7.16 +definition
    7.17 +  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
    7.18 +where
    7.19 +  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    7.20 +
    7.21 +definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    7.22 +where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
    7.23 +
    7.24 +lemma prod_rel_apply [simp]:
    7.25 +  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    7.26 +  by (simp add: prod_rel_def)
    7.27 +
    7.28 +lemma prod_pred_apply [simp]:
    7.29 +  "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
    7.30 +  by (simp add: prod_pred_def)
    7.31 +
    7.32 +lemma prod_rel_eq [relator_eq]:
    7.33 +  shows "prod_rel (op =) (op =) = (op =)"
    7.34 +  by (simp add: fun_eq_iff)
    7.35 +
    7.36 +lemma prod_rel_mono[relator_mono]:
    7.37 +  assumes "A \<le> C"
    7.38 +  assumes "B \<le> D"
    7.39 +  shows "(prod_rel A B) \<le> (prod_rel C D)"
    7.40 +using assms by (auto simp: prod_rel_def)
    7.41 +
    7.42 +lemma prod_rel_OO[relator_distr]:
    7.43 +  "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
    7.44 +by (rule ext)+ (auto simp: prod_rel_def OO_def)
    7.45 +
    7.46 +lemma Domainp_prod[relator_domain]:
    7.47 +  assumes "Domainp T1 = P1"
    7.48 +  assumes "Domainp T2 = P2"
    7.49 +  shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
    7.50 +using assms unfolding prod_rel_def prod_pred_def by blast
    7.51 +
    7.52 +lemma reflp_prod_rel [reflexivity_rule]:
    7.53 +  assumes "reflp R1"
    7.54 +  assumes "reflp R2"
    7.55 +  shows "reflp (prod_rel R1 R2)"
    7.56 +using assms by (auto intro!: reflpI elim: reflpE)
    7.57 +
    7.58 +lemma left_total_prod_rel [reflexivity_rule]:
    7.59 +  assumes "left_total R1"
    7.60 +  assumes "left_total R2"
    7.61 +  shows "left_total (prod_rel R1 R2)"
    7.62 +  using assms unfolding left_total_def prod_rel_def by auto
    7.63 +
    7.64 +lemma left_unique_prod_rel [reflexivity_rule]:
    7.65 +  assumes "left_unique R1" and "left_unique R2"
    7.66 +  shows "left_unique (prod_rel R1 R2)"
    7.67 +  using assms unfolding left_unique_def prod_rel_def by auto
    7.68 +
    7.69 +lemma right_total_prod_rel [transfer_rule]:
    7.70 +  assumes "right_total R1" and "right_total R2"
    7.71 +  shows "right_total (prod_rel R1 R2)"
    7.72 +  using assms unfolding right_total_def prod_rel_def by auto
    7.73 +
    7.74 +lemma right_unique_prod_rel [transfer_rule]:
    7.75 +  assumes "right_unique R1" and "right_unique R2"
    7.76 +  shows "right_unique (prod_rel R1 R2)"
    7.77 +  using assms unfolding right_unique_def prod_rel_def by auto
    7.78 +
    7.79 +lemma bi_total_prod_rel [transfer_rule]:
    7.80 +  assumes "bi_total R1" and "bi_total R2"
    7.81 +  shows "bi_total (prod_rel R1 R2)"
    7.82 +  using assms unfolding bi_total_def prod_rel_def by auto
    7.83 +
    7.84 +lemma bi_unique_prod_rel [transfer_rule]:
    7.85 +  assumes "bi_unique R1" and "bi_unique R2"
    7.86 +  shows "bi_unique (prod_rel R1 R2)"
    7.87 +  using assms unfolding bi_unique_def prod_rel_def by auto
    7.88 +
    7.89 +lemma prod_invariant_commute [invariant_commute]: 
    7.90 +  "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
    7.91 +  by (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) blast
    7.92 +
    7.93 +subsection {* Quotient theorem for the Lifting package *}
    7.94 +
    7.95 +lemma Quotient_prod[quot_map]:
    7.96 +  assumes "Quotient R1 Abs1 Rep1 T1"
    7.97 +  assumes "Quotient R2 Abs2 Rep2 T2"
    7.98 +  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2)
    7.99 +    (map_pair Rep1 Rep2) (prod_rel T1 T2)"
   7.100 +  using assms unfolding Quotient_alt_def by auto
   7.101 +
   7.102 +subsection {* Transfer rules for the Transfer package *}
   7.103 +
   7.104 +context
   7.105 +begin
   7.106 +interpretation lifting_syntax .
   7.107 +
   7.108 +lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
   7.109 +  unfolding fun_rel_def prod_rel_def by simp
   7.110 +
   7.111 +lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst"
   7.112 +  unfolding fun_rel_def prod_rel_def by simp
   7.113 +
   7.114 +lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
   7.115 +  unfolding fun_rel_def prod_rel_def by simp
   7.116 +
   7.117 +lemma prod_case_transfer [transfer_rule]:
   7.118 +  "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case"
   7.119 +  unfolding fun_rel_def prod_rel_def by simp
   7.120 +
   7.121 +lemma curry_transfer [transfer_rule]:
   7.122 +  "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
   7.123 +  unfolding curry_def by transfer_prover
   7.124 +
   7.125 +lemma map_pair_transfer [transfer_rule]:
   7.126 +  "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
   7.127 +    map_pair map_pair"
   7.128 +  unfolding map_pair_def [abs_def] by transfer_prover
   7.129 +
   7.130 +lemma prod_rel_transfer [transfer_rule]:
   7.131 +  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
   7.132 +    prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel"
   7.133 +  unfolding fun_rel_def by auto
   7.134 +
   7.135 +end
   7.136 +
   7.137 +end
   7.138 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Lifting_Set.thy	Tue Aug 13 15:59:22 2013 +0200
     8.3 @@ -0,0 +1,273 @@
     8.4 +(*  Title:      HOL/Lifting_Set.thy
     8.5 +    Author:     Brian Huffman and Ondrej Kuncar
     8.6 +*)
     8.7 +
     8.8 +header {* Setup for Lifting/Transfer for the set type *}
     8.9 +
    8.10 +theory Lifting_Set
    8.11 +imports Lifting
    8.12 +begin
    8.13 +
    8.14 +subsection {* Relator and predicator properties *}
    8.15 +
    8.16 +definition set_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
    8.17 +  where "set_rel R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))"
    8.18 +
    8.19 +lemma set_relI:
    8.20 +  assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y"
    8.21 +  assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y"
    8.22 +  shows "set_rel R A B"
    8.23 +  using assms unfolding set_rel_def by simp
    8.24 +
    8.25 +lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
    8.26 +  unfolding set_rel_def by auto
    8.27 +
    8.28 +lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
    8.29 +  unfolding set_rel_def fun_eq_iff by auto
    8.30 +
    8.31 +lemma set_rel_mono[relator_mono]:
    8.32 +  assumes "A \<le> B"
    8.33 +  shows "set_rel A \<le> set_rel B"
    8.34 +using assms unfolding set_rel_def by blast
    8.35 +
    8.36 +lemma set_rel_OO[relator_distr]: "set_rel R OO set_rel S = set_rel (R OO S)"
    8.37 +  apply (rule sym)
    8.38 +  apply (intro ext, rename_tac X Z)
    8.39 +  apply (rule iffI)
    8.40 +  apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI)
    8.41 +  apply (simp add: set_rel_def, fast)
    8.42 +  apply (simp add: set_rel_def, fast)
    8.43 +  apply (simp add: set_rel_def, fast)
    8.44 +  done
    8.45 +
    8.46 +lemma Domainp_set[relator_domain]:
    8.47 +  assumes "Domainp T = R"
    8.48 +  shows "Domainp (set_rel T) = (\<lambda>A. Ball A R)"
    8.49 +using assms unfolding set_rel_def Domainp_iff[abs_def]
    8.50 +apply (intro ext)
    8.51 +apply (rule iffI) 
    8.52 +apply blast
    8.53 +apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
    8.54 +done
    8.55 +
    8.56 +lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
    8.57 +  unfolding reflp_def set_rel_def by fast
    8.58 +
    8.59 +lemma left_total_set_rel[reflexivity_rule]: 
    8.60 +  "left_total A \<Longrightarrow> left_total (set_rel A)"
    8.61 +  unfolding left_total_def set_rel_def
    8.62 +  apply safe
    8.63 +  apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
    8.64 +done
    8.65 +
    8.66 +lemma left_unique_set_rel[reflexivity_rule]: 
    8.67 +  "left_unique A \<Longrightarrow> left_unique (set_rel A)"
    8.68 +  unfolding left_unique_def set_rel_def
    8.69 +  by fast
    8.70 +
    8.71 +lemma right_total_set_rel [transfer_rule]:
    8.72 +  "right_total A \<Longrightarrow> right_total (set_rel A)"
    8.73 +  unfolding right_total_def set_rel_def
    8.74 +  by (rule allI, rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
    8.75 +
    8.76 +lemma right_unique_set_rel [transfer_rule]:
    8.77 +  "right_unique A \<Longrightarrow> right_unique (set_rel A)"
    8.78 +  unfolding right_unique_def set_rel_def by fast
    8.79 +
    8.80 +lemma bi_total_set_rel [transfer_rule]:
    8.81 +  "bi_total A \<Longrightarrow> bi_total (set_rel A)"
    8.82 +  unfolding bi_total_def set_rel_def
    8.83 +  apply safe
    8.84 +  apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
    8.85 +  apply (rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
    8.86 +  done
    8.87 +
    8.88 +lemma bi_unique_set_rel [transfer_rule]:
    8.89 +  "bi_unique A \<Longrightarrow> bi_unique (set_rel A)"
    8.90 +  unfolding bi_unique_def set_rel_def by fast
    8.91 +
    8.92 +lemma set_invariant_commute [invariant_commute]:
    8.93 +  "set_rel (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)"
    8.94 +  unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast
    8.95 +
    8.96 +subsection {* Quotient theorem for the Lifting package *}
    8.97 +
    8.98 +lemma Quotient_set[quot_map]:
    8.99 +  assumes "Quotient R Abs Rep T"
   8.100 +  shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
   8.101 +  using assms unfolding Quotient_alt_def4
   8.102 +  apply (simp add: set_rel_OO[symmetric] set_rel_conversep)
   8.103 +  apply (simp add: set_rel_def, fast)
   8.104 +  done
   8.105 +
   8.106 +subsection {* Transfer rules for the Transfer package *}
   8.107 +
   8.108 +subsubsection {* Unconditional transfer rules *}
   8.109 +
   8.110 +context
   8.111 +begin
   8.112 +interpretation lifting_syntax .
   8.113 +
   8.114 +lemma empty_transfer [transfer_rule]: "(set_rel A) {} {}"
   8.115 +  unfolding set_rel_def by simp
   8.116 +
   8.117 +lemma insert_transfer [transfer_rule]:
   8.118 +  "(A ===> set_rel A ===> set_rel A) insert insert"
   8.119 +  unfolding fun_rel_def set_rel_def by auto
   8.120 +
   8.121 +lemma union_transfer [transfer_rule]:
   8.122 +  "(set_rel A ===> set_rel A ===> set_rel A) union union"
   8.123 +  unfolding fun_rel_def set_rel_def by auto
   8.124 +
   8.125 +lemma Union_transfer [transfer_rule]:
   8.126 +  "(set_rel (set_rel A) ===> set_rel A) Union Union"
   8.127 +  unfolding fun_rel_def set_rel_def by simp fast
   8.128 +
   8.129 +lemma image_transfer [transfer_rule]:
   8.130 +  "((A ===> B) ===> set_rel A ===> set_rel B) image image"
   8.131 +  unfolding fun_rel_def set_rel_def by simp fast
   8.132 +
   8.133 +lemma UNION_transfer [transfer_rule]:
   8.134 +  "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) UNION UNION"
   8.135 +  unfolding SUP_def [abs_def] by transfer_prover
   8.136 +
   8.137 +lemma Ball_transfer [transfer_rule]:
   8.138 +  "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball"
   8.139 +  unfolding set_rel_def fun_rel_def by fast
   8.140 +
   8.141 +lemma Bex_transfer [transfer_rule]:
   8.142 +  "(set_rel A ===> (A ===> op =) ===> op =) Bex Bex"
   8.143 +  unfolding set_rel_def fun_rel_def by fast
   8.144 +
   8.145 +lemma Pow_transfer [transfer_rule]:
   8.146 +  "(set_rel A ===> set_rel (set_rel A)) Pow Pow"
   8.147 +  apply (rule fun_relI, rename_tac X Y, rule set_relI)
   8.148 +  apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp)
   8.149 +  apply (simp add: set_rel_def, fast)
   8.150 +  apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp)
   8.151 +  apply (simp add: set_rel_def, fast)
   8.152 +  done
   8.153 +
   8.154 +lemma set_rel_transfer [transfer_rule]:
   8.155 +  "((A ===> B ===> op =) ===> set_rel A ===> set_rel B ===> op =)
   8.156 +    set_rel set_rel"
   8.157 +  unfolding fun_rel_def set_rel_def by fast
   8.158 +
   8.159 +
   8.160 +subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
   8.161 +
   8.162 +lemma member_transfer [transfer_rule]:
   8.163 +  assumes "bi_unique A"
   8.164 +  shows "(A ===> set_rel A ===> op =) (op \<in>) (op \<in>)"
   8.165 +  using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
   8.166 +
   8.167 +lemma right_total_Collect_transfer[transfer_rule]:
   8.168 +  assumes "right_total A"
   8.169 +  shows "((A ===> op =) ===> set_rel A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect"
   8.170 +  using assms unfolding right_total_def set_rel_def fun_rel_def Domainp_iff by fast
   8.171 +
   8.172 +lemma Collect_transfer [transfer_rule]:
   8.173 +  assumes "bi_total A"
   8.174 +  shows "((A ===> op =) ===> set_rel A) Collect Collect"
   8.175 +  using assms unfolding fun_rel_def set_rel_def bi_total_def by fast
   8.176 +
   8.177 +lemma inter_transfer [transfer_rule]:
   8.178 +  assumes "bi_unique A"
   8.179 +  shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter"
   8.180 +  using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
   8.181 +
   8.182 +lemma Diff_transfer [transfer_rule]:
   8.183 +  assumes "bi_unique A"
   8.184 +  shows "(set_rel A ===> set_rel A ===> set_rel A) (op -) (op -)"
   8.185 +  using assms unfolding fun_rel_def set_rel_def bi_unique_def
   8.186 +  unfolding Ball_def Bex_def Diff_eq
   8.187 +  by (safe, simp, metis, simp, metis)
   8.188 +
   8.189 +lemma subset_transfer [transfer_rule]:
   8.190 +  assumes [transfer_rule]: "bi_unique A"
   8.191 +  shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)"
   8.192 +  unfolding subset_eq [abs_def] by transfer_prover
   8.193 +
   8.194 +lemma right_total_UNIV_transfer[transfer_rule]: 
   8.195 +  assumes "right_total A"
   8.196 +  shows "(set_rel A) (Collect (Domainp A)) UNIV"
   8.197 +  using assms unfolding right_total_def set_rel_def Domainp_iff by blast
   8.198 +
   8.199 +lemma UNIV_transfer [transfer_rule]:
   8.200 +  assumes "bi_total A"
   8.201 +  shows "(set_rel A) UNIV UNIV"
   8.202 +  using assms unfolding set_rel_def bi_total_def by simp
   8.203 +
   8.204 +lemma right_total_Compl_transfer [transfer_rule]:
   8.205 +  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
   8.206 +  shows "(set_rel A ===> set_rel A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus"
   8.207 +  unfolding Compl_eq [abs_def]
   8.208 +  by (subst Collect_conj_eq[symmetric]) transfer_prover
   8.209 +
   8.210 +lemma Compl_transfer [transfer_rule]:
   8.211 +  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
   8.212 +  shows "(set_rel A ===> set_rel A) uminus uminus"
   8.213 +  unfolding Compl_eq [abs_def] by transfer_prover
   8.214 +
   8.215 +lemma right_total_Inter_transfer [transfer_rule]:
   8.216 +  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
   8.217 +  shows "(set_rel (set_rel A) ===> set_rel A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter"
   8.218 +  unfolding Inter_eq[abs_def]
   8.219 +  by (subst Collect_conj_eq[symmetric]) transfer_prover
   8.220 +
   8.221 +lemma Inter_transfer [transfer_rule]:
   8.222 +  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
   8.223 +  shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter"
   8.224 +  unfolding Inter_eq [abs_def] by transfer_prover
   8.225 +
   8.226 +lemma filter_transfer [transfer_rule]:
   8.227 +  assumes [transfer_rule]: "bi_unique A"
   8.228 +  shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter"
   8.229 +  unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast
   8.230 +
   8.231 +lemma bi_unique_set_rel_lemma:
   8.232 +  assumes "bi_unique R" and "set_rel R X Y"
   8.233 +  obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)"
   8.234 +proof
   8.235 +  let ?f = "\<lambda>x. THE y. R x y"
   8.236 +  from assms show f: "\<forall>x\<in>X. R x (?f x)"
   8.237 +    apply (clarsimp simp add: set_rel_def)
   8.238 +    apply (drule (1) bspec, clarify)
   8.239 +    apply (rule theI2, assumption)
   8.240 +    apply (simp add: bi_unique_def)
   8.241 +    apply assumption
   8.242 +    done
   8.243 +  from assms show "Y = image ?f X"
   8.244 +    apply safe
   8.245 +    apply (clarsimp simp add: set_rel_def)
   8.246 +    apply (drule (1) bspec, clarify)
   8.247 +    apply (rule image_eqI)
   8.248 +    apply (rule the_equality [symmetric], assumption)
   8.249 +    apply (simp add: bi_unique_def)
   8.250 +    apply assumption
   8.251 +    apply (clarsimp simp add: set_rel_def)
   8.252 +    apply (frule (1) bspec, clarify)
   8.253 +    apply (rule theI2, assumption)
   8.254 +    apply (clarsimp simp add: bi_unique_def)
   8.255 +    apply (simp add: bi_unique_def, metis)
   8.256 +    done
   8.257 +  show "inj_on ?f X"
   8.258 +    apply (rule inj_onI)
   8.259 +    apply (drule f [rule_format])
   8.260 +    apply (drule f [rule_format])
   8.261 +    apply (simp add: assms(1) [unfolded bi_unique_def])
   8.262 +    done
   8.263 +qed
   8.264 +
   8.265 +lemma finite_transfer [transfer_rule]:
   8.266 +  "bi_unique A \<Longrightarrow> (set_rel A ===> op =) finite finite"
   8.267 +  by (rule fun_relI, erule (1) bi_unique_set_rel_lemma,
   8.268 +    auto dest: finite_imageD)
   8.269 +
   8.270 +lemma card_transfer [transfer_rule]:
   8.271 +  "bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card"
   8.272 +  by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image)
   8.273 +
   8.274 +end
   8.275 +
   8.276 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Lifting_Sum.thy	Tue Aug 13 15:59:22 2013 +0200
     9.3 @@ -0,0 +1,119 @@
     9.4 +(*  Title:      HOL/Lifting_Sum.thy
     9.5 +    Author:     Brian Huffman and Ondrej Kuncar
     9.6 +*)
     9.7 +
     9.8 +header {* Setup for Lifting/Transfer for the sum type *}
     9.9 +
    9.10 +theory Lifting_Sum
    9.11 +imports Lifting FunDef
    9.12 +begin
    9.13 +
    9.14 +subsection {* Relator and predicator properties *}
    9.15 +
    9.16 +fun
    9.17 +  sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
    9.18 +where
    9.19 +  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    9.20 +| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    9.21 +| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    9.22 +| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    9.23 +
    9.24 +lemma sum_rel_unfold:
    9.25 +  "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    9.26 +    | (Inr x, Inr y) \<Rightarrow> R2 x y
    9.27 +    | _ \<Rightarrow> False)"
    9.28 +  by (cases x) (cases y, simp_all)+
    9.29 +
    9.30 +fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
    9.31 +where
    9.32 +  "sum_pred P1 P2 (Inl a) = P1 a"
    9.33 +| "sum_pred P1 P2 (Inr a) = P2 a"
    9.34 +
    9.35 +lemma sum_pred_unfold:
    9.36 +  "sum_pred P1 P2 x = (case x of Inl x \<Rightarrow> P1 x
    9.37 +    | Inr x \<Rightarrow> P2 x)"
    9.38 +by (cases x) simp_all
    9.39 +
    9.40 +lemma sum_rel_eq [relator_eq]:
    9.41 +  "sum_rel (op =) (op =) = (op =)"
    9.42 +  by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
    9.43 +
    9.44 +lemma sum_rel_mono[relator_mono]:
    9.45 +  assumes "A \<le> C"
    9.46 +  assumes "B \<le> D"
    9.47 +  shows "(sum_rel A B) \<le> (sum_rel C D)"
    9.48 +using assms by (auto simp: sum_rel_unfold split: sum.splits)
    9.49 +
    9.50 +lemma sum_rel_OO[relator_distr]:
    9.51 +  "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
    9.52 +by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
    9.53 +
    9.54 +lemma Domainp_sum[relator_domain]:
    9.55 +  assumes "Domainp R1 = P1"
    9.56 +  assumes "Domainp R2 = P2"
    9.57 +  shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
    9.58 +using assms
    9.59 +by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
    9.60 +
    9.61 +lemma reflp_sum_rel[reflexivity_rule]:
    9.62 +  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    9.63 +  unfolding reflp_def split_sum_all sum_rel.simps by fast
    9.64 +
    9.65 +lemma left_total_sum_rel[reflexivity_rule]:
    9.66 +  "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
    9.67 +  using assms unfolding left_total_def split_sum_all split_sum_ex by simp
    9.68 +
    9.69 +lemma left_unique_sum_rel [reflexivity_rule]:
    9.70 +  "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)"
    9.71 +  using assms unfolding left_unique_def split_sum_all by simp
    9.72 +
    9.73 +lemma right_total_sum_rel [transfer_rule]:
    9.74 +  "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
    9.75 +  unfolding right_total_def split_sum_all split_sum_ex by simp
    9.76 +
    9.77 +lemma right_unique_sum_rel [transfer_rule]:
    9.78 +  "right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (sum_rel R1 R2)"
    9.79 +  unfolding right_unique_def split_sum_all by simp
    9.80 +
    9.81 +lemma bi_total_sum_rel [transfer_rule]:
    9.82 +  "bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (sum_rel R1 R2)"
    9.83 +  using assms unfolding bi_total_def split_sum_all split_sum_ex by simp
    9.84 +
    9.85 +lemma bi_unique_sum_rel [transfer_rule]:
    9.86 +  "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
    9.87 +  using assms unfolding bi_unique_def split_sum_all by simp
    9.88 +
    9.89 +lemma sum_invariant_commute [invariant_commute]: 
    9.90 +  "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
    9.91 +  by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split)
    9.92 +
    9.93 +subsection {* Quotient theorem for the Lifting package *}
    9.94 +
    9.95 +lemma Quotient_sum[quot_map]:
    9.96 +  assumes "Quotient R1 Abs1 Rep1 T1"
    9.97 +  assumes "Quotient R2 Abs2 Rep2 T2"
    9.98 +  shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2)
    9.99 +    (sum_map Rep1 Rep2) (sum_rel T1 T2)"
   9.100 +  using assms unfolding Quotient_alt_def
   9.101 +  by (simp add: split_sum_all)
   9.102 +
   9.103 +subsection {* Transfer rules for the Transfer package *}
   9.104 +
   9.105 +context
   9.106 +begin
   9.107 +interpretation lifting_syntax .
   9.108 +
   9.109 +lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
   9.110 +  unfolding fun_rel_def by simp
   9.111 +
   9.112 +lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr"
   9.113 +  unfolding fun_rel_def by simp
   9.114 +
   9.115 +lemma sum_case_transfer [transfer_rule]:
   9.116 +  "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case"
   9.117 +  unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split)
   9.118 +
   9.119 +end
   9.120 +
   9.121 +end
   9.122 +
    10.1 --- a/src/HOL/List.thy	Tue Aug 13 15:59:22 2013 +0200
    10.2 +++ b/src/HOL/List.thy	Tue Aug 13 15:59:22 2013 +0200
    10.3 @@ -5,7 +5,7 @@
    10.4  header {* The datatype of finite lists *}
    10.5  
    10.6  theory List
    10.7 -imports Presburger Code_Numeral Quotient ATP
    10.8 +imports Presburger Code_Numeral Quotient ATP Lifting_Set Lifting_Option Lifting_Product
    10.9  begin
   10.10  
   10.11  datatype 'a list =
   10.12 @@ -6228,5 +6228,338 @@
   10.13    "wf (set xs) = acyclic (set xs)"
   10.14    by (simp add: wf_iff_acyclic_if_finite)
   10.15  
   10.16 +subsection {* Setup for Lifting/Transfer *}
   10.17 +
   10.18 +subsubsection {* Relator and predicator properties *}
   10.19 +
   10.20 +lemma list_all2_eq'[relator_eq]:
   10.21 +  "list_all2 (op =) = (op =)"
   10.22 +by (rule ext)+ (simp add: list_all2_eq)
   10.23 +
   10.24 +lemma list_all2_mono'[relator_mono]:
   10.25 +  assumes "A \<le> B"
   10.26 +  shows "(list_all2 A) \<le> (list_all2 B)"
   10.27 +using assms by (auto intro: list_all2_mono)
   10.28 +
   10.29 +lemma list_all2_OO[relator_distr]: "list_all2 A OO list_all2 B = list_all2 (A OO B)"
   10.30 +proof (intro ext iffI)
   10.31 +  fix xs ys
   10.32 +  assume "list_all2 (A OO B) xs ys"
   10.33 +  thus "(list_all2 A OO list_all2 B) xs ys"
   10.34 +    unfolding OO_def
   10.35 +    by (induct, simp, simp add: list_all2_Cons1 list_all2_Cons2, fast)
   10.36 +next
   10.37 +  fix xs ys
   10.38 +  assume "(list_all2 A OO list_all2 B) xs ys"
   10.39 +  then obtain zs where "list_all2 A xs zs" and "list_all2 B zs ys" ..
   10.40 +  thus "list_all2 (A OO B) xs ys"
   10.41 +    by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
   10.42 +qed
   10.43 +
   10.44 +lemma Domainp_list[relator_domain]:
   10.45 +  assumes "Domainp A = P"
   10.46 +  shows "Domainp (list_all2 A) = (list_all P)"
   10.47 +proof -
   10.48 +  {
   10.49 +    fix x
   10.50 +    have *: "\<And>x. (\<exists>y. A x y) = P x" using assms unfolding Domainp_iff by blast
   10.51 +    have "(\<exists>y. (list_all2 A x y)) = list_all P x"
   10.52 +    by (induction x) (simp_all add: * list_all2_Cons1)
   10.53 +  }
   10.54 +  then show ?thesis
   10.55 +  unfolding Domainp_iff[abs_def]
   10.56 +  by (auto iff: fun_eq_iff)
   10.57 +qed 
   10.58 +
   10.59 +lemma reflp_list_all2[reflexivity_rule]:
   10.60 +  assumes "reflp R"
   10.61 +  shows "reflp (list_all2 R)"
   10.62 +proof (rule reflpI)
   10.63 +  from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
   10.64 +  fix xs
   10.65 +  show "list_all2 R xs xs"
   10.66 +    by (induct xs) (simp_all add: *)
   10.67 +qed
   10.68 +
   10.69 +lemma left_total_list_all2[reflexivity_rule]:
   10.70 +  "left_total R \<Longrightarrow> left_total (list_all2 R)"
   10.71 +  unfolding left_total_def
   10.72 +  apply safe
   10.73 +  apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
   10.74 +done
   10.75 +
   10.76 +lemma left_unique_list_all2 [reflexivity_rule]:
   10.77 +  "left_unique R \<Longrightarrow> left_unique (list_all2 R)"
   10.78 +  unfolding left_unique_def
   10.79 +  apply (subst (2) all_comm, subst (1) all_comm)
   10.80 +  apply (rule allI, rename_tac zs, induct_tac zs)
   10.81 +  apply (auto simp add: list_all2_Cons2)
   10.82 +  done
   10.83 +
   10.84 +lemma right_total_list_all2 [transfer_rule]:
   10.85 +  "right_total R \<Longrightarrow> right_total (list_all2 R)"
   10.86 +  unfolding right_total_def
   10.87 +  by (rule allI, induct_tac y, simp, simp add: list_all2_Cons2)
   10.88 +
   10.89 +lemma right_unique_list_all2 [transfer_rule]:
   10.90 +  "right_unique R \<Longrightarrow> right_unique (list_all2 R)"
   10.91 +  unfolding right_unique_def
   10.92 +  apply (rule allI, rename_tac xs, induct_tac xs)
   10.93 +  apply (auto simp add: list_all2_Cons1)
   10.94 +  done
   10.95 +
   10.96 +lemma bi_total_list_all2 [transfer_rule]:
   10.97 +  "bi_total A \<Longrightarrow> bi_total (list_all2 A)"
   10.98 +  unfolding bi_total_def
   10.99 +  apply safe
  10.100 +  apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
  10.101 +  apply (rename_tac ys, induct_tac ys, simp, simp add: list_all2_Cons2)
  10.102 +  done
  10.103 +
  10.104 +lemma bi_unique_list_all2 [transfer_rule]:
  10.105 +  "bi_unique A \<Longrightarrow> bi_unique (list_all2 A)"
  10.106 +  unfolding bi_unique_def
  10.107 +  apply (rule conjI)
  10.108 +  apply (rule allI, rename_tac xs, induct_tac xs)
  10.109 +  apply (simp, force simp add: list_all2_Cons1)
  10.110 +  apply (subst (2) all_comm, subst (1) all_comm)
  10.111 +  apply (rule allI, rename_tac xs, induct_tac xs)
  10.112 +  apply (simp, force simp add: list_all2_Cons2)
  10.113 +  done
  10.114 +
  10.115 +lemma list_invariant_commute [invariant_commute]:
  10.116 +  "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
  10.117 +  apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def) 
  10.118 +  apply (intro allI) 
  10.119 +  apply (induct_tac rule: list_induct2') 
  10.120 +  apply simp_all 
  10.121 +  apply fastforce
  10.122 +done
  10.123 +
  10.124 +subsubsection {* Quotient theorem for the Lifting package *}
  10.125 +
  10.126 +lemma Quotient_list[quot_map]:
  10.127 +  assumes "Quotient R Abs Rep T"
  10.128 +  shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"
  10.129 +proof (unfold Quotient_alt_def, intro conjI allI impI)
  10.130 +  from assms have 1: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
  10.131 +    unfolding Quotient_alt_def by simp
  10.132 +  fix xs ys assume "list_all2 T xs ys" thus "map Abs xs = ys"
  10.133 +    by (induct, simp, simp add: 1)
  10.134 +next
  10.135 +  from assms have 2: "\<And>x. T (Rep x) x"
  10.136 +    unfolding Quotient_alt_def by simp
  10.137 +  fix xs show "list_all2 T (map Rep xs) xs"
  10.138 +    by (induct xs, simp, simp add: 2)
  10.139 +next
  10.140 +  from assms have 3: "\<And>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y"
  10.141 +    unfolding Quotient_alt_def by simp
  10.142 +  fix xs ys show "list_all2 R xs ys \<longleftrightarrow> list_all2 T xs (map Abs xs) \<and>
  10.143 +    list_all2 T ys (map Abs ys) \<and> map Abs xs = map Abs ys"
  10.144 +    by (induct xs ys rule: list_induct2', simp_all, metis 3)
  10.145 +qed
  10.146 +
  10.147 +subsubsection {* Transfer rules for the Transfer package *}
  10.148 +
  10.149 +context
  10.150 +begin
  10.151 +interpretation lifting_syntax .
  10.152 +
  10.153 +lemma Nil_transfer [transfer_rule]: "(list_all2 A) [] []"
  10.154 +  by simp
  10.155 +
  10.156 +lemma Cons_transfer [transfer_rule]:
  10.157 +  "(A ===> list_all2 A ===> list_all2 A) Cons Cons"
  10.158 +  unfolding fun_rel_def by simp
  10.159 +
  10.160 +lemma list_case_transfer [transfer_rule]:
  10.161 +  "(B ===> (A ===> list_all2 A ===> B) ===> list_all2 A ===> B)
  10.162 +    list_case list_case"
  10.163 +  unfolding fun_rel_def by (simp split: list.split)
  10.164 +
  10.165 +lemma list_rec_transfer [transfer_rule]:
  10.166 +  "(B ===> (A ===> list_all2 A ===> B ===> B) ===> list_all2 A ===> B)
  10.167 +    list_rec list_rec"
  10.168 +  unfolding fun_rel_def by (clarify, erule list_all2_induct, simp_all)
  10.169 +
  10.170 +lemma tl_transfer [transfer_rule]:
  10.171 +  "(list_all2 A ===> list_all2 A) tl tl"
  10.172 +  unfolding tl_def by transfer_prover
  10.173 +
  10.174 +lemma butlast_transfer [transfer_rule]:
  10.175 +  "(list_all2 A ===> list_all2 A) butlast butlast"
  10.176 +  by (rule fun_relI, erule list_all2_induct, auto)
  10.177 +
  10.178 +lemma set_transfer [transfer_rule]:
  10.179 +  "(list_all2 A ===> set_rel A) set set"
  10.180 +  unfolding set_def by transfer_prover
  10.181 +
  10.182 +lemma map_transfer [transfer_rule]:
  10.183 +  "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"
  10.184 +  unfolding List.map_def by transfer_prover
  10.185 +
  10.186 +lemma append_transfer [transfer_rule]:
  10.187 +  "(list_all2 A ===> list_all2 A ===> list_all2 A) append append"
  10.188 +  unfolding List.append_def by transfer_prover
  10.189 +
  10.190 +lemma rev_transfer [transfer_rule]:
  10.191 +  "(list_all2 A ===> list_all2 A) rev rev"
  10.192 +  unfolding List.rev_def by transfer_prover
  10.193 +
  10.194 +lemma filter_transfer [transfer_rule]:
  10.195 +  "((A ===> op =) ===> list_all2 A ===> list_all2 A) filter filter"
  10.196 +  unfolding List.filter_def by transfer_prover
  10.197 +
  10.198 +lemma fold_transfer [transfer_rule]:
  10.199 +  "((A ===> B ===> B) ===> list_all2 A ===> B ===> B) fold fold"
  10.200 +  unfolding List.fold_def by transfer_prover
  10.201 +
  10.202 +lemma foldr_transfer [transfer_rule]:
  10.203 +  "((A ===> B ===> B) ===> list_all2 A ===> B ===> B) foldr foldr"
  10.204 +  unfolding List.foldr_def by transfer_prover
  10.205 +
  10.206 +lemma foldl_transfer [transfer_rule]:
  10.207 +  "((B ===> A ===> B) ===> B ===> list_all2 A ===> B) foldl foldl"
  10.208 +  unfolding List.foldl_def by transfer_prover
  10.209 +
  10.210 +lemma concat_transfer [transfer_rule]:
  10.211 +  "(list_all2 (list_all2 A) ===> list_all2 A) concat concat"
  10.212 +  unfolding List.concat_def by transfer_prover
  10.213 +
  10.214 +lemma drop_transfer [transfer_rule]:
  10.215 +  "(op = ===> list_all2 A ===> list_all2 A) drop drop"
  10.216 +  unfolding List.drop_def by transfer_prover
  10.217 +
  10.218 +lemma take_transfer [transfer_rule]:
  10.219 +  "(op = ===> list_all2 A ===> list_all2 A) take take"
  10.220 +  unfolding List.take_def by transfer_prover
  10.221 +
  10.222 +lemma list_update_transfer [transfer_rule]:
  10.223 +  "(list_all2 A ===> op = ===> A ===> list_all2 A) list_update list_update"
  10.224 +  unfolding list_update_def by transfer_prover
  10.225 +
  10.226 +lemma takeWhile_transfer [transfer_rule]:
  10.227 +  "((A ===> op =) ===> list_all2 A ===> list_all2 A) takeWhile takeWhile"
  10.228 +  unfolding takeWhile_def by transfer_prover
  10.229 +
  10.230 +lemma dropWhile_transfer [transfer_rule]:
  10.231 +  "((A ===> op =) ===> list_all2 A ===> list_all2 A) dropWhile dropWhile"
  10.232 +  unfolding dropWhile_def by transfer_prover
  10.233 +
  10.234 +lemma zip_transfer [transfer_rule]:
  10.235 +  "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) zip zip"
  10.236 +  unfolding zip_def by transfer_prover
  10.237 +
  10.238 +lemma insert_transfer [transfer_rule]:
  10.239 +  assumes [transfer_rule]: "bi_unique A"
  10.240 +  shows "(A ===> list_all2 A ===> list_all2 A) List.insert List.insert"
  10.241 +  unfolding List.insert_def [abs_def] by transfer_prover
  10.242 +
  10.243 +lemma find_transfer [transfer_rule]:
  10.244 +  "((A ===> op =) ===> list_all2 A ===> option_rel A) List.find List.find"
  10.245 +  unfolding List.find_def by transfer_prover
  10.246 +
  10.247 +lemma remove1_transfer [transfer_rule]:
  10.248 +  assumes [transfer_rule]: "bi_unique A"
  10.249 +  shows "(A ===> list_all2 A ===> list_all2 A) remove1 remove1"
  10.250 +  unfolding remove1_def by transfer_prover
  10.251 +
  10.252 +lemma removeAll_transfer [transfer_rule]:
  10.253 +  assumes [transfer_rule]: "bi_unique A"
  10.254 +  shows "(A ===> list_all2 A ===> list_all2 A) removeAll removeAll"
  10.255 +  unfolding removeAll_def by transfer_prover
  10.256 +
  10.257 +lemma distinct_transfer [transfer_rule]:
  10.258 +  assumes [transfer_rule]: "bi_unique A"
  10.259 +  shows "(list_all2 A ===> op =) distinct distinct"
  10.260 +  unfolding distinct_def by transfer_prover
  10.261 +
  10.262 +lemma remdups_transfer [transfer_rule]:
  10.263 +  assumes [transfer_rule]: "bi_unique A"
  10.264 +  shows "(list_all2 A ===> list_all2 A) remdups remdups"
  10.265 +  unfolding remdups_def by transfer_prover
  10.266 +
  10.267 +lemma replicate_transfer [transfer_rule]:
  10.268 +  "(op = ===> A ===> list_all2 A) replicate replicate"
  10.269 +  unfolding replicate_def by transfer_prover
  10.270 +
  10.271 +lemma length_transfer [transfer_rule]:
  10.272 +  "(list_all2 A ===> op =) length length"
  10.273 +  unfolding list_size_overloaded_def by transfer_prover
  10.274 +
  10.275 +lemma rotate1_transfer [transfer_rule]:
  10.276 +  "(list_all2 A ===> list_all2 A) rotate1 rotate1"
  10.277 +  unfolding rotate1_def by transfer_prover
  10.278 +
  10.279 +lemma rotate_transfer [transfer_rule]:
  10.280 +  "(op = ===> list_all2 A ===> list_all2 A) rotate rotate"
  10.281 +  unfolding rotate_def [abs_def] by transfer_prover
  10.282 +
  10.283 +lemma list_all2_transfer [transfer_rule]:
  10.284 +  "((A ===> B ===> op =) ===> list_all2 A ===> list_all2 B ===> op =)
  10.285 +    list_all2 list_all2"
  10.286 +  apply (subst (4) list_all2_def [abs_def])
  10.287 +  apply (subst (3) list_all2_def [abs_def])
  10.288 +  apply transfer_prover
  10.289 +  done
  10.290 +
  10.291 +lemma sublist_transfer [transfer_rule]:
  10.292 +  "(list_all2 A ===> set_rel (op =) ===> list_all2 A) sublist sublist"
  10.293 +  unfolding sublist_def [abs_def] by transfer_prover
  10.294 +
  10.295 +lemma partition_transfer [transfer_rule]:
  10.296 +  "((A ===> op =) ===> list_all2 A ===> prod_rel (list_all2 A) (list_all2 A))
  10.297 +    partition partition"
  10.298 +  unfolding partition_def by transfer_prover
  10.299 +
  10.300 +lemma lists_transfer [transfer_rule]:
  10.301 +  "(set_rel A ===> set_rel (list_all2 A)) lists lists"
  10.302 +  apply (rule fun_relI, rule set_relI)
  10.303 +  apply (erule lists.induct, simp)
  10.304 +  apply (simp only: set_rel_def list_all2_Cons1, metis lists.Cons)
  10.305 +  apply (erule lists.induct, simp)
  10.306 +  apply (simp only: set_rel_def list_all2_Cons2, metis lists.Cons)
  10.307 +  done
  10.308 +
  10.309 +lemma set_Cons_transfer [transfer_rule]:
  10.310 +  "(set_rel A ===> set_rel (list_all2 A) ===> set_rel (list_all2 A))
  10.311 +    set_Cons set_Cons"
  10.312 +  unfolding fun_rel_def set_rel_def set_Cons_def
  10.313 +  apply safe
  10.314 +  apply (simp add: list_all2_Cons1, fast)
  10.315 +  apply (simp add: list_all2_Cons2, fast)
  10.316 +  done
  10.317 +
  10.318 +lemma listset_transfer [transfer_rule]:
  10.319 +  "(list_all2 (set_rel A) ===> set_rel (list_all2 A)) listset listset"
  10.320 +  unfolding listset_def by transfer_prover
  10.321 +
  10.322 +lemma null_transfer [transfer_rule]:
  10.323 +  "(list_all2 A ===> op =) List.null List.null"
  10.324 +  unfolding fun_rel_def List.null_def by auto
  10.325 +
  10.326 +lemma list_all_transfer [transfer_rule]:
  10.327 +  "((A ===> op =) ===> list_all2 A ===> op =) list_all list_all"
  10.328 +  unfolding list_all_iff [abs_def] by transfer_prover
  10.329 +
  10.330 +lemma list_ex_transfer [transfer_rule]:
  10.331 +  "((A ===> op =) ===> list_all2 A ===> op =) list_ex list_ex"
  10.332 +  unfolding list_ex_iff [abs_def] by transfer_prover
  10.333 +
  10.334 +lemma splice_transfer [transfer_rule]:
  10.335 +  "(list_all2 A ===> list_all2 A ===> list_all2 A) splice splice"
  10.336 +  apply (rule fun_relI, erule list_all2_induct, simp add: fun_rel_def, simp)
  10.337 +  apply (rule fun_relI)
  10.338 +  apply (erule_tac xs=x in list_all2_induct, simp, simp add: fun_rel_def)
  10.339 +  done
  10.340 +
  10.341 +lemma listsum_transfer[transfer_rule]:
  10.342 +  assumes [transfer_rule]: "A 0 0"
  10.343 +  assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
  10.344 +  shows "(list_all2 A ===> A) listsum listsum"
  10.345 +  unfolding listsum_def[abs_def]
  10.346 +  by transfer_prover
  10.347 +
  10.348  end
  10.349  
  10.350 +end
    11.1 --- a/src/HOL/Main.thy	Tue Aug 13 15:59:22 2013 +0200
    11.2 +++ b/src/HOL/Main.thy	Tue Aug 13 15:59:22 2013 +0200
    11.3 @@ -1,7 +1,7 @@
    11.4  header {* Main HOL *}
    11.5  
    11.6  theory Main
    11.7 -imports Predicate_Compile Nitpick Extraction
    11.8 +imports Predicate_Compile Nitpick Extraction Lifting_Sum
    11.9  begin
   11.10  
   11.11  text {*
    12.1 --- a/src/HOL/Rat.thy	Tue Aug 13 15:59:22 2013 +0200
    12.2 +++ b/src/HOL/Rat.thy	Tue Aug 13 15:59:22 2013 +0200
    12.3 @@ -49,8 +49,8 @@
    12.4    morphisms Rep_Rat Abs_Rat
    12.5    by (rule part_equivp_ratrel)
    12.6  
    12.7 -lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp cr_rat = (\<lambda>x. snd x \<noteq> 0)"
    12.8 -by (simp add: rat.domain)
    12.9 +lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp pcr_rat = (\<lambda>x. snd x \<noteq> 0)"
   12.10 +by (simp add: rat.domain_eq)
   12.11  
   12.12  subsubsection {* Representation and basic operations *}
   12.13