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