src/HOL/Basic_BNFs.thy
 changeset 55943 5c2df04e97d1 parent 55935 8f20d09d294e child 55944 7ab8f003fe41
```     1.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:14:09 2014 +0100
1.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:25:21 2014 +0100
1.3 @@ -22,26 +22,26 @@
1.4  lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
1.5
1.6  definition
1.7 -   sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
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  where
1.10 -   "sum_rel R1 R2 x y =
1.11 +   "rel_sum R1 R2 x y =
1.12       (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
1.13       | (Inr x, Inr y) \<Rightarrow> R2 x y
1.14       | _ \<Rightarrow> False)"
1.15
1.16 -lemma sum_rel_simps[simp]:
1.17 -  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
1.18 -  "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
1.19 -  "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
1.20 -  "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
1.21 -  unfolding sum_rel_def by simp_all
1.22 +lemma rel_sum_simps[simp]:
1.23 +  "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
1.24 +  "rel_sum R1 R2 (Inl a1) (Inr b2) = False"
1.25 +  "rel_sum R1 R2 (Inr a2) (Inl b1) = False"
1.26 +  "rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
1.27 +  unfolding rel_sum_def by simp_all
1.28
1.29  bnf "'a + 'b"
1.30    map: map_sum
1.31    sets: setl setr
1.32    bd: natLeq
1.33    wits: Inl Inr
1.34 -  rel: sum_rel
1.35 +  rel: rel_sum
1.36  proof -
1.37    show "map_sum id id = id" by (rule map_sum.id)
1.38  next
1.39 @@ -84,14 +84,14 @@
1.40      by (simp add: setr_def split: sum.split)
1.41  next
1.42    fix R1 R2 S1 S2
1.43 -  show "sum_rel R1 R2 OO sum_rel S1 S2 \<le> sum_rel (R1 OO S1) (R2 OO S2)"
1.44 -    by (auto simp: sum_rel_def split: sum.splits)
1.45 +  show "rel_sum R1 R2 OO rel_sum S1 S2 \<le> rel_sum (R1 OO S1) (R2 OO S2)"
1.46 +    by (auto simp: rel_sum_def split: sum.splits)
1.47  next
1.48    fix R S
1.49 -  show "sum_rel R S =
1.50 +  show "rel_sum R S =
1.51          (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
1.52          Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
1.53 -  unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
1.54 +  unfolding setl_def setr_def rel_sum_def Grp_def relcompp.simps conversep.simps fun_eq_iff
1.55    by (fastforce split: sum.splits)
1.56  qed (auto simp: sum_set_defs)
1.57
```