equal
deleted
inserted
replaced
484 by (induct xss rule: upper_pd_induct, simp_all) |
484 by (induct xss rule: upper_pd_induct, simp_all) |
485 |
485 |
486 lemma upper_map_approx: "upper_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs" |
486 lemma upper_map_approx: "upper_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs" |
487 by (induct xs rule: upper_pd_induct, simp_all) |
487 by (induct xs rule: upper_pd_induct, simp_all) |
488 |
488 |
|
489 lemma ep_pair_upper_map: "ep_pair e p \<Longrightarrow> ep_pair (upper_map\<cdot>e) (upper_map\<cdot>p)" |
|
490 apply default |
|
491 apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse) |
|
492 apply (induct_tac y rule: upper_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun) |
|
493 done |
|
494 |
|
495 lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)" |
|
496 apply default |
|
497 apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem) |
|
498 apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.below monofun_cfun) |
|
499 done |
|
500 |
489 end |
501 end |