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