more complete fp_sugars for sum and prod;
authortraytel
Fri Nov 07 11:28:37 2014 +0100 (2014-11-07)
changeset 58916229765cc3414
parent 58915 7d673ab6a8d9
child 58917 a3be9a47e2d7
more complete fp_sugars for sum and prod;
tuned;
removed theorem duplicates;
removed obsolete Lifting_{Option,Product,Sum} theories
src/HOL/BNF_Def.thy
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Basic_BNF_Least_Fixpoints.thy
src/HOL/Basic_BNFs.thy
src/HOL/Datatype_Examples/Process.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Lifting_Option.thy
src/HOL/Lifting_Product.thy
src/HOL/Lifting_Sum.thy
src/HOL/List.thy
src/HOL/Main.thy
src/HOL/Option.thy
src/HOL/Product_Type.thy
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/BNF_Def.thy	Fri Nov 07 12:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_Def.thy	Fri Nov 07 11:28:37 2014 +0100
     1.3 @@ -18,13 +18,13 @@
     1.4  lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
     1.5    by auto
     1.6  
     1.7 -definition
     1.8 -   rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
     1.9 +inductive
    1.10 +   rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool" for R1 R2
    1.11  where
    1.12 -   "rel_sum R1 R2 x y =
    1.13 -     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    1.14 -     | (Inr x, Inr y) \<Rightarrow> R2 x y
    1.15 -     | _ \<Rightarrow> False)"
    1.16 +  "R1 a c \<Longrightarrow> rel_sum R1 R2 (Inl a) (Inl c)"
    1.17 +| "R2 b d \<Longrightarrow> rel_sum R1 R2 (Inr b) (Inr d)"
    1.18 +
    1.19 +hide_fact rel_sum_def
    1.20  
    1.21  definition
    1.22    rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
     2.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Fri Nov 07 12:24:56 2014 +0100
     2.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Fri Nov 07 11:28:37 2014 +0100
     2.3 @@ -85,7 +85,7 @@
     2.4  lemma prod_set_simps:
     2.5    "fsts (x, y) = {x}"
     2.6    "snds (x, y) = {y}"
     2.7 -  unfolding fsts_def snds_def by simp+
     2.8 +  unfolding prod_set_defs by simp+
     2.9  
    2.10  lemma sum_set_simps:
    2.11    "setl (Inl x) = {x}"
    2.12 @@ -204,7 +204,7 @@
    2.13  
    2.14  lemma case_sum_transfer:
    2.15    "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
    2.16 -  unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
    2.17 +  unfolding rel_fun_def by (auto split: sum.splits)
    2.18  
    2.19  lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
    2.20    by (case_tac x) simp+
    2.21 @@ -214,10 +214,7 @@
    2.22  
    2.23  lemma case_prod_transfer:
    2.24    "(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod"
    2.25 -  unfolding rel_fun_def rel_prod_def by simp
    2.26 -
    2.27 -lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
    2.28 -  by (simp add: inj_on_def)
    2.29 +  unfolding rel_fun_def by simp
    2.30  
    2.31  lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
    2.32    by simp
    2.33 @@ -246,7 +243,7 @@
    2.34    by auto
    2.35  
    2.36  lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair"
    2.37 -  unfolding rel_fun_def rel_prod_def by simp
    2.38 +  unfolding rel_fun_def by simp
    2.39  
    2.40  ML_file "Tools/BNF/bnf_fp_util.ML"
    2.41  ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
     3.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Fri Nov 07 12:24:56 2014 +0100
     3.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Fri Nov 07 11:28:37 2014 +0100
     3.3 @@ -176,18 +176,14 @@
     3.4    unfolding rel_fun_def by simp
     3.5  
     3.6  lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
     3.7 -  unfolding rel_fun_def rel_prod_def by simp
     3.8 +  unfolding rel_fun_def by simp
     3.9  
    3.10  lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
    3.11 -  unfolding rel_fun_def rel_prod_def by simp
    3.12 -
    3.13 -lemma map_sum_transfer:
    3.14 -  "rel_fun (rel_fun R T) (rel_fun (rel_fun S U) (rel_fun (rel_sum R S) (rel_sum T U))) map_sum map_sum"
    3.15 -  unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
    3.16 +  unfolding rel_fun_def by simp
    3.17  
    3.18  lemma convol_transfer:
    3.19    "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol"
    3.20 -  unfolding rel_prod_def rel_fun_def convol_def by auto
    3.21 +  unfolding rel_fun_def convol_def by auto
    3.22  
    3.23  lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
    3.24    by (rule ssubst)
    3.25 @@ -243,6 +239,4 @@
    3.26  ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
    3.27  ML_file "Tools/BNF/bnf_lfp_size.ML"
    3.28  
    3.29 -hide_fact (open) id_transfer
    3.30 -
    3.31  end
     4.1 --- a/src/HOL/Basic_BNF_Least_Fixpoints.thy	Fri Nov 07 12:24:56 2014 +0100
     4.2 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy	Fri Nov 07 11:28:37 2014 +0100
     4.3 @@ -53,6 +53,43 @@
     4.4  lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
     4.5    unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
     4.6  
     4.7 +lemma eq_fst_iff: "a = fst p \<longleftrightarrow> (\<exists>b. p = (a, b))"
     4.8 +  by (cases p) auto
     4.9 +
    4.10 +lemma eq_snd_iff: "b = snd p \<longleftrightarrow> (\<exists>a. p = (a, b))"
    4.11 +  by (cases p) auto
    4.12 +
    4.13 +lemma ex_neg_all_pos: "((\<exists>x. P x) \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
    4.14 +  by default blast+
    4.15 +
    4.16 +lemma hypsubst_in_prems: "(\<And>x. y = x \<Longrightarrow> z = f x \<Longrightarrow> P) \<equiv> (z = f y \<Longrightarrow> P)"
    4.17 +  by default blast+
    4.18 +
    4.19 +lemma isl_map_sum:
    4.20 +  "isl (map_sum f g s) = isl s"
    4.21 +  by (cases s) simp_all
    4.22 +
    4.23 +lemma map_sum_sel:
    4.24 +  "isl s \<Longrightarrow> projl (map_sum f g s) = f (projl s)"
    4.25 +  "\<not> isl s \<Longrightarrow> projr (map_sum f g s) = g (projr s)"
    4.26 +  by (case_tac [!] s) simp_all
    4.27 +
    4.28 +lemma set_sum_sel:
    4.29 +  "isl s \<Longrightarrow> projl s \<in> setl s"
    4.30 +  "\<not> isl s \<Longrightarrow> projr s \<in> setr s"
    4.31 +  by (case_tac [!] s) (auto intro: setl.intros setr.intros)
    4.32 +
    4.33 +lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b \<and>
    4.34 +  (isl a \<longrightarrow> isl b \<longrightarrow> R1 (projl a) (projl b)) \<and>
    4.35 +  (\<not> isl a \<longrightarrow> \<not> isl b \<longrightarrow> R2 (projr a) (projr b)))"
    4.36 +  by (cases a b rule: sum.exhaust[case_product sum.exhaust]) simp_all
    4.37 +
    4.38 +lemma isl_transfer: "rel_fun (rel_sum A B) (op =) isl isl"
    4.39 +  unfolding rel_fun_def rel_sum_sel by simp
    4.40 +
    4.41 +lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) \<and> R2 (snd p) (snd q))"
    4.42 +  by (force simp: rel_prod.simps elim: rel_prod.cases)
    4.43 +
    4.44  ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
    4.45  
    4.46  ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
     5.1 --- a/src/HOL/Basic_BNFs.thy	Fri Nov 07 12:24:56 2014 +0100
     5.2 +++ b/src/HOL/Basic_BNFs.thy	Fri Nov 07 11:28:37 2014 +0100
     5.3 @@ -13,20 +13,22 @@
     5.4  imports BNF_Def
     5.5  begin
     5.6  
     5.7 -definition setl :: "'a + 'b \<Rightarrow> 'a set" where
     5.8 -"setl x = (case x of Inl z => {z} | _ => {})"
     5.9 +inductive_set setl :: "'a + 'b \<Rightarrow> 'a set" for s :: "'a + 'b" where
    5.10 +  "s = Inl x \<Longrightarrow> x \<in> setl s"
    5.11 +inductive_set setr :: "'a + 'b \<Rightarrow> 'b set" for s :: "'a + 'b" where
    5.12 +  "s = Inr x \<Longrightarrow> x \<in> setr s"
    5.13  
    5.14 -definition setr :: "'a + 'b \<Rightarrow> 'b set" where
    5.15 -"setr x = (case x of Inr z => {z} | _ => {})"
    5.16 +lemma sum_set_defs[code]:
    5.17 +  "setl = (\<lambda>x. case x of Inl z => {z} | _ => {})"
    5.18 +  "setr = (\<lambda>x. case x of Inr z => {z} | _ => {})"
    5.19 +  by (auto simp: fun_eq_iff intro: setl.intros setr.intros elim: setl.cases setr.cases split: sum.splits)
    5.20  
    5.21 -lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
    5.22 -
    5.23 -lemma rel_sum_simps[simp]:
    5.24 +lemma rel_sum_simps[code, simp]:
    5.25    "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    5.26    "rel_sum R1 R2 (Inl a1) (Inr b2) = False"
    5.27    "rel_sum R1 R2 (Inr a2) (Inl b1) = False"
    5.28    "rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    5.29 -  unfolding rel_sum_def by simp_all
    5.30 +  by (auto intro: rel_sum.intros elim: rel_sum.cases)
    5.31  
    5.32  bnf "'a + 'b"
    5.33    map: map_sum
    5.34 @@ -46,18 +48,18 @@
    5.35           a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
    5.36    thus "map_sum f1 f2 x = map_sum g1 g2 x"
    5.37    proof (cases x)
    5.38 -    case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
    5.39 +    case Inl thus ?thesis using a1 by (clarsimp simp: sum_set_defs(1))
    5.40    next
    5.41 -    case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
    5.42 +    case Inr thus ?thesis using a2 by (clarsimp simp: sum_set_defs(2))
    5.43    qed
    5.44  next
    5.45    fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    5.46    show "setl o map_sum f1 f2 = image f1 o setl"
    5.47 -    by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
    5.48 +    by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split)
    5.49  next
    5.50    fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    5.51    show "setr o map_sum f1 f2 = image f2 o setr"
    5.52 -    by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
    5.53 +    by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split)
    5.54  next
    5.55    show "card_order natLeq" by (rule natLeq_card_order)
    5.56  next
    5.57 @@ -67,42 +69,48 @@
    5.58    show "|setl x| \<le>o natLeq"
    5.59      apply (rule ordLess_imp_ordLeq)
    5.60      apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
    5.61 -    by (simp add: setl_def split: sum.split)
    5.62 +    by (simp add: sum_set_defs(1) split: sum.split)
    5.63  next
    5.64    fix x :: "'o + 'p"
    5.65    show "|setr x| \<le>o natLeq"
    5.66      apply (rule ordLess_imp_ordLeq)
    5.67      apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
    5.68 -    by (simp add: setr_def split: sum.split)
    5.69 +    by (simp add: sum_set_defs(2) split: sum.split)
    5.70  next
    5.71    fix R1 R2 S1 S2
    5.72    show "rel_sum R1 R2 OO rel_sum S1 S2 \<le> rel_sum (R1 OO S1) (R2 OO S2)"
    5.73 -    by (auto simp: rel_sum_def split: sum.splits)
    5.74 +    by (force elim: rel_sum.cases)
    5.75  next
    5.76    fix R S
    5.77    show "rel_sum R S =
    5.78          (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
    5.79          Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
    5.80 -  unfolding setl_def setr_def rel_sum_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    5.81 -  by (fastforce split: sum.splits)
    5.82 +  unfolding sum_set_defs Grp_def relcompp.simps conversep.simps fun_eq_iff
    5.83 +  by (fastforce elim: rel_sum.cases split: sum.splits)
    5.84  qed (auto simp: sum_set_defs)
    5.85  
    5.86 -definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
    5.87 -"fsts x = {fst x}"
    5.88 +inductive_set fsts :: "'a \<times> 'b \<Rightarrow> 'a set" for p :: "'a \<times> 'b" where
    5.89 +  "fst p \<in> fsts p"
    5.90 +inductive_set snds :: "'a \<times> 'b \<Rightarrow> 'b set" for p :: "'a \<times> 'b" where
    5.91 +  "snd p \<in> snds p"
    5.92  
    5.93 -definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
    5.94 -"snds x = {snd x}"
    5.95 -
    5.96 -lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
    5.97 +lemma prod_set_defs[code]: "fsts = (\<lambda>p. {fst p})" "snds = (\<lambda>p. {snd p})"
    5.98 +  by (auto intro: fsts.intros snds.intros elim: fsts.cases snds.cases)
    5.99  
   5.100 -definition
   5.101 -  rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
   5.102 +inductive
   5.103 +  rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" for R1 R2
   5.104  where
   5.105 +  "\<lbrakk>R1 a b; R2 c d\<rbrakk> \<Longrightarrow> rel_prod R1 R2 (a, c) (b, d)"
   5.106 +
   5.107 +hide_fact rel_prod_def
   5.108 +
   5.109 +lemma rel_prod_apply [code, simp]:
   5.110 +  "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
   5.111 +  by (auto intro: rel_prod.intros elim: rel_prod.cases)
   5.112 +
   5.113 +lemma rel_prod_conv:
   5.114    "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
   5.115 -
   5.116 -lemma rel_prod_apply [simp]:
   5.117 -  "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
   5.118 -  by (simp add: rel_prod_def)
   5.119 +  by (rule ext, rule ext) auto
   5.120  
   5.121  bnf "'a \<times> 'b"
   5.122    map: map_prod
   5.123 @@ -147,7 +155,7 @@
   5.124    show "rel_prod R S =
   5.125          (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
   5.126          Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
   5.127 -  unfolding prod_set_defs rel_prod_def Grp_def relcompp.simps conversep.simps fun_eq_iff
   5.128 +  unfolding prod_set_defs rel_prod_apply Grp_def relcompp.simps conversep.simps fun_eq_iff
   5.129    by auto
   5.130  qed
   5.131  
     6.1 --- a/src/HOL/Datatype_Examples/Process.thy	Fri Nov 07 12:24:56 2014 +0100
     6.2 +++ b/src/HOL/Datatype_Examples/Process.thy	Fri Nov 07 11:28:37 2014 +0100
     6.3 @@ -17,15 +17,8 @@
     6.4  
     6.5  (* Read: prefix of, continuation of, choice 1 of, choice 2 of *)
     6.6  
     6.7 -section {* Customization *}
     6.8 -
     6.9  subsection {* Basic properties *}
    6.10  
    6.11 -declare
    6.12 -  rel_pre_process_def[simp]
    6.13 -  rel_sum_def[simp]
    6.14 -  rel_prod_def[simp]
    6.15 -
    6.16  (* Constructors versus discriminators *)
    6.17  theorem isAction_isChoice:
    6.18  "isAction p \<or> isChoice p"
     7.1 --- a/src/HOL/Library/Quotient_Option.thy	Fri Nov 07 12:24:56 2014 +0100
     7.2 +++ b/src/HOL/Library/Quotient_Option.thy	Fri Nov 07 11:28:37 2014 +0100
     7.3 @@ -54,12 +54,12 @@
     7.4  lemma option_None_rsp [quot_respect]:
     7.5    assumes q: "Quotient3 R Abs Rep"
     7.6    shows "rel_option R None None"
     7.7 -  by (rule None_transfer)
     7.8 +  by (rule option.ctr_transfer(1))
     7.9  
    7.10  lemma option_Some_rsp [quot_respect]:
    7.11    assumes q: "Quotient3 R Abs Rep"
    7.12    shows "(R ===> rel_option R) Some Some"
    7.13 -  by (rule Some_transfer)
    7.14 +  by (rule option.ctr_transfer(2))
    7.15  
    7.16  lemma option_None_prs [quot_preserve]:
    7.17    assumes q: "Quotient3 R Abs Rep"
     8.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Nov 07 12:24:56 2014 +0100
     8.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Nov 07 11:28:37 2014 +0100
     8.3 @@ -89,7 +89,7 @@
     8.4  lemma [quot_respect]:
     8.5    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
     8.6    rel_prod R2 R1 ===> rel_prod R2 R1 ===> op =) rel_prod rel_prod"
     8.7 -  by (rule rel_prod_transfer)
     8.8 +  by (rule prod.rel_transfer)
     8.9  
    8.10  lemma [quot_preserve]:
    8.11    assumes q1: "Quotient3 R1 abs1 rep1"
     9.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Nov 07 12:24:56 2014 +0100
     9.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Nov 07 11:28:37 2014 +0100
     9.3 @@ -12,11 +12,11 @@
     9.4  
     9.5  lemma rel_sum_map1:
     9.6    "rel_sum R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> rel_sum (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
     9.7 -  by (simp add: rel_sum_def split: sum.split)
     9.8 +  by (rule sum.rel_map(1))
     9.9  
    9.10  lemma rel_sum_map2:
    9.11    "rel_sum R1 R2 x (map_sum f1 f2 y) \<longleftrightarrow> rel_sum (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
    9.12 -  by (simp add: rel_sum_def split: sum.split)
    9.13 +  by (rule sum.rel_map(2))
    9.14  
    9.15  lemma map_sum_id [id_simps]:
    9.16    "map_sum id id = id"
    9.17 @@ -24,7 +24,7 @@
    9.18  
    9.19  lemma rel_sum_eq [id_simps]:
    9.20    "rel_sum (op =) (op =) = (op =)"
    9.21 -  by (simp add: rel_sum_def fun_eq_iff split: sum.split)
    9.22 +  by (rule sum.rel_eq)
    9.23  
    9.24  lemma reflp_rel_sum:
    9.25    "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (rel_sum R1 R2)"
    9.26 @@ -50,7 +50,7 @@
    9.27    apply (simp_all add: map_sum.compositionality comp_def map_sum.identity rel_sum_eq rel_sum_map1 rel_sum_map2
    9.28      Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
    9.29    using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
    9.30 -  apply (simp add: rel_sum_def comp_def split: sum.split)
    9.31 +  apply (fastforce elim!: rel_sum.cases simp add: comp_def split: sum.split)
    9.32    done
    9.33  
    9.34  declare [[mapQ3 sum = (rel_sum, sum_quotient)]]
    10.1 --- a/src/HOL/Lifting_Option.thy	Fri Nov 07 12:24:56 2014 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,47 +0,0 @@
    10.4 -(*  Title:      HOL/Lifting_Option.thy
    10.5 -    Author:     Brian Huffman and Ondrej Kuncar
    10.6 -    Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
    10.7 -*)
    10.8 -
    10.9 -section {* Setup for Lifting/Transfer for the option type *}
   10.10 -
   10.11 -theory Lifting_Option
   10.12 -imports Lifting Option
   10.13 -begin
   10.14 -
   10.15 -subsection {* Relator and predicator properties *}
   10.16 -
   10.17 -lemma rel_option_iff:
   10.18 -  "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
   10.19 -    | (Some x, Some y) \<Rightarrow> R x y
   10.20 -    | _ \<Rightarrow> False)"
   10.21 -by (auto split: prod.split option.split)
   10.22 -
   10.23 -subsection {* Transfer rules for the Transfer package *}
   10.24 -
   10.25 -context
   10.26 -begin
   10.27 -interpretation lifting_syntax .
   10.28 -
   10.29 -lemma None_transfer [transfer_rule]: "(rel_option A) None None"
   10.30 -  by (rule option.rel_inject)
   10.31 -
   10.32 -lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
   10.33 -  unfolding rel_fun_def by simp
   10.34 -
   10.35 -lemma case_option_transfer [transfer_rule]:
   10.36 -  "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
   10.37 -  unfolding rel_fun_def split_option_all by simp
   10.38 -
   10.39 -lemma map_option_transfer [transfer_rule]:
   10.40 -  "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
   10.41 -  unfolding map_option_case[abs_def] by transfer_prover
   10.42 -
   10.43 -lemma option_bind_transfer [transfer_rule]:
   10.44 -  "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
   10.45 -    Option.bind Option.bind"
   10.46 -  unfolding rel_fun_def split_option_all by simp
   10.47 -
   10.48 -end
   10.49 -
   10.50 -end
    11.1 --- a/src/HOL/Lifting_Product.thy	Fri Nov 07 12:24:56 2014 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,43 +0,0 @@
    11.4 -(*  Title:      HOL/Lifting_Product.thy
    11.5 -    Author:     Brian Huffman and Ondrej Kuncar
    11.6 -*)
    11.7 -
    11.8 -section {* Setup for Lifting/Transfer for the product type *}
    11.9 -
   11.10 -theory Lifting_Product
   11.11 -imports Lifting Basic_BNFs
   11.12 -begin
   11.13 -
   11.14 -(* The following lemma can be deleted when product is added to FP sugar *)
   11.15 -lemma prod_pred_inject [simp]:
   11.16 -  "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)"
   11.17 -  unfolding pred_prod_def fun_eq_iff prod_set_simps by blast
   11.18 -
   11.19 -subsection {* Transfer rules for the Transfer package *}
   11.20 -
   11.21 -context
   11.22 -begin
   11.23 -interpretation lifting_syntax .
   11.24 -
   11.25 -declare Pair_transfer [transfer_rule]
   11.26 -declare fst_transfer [transfer_rule]
   11.27 -declare snd_transfer [transfer_rule]
   11.28 -declare case_prod_transfer [transfer_rule]
   11.29 -
   11.30 -lemma curry_transfer [transfer_rule]:
   11.31 -  "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
   11.32 -  unfolding curry_def by transfer_prover
   11.33 -
   11.34 -lemma map_prod_transfer [transfer_rule]:
   11.35 -  "((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D)
   11.36 -    map_prod map_prod"
   11.37 -  unfolding map_prod_def [abs_def] by transfer_prover
   11.38 -
   11.39 -lemma rel_prod_transfer [transfer_rule]:
   11.40 -  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
   11.41 -    rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
   11.42 -  unfolding rel_fun_def by auto
   11.43 -
   11.44 -end
   11.45 -
   11.46 -end
    12.1 --- a/src/HOL/Lifting_Sum.thy	Fri Nov 07 12:24:56 2014 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,34 +0,0 @@
    12.4 -(*  Title:      HOL/Lifting_Sum.thy
    12.5 -    Author:     Brian Huffman and Ondrej Kuncar
    12.6 -*)
    12.7 -
    12.8 -section {* Setup for Lifting/Transfer for the sum type *}
    12.9 -
   12.10 -theory Lifting_Sum
   12.11 -imports Lifting Basic_BNFs
   12.12 -begin
   12.13 -
   12.14 -(* The following lemma can be deleted when sum is added to FP sugar *)
   12.15 -lemma sum_pred_inject [simp]:
   12.16 -  "pred_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a"
   12.17 -  unfolding pred_sum_def fun_eq_iff sum_set_simps by auto
   12.18 -
   12.19 -subsection {* Transfer rules for the Transfer package *}
   12.20 -
   12.21 -context
   12.22 -begin
   12.23 -interpretation lifting_syntax .
   12.24 -
   12.25 -lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
   12.26 -  unfolding rel_fun_def by simp
   12.27 -
   12.28 -lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
   12.29 -  unfolding rel_fun_def by simp
   12.30 -
   12.31 -lemma case_sum_transfer [transfer_rule]:
   12.32 -  "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
   12.33 -  unfolding rel_fun_def rel_sum_def by (simp split: sum.split)
   12.34 -
   12.35 -end
   12.36 -
   12.37 -end
    13.1 --- a/src/HOL/List.thy	Fri Nov 07 12:24:56 2014 +0100
    13.2 +++ b/src/HOL/List.thy	Fri Nov 07 11:28:37 2014 +0100
    13.3 @@ -5,7 +5,7 @@
    13.4  section {* The datatype of finite lists *}
    13.5  
    13.6  theory List
    13.7 -imports Sledgehammer Code_Numeral Lifting_Set Lifting_Option Lifting_Product
    13.8 +imports Sledgehammer Code_Numeral Lifting_Set
    13.9  begin
   13.10  
   13.11  datatype (set: 'a) list =
    14.1 --- a/src/HOL/Main.thy	Fri Nov 07 12:24:56 2014 +0100
    14.2 +++ b/src/HOL/Main.thy	Fri Nov 07 11:28:37 2014 +0100
    14.3 @@ -1,8 +1,7 @@
    14.4  section {* Main HOL *}
    14.5  
    14.6  theory Main
    14.7 -imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
    14.8 -  BNF_Greatest_Fixpoint
    14.9 +imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint
   14.10  begin
   14.11  
   14.12  text {*
    15.1 --- a/src/HOL/Option.thy	Fri Nov 07 12:24:56 2014 +0100
    15.2 +++ b/src/HOL/Option.thy	Fri Nov 07 11:28:37 2014 +0100
    15.3 @@ -5,7 +5,7 @@
    15.4  section {* Datatype option *}
    15.5  
    15.6  theory Option
    15.7 -imports BNF_Least_Fixpoint Finite_Set
    15.8 +imports Lifting Finite_Set
    15.9  begin
   15.10  
   15.11  datatype 'a option =
   15.12 @@ -114,6 +114,12 @@
   15.13    "case_option g h (map_option f x) = case_option g (h \<circ> f) x"
   15.14    by (cases x) simp_all
   15.15  
   15.16 +lemma rel_option_iff:
   15.17 +  "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
   15.18 +    | (Some x, Some y) \<Rightarrow> R x y
   15.19 +    | _ \<Rightarrow> False)"
   15.20 +by (auto split: prod.split option.split)
   15.21 +
   15.22  primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
   15.23  bind_lzero: "bind None f = None" |
   15.24  bind_lunit: "bind (Some x) f = f x"
   15.25 @@ -192,6 +198,20 @@
   15.26  hide_fact (open) bind_cong
   15.27  
   15.28  
   15.29 +subsection {* Transfer rules for the Transfer package *}
   15.30 +
   15.31 +context
   15.32 +begin
   15.33 +interpretation lifting_syntax .
   15.34 +
   15.35 +lemma option_bind_transfer [transfer_rule]:
   15.36 +  "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
   15.37 +    Option.bind Option.bind"
   15.38 +  unfolding rel_fun_def split_option_all by simp
   15.39 +
   15.40 +end
   15.41 +
   15.42 +
   15.43  subsubsection {* Interaction with finite sets *}
   15.44  
   15.45  lemma finite_option_UNIV [simp]:
    16.1 --- a/src/HOL/Product_Type.thy	Fri Nov 07 12:24:56 2014 +0100
    16.2 +++ b/src/HOL/Product_Type.thy	Fri Nov 07 11:28:37 2014 +0100
    16.3 @@ -867,7 +867,7 @@
    16.4    "fst (map_prod f g x) = f (fst x)"
    16.5    by (cases x) simp_all
    16.6  
    16.7 -lemma snd_prod_fun [simp]:
    16.8 +lemma snd_map_prod [simp]:
    16.9    "snd (map_prod f g x) = g (snd x)"
   16.10    by (cases x) simp_all
   16.11  
    17.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Fri Nov 07 12:24:56 2014 +0100
    17.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Fri Nov 07 11:28:37 2014 +0100
    17.3 @@ -81,23 +81,25 @@
    17.4         {ctrXs_Tss = ctr_Tss,
    17.5          ctr_defs = @{thms Inl_def_alt Inr_def_alt},
    17.6          ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
    17.7 -        ctr_transfers = [],
    17.8 -        case_transfers = [],
    17.9 -        disc_transfers = [],
   17.10 +        ctr_transfers = @{thms Inl_transfer Inr_transfer},
   17.11 +        case_transfers = @{thms case_sum_transfer},
   17.12 +        disc_transfers = @{thms isl_transfer},
   17.13          sel_transfers = []},
   17.14       fp_bnf_sugar =
   17.15         {map_thms = @{thms map_sum.simps},
   17.16 -        map_disc_iffs = [],
   17.17 -        map_selss = [],
   17.18 +        map_disc_iffs = @{thms isl_map_sum},
   17.19 +        map_selss = map single @{thms map_sum_sel},
   17.20          rel_injects = @{thms rel_sum_simps(1,4)},
   17.21          rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
   17.22 -        rel_sels = [],
   17.23 -        rel_intros = [],
   17.24 -        rel_cases = [],
   17.25 -        set_thms = [],
   17.26 -        set_selssss = [],
   17.27 -        set_introssss = [],
   17.28 -        set_cases = []},
   17.29 +        rel_sels = @{thms rel_sum_sel},
   17.30 +        rel_intros = @{thms rel_sum.intros},
   17.31 +        rel_cases = @{thms rel_sum.cases},
   17.32 +        set_thms = @{thms sum_set_simps},
   17.33 +        set_selssss = [[[@{thms set_sum_sel(1)}], [[]]], [[[]], [@{thms set_sum_sel(2)}]]],
   17.34 +        set_introssss = [[[@{thms setl.intros[OF refl]}], [[]]],
   17.35 +          [[[]], [@{thms setr.intros[OF refl]}]]],
   17.36 +        set_cases = @{thms setl.cases[unfolded hypsubst_in_prems]
   17.37 +          setr.cases[unfolded hypsubst_in_prems]}},
   17.38       fp_co_induct_sugar =
   17.39         {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
   17.40          common_co_inducts = @{thms sum.induct},
   17.41 @@ -108,10 +110,10 @@
   17.42          co_rec_disc_iffs = [],
   17.43          co_rec_selss = [],
   17.44          co_rec_codes = [],
   17.45 -        co_rec_transfers = [],
   17.46 +        co_rec_transfers = @{thms case_sum_transfer},
   17.47          co_rec_o_maps = @{thms case_sum_o_map_sum},
   17.48 -        common_rel_co_inducts = [],
   17.49 -        rel_co_inducts = [],
   17.50 +        common_rel_co_inducts = @{thms rel_sum.inducts},
   17.51 +        rel_co_inducts = @{thms rel_sum.induct},
   17.52          common_set_inducts = [],
   17.53          set_inducts = []}}
   17.54    end;
   17.55 @@ -147,23 +149,25 @@
   17.56         {ctrXs_Tss = [ctr_Ts],
   17.57          ctr_defs = @{thms Pair_def_alt},
   17.58          ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
   17.59 -        ctr_transfers = [],
   17.60 -        case_transfers = [],
   17.61 +        ctr_transfers = @{thms Pair_transfer},
   17.62 +        case_transfers = @{thms case_prod_transfer},
   17.63          disc_transfers = [],
   17.64 -        sel_transfers = []},
   17.65 +        sel_transfers = @{thms fst_transfer snd_transfer}},
   17.66       fp_bnf_sugar =
   17.67         {map_thms = @{thms map_prod_simp},
   17.68          map_disc_iffs = [],
   17.69 -        map_selss = [],
   17.70 +        map_selss = [@{thms fst_map_prod snd_map_prod}],
   17.71          rel_injects = @{thms rel_prod_apply},
   17.72          rel_distincts = [],
   17.73 -        rel_sels = [],
   17.74 -        rel_intros = [],
   17.75 -        rel_cases = [],
   17.76 -        set_thms = [],
   17.77 -        set_selssss = [],
   17.78 -        set_introssss = [],
   17.79 -        set_cases = []},
   17.80 +        rel_sels = @{thms rel_prod_sel},
   17.81 +        rel_intros = @{thms rel_prod.intros},
   17.82 +        rel_cases = @{thms rel_prod.cases},
   17.83 +        set_thms = @{thms prod_set_simps},
   17.84 +        set_selssss = [[[@{thms fsts.intros}, []]], [[[], @{thms snds.intros}]]],
   17.85 +        set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, unfolded fst_conv]}, []]],
   17.86 +          [[[], @{thms snds.intros[of "(a, b)" for a b, unfolded snd_conv]}]]],
   17.87 +        set_cases = @{thms fsts.cases[unfolded eq_fst_iff ex_neg_all_pos]
   17.88 +          snds.cases[unfolded eq_snd_iff ex_neg_all_pos]}},
   17.89       fp_co_induct_sugar =
   17.90         {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
   17.91          common_co_inducts = @{thms prod.induct},
   17.92 @@ -174,10 +178,10 @@
   17.93          co_rec_disc_iffs = [],
   17.94          co_rec_selss = [],
   17.95          co_rec_codes = [],
   17.96 -        co_rec_transfers = [],
   17.97 +        co_rec_transfers = @{thms case_prod_transfer},
   17.98          co_rec_o_maps = @{thms case_prod_o_map_prod},
   17.99 -        common_rel_co_inducts = [],
  17.100 -        rel_co_inducts = [],
  17.101 +        common_rel_co_inducts = @{thms rel_prod.inducts},
  17.102 +        rel_co_inducts = @{thms rel_prod.induct},
  17.103          common_set_inducts = [],
  17.104          set_inducts = []}}
  17.105    end;
    18.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Nov 07 12:24:56 2014 +0100
    18.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Nov 07 11:28:37 2014 +0100
    18.3 @@ -62,7 +62,7 @@
    18.4  val rec_o_map_simps =
    18.5    @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def};
    18.6  
    18.7 -val size_gen_o_map_simps = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
    18.8 +val size_gen_o_map_simps = @{thms prod.inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
    18.9  
   18.10  fun mk_size_gen_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
   18.11    unfold_thms_tac ctxt [size_def] THEN
    19.1 --- a/src/HOL/Transfer.thy	Fri Nov 07 12:24:56 2014 +0100
    19.2 +++ b/src/HOL/Transfer.thy	Fri Nov 07 11:28:37 2014 +0100
    19.3 @@ -6,13 +6,9 @@
    19.4  section {* Generic theorem transfer using relations *}
    19.5  
    19.6  theory Transfer
    19.7 -imports Hilbert_Choice Metis Option
    19.8 +imports Hilbert_Choice Metis Basic_BNF_Least_Fixpoints
    19.9  begin
   19.10  
   19.11 -(* We import Option here although it's not needed here.
   19.12 -   By doing this, we avoid a diamond problem for BNF and
   19.13 -   FP sugar interpretation defined in this file. *)
   19.14 -
   19.15  subsection {* Relator for function space *}
   19.16  
   19.17  locale lifting_syntax
   19.18 @@ -453,11 +449,14 @@
   19.19  lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
   19.20    unfolding rel_fun_def by simp
   19.21  
   19.22 -lemma id_transfer [transfer_rule]: "(A ===> A) id id"
   19.23 -  unfolding rel_fun_def by simp
   19.24 +declare id_transfer [transfer_rule]
   19.25  
   19.26  declare comp_transfer [transfer_rule]
   19.27  
   19.28 +lemma curry_transfer [transfer_rule]:
   19.29 +  "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
   19.30 +  unfolding curry_def by transfer_prover
   19.31 +
   19.32  lemma fun_upd_transfer [transfer_rule]:
   19.33    assumes [transfer_rule]: "bi_unique A"
   19.34    shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"