equal
deleted
inserted
replaced
6 (* ---------------------------------------------------------- *) |
6 (* ---------------------------------------------------------- *) |
7 |
7 |
8 |
8 |
9 (* flift1 is continuous in its argument itself*) |
9 (* flift1 is continuous in its argument itself*) |
10 goal thy "cont (lift_case UU f)"; |
10 goal thy "cont (lift_case UU f)"; |
11 br flatdom_strict2cont 1; |
11 by (rtac flatdom_strict2cont 1); |
12 by (Simp_tac 1); |
12 by (Simp_tac 1); |
13 qed"cont_flift1_arg"; |
13 qed"cont_flift1_arg"; |
14 |
14 |
15 (* flift1 is continuous in a variable that occurs only |
15 (* flift1 is continuous in a variable that occurs only |
16 in the Def branch *) |
16 in the Def branch *) |
17 |
17 |
18 goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \ |
18 goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \ |
19 \ cont (%y. lift_case UU (f y))"; |
19 \ cont (%y. lift_case UU (f y))"; |
20 br cont2cont_CF1L_rev 1; |
20 by (rtac cont2cont_CF1L_rev 1); |
21 by (strip_tac 1); |
21 by (strip_tac 1); |
22 by (res_inst_tac [("x","y")] Lift_cases 1); |
22 by (res_inst_tac [("x","y")] Lift_cases 1); |
23 by (Asm_simp_tac 1); |
23 by (Asm_simp_tac 1); |
24 by (fast_tac (HOL_cs addss !simpset) 1); |
24 by (fast_tac (HOL_cs addss !simpset) 1); |
25 qed"cont_flift1_not_arg"; |
25 qed"cont_flift1_not_arg"; |
27 (* flift1 is continuous in a variable that occurs either |
27 (* flift1 is continuous in a variable that occurs either |
28 in the Def branch or in the argument *) |
28 in the Def branch or in the argument *) |
29 |
29 |
30 goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \ |
30 goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \ |
31 \ cont (%y. lift_case UU (f y) (g y))"; |
31 \ cont (%y. lift_case UU (f y) (g y))"; |
32 br cont2cont_app 1; |
32 by (rtac cont2cont_app 1); |
33 back(); |
33 back(); |
34 by (safe_tac set_cs); |
34 by (safe_tac set_cs); |
35 br cont_flift1_not_arg 1; |
35 by (rtac cont_flift1_not_arg 1); |
36 auto(); |
36 by (Auto_tac()); |
37 br cont_flift1_arg 1; |
37 by (rtac cont_flift1_arg 1); |
38 qed"cont_flift1_arg_and_not_arg"; |
38 qed"cont_flift1_arg_and_not_arg"; |
39 |
39 |
40 (* flift2 is continuous in its argument itself *) |
40 (* flift2 is continuous in its argument itself *) |
41 |
41 |
42 goal thy "cont (lift_case UU (%y. Def (f y)))"; |
42 goal thy "cont (lift_case UU (%y. Def (f y)))"; |
43 br flatdom_strict2cont 1; |
43 by (rtac flatdom_strict2cont 1); |
44 by (Simp_tac 1); |
44 by (Simp_tac 1); |
45 qed"cont_flift2_arg"; |
45 qed"cont_flift2_arg"; |
46 |
46 |
47 |
47 |
48 (* ---------------------------------------------------------- *) |
48 (* ---------------------------------------------------------- *) |