src/HOLCF/Lift.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4098 71e05eb27fb6
child 5068 fb28eaa07e01
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
     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 thy "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 thy "!!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 thy "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \
    38 \   cont (%y. lift_case UU (f y) (g y))";
    39 by (rtac cont2cont_app 1);
    40 back();
    41 by (safe_tac set_cs);
    42 by (rtac cont_flift1_not_arg 1);
    43 by Auto_tac;
    44 by (rtac cont_flift1_arg 1);
    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)))";
    50 by (rtac flatdom_strict2cont 1);
    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 
    72 fun cont_tacRs i = simp_tac (simpset() addsimps [flift1_def,flift2_def]) i THEN
    73                   REPEAT (cont_tac i);
    74 
    75 
    76 simpset_ref() := simpset() addSolver (K (DEPTH_SOLVE_1 o cont_tac));
    77 
    78 
    79 
    80 (* ---------------------------------------------------------- *)
    81               section"flift1, flift2";
    82 (* ---------------------------------------------------------- *)
    83 
    84 
    85 goal thy "flift1 f`(Def x) = (f x)";
    86 by (simp_tac (simpset() addsimps [flift1_def]) 1);
    87 qed"flift1_Def";
    88 
    89 goal thy "flift2 f`(Def x) = Def (f x)";
    90 by (simp_tac (simpset() addsimps [flift2_def]) 1);
    91 qed"flift2_Def";
    92 
    93 goal thy "flift1 f`UU = UU";
    94 by (simp_tac (simpset() addsimps [flift1_def]) 1);
    95 qed"flift1_UU";
    96 
    97 goal thy "flift2 f`UU = UU";
    98 by (simp_tac (simpset() addsimps [flift2_def]) 1);
    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