author | sandnerr |
Mon, 09 Dec 1996 19:27:07 +0100 | |
changeset 2357 | dd2e5e655fd2 |
parent 2356 | 125260ef480c |
child 2640 | ee4dfce170a0 |
permissions | -rw-r--r-- |
2357 | 1 |
(* Title: HOLCF/Lift2.ML |
2 |
ID: $Id$ |
|
3 |
Author: Olaf Mueller, Robert Sandner |
|
4 |
Copyright 1996 Technische Universitaet Muenchen |
|
5 |
||
6 |
Theorems for Lift2.thy |
|
7 |
*) |
|
8 |
||
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
9 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
10 |
open Lift2; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
11 |
Addsimps [less_lift_def]; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
12 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
13 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
14 |
(* -------------------------------------------------------------------------*) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
15 |
(* type ('a)lift is pointed *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
16 |
(* ------------------------------------------------------------------------ *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
17 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
18 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
19 |
goal Lift2.thy "Undef << x"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
20 |
by (simp_tac (!simpset addsimps [inst_lift_po]) 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
21 |
qed"minimal_lift"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
22 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
23 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
24 |
(* ------------------------------------------------------------------------ *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
25 |
(* ('a)lift is a cpo *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
26 |
(* ------------------------------------------------------------------------ *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
27 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
28 |
(* The following Lemmata have already been proved in Pcpo.ML and Fix.ML, |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
29 |
but there class pcpo is assumed, although only po is necessary and a |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
30 |
least element. Therefore they are redone here for the po lift with |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
31 |
least element Undef. *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
32 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
33 |
(* Tailoring notUU_I of Pcpo.ML to Undef *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
34 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
35 |
goal Lift2.thy "!!x. [| x<<y; ~x=Undef |] ==> ~y=Undef"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
36 |
by (etac contrapos 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
37 |
by (hyp_subst_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
38 |
by (rtac antisym_less 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
39 |
by (atac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
40 |
by (rtac minimal_lift 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
41 |
qed"notUndef_I"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
42 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
43 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
44 |
(* Tailoring chain_mono2 of Pcpo.ML to Undef *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
45 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
46 |
goal Lift2.thy |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
47 |
"!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \ |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
48 |
\ ==> ? j.!i.j<i-->~Y(i)=Undef"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
49 |
by (safe_tac HOL_cs); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
50 |
by (step_tac HOL_cs 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
51 |
by (strip_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
52 |
by (rtac notUndef_I 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
53 |
by (atac 2); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
54 |
by (etac (chain_mono RS mp) 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
55 |
by (atac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
56 |
qed"chain_mono2_po"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
57 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
58 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
59 |
(* Tailoring flat_imp_chain_finite of Fix.ML to lift *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
60 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
61 |
goal Lift2.thy |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
62 |
"(! Y. is_chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
63 |
by (rewtac max_in_chain_def); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
64 |
by (strip_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
65 |
by (res_inst_tac [("P","!i.Y(i)=Undef")] case_split_thm 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
66 |
by (res_inst_tac [("x","0")] exI 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
67 |
by (strip_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
68 |
by (rtac trans 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
69 |
by (etac spec 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
70 |
by (rtac sym 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
71 |
by (etac spec 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
72 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
73 |
by (subgoal_tac "!x y.x<<(y::('a)lift) --> x=Undef | x=y" 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
74 |
by (simp_tac (!simpset addsimps [inst_lift_po]) 2); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
75 |
by (rtac (chain_mono2_po RS exE) 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
76 |
by (fast_tac HOL_cs 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
77 |
by (atac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
78 |
by (res_inst_tac [("x","Suc(x)")] exI 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
79 |
by (strip_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
80 |
by (rtac disjE 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
81 |
by (atac 3); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
82 |
by (rtac mp 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
83 |
by (dtac spec 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
84 |
by (etac spec 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
85 |
by (etac (le_imp_less_or_eq RS disjE) 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
86 |
by (etac (chain_mono RS mp) 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
87 |
by (atac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
88 |
by (hyp_subst_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
89 |
by (rtac refl_less 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
90 |
by (res_inst_tac [("P","Y(Suc(x)) = Undef")] notE 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
91 |
by (atac 2); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
92 |
by (rtac mp 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
93 |
by (etac spec 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
94 |
by (Asm_simp_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
95 |
qed"flat_imp_chain_finite_poo"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
96 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
97 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
98 |
(* Main Lemma: cpo_lift *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
99 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
100 |
goal Lift2.thy |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
101 |
"!!Y. is_chain(Y::nat=>('a)lift) ==> ? x.range(Y) <<|x"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
102 |
by (cut_inst_tac [] flat_imp_chain_finite_poo 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
103 |
by (step_tac HOL_cs 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
104 |
by (safe_tac HOL_cs); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
105 |
by (step_tac HOL_cs 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
106 |
by (rtac exI 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
107 |
by (rtac lub_finch1 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
108 |
by (atac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
109 |
by (atac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
110 |
qed"cpo_lift"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
111 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
112 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
113 |