author | wenzelm |
Sat, 12 Jan 2013 14:53:56 +0100 | |
changeset 50843 | 1465521b92a1 |
parent 49759 | ecf1d5d87e5e |
child 51717 | 9e7d1c139569 |
permissions | -rw-r--r-- |
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 |
|
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
42814
diff
changeset
|
13 |
pcpodef '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))) |
42814 | 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 cpodef-generated 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 |