src/HOLCF/Lift2.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5143 b94cd208f073
child 9245 428385c4bc50
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/Lift2.ML
     2     ID:         $Id$
     3     Author:     Olaf Mueller
     4     Copyright   1996 Technische Universitaet Muenchen
     5 
     6 Theorems for Lift2.thy
     7 *)
     8 
     9 open Lift2;
    10 
    11 (* for compatibility with old HOLCF-Version *)
    12 qed_goal "inst_lift_po" thy "(op <<)=(%x y. x=y|x=Undef)"
    13  (fn prems => 
    14         [
    15         (fold_goals_tac [less_lift_def]),
    16         (rtac refl 1)
    17         ]);
    18 
    19 (* -------------------------------------------------------------------------*)
    20 (* type ('a)lift is pointed                                                *)
    21 (* ------------------------------------------------------------------------ *)
    22 
    23 Goal  "Undef << x";
    24 by (simp_tac (simpset() addsimps [inst_lift_po]) 1);
    25 qed"minimal_lift";
    26 
    27 bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
    28 
    29 qed_goal "least_lift" thy "? x::'a lift.!y. x<<y"
    30 (fn prems =>
    31         [
    32         (res_inst_tac [("x","Undef")] exI 1),
    33         (rtac (minimal_lift RS allI) 1)
    34         ]);
    35 
    36 (* ------------------------------------------------------------------------ *)
    37 (* ('a)lift is a cpo                                                       *)
    38 (* ------------------------------------------------------------------------ *)
    39 
    40 (* The following Lemmata have already been proved in Pcpo.ML and Fix.ML, 
    41    but there class pcpo is assumed, although only po is necessary and a
    42    least element. Therefore they are redone here for the po lift with 
    43    least element Undef.   *)
    44 
    45 (* Tailoring notUU_I of Pcpo.ML to Undef *)
    46 
    47 Goal "[| x<<y; ~x=Undef |] ==> ~y=Undef";
    48 by (etac contrapos 1);
    49 by (hyp_subst_tac 1);
    50 by (rtac antisym_less 1);
    51 by (atac 1);
    52 by (rtac minimal_lift 1);
    53 qed"notUndef_I";
    54 
    55 
    56 (* Tailoring chain_mono2 of Pcpo.ML to Undef *)
    57 
    58 Goal
    59 "!!Y. [|? j.~Y(j)=Undef;chain(Y::nat=>('a)lift)|] \
    60 \ ==> ? j.!i. j<i-->~Y(i)=Undef";
    61 by Safe_tac;
    62 by (Step_tac 1);
    63 by (strip_tac 1);
    64 by (rtac notUndef_I 1);
    65 by (atac 2);
    66 by (etac (chain_mono RS mp) 1);
    67 by (atac 1);
    68 qed"chain_mono2_po";
    69 
    70 
    71 (* Tailoring flat_imp_chfin of Fix.ML to lift *)
    72 
    73 Goal
    74         "(! Y. chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
    75 by (rewtac max_in_chain_def);  
    76 by (strip_tac 1);
    77 by (res_inst_tac [("P","!i. Y(i)=Undef")] case_split_thm  1);
    78 by (res_inst_tac [("x","0")] exI 1);
    79 by (strip_tac 1);
    80 by (rtac trans 1);
    81 by (etac spec 1);
    82 by (rtac sym 1);
    83 by (etac spec 1); 
    84 
    85 by (subgoal_tac "!x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
    86 by (simp_tac (simpset() addsimps [inst_lift_po]) 2);
    87 by (rtac (chain_mono2_po RS exE) 1); 
    88 by (Fast_tac 1); 
    89 by (atac 1); 
    90 by (res_inst_tac [("x","Suc(x)")] exI 1); 
    91 by (strip_tac 1); 
    92 by (rtac disjE 1); 
    93 by (atac 3); 
    94 by (rtac mp 1); 
    95 by (dtac spec 1);
    96 by (etac spec 1); 
    97 by (etac (le_imp_less_or_eq RS disjE) 1); 
    98 by (etac (chain_mono RS mp) 1); 
    99 by (atac 1); 
   100 by (hyp_subst_tac 1); 
   101 by (rtac refl_less 1); 
   102 by (res_inst_tac [("P","Y(Suc(x)) = Undef")] notE 1); 
   103 by (atac 2); 
   104 by (rtac mp 1); 
   105 by (etac spec 1); 
   106 by (Asm_simp_tac 1);
   107 qed"flat_imp_chfin_poo";
   108 
   109 
   110 (* Main Lemma: cpo_lift *)
   111 
   112 Goal  
   113   "!!Y. chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
   114 by (cut_inst_tac [] flat_imp_chfin_poo 1);
   115 by (Step_tac 1);
   116 by Safe_tac;
   117 by (Step_tac 1); 
   118 by (rtac exI 1);
   119 by (rtac lub_finch1 1);
   120 by (atac 1);
   121 by (atac 1);
   122 qed"cpo_lift";
   123 
   124 
   125