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
```