author  huffman 
Sat, 27 Nov 2010 16:08:10 0800  
changeset 40774  0437dbc127b3 
parent 40737  src/HOLCF/Powerdomains.thy@2037021f034f 
child 41289  f655912ac235 
permissions  rwrr 
35473  1 
(* Title: HOLCF/Powerdomains.thy 
2 
Author: Brian Huffman 

3 
*) 

4 

5 
header {* Powerdomains *} 

6 

7 
theory Powerdomains 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39973
diff
changeset

8 
imports ConvexPD Domain 
35473  9 
begin 
10 

11 
lemma isodefl_upper: 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset

12 
"isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)" 
35473  13 
apply (rule isodeflI) 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset

14 
apply (simp add: cast_upper_defl cast_isodefl) 
35473  15 
apply (simp add: emb_upper_pd_def prj_upper_pd_def) 
16 
apply (simp add: upper_map_map) 

17 
done 

18 

19 
lemma isodefl_lower: 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset

20 
"isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)" 
35473  21 
apply (rule isodeflI) 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset

22 
apply (simp add: cast_lower_defl cast_isodefl) 
35473  23 
apply (simp add: emb_lower_pd_def prj_lower_pd_def) 
24 
apply (simp add: lower_map_map) 

25 
done 

26 

27 
lemma isodefl_convex: 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset

28 
"isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)" 
35473  29 
apply (rule isodeflI) 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset

30 
apply (simp add: cast_convex_defl cast_isodefl) 
35473  31 
apply (simp add: emb_convex_pd_def prj_convex_pd_def) 
32 
apply (simp add: convex_map_map) 

33 
done 

34 

35 
subsection {* Domain package setup for powerdomains *} 

36 

40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset

37 
lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex 
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset

38 
lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID 
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset

39 
lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex 
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset

40 

366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset

41 
lemmas [domain_deflation] = 
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset

42 
deflation_upper_map deflation_lower_map deflation_convex_map 
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
39989
diff
changeset

43 

35473  44 
setup {* 
40737
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset

45 
fold Domain_Take_Proofs.add_rec_type 
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset

46 
[(@{type_name "upper_pd"}, [true]), 
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset

47 
(@{type_name "lower_pd"}, [true]), 
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40487
diff
changeset

48 
(@{type_name "convex_pd"}, [true])] 
35473  49 
*} 
50 

51 
end 