equal
deleted
inserted
replaced
100 |
100 |
101 subsection {* Continuous function space is pointed *} |
101 subsection {* Continuous function space is pointed *} |
102 |
102 |
103 lemma UU_CFun: "\<bottom> \<in> CFun" |
103 lemma UU_CFun: "\<bottom> \<in> CFun" |
104 by (simp add: CFun_def inst_fun_pcpo cont_const) |
104 by (simp add: CFun_def inst_fun_pcpo cont_const) |
|
105 |
|
106 instance "->" :: (finite_po, finite_po) finite_po |
|
107 by (rule typedef_finite_po [OF type_definition_CFun]) |
|
108 |
|
109 instance "->" :: (finite_po, chfin) chfin |
|
110 by (rule typedef_chfin [OF type_definition_CFun less_CFun_def]) |
105 |
111 |
106 instance "->" :: (cpo, pcpo) pcpo |
112 instance "->" :: (cpo, pcpo) pcpo |
107 by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun]) |
113 by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun]) |
108 |
114 |
109 lemmas Rep_CFun_strict = |
115 lemmas Rep_CFun_strict = |