equal
deleted
inserted
replaced
145 rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" |
145 rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" |
146 by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite) |
146 by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite) |
147 |
147 |
148 definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)" |
148 definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)" |
149 |
149 |
|
150 lemma id_bnf_comp_apply: "id_bnf_comp x = x" |
|
151 unfolding id_bnf_comp_def by simp |
|
152 |
150 bnf ID: 'a |
153 bnf ID: 'a |
151 map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
154 map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
152 sets: "\<lambda>x. {x}" |
155 sets: "\<lambda>x. {x}" |
153 bd: natLeq |
156 bd: natLeq |
154 rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
157 rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |