3655
|
1 |
(* Title: HOLCF/Lift.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Olaf Mueller
|
|
4 |
Copyright 1997 Technische Universitaet Muenchen
|
|
5 |
|
|
6 |
Theorems for Lift.thy
|
|
7 |
*)
|
|
8 |
|
3324
|
9 |
|
|
10 |
(* ---------------------------------------------------------- *)
|
|
11 |
section"Continuity Proofs for flift1, flift2, if";
|
3655
|
12 |
(* ---------------------------------------------------------- *)
|
3324
|
13 |
(* need the instance into flat *)
|
|
14 |
|
|
15 |
|
|
16 |
(* flift1 is continuous in its argument itself*)
|
|
17 |
goal thy "cont (lift_case UU f)";
|
3457
|
18 |
by (rtac flatdom_strict2cont 1);
|
3324
|
19 |
by (Simp_tac 1);
|
|
20 |
qed"cont_flift1_arg";
|
|
21 |
|
|
22 |
(* flift1 is continuous in a variable that occurs only
|
|
23 |
in the Def branch *)
|
|
24 |
|
3842
|
25 |
goal thy "!!f. [| !! a. cont (%y. (f y) a) |] ==> \
|
3324
|
26 |
\ cont (%y. lift_case UU (f y))";
|
3457
|
27 |
by (rtac cont2cont_CF1L_rev 1);
|
3324
|
28 |
by (strip_tac 1);
|
|
29 |
by (res_inst_tac [("x","y")] Lift_cases 1);
|
|
30 |
by (Asm_simp_tac 1);
|
4098
|
31 |
by (fast_tac (HOL_cs addss simpset()) 1);
|
3324
|
32 |
qed"cont_flift1_not_arg";
|
|
33 |
|
|
34 |
(* flift1 is continuous in a variable that occurs either
|
|
35 |
in the Def branch or in the argument *)
|
|
36 |
|
3842
|
37 |
goal thy "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \
|
3324
|
38 |
\ cont (%y. lift_case UU (f y) (g y))";
|
3457
|
39 |
by (rtac cont2cont_app 1);
|
3324
|
40 |
back();
|
|
41 |
by (safe_tac set_cs);
|
3457
|
42 |
by (rtac cont_flift1_not_arg 1);
|
|
43 |
by (Auto_tac());
|
|
44 |
by (rtac cont_flift1_arg 1);
|
3324
|
45 |
qed"cont_flift1_arg_and_not_arg";
|
|
46 |
|
|
47 |
(* flift2 is continuous in its argument itself *)
|
|
48 |
|
|
49 |
goal thy "cont (lift_case UU (%y. Def (f y)))";
|
3457
|
50 |
by (rtac flatdom_strict2cont 1);
|
3324
|
51 |
by (Simp_tac 1);
|
|
52 |
qed"cont_flift2_arg";
|
|
53 |
|
|
54 |
|
|
55 |
(* ---------------------------------------------------------- *)
|
|
56 |
(* Extension of cont_tac and installation of simplifier *)
|
|
57 |
(* ---------------------------------------------------------- *)
|
|
58 |
|
|
59 |
bind_thm("cont2cont_CF1L_rev2",allI RS cont2cont_CF1L_rev);
|
|
60 |
|
|
61 |
val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg,
|
|
62 |
cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2,
|
|
63 |
cont_fapp_app,cont_fapp_app_app,cont_if];
|
|
64 |
|
|
65 |
val cont_lemmas2 = cont_lemmas1 @ cont_lemmas_ext;
|
|
66 |
|
|
67 |
Addsimps cont_lemmas_ext;
|
|
68 |
|
|
69 |
fun cont_tac i = resolve_tac cont_lemmas2 i;
|
|
70 |
fun cont_tacR i = REPEAT (cont_tac i);
|
|
71 |
|
4098
|
72 |
fun cont_tacRs i = simp_tac (simpset() addsimps [flift1_def,flift2_def]) i THEN
|
3324
|
73 |
REPEAT (cont_tac i);
|
|
74 |
|
|
75 |
|
4098
|
76 |
simpset_ref() := simpset() addSolver (K (DEPTH_SOLVE_1 o cont_tac));
|
3324
|
77 |
|
3661
|
78 |
|
|
79 |
|
3324
|
80 |
(* ---------------------------------------------------------- *)
|
|
81 |
section"flift1, flift2";
|
|
82 |
(* ---------------------------------------------------------- *)
|
|
83 |
|
|
84 |
|
|
85 |
goal thy "flift1 f`(Def x) = (f x)";
|
4098
|
86 |
by (simp_tac (simpset() addsimps [flift1_def]) 1);
|
3324
|
87 |
qed"flift1_Def";
|
|
88 |
|
|
89 |
goal thy "flift2 f`(Def x) = Def (f x)";
|
4098
|
90 |
by (simp_tac (simpset() addsimps [flift2_def]) 1);
|
3324
|
91 |
qed"flift2_Def";
|
|
92 |
|
|
93 |
goal thy "flift1 f`UU = UU";
|
4098
|
94 |
by (simp_tac (simpset() addsimps [flift1_def]) 1);
|
3324
|
95 |
qed"flift1_UU";
|
|
96 |
|
|
97 |
goal thy "flift2 f`UU = UU";
|
4098
|
98 |
by (simp_tac (simpset() addsimps [flift2_def]) 1);
|
3324
|
99 |
qed"flift2_UU";
|
|
100 |
|
|
101 |
Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
|
|
102 |
|
|
103 |
goal thy "!!x. x~=UU ==> (flift2 f)`x~=UU";
|
|
104 |
by (def_tac 1);
|
|
105 |
qed"flift2_nUU";
|
|
106 |
|
|
107 |
Addsimps [flift2_nUU];
|
|
108 |
|
|
109 |
|