src/HOL/Basic_BNFs.thy
changeset 67091 1393c2340eec
parent 62335 e85c42f4f30a
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Basic_BNFs.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -19,8 +19,8 @@
     1.4    "s = Inr x \<Longrightarrow> x \<in> setr s"
     1.5  
     1.6  lemma sum_set_defs[code]:
     1.7 -  "setl = (\<lambda>x. case x of Inl z => {z} | _ => {})"
     1.8 -  "setr = (\<lambda>x. case x of Inr z => {z} | _ => {})"
     1.9 +  "setl = (\<lambda>x. case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {})"
    1.10 +  "setr = (\<lambda>x. case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {})"
    1.11    by (auto simp: fun_eq_iff intro: setl.intros setr.intros elim: setl.cases setr.cases split: sum.splits)
    1.12  
    1.13  lemma rel_sum_simps[code, simp]:
    1.14 @@ -52,7 +52,7 @@
    1.15    show "map_sum id id = id" by (rule map_sum.id)
    1.16  next
    1.17    fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
    1.18 -  show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2"
    1.19 +  show "map_sum (g1 \<circ> f1) (g2 \<circ> f2) = map_sum g1 g2 \<circ> map_sum f1 f2"
    1.20      by (rule map_sum.comp[symmetric])
    1.21  next
    1.22    fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
    1.23 @@ -66,11 +66,11 @@
    1.24    qed
    1.25  next
    1.26    fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    1.27 -  show "setl o map_sum f1 f2 = image f1 o setl"
    1.28 +  show "setl \<circ> map_sum f1 f2 = image f1 \<circ> setl"
    1.29      by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split)
    1.30  next
    1.31    fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    1.32 -  show "setr o map_sum f1 f2 = image f2 o setr"
    1.33 +  show "setr \<circ> map_sum f1 f2 = image f2 \<circ> setr"
    1.34      by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split)
    1.35  next
    1.36    show "card_order natLeq" by (rule natLeq_card_order)
    1.37 @@ -149,7 +149,7 @@
    1.38    show "map_prod id id = id" by (rule map_prod.id)
    1.39  next
    1.40    fix f1 f2 g1 g2
    1.41 -  show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2"
    1.42 +  show "map_prod (g1 \<circ> f1) (g2 \<circ> f2) = map_prod g1 g2 \<circ> map_prod f1 f2"
    1.43      by (rule map_prod.comp[symmetric])
    1.44  next
    1.45    fix x f1 f2 g1 g2
    1.46 @@ -157,11 +157,11 @@
    1.47    thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp
    1.48  next
    1.49    fix f1 f2
    1.50 -  show "(\<lambda>x. {fst x}) o map_prod f1 f2 = image f1 o (\<lambda>x. {fst x})"
    1.51 +  show "(\<lambda>x. {fst x}) \<circ> map_prod f1 f2 = image f1 \<circ> (\<lambda>x. {fst x})"
    1.52      by (rule ext, unfold o_apply) simp
    1.53  next
    1.54    fix f1 f2
    1.55 -  show "(\<lambda>x. {snd x}) o map_prod f1 f2 = image f2 o (\<lambda>x. {snd x})"
    1.56 +  show "(\<lambda>x. {snd x}) \<circ> map_prod f1 f2 = image f2 \<circ> (\<lambda>x. {snd x})"
    1.57      by (rule ext, unfold o_apply) simp
    1.58  next
    1.59    show "card_order natLeq" by (rule natLeq_card_order)