equal
deleted
inserted
replaced
101 \medskip Two specific lemmas for the combination of LCF and HOL |
101 \medskip Two specific lemmas for the combination of LCF and HOL |
102 terms. |
102 terms. |
103 *} |
103 *} |
104 |
104 |
105 lemma cont_Rep_CFun_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)" |
105 lemma cont_Rep_CFun_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)" |
106 by (rule cont2cont_Rep_CFun [THEN cont2cont_CF1L]) |
106 by (rule cont2cont_Rep_CFun [THEN cont2cont_fun]) |
107 |
107 |
108 lemma cont_Rep_CFun_app_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)" |
108 lemma cont_Rep_CFun_app_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)" |
109 by (rule cont_Rep_CFun_app [THEN cont2cont_CF1L]) |
109 by (rule cont_Rep_CFun_app [THEN cont2cont_fun]) |
110 |
110 |
111 subsection {* Further operations *} |
111 subsection {* Further operations *} |
112 |
112 |
113 constdefs |
113 constdefs |
114 flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) |
114 flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) |
126 |
126 |
127 lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)" |
127 lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)" |
128 apply (induct x) |
128 apply (induct x) |
129 apply simp |
129 apply simp |
130 apply simp |
130 apply simp |
131 apply (rule cont_id [THEN cont2cont_CF1L]) |
131 apply (rule cont_id [THEN cont2cont_fun]) |
132 done |
132 done |
133 |
133 |
134 lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)" |
134 lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)" |
135 apply (rule flatdom_strict2cont) |
135 apply (rule flatdom_strict2cont) |
136 apply simp |
136 apply simp |