author | wenzelm |
Mon, 03 Nov 1997 14:06:27 +0100 | |
changeset 4098 | 71e05eb27fb6 |
parent 3457 | a8ab7c64817c |
child 4833 | 2e53109d4bc8 |
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 |
||
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
9 |
goalw thy [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 |
|
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
14 |
goalw thy [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 |
|
2846 | 19 |
goalw thy [dlift_def] |
20 |
"(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)"; |
|
4098 | 21 |
by (simp_tac (simpset() setloop (split_tac[expand_lift_case])) 1); |
2846 | 22 |
qed "dlift_is_Def"; |
23 |
Addsimps [dlift_is_Def]; |
|
2798 | 24 |
|
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
25 |
goal thy "!!c. <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 |
||
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
31 |
goal thy "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t"; |
2798 | 32 |
by (com.induct_tac "c" 1); |
4098 | 33 |
by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1); |
34 |
by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1); |
|
35 |
by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1); |
|
36 |
by (simp_tac (simpset() setloop (split_tac[expand_if])) 1); |
|
37 |
by (fast_tac ((HOL_cs addIs evalc.intrs) addss simpset()) 1); |
|
2798 | 38 |
by (Simp_tac 1); |
3457 | 39 |
by (rtac fix_ind 1); |
40 |
by (fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1); |
|
2798 | 41 |
by (Simp_tac 1); |
4098 | 42 |
by (simp_tac (simpset() setloop (split_tac[expand_if])) 1); |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
43 |
by (safe_tac HOL_cs); |
2798 | 44 |
by (fast_tac (HOL_cs addIs evalc.intrs) 1); |
4098 | 45 |
by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1); |
2798 | 46 |
qed_spec_mp "D_implies_eval"; |
47 |
||
48 |
||
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
49 |
goal thy "(D c`(Discr s) = (Def t)) = (<c,s> -c-> t)"; |
2798 | 50 |
by (fast_tac (HOL_cs addSEs [D_implies_eval,eval_implies_D]) 1); |
51 |
qed "D_is_eval"; |