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 lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex |
|
38 lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID |
|
39 lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex |
|
40 |
|
41 lemmas [domain_deflation] = |
|
42 deflation_upper_map deflation_lower_map deflation_convex_map |
|
43 |
37 setup {* |
44 setup {* |
38 fold Domain_Isomorphism.add_type_constructor |
45 fold Domain_Isomorphism.add_type_constructor |
39 [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}, |
46 [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}), |
40 @{thm DEFL_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}, |
47 (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}), |
41 @{thm deflation_upper_map}), |
48 (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map})] |
42 |
|
43 (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}, |
|
44 @{thm DEFL_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}, |
|
45 @{thm deflation_lower_map}), |
|
46 |
|
47 (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map}, |
|
48 @{thm DEFL_convex}, @{thm isodefl_convex}, @{thm convex_map_ID}, |
|
49 @{thm deflation_convex_map})] |
|
50 *} |
49 *} |
51 |
50 |
52 end |
51 end |