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