7 theory Powerdomains |
7 theory Powerdomains |
8 imports ConvexPD Domain |
8 imports ConvexPD Domain |
9 begin |
9 begin |
10 |
10 |
11 lemma isodefl_upper: |
11 lemma isodefl_upper: |
12 "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_sfp\<cdot>t)" |
12 "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)" |
13 apply (rule isodeflI) |
13 apply (rule isodeflI) |
14 apply (simp add: cast_upper_sfp cast_isodefl) |
14 apply (simp add: cast_upper_defl cast_isodefl) |
15 apply (simp add: emb_upper_pd_def prj_upper_pd_def) |
15 apply (simp add: emb_upper_pd_def prj_upper_pd_def) |
16 apply (simp add: upper_map_map) |
16 apply (simp add: upper_map_map) |
17 done |
17 done |
18 |
18 |
19 lemma isodefl_lower: |
19 lemma isodefl_lower: |
20 "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_sfp\<cdot>t)" |
20 "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)" |
21 apply (rule isodeflI) |
21 apply (rule isodeflI) |
22 apply (simp add: cast_lower_sfp cast_isodefl) |
22 apply (simp add: cast_lower_defl cast_isodefl) |
23 apply (simp add: emb_lower_pd_def prj_lower_pd_def) |
23 apply (simp add: emb_lower_pd_def prj_lower_pd_def) |
24 apply (simp add: lower_map_map) |
24 apply (simp add: lower_map_map) |
25 done |
25 done |
26 |
26 |
27 lemma isodefl_convex: |
27 lemma isodefl_convex: |
28 "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_sfp\<cdot>t)" |
28 "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)" |
29 apply (rule isodeflI) |
29 apply (rule isodeflI) |
30 apply (simp add: cast_convex_sfp cast_isodefl) |
30 apply (simp add: cast_convex_defl cast_isodefl) |
31 apply (simp add: emb_convex_pd_def prj_convex_pd_def) |
31 apply (simp add: emb_convex_pd_def prj_convex_pd_def) |
32 apply (simp add: convex_map_map) |
32 apply (simp add: convex_map_map) |
33 done |
33 done |
34 |
34 |
35 subsection {* Domain package setup for powerdomains *} |
35 subsection {* Domain package setup for powerdomains *} |
36 |
36 |
37 setup {* |
37 setup {* |
38 fold Domain_Isomorphism.add_type_constructor |
38 fold Domain_Isomorphism.add_type_constructor |
39 [(@{type_name "upper_pd"}, @{term upper_sfp}, @{const_name upper_map}, |
39 [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}, |
40 @{thm SFP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}, |
40 @{thm DEFL_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}, |
41 @{thm deflation_upper_map}), |
41 @{thm deflation_upper_map}), |
42 |
42 |
43 (@{type_name "lower_pd"}, @{term lower_sfp}, @{const_name lower_map}, |
43 (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}, |
44 @{thm SFP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}, |
44 @{thm DEFL_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}, |
45 @{thm deflation_lower_map}), |
45 @{thm deflation_lower_map}), |
46 |
46 |
47 (@{type_name "convex_pd"}, @{term convex_sfp}, @{const_name convex_map}, |
47 (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map}, |
48 @{thm SFP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID}, |
48 @{thm DEFL_convex}, @{thm isodefl_convex}, @{thm convex_map_ID}, |
49 @{thm deflation_convex_map})] |
49 @{thm deflation_convex_map})] |
50 *} |
50 *} |
51 |
51 |
52 end |
52 end |