31 begin |
31 begin |
32 |
32 |
33 lemma swap: "iso rep abs" |
33 lemma swap: "iso rep abs" |
34 by (rule iso.intro [OF rep_iso abs_iso]) |
34 by (rule iso.intro [OF rep_iso abs_iso]) |
35 |
35 |
36 lemma abs_less: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)" |
36 lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)" |
37 proof |
37 proof |
38 assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" |
38 assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" |
39 then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg) |
39 then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg) |
40 then show "x \<sqsubseteq> y" by simp |
40 then show "x \<sqsubseteq> y" by simp |
41 next |
41 next |
42 assume "x \<sqsubseteq> y" |
42 assume "x \<sqsubseteq> y" |
43 then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg) |
43 then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg) |
44 qed |
44 qed |
45 |
45 |
46 lemma rep_less: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)" |
46 lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)" |
47 by (rule iso.abs_less [OF swap]) |
47 by (rule iso.abs_below [OF swap]) |
48 |
48 |
49 lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)" |
49 lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)" |
50 by (simp add: po_eq_conv abs_less) |
50 by (simp add: po_eq_conv abs_below) |
51 |
51 |
52 lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)" |
52 lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)" |
53 by (rule iso.abs_eq [OF swap]) |
53 by (rule iso.abs_eq [OF swap]) |
54 |
54 |
55 lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>" |
55 lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>" |
89 lemma (in iso) compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x" |
89 lemma (in iso) compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x" |
90 proof (unfold compact_def) |
90 proof (unfold compact_def) |
91 assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)" |
91 assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)" |
92 with cont_Rep_CFun2 |
92 with cont_Rep_CFun2 |
93 have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst) |
93 have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst) |
94 then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_less by simp |
94 then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp |
95 qed |
95 qed |
96 |
96 |
97 lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x" |
97 lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x" |
98 by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms) |
98 by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms) |
99 |
99 |