src/HOL/Basic_BNFs.thy
changeset 55083 0a689157e3ce
parent 55075 b3d0a02a756d
child 55084 8ee9aabb2bca
     1.1 --- a/src/HOL/Basic_BNFs.thy	Mon Jan 20 20:00:33 2014 +0100
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Mon Jan 20 20:21:12 2014 +0100
     1.3 @@ -12,8 +12,6 @@
     1.4  theory Basic_BNFs
     1.5  imports BNF_Def
     1.6     (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
     1.7 -  Lifting_Sum
     1.8 -  Lifting_Product
     1.9  begin
    1.10  
    1.11  bnf ID: 'a
    1.12 @@ -42,6 +40,21 @@
    1.13  
    1.14  lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
    1.15  
    1.16 +definition
    1.17 +   sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
    1.18 +where
    1.19 +   "sum_rel R1 R2 x y =
    1.20 +     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    1.21 +     | (Inr x, Inr y) \<Rightarrow> R2 x y
    1.22 +     | _ \<Rightarrow> False)"
    1.23 +
    1.24 +lemma sum_rel_simps[simp]:
    1.25 +  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    1.26 +  "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    1.27 +  "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    1.28 +  "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    1.29 +  unfolding sum_rel_def by simp_all
    1.30 +
    1.31  bnf "'a + 'b"
    1.32    map: sum_map
    1.33    sets: setl setr
    1.34 @@ -109,6 +122,15 @@
    1.35  
    1.36  lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
    1.37  
    1.38 +definition
    1.39 +  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
    1.40 +where
    1.41 +  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    1.42 +
    1.43 +lemma prod_rel_apply [simp]:
    1.44 +  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.45 +  by (simp add: prod_rel_def)
    1.46 +
    1.47  bnf "'a \<times> 'b"
    1.48    map: map_pair
    1.49    sets: fsts snds