src/HOLCF/Lift3.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4098 71e05eb27fb6
child 4833 2e53109d4bc8
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
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
mueller@3035
    73
goal thy "(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@3842
    83
goal thy "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
nipkow@2841
    97
goal thy
nipkow@2841
    98
  "P(lift_case a b x) = ((x=UU --> P a) & (!y. x = Def y --> P(b y)))";
paulson@3457
    99
by (lift.induct_tac "x" 1);
paulson@3457
   100
by (ALLGOALS Asm_simp_tac);
nipkow@2841
   101
qed "expand_lift_case";
nipkow@2841
   102
wenzelm@3842
   103
goal thy "(x~=UU)=(? y. x=Def y)";
paulson@3457
   104
by (rtac iffI 1);
paulson@3457
   105
by (rtac Lift_cases 1);
mueller@3035
   106
by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));
sandnerr@2356
   107
qed"not_Undef_is_Def";
sandnerr@2356
   108
mueller@3035
   109
(* For x~=UU in assumptions def_tac replaces x by (Def a) in conclusion *)
mueller@3035
   110
val def_tac = etac (not_Undef_is_Def RS iffD1 RS exE) THEN' Asm_simp_tac;
sandnerr@2356
   111
mueller@3035
   112
bind_thm("Undef_eq_UU", inst_lift_pcpo RS sym);
mueller@3035
   113
mueller@3035
   114
val DefE = prove_goal thy "Def x = UU ==> R" 
sandnerr@2356
   115
    (fn prems => [
sandnerr@2356
   116
        cut_facts_tac prems 1,
sandnerr@2356
   117
        asm_full_simp_tac (HOL_ss addsimps [Def_not_UU]) 1]);
sandnerr@2356
   118
mueller@3035
   119
val prems = goal thy "[| x = Def s; x = UU |] ==> R";
sandnerr@2356
   120
by (cut_facts_tac prems 1);
sandnerr@2356
   121
by (fast_tac (HOL_cs addSDs [DefE]) 1);
mueller@3035
   122
qed"DefE2";
mueller@3035
   123
mueller@3035
   124
goal thy "Def x << Def y = (x = y)";
mueller@3035
   125
by (stac (hd lift.inject RS sym) 1);
mueller@3035
   126
back();
mueller@3035
   127
by (rtac iffI 1);
wenzelm@4098
   128
by (asm_full_simp_tac (simpset() addsimps [inst_lift_po] ) 1);
paulson@3457
   129
by (etac (antisym_less_inverse RS conjunct1) 1);
mueller@3035
   130
qed"Def_inject_less_eq";
mueller@3035
   131
mueller@3035
   132
goal thy "Def x << y = (Def x = y)";
wenzelm@4098
   133
by (simp_tac (simpset() addsimps [less_lift]) 1);
mueller@3035
   134
qed"Def_less_is_eq";
mueller@3035
   135
mueller@3035
   136
Addsimps [Def_less_is_eq];
sandnerr@2356
   137
sandnerr@2356
   138
(* ---------------------------------------------------------- *)
mueller@3035
   139
              section"Lift is flat";
sandnerr@2356
   140
(* ---------------------------------------------------------- *)
sandnerr@2356
   141
slotosch@3324
   142
goal thy "! x y::'a lift. x << y --> x = UU | x = y";
wenzelm@4098
   143
by (simp_tac (simpset() addsimps [less_lift]) 1);
slotosch@3324
   144
qed"ax_flat_lift";
mueller@3035
   145
mueller@3035
   146
(* Two specific lemmas for the combination of LCF and HOL terms *)
mueller@3035
   147
mueller@3035
   148
goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
paulson@3457
   149
by (rtac cont2cont_CF1L 1);
mueller@3035
   150
by (REPEAT (resolve_tac cont_lemmas1 1));
paulson@4477
   151
by Auto_tac;
mueller@3035
   152
qed"cont_fapp_app";
mueller@3035
   153
mueller@3035
   154
goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
paulson@3457
   155
by (rtac cont2cont_CF1L 1);
paulson@3457
   156
by (etac cont_fapp_app 1);
paulson@3457
   157
by (assume_tac 1);
mueller@3035
   158
qed"cont_fapp_app_app";
sandnerr@2356
   159
sandnerr@2356
   160
mueller@3035
   161
(* continuity of if then else *)
mueller@3035
   162
val prems = goal thy "[| cont f1; cont f2 |] ==> \
sandnerr@2356
   163
\   cont (%x. if b then f1 x else f2 x)";
sandnerr@2356
   164
by (cut_facts_tac prems 1);
sandnerr@2356
   165
by (case_tac "b" 1);
sandnerr@2356
   166
by (TRYALL (fast_tac (HOL_cs addss HOL_ss)));
mueller@3035
   167
qed"cont_if";
sandnerr@2356
   168