1.1 --- a/src/HOL/BNF/Basic_BNFs.thy	Wed Aug 14 00:15:03 2013 +0200
     1.2 +++ b/src/HOL/BNF/Basic_BNFs.thy	Tue Aug 13 18:22:55 2013 +0200
     1.3 @@ -48,11 +48,6 @@
     1.4  
     1.5  lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
     1.6  
     1.7 -definition sum_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'c \<Rightarrow> 'b + 'd \<Rightarrow> bool" where
     1.8 -"sum_rel \<phi> \<psi> x y =
     1.9 - (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
    1.10 -          | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
    1.11 -
    1.12  bnf sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
    1.13  proof -
    1.14    show "sum_map id id = id" by (rule sum_map.id)
    1.15 @@ -153,9 +148,6 @@
    1.16  
    1.17  lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
    1.18  
    1.19 -definition prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" where
    1.20 -"prod_rel \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> \<phi> a1 a2 \<and> \<psi> b1 b2)"
    1.21 -
    1.22  bnf map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. natLeq" [Pair] prod_rel
    1.23  proof (unfold prod_set_defs)
    1.24    show "map_pair id id = id" by (rule map_pair.id)

     2.1 --- a/src/HOL/BNF/Examples/Process.thy	Wed Aug 14 00:15:03 2013 +0200
     2.2 +++ b/src/HOL/BNF/Examples/Process.thy	Tue Aug 13 18:22:55 2013 +0200
     2.3 @@ -11,8 +11,6 @@
     2.4  imports "../BNF"
     2.5  begin
     2.6  
     2.7 -hide_fact (open) Lifting_Product.prod_rel_def
     2.8 -
     2.9  codatatype 'a process =
    2.10    isAction: Action (prefOf: 'a) (contOf: "'a process") |
    2.11    isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process")

     3.1 --- a/src/HOL/BNF/More_BNFs.thy	Wed Aug 14 00:15:03 2013 +0200
     3.2 +++ b/src/HOL/BNF/More_BNFs.thy	Tue Aug 13 18:22:55 2013 +0200
     3.3 @@ -68,7 +68,7 @@
     3.4    show "option_rel R =
     3.5          (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
     3.6           Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
     3.7 -  unfolding option_rel_unfold Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
     3.8 +  unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
     3.9    by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
    3.10             split: option.splits)
    3.11  qed

     4.1 --- a/src/HOL/Library/Mapping.thy	Wed Aug 14 00:15:03 2013 +0200
     4.2 +++ b/src/HOL/Library/Mapping.thy	Tue Aug 13 18:22:55 2013 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4  definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None"
     4.5  
     4.6  lemma [transfer_rule]: "(option_rel A ===> op=) equal_None equal_None" 
     4.7 -unfolding fun_rel_def option_rel_unfold equal_None_def by (auto split: option.split)
     4.8 +unfolding fun_rel_def option_rel_def equal_None_def by (auto split: option.split)
     4.9  
    4.10  lemma dom_transfer:
    4.11    assumes [transfer_rule]: "bi_total A"

     5.1 --- a/src/HOL/Library/Quotient_Option.thy	Wed Aug 14 00:15:03 2013 +0200
     5.2 +++ b/src/HOL/Library/Quotient_Option.thy	Tue Aug 13 18:22:55 2013 +0200
     5.3 @@ -12,11 +12,11 @@
     5.4  
     5.5  lemma option_rel_map1:
     5.6    "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
     5.7 -  by (simp add: option_rel_unfold split: option.split)
     5.8 +  by (simp add: option_rel_def split: option.split)
     5.9  
    5.10  lemma option_rel_map2:
    5.11    "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
    5.12 -  by (simp add: option_rel_unfold split: option.split)
    5.13 +  by (simp add: option_rel_def split: option.split)
    5.14  
    5.15  lemma option_map_id [id_simps]:
    5.16    "Option.map id = id"
    5.17 @@ -24,15 +24,15 @@
    5.18  
    5.19  lemma option_rel_eq [id_simps]:
    5.20    "option_rel (op =) = (op =)"
    5.21 -  by (simp add: option_rel_unfold fun_eq_iff split: option.split)
    5.22 +  by (simp add: option_rel_def fun_eq_iff split: option.split)
    5.23  
    5.24  lemma option_symp:
    5.25    "symp R \<Longrightarrow> symp (option_rel R)"
    5.26 -  unfolding symp_def split_option_all option_rel.simps by fast
    5.27 +  unfolding symp_def split_option_all option_rel_simps by fast
    5.28  
    5.29  lemma option_transp:
    5.30    "transp R \<Longrightarrow> transp (option_rel R)"
    5.31 -  unfolding transp_def split_option_all option_rel.simps by fast
    5.32 +  unfolding transp_def split_option_all option_rel_simps by fast
    5.33  
    5.34  lemma option_equivp [quot_equiv]:
    5.35    "equivp R \<Longrightarrow> equivp (option_rel R)"
    5.36 @@ -44,7 +44,7 @@
    5.37    apply (rule Quotient3I)
    5.38    apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
    5.39    using Quotient3_rel [OF assms]
    5.40 -  apply (simp add: option_rel_unfold split: option.split)
    5.41 +  apply (simp add: option_rel_def split: option.split)
    5.42    done
    5.43  
    5.44  declare [[mapQ3 option = (option_rel, option_quotient)]]

     6.1 --- a/src/HOL/Library/Quotient_Sum.thy	Wed Aug 14 00:15:03 2013 +0200
     6.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Aug 13 18:22:55 2013 +0200
     6.3 @@ -12,11 +12,11 @@
     6.4  
     6.5  lemma sum_rel_map1:
     6.6    "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"
     6.7 -  by (simp add: sum_rel_unfold split: sum.split)
     6.8 +  by (simp add: sum_rel_def split: sum.split)
     6.9  
    6.10  lemma sum_rel_map2:
    6.11    "sum_rel R1 R2 x (sum_map f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
    6.12 -  by (simp add: sum_rel_unfold split: sum.split)
    6.13 +  by (simp add: sum_rel_def split: sum.split)
    6.14  
    6.15  lemma sum_map_id [id_simps]:
    6.16    "sum_map id id = id"
    6.17 @@ -24,15 +24,15 @@
    6.18  
    6.19  lemma sum_rel_eq [id_simps]:
    6.20    "sum_rel (op =) (op =) = (op =)"
    6.21 -  by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
    6.22 +  by (simp add: sum_rel_def fun_eq_iff split: sum.split)
    6.23  
    6.24  lemma sum_symp:
    6.25    "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    6.26 -  unfolding symp_def split_sum_all sum_rel.simps by fast
    6.27 +  unfolding symp_def split_sum_all sum_rel_simps by fast
    6.28  
    6.29  lemma sum_transp:
    6.30    "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
    6.31 -  unfolding transp_def split_sum_all sum_rel.simps by fast
    6.32 +  unfolding transp_def split_sum_all sum_rel_simps by fast
    6.33  
    6.34  lemma sum_equivp [quot_equiv]:
    6.35    "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    6.36 @@ -46,7 +46,7 @@
    6.37    apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
    6.38      Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
    6.39    using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
    6.40 -  apply (simp add: sum_rel_unfold comp_def split: sum.split)
    6.41 +  apply (simp add: sum_rel_def comp_def split: sum.split)
    6.42    done
    6.43  
    6.44  declare [[mapQ3 sum = (sum_rel, sum_quotient)]]

     7.1 --- a/src/HOL/Lifting_Option.thy	Wed Aug 14 00:15:03 2013 +0200
     7.2 +++ b/src/HOL/Lifting_Option.thy	Tue Aug 13 18:22:55 2013 +0200
     7.3 @@ -5,52 +5,45 @@
     7.4  header {* Setup for Lifting/Transfer for the option type *}
     7.5  
     7.6  theory Lifting_Option
     7.7 -imports Lifting FunDef
     7.8 +imports Lifting
     7.9  begin
    7.10  
    7.11  subsection {* Relator and predicator properties *}
    7.12  
    7.13 -fun
    7.14 +definition
    7.15    option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
    7.16  where
    7.17 -  "option_rel R None None = True"
    7.18 -| "option_rel R (Some x) None = False"
    7.19 -| "option_rel R None (Some x) = False"
    7.20 -| "option_rel R (Some x) (Some y) = R x y"
    7.21 -
    7.22 -lemma option_rel_unfold:
    7.23    "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
    7.24      | (Some x, Some y) \<Rightarrow> R x y
    7.25      | _ \<Rightarrow> False)"
    7.26 -  by (cases x) (cases y, simp_all)+
    7.27  
    7.28 -fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
    7.29 -where
    7.30 -  "option_pred R None = True"
    7.31 -| "option_pred R (Some x) = R x"
    7.32 +lemma option_rel_simps[simp]:
    7.33 +  "option_rel R None None = True"
    7.34 +  "option_rel R (Some x) None = False"
    7.35 +  "option_rel R None (Some y) = False"
    7.36 +  "option_rel R (Some x) (Some y) = R x y"
    7.37 +  unfolding option_rel_def by simp_all
    7.38  
    7.39 -lemma option_pred_unfold:
    7.40 -  "option_pred P x = (case x of None \<Rightarrow> True
    7.41 -    | Some x \<Rightarrow> P x)"
    7.42 -by (cases x) simp_all
    7.43 +abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
    7.44 +  "option_pred \<equiv> option_case True"
    7.45  
    7.46  lemma option_rel_eq [relator_eq]:
    7.47    "option_rel (op =) = (op =)"
    7.48 -  by (simp add: option_rel_unfold fun_eq_iff split: option.split)
    7.49 +  by (simp add: option_rel_def fun_eq_iff split: option.split)
    7.50  
    7.51  lemma option_rel_mono[relator_mono]:
    7.52    assumes "A \<le> B"
    7.53    shows "(option_rel A) \<le> (option_rel B)"
    7.54 -using assms by (auto simp: option_rel_unfold split: option.splits)
    7.55 +using assms by (auto simp: option_rel_def split: option.splits)
    7.56  
    7.57  lemma option_rel_OO[relator_distr]:
    7.58    "(option_rel A) OO (option_rel B) = option_rel (A OO B)"
    7.59 -by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split)
    7.60 +by (rule ext)+ (auto simp: option_rel_def OO_def split: option.split)
    7.61  
    7.62  lemma Domainp_option[relator_domain]:
    7.63    assumes "Domainp A = P"
    7.64    shows "Domainp (option_rel A) = (option_pred P)"
    7.65 -using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def]
    7.66 +using assms unfolding Domainp_iff[abs_def] option_rel_def[abs_def]
    7.67  by (auto iff: fun_eq_iff split: option.split)
    7.68  
    7.69  lemma reflp_option_rel[reflexivity_rule]:
    7.70 @@ -91,7 +84,7 @@
    7.71    assumes "Quotient R Abs Rep T"
    7.72    shows "Quotient (option_rel R) (Option.map Abs)
    7.73      (Option.map Rep) (option_rel T)"
    7.74 -  using assms unfolding Quotient_alt_def option_rel_unfold
    7.75 +  using assms unfolding Quotient_alt_def option_rel_def
    7.76    by (simp split: option.split)
    7.77  
    7.78  subsection {* Transfer rules for the Transfer package *}

     8.1 --- a/src/HOL/Lifting_Sum.thy	Wed Aug 14 00:15:03 2013 +0200
     8.2 +++ b/src/HOL/Lifting_Sum.thy	Tue Aug 13 18:22:55 2013 +0200
     8.3 @@ -5,59 +5,52 @@
     8.4  header {* Setup for Lifting/Transfer for the sum type *}
     8.5  
     8.6  theory Lifting_Sum
     8.7 -imports Lifting FunDef
     8.8 +imports Lifting
     8.9  begin
    8.10  
    8.11  subsection {* Relator and predicator properties *}
    8.12  
    8.13 -fun
    8.14 -  sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
    8.15 +definition
    8.16 +   sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
    8.17  where
    8.18 +   "sum_rel R1 R2 x y =
    8.19 +     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    8.20 +     | (Inr x, Inr y) \<Rightarrow> R2 x y
    8.21 +     | _ \<Rightarrow> False)"
    8.22 +
    8.23 +lemma sum_rel_simps[simp]:
    8.24    "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    8.25 -| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    8.26 -| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    8.27 -| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    8.28 +  "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    8.29 +  "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    8.30 +  "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    8.31 +  unfolding sum_rel_def by simp_all
    8.32  
    8.33 -lemma sum_rel_unfold:
    8.34 -  "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    8.35 -    | (Inr x, Inr y) \<Rightarrow> R2 x y
    8.36 -    | _ \<Rightarrow> False)"
    8.37 -  by (cases x) (cases y, simp_all)+
    8.38 -
    8.39 -fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
    8.40 -where
    8.41 -  "sum_pred P1 P2 (Inl a) = P1 a"
    8.42 -| "sum_pred P1 P2 (Inr a) = P2 a"
    8.43 -
    8.44 -lemma sum_pred_unfold:
    8.45 -  "sum_pred P1 P2 x = (case x of Inl x \<Rightarrow> P1 x
    8.46 -    | Inr x \<Rightarrow> P2 x)"
    8.47 -by (cases x) simp_all
    8.48 +abbreviation (input) "sum_pred \<equiv> sum_case"
    8.49  
    8.50  lemma sum_rel_eq [relator_eq]:
    8.51    "sum_rel (op =) (op =) = (op =)"
    8.52 -  by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
    8.53 +  by (simp add: sum_rel_def fun_eq_iff split: sum.split)
    8.54  
    8.55  lemma sum_rel_mono[relator_mono]:
    8.56    assumes "A \<le> C"
    8.57    assumes "B \<le> D"
    8.58    shows "(sum_rel A B) \<le> (sum_rel C D)"
    8.59 -using assms by (auto simp: sum_rel_unfold split: sum.splits)
    8.60 +using assms by (auto simp: sum_rel_def split: sum.splits)
    8.61  
    8.62  lemma sum_rel_OO[relator_distr]:
    8.63    "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
    8.64 -by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
    8.65 +by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split)
    8.66  
    8.67  lemma Domainp_sum[relator_domain]:
    8.68    assumes "Domainp R1 = P1"
    8.69    assumes "Domainp R2 = P2"
    8.70    shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
    8.71  using assms
    8.72 -by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
    8.73 +by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
    8.74  
    8.75  lemma reflp_sum_rel[reflexivity_rule]:
    8.76    "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    8.77 -  unfolding reflp_def split_sum_all sum_rel.simps by fast
    8.78 +  unfolding reflp_def split_sum_all sum_rel_simps by fast
    8.79  
    8.80  lemma left_total_sum_rel[reflexivity_rule]:
    8.81    "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
    8.82 @@ -85,7 +78,7 @@
    8.83  
    8.84  lemma sum_invariant_commute [invariant_commute]: 
    8.85    "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
    8.86 -  by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split)
    8.87 +  by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_def split: sum.split)
    8.88  
    8.89  subsection {* Quotient theorem for the Lifting package *}
    8.90  
    8.91 @@ -111,7 +104,7 @@
    8.92  
    8.93  lemma sum_case_transfer [transfer_rule]:
    8.94    "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case"
    8.95 -  unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split)
    8.96 +  unfolding fun_rel_def sum_rel_def by (simp split: sum.split)
    8.97  
    8.98  end
    8.99