author | wenzelm |
Fri, 01 Dec 2000 19:42:05 +0100 | |
changeset 10567 | e7c9900cca4d |
parent 5618 | 721671c68324 |
child 10835 | f4745d77e620 |
permissions | -rw-r--r-- |
2798 | 1 |
(* Title: HOLCF/IMP/Denotational.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow & Robert Sandner |
|
4 |
Copyright 1996 TUM |
|
5 |
||
6 |
Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL |
|
7 |
*) |
|
8 |
||
5068 | 9 |
Goalw [dlift_def] "dlift f`(Def x) = f`(Discr x)"; |
3457 | 10 |
by (Simp_tac 1); |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
11 |
qed "dlift_Def"; |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
12 |
Addsimps [dlift_Def]; |
2798 | 13 |
|
5068 | 14 |
Goalw [dlift_def] "cont(%f. dlift f)"; |
3457 | 15 |
by (Simp_tac 1); |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
16 |
qed "cont_dlift"; |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
17 |
AddIffs [cont_dlift]; |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
18 |
|
5068 | 19 |
Goalw [dlift_def] |
2846 | 20 |
"(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)"; |
5192 | 21 |
by (simp_tac (simpset() addsplits [Lift1.lift.split]) 1); |
2846 | 22 |
qed "dlift_is_Def"; |
23 |
Addsimps [dlift_is_Def]; |
|
2798 | 24 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5068
diff
changeset
|
25 |
Goal "<c,s> -c-> t ==> D c`(Discr s) = (Def t)"; |
3457 | 26 |
by (etac evalc.induct 1); |
2798 | 27 |
by (ALLGOALS Asm_simp_tac); |
3457 | 28 |
by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac)); |
2798 | 29 |
qed_spec_mp "eval_implies_D"; |
30 |
||
5068 | 31 |
Goal "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t"; |
5192 | 32 |
by (induct_tac "c" 1); |
5618 | 33 |
by (Force_tac 1); |
5525 | 34 |
by (Force_tac 1); |
35 |
by (Force_tac 1); |
|
4833 | 36 |
by (Simp_tac 1); |
5618 | 37 |
by (Force_tac 1); |
2798 | 38 |
by (Simp_tac 1); |
3457 | 39 |
by (rtac fix_ind 1); |
5618 | 40 |
by (fast_tac (claset() addSIs adm_lemmas@[adm_chfindom,ax_flat_lift]) 1); |
2798 | 41 |
by (Simp_tac 1); |
4833 | 42 |
by (Simp_tac 1); |
5618 | 43 |
by Safe_tac; |
44 |
by (Fast_tac 1); |
|
45 |
by (Force_tac 1); |
|
2798 | 46 |
qed_spec_mp "D_implies_eval"; |
47 |
||
48 |
||
5068 | 49 |
Goal "(D c`(Discr s) = (Def t)) = (<c,s> -c-> t)"; |
5618 | 50 |
by (fast_tac (claset() addSEs [D_implies_eval,eval_implies_D]) 1); |
2798 | 51 |
qed "D_is_eval"; |