equal
deleted
inserted
replaced
8 |
8 |
9 section \<open>Composition of Bounded Natural Functors\<close> |
9 section \<open>Composition of Bounded Natural Functors\<close> |
10 |
10 |
11 theory BNF_Composition |
11 theory BNF_Composition |
12 imports BNF_Def |
12 imports BNF_Def |
13 keywords |
|
14 "copy_bnf" :: thy_defn and |
|
15 "lift_bnf" :: thy_goal_defn |
|
16 begin |
13 begin |
17 |
14 |
18 lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" |
15 lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" |
19 by simp |
16 by simp |
20 |
17 |
178 lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV" |
175 lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV" |
179 unfolding id_bnf_def by unfold_locales auto |
176 unfolding id_bnf_def by unfold_locales auto |
180 |
177 |
181 ML_file \<open>Tools/BNF/bnf_comp_tactics.ML\<close> |
178 ML_file \<open>Tools/BNF/bnf_comp_tactics.ML\<close> |
182 ML_file \<open>Tools/BNF/bnf_comp.ML\<close> |
179 ML_file \<open>Tools/BNF/bnf_comp.ML\<close> |
183 ML_file \<open>Tools/BNF/bnf_lift.ML\<close> |
|
184 |
180 |
185 hide_fact |
181 hide_fact |
186 DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0 |
182 DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0 |
187 DEADID.map_cong_simp DEADID.map_id DEADID.map_id0 DEADID.map_ident DEADID.map_transfer |
183 DEADID.map_cong_simp DEADID.map_id DEADID.map_id0 DEADID.map_ident DEADID.map_transfer |
188 DEADID.rel_Grp DEADID.rel_compp DEADID.rel_compp_Grp DEADID.rel_conversep DEADID.rel_eq |
184 DEADID.rel_Grp DEADID.rel_compp DEADID.rel_compp_Grp DEADID.rel_conversep DEADID.rel_eq |