equal
deleted
inserted
replaced
307 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo) |
307 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo) |
308 |
308 |
309 lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x" |
309 lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x" |
310 by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 ) |
310 by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 ) |
311 |
311 |
312 lemma fup3: "fup\<cdot>up\<cdot>x = x" |
312 lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x" |
313 by (rule_tac p=x in upE1, simp_all) |
313 by (rule_tac p=x in upE1, simp_all) |
314 |
314 |
315 end |
315 end |