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