author | paulson |
Tue, 04 Jul 2000 15:58:11 +0200 | |
changeset 9245 | 428385c4bc50 |
parent 5291 | 5706f0ef1d43 |
child 9248 | e1dee89de037 |
permissions | -rw-r--r-- |
2357 | 1 |
(* Title: HOLCF/Lift3.ML |
2 |
ID: $Id$ |
|
3035 | 3 |
Author: Olaf Mueller |
2357 | 4 |
Copyright 1996 Technische Universitaet Muenchen |
5 |
||
9245 | 6 |
Class Instance lift::(term)pcpo |
2357 | 7 |
*) |
8 |
||
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
9 |
|
2640 | 10 |
(* for compatibility with old HOLCF-Version *) |
9245 | 11 |
val prems = goal thy "UU = Undef"; |
12 |
by (simp_tac (HOL_ss addsimps [UU_def,UU_lift_def]) 1); |
|
13 |
qed "inst_lift_pcpo"; |
|
2640 | 14 |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
15 |
(* ----------------------------------------------------------- *) |
3035 | 16 |
(* In lift.simps Undef is replaced by UU *) |
17 |
(* Undef should be invisible from now on *) |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
18 |
(* ----------------------------------------------------------- *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
19 |
|
3035 | 20 |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
21 |
Addsimps [inst_lift_pcpo]; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
22 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
23 |
local |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
24 |
|
3035 | 25 |
val case1' = prove_goal thy "lift_case f1 f2 UU = f1" |
4098 | 26 |
(fn _ => [simp_tac (simpset() addsimps lift.simps) 1]); |
3035 | 27 |
val case2' = prove_goal thy "lift_case f1 f2 (Def a) = f2 a" |
3041 | 28 |
(fn _ => [Simp_tac 1]); |
3035 | 29 |
val distinct1' = prove_goal thy "UU ~= Def a" |
3041 | 30 |
(fn _ => [Simp_tac 1]); |
3035 | 31 |
val distinct2' = prove_goal thy "Def a ~= UU" |
3041 | 32 |
(fn _ => [Simp_tac 1]); |
3035 | 33 |
val inject' = prove_goal thy "Def a = Def aa = (a = aa)" |
3041 | 34 |
(fn _ => [Simp_tac 1]); |
3035 | 35 |
val rec1' = prove_goal thy "lift_rec f1 f2 UU = f1" |
3041 | 36 |
(fn _ => [Simp_tac 1]); |
3035 | 37 |
val rec2' = prove_goal thy "lift_rec f1 f2 (Def a) = f2 a" |
3041 | 38 |
(fn _ => [Simp_tac 1]); |
3035 | 39 |
val induct' = prove_goal thy "[| P UU; !a. P (Def a) |] ==> P lift" |
3041 | 40 |
(fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1, |
41 |
etac Lift1.lift.induct 1,fast_tac HOL_cs 1]); |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
42 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
43 |
in |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
44 |
|
3035 | 45 |
val Def_not_UU = distinct2'; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
46 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
47 |
structure lift = |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
48 |
struct |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
49 |
val cases = [case1',case2']; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
50 |
val distinct = [distinct1',distinct2']; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
51 |
val inject = [inject']; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
52 |
val induct = allI RSN(2,induct'); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
53 |
val recs = [rec1',rec2']; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
54 |
val simps = cases@distinct@inject@recs; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
55 |
fun induct_tac (s:string) (i:int) = |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
56 |
(res_inst_tac [("lift",s)] induct i); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
57 |
end; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
58 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
59 |
end; (* local *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
60 |
|
3250 | 61 |
Delsimps Lift1.lift.simps; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
62 |
Delsimps [inst_lift_pcpo]; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
63 |
Addsimps [inst_lift_pcpo RS sym]; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
64 |
Addsimps lift.simps; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
65 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
66 |
|
3035 | 67 |
(* --------------------------------------------------------*) |
68 |
section"less_lift"; |
|
69 |
(* --------------------------------------------------------*) |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
70 |
|
5068 | 71 |
Goal "(x::'a lift) << y = (x=y | x=UU)"; |
3457 | 72 |
by (stac inst_lift_po 1); |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
73 |
by (Simp_tac 1); |
3035 | 74 |
qed"less_lift"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
75 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
76 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
77 |
(* ---------------------------------------------------------- *) |
3035 | 78 |
section"UU and Def"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
79 |
(* ---------------------------------------------------------- *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
80 |
|
5068 | 81 |
Goal "x=UU | (? y. x=Def y)"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
82 |
by (lift.induct_tac "x" 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
83 |
by (Asm_simp_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
84 |
by (rtac disjI2 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
85 |
by (rtac exI 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
86 |
by (Asm_simp_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
87 |
qed"Lift_exhaust"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
88 |
|
3035 | 89 |
val prems = goal thy |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
90 |
"[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
91 |
by (cut_facts_tac [Lift_exhaust] 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
92 |
by (fast_tac (HOL_cs addSEs prems) 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
93 |
qed"Lift_cases"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
94 |
|
5068 | 95 |
Goal "(x~=UU)=(? y. x=Def y)"; |
3457 | 96 |
by (rtac iffI 1); |
97 |
by (rtac Lift_cases 1); |
|
3035 | 98 |
by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1)); |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
99 |
qed"not_Undef_is_Def"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
100 |
|
3035 | 101 |
(* For x~=UU in assumptions def_tac replaces x by (Def a) in conclusion *) |
102 |
val def_tac = etac (not_Undef_is_Def RS iffD1 RS exE) THEN' Asm_simp_tac; |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
103 |
|
3035 | 104 |
bind_thm("Undef_eq_UU", inst_lift_pcpo RS sym); |
105 |
||
9245 | 106 |
val prems = goal thy "Def x = UU ==> R"; |
107 |
by (cut_facts_tac prems 1); |
|
108 |
by (asm_full_simp_tac (HOL_ss addsimps [Def_not_UU]) 1); |
|
109 |
qed "DefE"; |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
110 |
|
3035 | 111 |
val prems = goal thy "[| x = Def s; x = UU |] ==> R"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
112 |
by (cut_facts_tac prems 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
113 |
by (fast_tac (HOL_cs addSDs [DefE]) 1); |
3035 | 114 |
qed"DefE2"; |
115 |
||
5068 | 116 |
Goal "Def x << Def y = (x = y)"; |
3035 | 117 |
by (stac (hd lift.inject RS sym) 1); |
118 |
back(); |
|
119 |
by (rtac iffI 1); |
|
4098 | 120 |
by (asm_full_simp_tac (simpset() addsimps [inst_lift_po] ) 1); |
3457 | 121 |
by (etac (antisym_less_inverse RS conjunct1) 1); |
3035 | 122 |
qed"Def_inject_less_eq"; |
123 |
||
5068 | 124 |
Goal "Def x << y = (Def x = y)"; |
4098 | 125 |
by (simp_tac (simpset() addsimps [less_lift]) 1); |
3035 | 126 |
qed"Def_less_is_eq"; |
127 |
||
128 |
Addsimps [Def_less_is_eq]; |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
129 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
130 |
(* ---------------------------------------------------------- *) |
3035 | 131 |
section"Lift is flat"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
132 |
(* ---------------------------------------------------------- *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
133 |
|
5068 | 134 |
Goal "! x y::'a lift. x << y --> x = UU | x = y"; |
4098 | 135 |
by (simp_tac (simpset() addsimps [less_lift]) 1); |
3324 | 136 |
qed"ax_flat_lift"; |
3035 | 137 |
|
138 |
(* Two specific lemmas for the combination of LCF and HOL terms *) |
|
139 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5068
diff
changeset
|
140 |
Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)"; |
3457 | 141 |
by (rtac cont2cont_CF1L 1); |
3035 | 142 |
by (REPEAT (resolve_tac cont_lemmas1 1)); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
143 |
by Auto_tac; |
5291 | 144 |
qed"cont_Rep_CFun_app"; |
3035 | 145 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5068
diff
changeset
|
146 |
Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)"; |
3457 | 147 |
by (rtac cont2cont_CF1L 1); |
5291 | 148 |
by (etac cont_Rep_CFun_app 1); |
3457 | 149 |
by (assume_tac 1); |
5291 | 150 |
qed"cont_Rep_CFun_app_app"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
151 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
152 |
|
3035 | 153 |
(* continuity of if then else *) |
154 |
val prems = goal thy "[| cont f1; cont f2 |] ==> \ |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
155 |
\ cont (%x. if b then f1 x else f2 x)"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
156 |
by (cut_facts_tac prems 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
157 |
by (case_tac "b" 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
158 |
by (TRYALL (fast_tac (HOL_cs addss HOL_ss))); |
3035 | 159 |
qed"cont_if"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
160 |