src/HOLCF/Lift.ML
author nipkow
Tue Sep 21 19:11:07 1999 +0200 (1999-09-21)
changeset 7570 a9391550eea1
parent 5291 5706f0ef1d43
child 10834 a7897aebbffc
permissions -rw-r--r--
Mod because of new solver interface.
     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 
     9 
    10 (* ---------------------------------------------------------- *)
    11     section"Continuity Proofs for flift1, flift2, if";
    12 (* ---------------------------------------------------------- *)
    13 (* need the instance into flat *)
    14 
    15 
    16 (* flift1 is continuous in its argument itself*)
    17 Goal "cont (lift_case UU f)"; 
    18 by (rtac flatdom_strict2cont 1);
    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 
    25 Goal "!!f. [| !! a. cont (%y. (f y) a) |] ==> \
    26 \          cont (%y. lift_case UU (f y))";
    27 by (rtac cont2cont_CF1L_rev 1);
    28 by (strip_tac 1);
    29 by (res_inst_tac [("x","y")] Lift_cases 1);
    30 by (Asm_simp_tac 1);
    31 by (fast_tac (HOL_cs addss simpset()) 1);
    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 
    37 Goal "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \
    38 \   cont (%y. lift_case UU (f y) (g y))";
    39 by (res_inst_tac [("tt","g")] cont2cont_app 1);
    40 by (rtac cont_flift1_not_arg 1);
    41 by Auto_tac;
    42 by (rtac cont_flift1_arg 1);
    43 qed"cont_flift1_arg_and_not_arg";
    44 
    45 (* flift2 is continuous in its argument itself *)
    46 
    47 Goal "cont (lift_case UU (%y. Def (f y)))";
    48 by (rtac flatdom_strict2cont 1);
    49 by (Simp_tac 1);
    50 qed"cont_flift2_arg";
    51 
    52 
    53 (* ---------------------------------------------------------- *)
    54 (*    Extension of cont_tac and installation of simplifier    *)
    55 (* ---------------------------------------------------------- *)
    56 
    57 bind_thm("cont2cont_CF1L_rev2",allI RS cont2cont_CF1L_rev);
    58 
    59 val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg,
    60                        cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2, 
    61                        cont_Rep_CFun_app,cont_Rep_CFun_app_app,cont_if];
    62 
    63 val cont_lemmas2 =  cont_lemmas1 @ cont_lemmas_ext;
    64                  
    65 Addsimps cont_lemmas_ext;         
    66 
    67 fun cont_tac  i = resolve_tac cont_lemmas2 i;
    68 fun cont_tacR i = REPEAT (cont_tac i);
    69 
    70 fun cont_tacRs i = simp_tac (simpset() addsimps [flift1_def,flift2_def]) i THEN
    71                   REPEAT (cont_tac i);
    72 
    73 
    74 simpset_ref() := simpset() addSolver
    75   (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac)));
    76 
    77 
    78 
    79 (* ---------------------------------------------------------- *)
    80               section"flift1, flift2";
    81 (* ---------------------------------------------------------- *)
    82 
    83 
    84 Goal "flift1 f`(Def x) = (f x)";
    85 by (simp_tac (simpset() addsimps [flift1_def]) 1);
    86 qed"flift1_Def";
    87 
    88 Goal "flift2 f`(Def x) = Def (f x)";
    89 by (simp_tac (simpset() addsimps [flift2_def]) 1);
    90 qed"flift2_Def";
    91 
    92 Goal "flift1 f`UU = UU";
    93 by (simp_tac (simpset() addsimps [flift1_def]) 1);
    94 qed"flift1_UU";
    95 
    96 Goal "flift2 f`UU = UU";
    97 by (simp_tac (simpset() addsimps [flift2_def]) 1);
    98 qed"flift2_UU";
    99 
   100 Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
   101 
   102 Goal "x~=UU ==> (flift2 f)`x~=UU";
   103 by (def_tac 1);
   104 qed"flift2_nUU";
   105 
   106 Addsimps [flift2_nUU];
   107 
   108