author  wenzelm 
Tue, 29 Mar 2011 17:47:11 +0200  
changeset 42151  4da4fc77664b 
parent 41430  1aa23e9f2c87 
child 42814  5af15f1e2ef6 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Lift.thy 
12026  2 
Author: Olaf Mueller 
2640  3 
*) 
4 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12026
diff
changeset

5 
header {* Lifting types of class type to flat pcpo's *} 
12026  6 

15577  7 
theory Lift 
40086  8 
imports Discrete Up 
15577  9 
begin 
12026  10 

36452  11 
default_sort type 
12026  12 

40082  13 
pcpodef (open) 'a lift = "UNIV :: 'a discr u set" 
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
27311
diff
changeset

14 
by simp_all 
12026  15 

16748  16 
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] 
12026  17 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset

18 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset

19 
Def :: "'a \<Rightarrow> 'a lift" where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset

20 
"Def x = Abs_lift (up\<cdot>(Discr x))" 
12026  21 

22 
subsection {* Lift as a datatype *} 

23 

16748  24 
lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y" 
25 
apply (induct y) 

16755
fd02f9d06e43
renamed upE1 to upE; added simp rule cont2cont_flift1
huffman
parents:
16749
diff
changeset

26 
apply (rule_tac p=y in upE) 
16748  27 
apply (simp add: Abs_lift_strict) 
28 
apply (case_tac x) 

29 
apply (simp add: Def_def) 

30 
done 

12026  31 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26963
diff
changeset

32 
rep_datatype "\<bottom>\<Colon>'a lift" Def 
40082  33 
by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo) 
12026  34 

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
40834
diff
changeset

35 
text {* @{term bottom} and @{term Def} *} 
12026  36 

16748  37 
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)" 
12026  38 
by (cases x) simp_all 
39 

16630
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset

40 
lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset

41 
by (cases x) simp_all 
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset

42 

12026  43 
text {* 
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
40834
diff
changeset

44 
For @{term "x ~= \<bottom>"} in assumptions @{text defined} replaces @{text 
12026  45 
x} by @{text "Def a"} in conclusion. *} 
46 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29138
diff
changeset

47 
method_setup defined = {* 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29138
diff
changeset

48 
Scan.succeed (fn ctxt => SIMPLE_METHOD' 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31076
diff
changeset

49 
(etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt))) 
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29138
diff
changeset

50 
*} "" 
12026  51 

16748  52 
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R" 
53 
by simp 

12026  54 

16748  55 
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R" 
12026  56 
by simp 
57 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30607
diff
changeset

58 
lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y" 
40082  59 
by (simp add: below_lift_def Def_def Abs_lift_inverse) 
12026  60 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30607
diff
changeset

61 
lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30607
diff
changeset

62 
by (induct y, simp, simp add: Def_below_Def) 
12026  63 

64 

65 
subsection {* Lift is flat *} 

66 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12026
diff
changeset

67 
instance lift :: (type) flat 
27292  68 
proof 
69 
fix x y :: "'a lift" 

70 
assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y" 

71 
by (induct x) auto 

72 
qed 

12026  73 

40088
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

74 
subsection {* Continuity of @{const lift_case} *} 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

75 

49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

76 
lemma lift_case_eq: "lift_case \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)" 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

77 
apply (induct x, unfold lift.cases) 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

78 
apply (simp add: Rep_lift_strict) 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

79 
apply (simp add: Def_def Abs_lift_inverse) 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

80 
done 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

81 

49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

82 
lemma cont2cont_lift_case [simp]: 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

83 
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))" 
40834
a1249aeff5b6
change cpodefgenerated cont_Rep rules to cont2cont format
huffman
parents:
40774
diff
changeset

84 
unfolding lift_case_eq by (simp add: cont_Rep_lift) 
40088
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

85 

16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

86 
subsection {* Further operations *} 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

87 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset

88 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset

89 
flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset

90 
"flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))" 
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

91 

40323
4cce7c708402
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman
parents:
40321
diff
changeset

92 
translations 
4cce7c708402
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman
parents:
40321
diff
changeset

93 
"\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)" 
4cce7c708402
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman
parents:
40321
diff
changeset

94 
"\<Lambda>(CONST Def x). FLIFT y. t" <= "FLIFT x y. t" 
4cce7c708402
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman
parents:
40321
diff
changeset

95 
"\<Lambda>(CONST Def x). t" <= "FLIFT x. t" 
4cce7c708402
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman
parents:
40321
diff
changeset

96 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset

97 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset

98 
flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset

99 
"flift2 f = (FLIFT x. Def (f x))" 
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

100 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

101 
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)" 
40088
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

102 
by (simp add: flift1_def) 
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

103 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

104 
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

105 
by (simp add: flift2_def) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

106 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

107 
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>" 
40088
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

108 
by (simp add: flift1_def) 
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

109 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

110 
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

111 
by (simp add: flift2_def) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

112 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

113 
lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

114 
by (erule lift_definedE, simp) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

115 

40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40089
diff
changeset

116 
lemma flift2_bottom_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)" 
19520  117 
by (cases x, simp_all) 
118 

40088
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

119 
lemma FLIFT_mono: 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

120 
"(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)" 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

121 
by (rule cfun_belowI, case_tac x, simp_all) 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

122 

49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

123 
lemma cont2cont_flift1 [simp, cont2cont]: 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

124 
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)" 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

125 
by (simp add: flift1_def cont2cont_LAM) 
49b9d301fadb
simplify proofs about flift; remove unneeded lemmas
huffman
parents:
40086
diff
changeset

126 

2640  127 
end 