src/HOLCF/Lift3.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5291 5706f0ef1d43
child 9245 428385c4bc50
permissions -rw-r--r--
tidying
sandnerr@2357
     1
(*  Title:      HOLCF/Lift3.ML
sandnerr@2357
     2
    ID:         $Id$
mueller@3035
     3
    Author:     Olaf Mueller
sandnerr@2357
     4
    Copyright   1996 Technische Universitaet Muenchen
sandnerr@2357
     5
sandnerr@2357
     6
Theorems for Lift3.thy
sandnerr@2357
     7
*)
sandnerr@2357
     8
sandnerr@2356
     9
slotosch@2640
    10
(* for compatibility with old HOLCF-Version *)
slotosch@2640
    11
qed_goal "inst_lift_pcpo" thy "UU = Undef"
slotosch@2640
    12
 (fn prems => 
slotosch@2640
    13
        [
slotosch@2640
    14
        (simp_tac (HOL_ss addsimps [UU_def,UU_lift_def]) 1)
slotosch@2640
    15
        ]);
slotosch@2640
    16
sandnerr@2356
    17
(* ----------------------------------------------------------- *)
mueller@3035
    18
(*           In lift.simps Undef is replaced by UU             *)
mueller@3035
    19
(*           Undef should be invisible from now on             *)
sandnerr@2356
    20
(* ----------------------------------------------------------- *)
sandnerr@2356
    21
mueller@3035
    22
sandnerr@2356
    23
Addsimps [inst_lift_pcpo];
sandnerr@2356
    24
sandnerr@2356
    25
local
sandnerr@2356
    26
mueller@3035
    27
val case1' = prove_goal thy "lift_case f1 f2 UU = f1"
wenzelm@4098
    28
             (fn _ => [simp_tac (simpset() addsimps lift.simps) 1]);
mueller@3035
    29
val case2' = prove_goal thy "lift_case f1 f2 (Def a) = f2 a"
mueller@3041
    30
             (fn _ => [Simp_tac 1]);
mueller@3035
    31
val distinct1' = prove_goal thy "UU ~= Def a" 
mueller@3041
    32
                 (fn _ => [Simp_tac 1]);
mueller@3035
    33
val distinct2' = prove_goal thy "Def a ~= UU"
mueller@3041
    34
                 (fn _ => [Simp_tac 1]);
mueller@3035
    35
val inject' = prove_goal thy "Def a = Def aa = (a = aa)"
mueller@3041
    36
               (fn _ => [Simp_tac 1]);
mueller@3035
    37
val rec1' = prove_goal thy "lift_rec f1 f2 UU = f1"
mueller@3041
    38
            (fn _ => [Simp_tac 1]);
mueller@3035
    39
val rec2' = prove_goal thy "lift_rec f1 f2 (Def a) = f2 a"
mueller@3041
    40
            (fn _ => [Simp_tac 1]);
mueller@3035
    41
val induct' = prove_goal thy "[| P UU; !a. P (Def a) |] ==> P lift"
mueller@3041
    42
            (fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1,
mueller@3041
    43
                      etac Lift1.lift.induct 1,fast_tac HOL_cs 1]);
sandnerr@2356
    44
sandnerr@2356
    45
in 
sandnerr@2356
    46
mueller@3035
    47
val Def_not_UU = distinct2';
sandnerr@2356
    48
sandnerr@2356
    49
structure lift =
sandnerr@2356
    50
struct
sandnerr@2356
    51
val cases = [case1',case2'];
sandnerr@2356
    52
val distinct = [distinct1',distinct2'];
sandnerr@2356
    53
val inject = [inject'];
sandnerr@2356
    54
val induct = allI RSN(2,induct');
sandnerr@2356
    55
val recs = [rec1',rec2'];
sandnerr@2356
    56
val simps = cases@distinct@inject@recs;
sandnerr@2356
    57
fun induct_tac (s:string) (i:int) = 
sandnerr@2356
    58
    (res_inst_tac [("lift",s)] induct i);
sandnerr@2356
    59
end;
sandnerr@2356
    60
sandnerr@2356
    61
end; (* local *)
sandnerr@2356
    62
mueller@3250
    63
Delsimps Lift1.lift.simps;
sandnerr@2356
    64
Delsimps [inst_lift_pcpo];
sandnerr@2356
    65
Addsimps [inst_lift_pcpo RS sym];
sandnerr@2356
    66
Addsimps lift.simps;
sandnerr@2356
    67
sandnerr@2356
    68
mueller@3035
    69
(* --------------------------------------------------------*)
mueller@3035
    70
              section"less_lift";
mueller@3035
    71
(* --------------------------------------------------------*)
sandnerr@2356
    72
wenzelm@5068
    73
Goal "(x::'a lift) << y = (x=y | x=UU)";
paulson@3457
    74
by (stac inst_lift_po 1);
sandnerr@2356
    75
by (Simp_tac 1);
mueller@3035
    76
qed"less_lift";
sandnerr@2356
    77
sandnerr@2356
    78
sandnerr@2356
    79
(* ---------------------------------------------------------- *)
mueller@3035
    80
                 section"UU and Def";             
sandnerr@2356
    81
(* ---------------------------------------------------------- *)
sandnerr@2356
    82
wenzelm@5068
    83
Goal "x=UU | (? y. x=Def y)"; 
sandnerr@2356
    84
by (lift.induct_tac "x" 1);
sandnerr@2356
    85
by (Asm_simp_tac 1);
sandnerr@2356
    86
by (rtac disjI2 1);
sandnerr@2356
    87
by (rtac exI 1);
sandnerr@2356
    88
by (Asm_simp_tac 1);
sandnerr@2356
    89
qed"Lift_exhaust";
sandnerr@2356
    90
mueller@3035
    91
val prems = goal thy 
sandnerr@2356
    92
  "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P";
sandnerr@2356
    93
by (cut_facts_tac [Lift_exhaust] 1);
sandnerr@2356
    94
by (fast_tac (HOL_cs addSEs prems) 1);
sandnerr@2356
    95
qed"Lift_cases";
sandnerr@2356
    96
wenzelm@5068
    97
Goal "(x~=UU)=(? y. x=Def y)";
paulson@3457
    98
by (rtac iffI 1);
paulson@3457
    99
by (rtac Lift_cases 1);
mueller@3035
   100
by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));
sandnerr@2356
   101
qed"not_Undef_is_Def";
sandnerr@2356
   102
mueller@3035
   103
(* For x~=UU in assumptions def_tac replaces x by (Def a) in conclusion *)
mueller@3035
   104
val def_tac = etac (not_Undef_is_Def RS iffD1 RS exE) THEN' Asm_simp_tac;
sandnerr@2356
   105
mueller@3035
   106
bind_thm("Undef_eq_UU", inst_lift_pcpo RS sym);
mueller@3035
   107
mueller@3035
   108
val DefE = prove_goal thy "Def x = UU ==> R" 
sandnerr@2356
   109
    (fn prems => [
sandnerr@2356
   110
        cut_facts_tac prems 1,
sandnerr@2356
   111
        asm_full_simp_tac (HOL_ss addsimps [Def_not_UU]) 1]);
sandnerr@2356
   112
mueller@3035
   113
val prems = goal thy "[| x = Def s; x = UU |] ==> R";
sandnerr@2356
   114
by (cut_facts_tac prems 1);
sandnerr@2356
   115
by (fast_tac (HOL_cs addSDs [DefE]) 1);
mueller@3035
   116
qed"DefE2";
mueller@3035
   117
wenzelm@5068
   118
Goal "Def x << Def y = (x = y)";
mueller@3035
   119
by (stac (hd lift.inject RS sym) 1);
mueller@3035
   120
back();
mueller@3035
   121
by (rtac iffI 1);
wenzelm@4098
   122
by (asm_full_simp_tac (simpset() addsimps [inst_lift_po] ) 1);
paulson@3457
   123
by (etac (antisym_less_inverse RS conjunct1) 1);
mueller@3035
   124
qed"Def_inject_less_eq";
mueller@3035
   125
wenzelm@5068
   126
Goal "Def x << y = (Def x = y)";
wenzelm@4098
   127
by (simp_tac (simpset() addsimps [less_lift]) 1);
mueller@3035
   128
qed"Def_less_is_eq";
mueller@3035
   129
mueller@3035
   130
Addsimps [Def_less_is_eq];
sandnerr@2356
   131
sandnerr@2356
   132
(* ---------------------------------------------------------- *)
mueller@3035
   133
              section"Lift is flat";
sandnerr@2356
   134
(* ---------------------------------------------------------- *)
sandnerr@2356
   135
wenzelm@5068
   136
Goal "! x y::'a lift. x << y --> x = UU | x = y";
wenzelm@4098
   137
by (simp_tac (simpset() addsimps [less_lift]) 1);
slotosch@3324
   138
qed"ax_flat_lift";
mueller@3035
   139
mueller@3035
   140
(* Two specific lemmas for the combination of LCF and HOL terms *)
mueller@3035
   141
paulson@5143
   142
Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
paulson@3457
   143
by (rtac cont2cont_CF1L 1);
mueller@3035
   144
by (REPEAT (resolve_tac cont_lemmas1 1));
paulson@4477
   145
by Auto_tac;
slotosch@5291
   146
qed"cont_Rep_CFun_app";
mueller@3035
   147
paulson@5143
   148
Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
paulson@3457
   149
by (rtac cont2cont_CF1L 1);
slotosch@5291
   150
by (etac cont_Rep_CFun_app 1);
paulson@3457
   151
by (assume_tac 1);
slotosch@5291
   152
qed"cont_Rep_CFun_app_app";
sandnerr@2356
   153
sandnerr@2356
   154
mueller@3035
   155
(* continuity of if then else *)
mueller@3035
   156
val prems = goal thy "[| cont f1; cont f2 |] ==> \
sandnerr@2356
   157
\   cont (%x. if b then f1 x else f2 x)";
sandnerr@2356
   158
by (cut_facts_tac prems 1);
sandnerr@2356
   159
by (case_tac "b" 1);
sandnerr@2356
   160
by (TRYALL (fast_tac (HOL_cs addss HOL_ss)));
mueller@3035
   161
qed"cont_if";
sandnerr@2356
   162