author | wenzelm |
Mon, 22 Jun 1998 17:26:46 +0200 | |
changeset 5069 | 3ea049f7979d |
parent 4477 | b3e5857d8d99 |
child 5117 | 7b5efef2ca74 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/IMP/Denotation.ML |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
1696 | 3 |
Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
4 |
Copyright 1994 TUM |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
5 |
*) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
6 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
7 |
open Denotation; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
8 |
|
1696 | 9 |
|
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
10 |
(**** mono (Gamma(b,c)) ****) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
11 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
12 |
qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def] |
1465 | 13 |
"mono (Gamma b c)" |
1973 | 14 |
(fn _ => [Fast_tac 1]); |
1481 | 15 |
|
1696 | 16 |
|
5069 | 17 |
Goal "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"; |
2031 | 18 |
by (Simp_tac 1); |
19 |
by (EVERY[stac (Gamma_mono RS lfp_Tarski) 1, |
|
1696 | 20 |
stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong) 1, |
2031 | 21 |
Simp_tac 1, |
22 |
IF_UNSOLVED no_tac]); |
|
1481 | 23 |
qed "C_While_If"; |
24 |
||
1696 | 25 |
|
26 |
(* Operational Semantics implies Denotational Semantics *) |
|
27 |
||
5069 | 28 |
Goal "!!c s t. <c,s> -c-> t ==> (s,t) : C(c)"; |
1696 | 29 |
|
30 |
(* start with rule induction *) |
|
1731 | 31 |
by (etac evalc.induct 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4089
diff
changeset
|
32 |
by Auto_tac; |
1696 | 33 |
(* while *) |
2031 | 34 |
by (rewtac Gamma_def); |
2036 | 35 |
by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1); |
1973 | 36 |
by (Fast_tac 1); |
2036 | 37 |
by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1); |
1973 | 38 |
by (Fast_tac 1); |
1696 | 39 |
|
1731 | 40 |
qed "com1"; |
1696 | 41 |
|
42 |
(* Denotational Semantics implies Operational Semantics *) |
|
43 |
||
5069 | 44 |
Goal "!s t. (s,t):C(c) --> <c,s> -c-> t"; |
1696 | 45 |
by (com.induct_tac "c" 1); |
1973 | 46 |
|
2031 | 47 |
by (ALLGOALS Full_simp_tac); |
48 |
by (ALLGOALS (TRY o Fast_tac)); |
|
1696 | 49 |
|
50 |
(* while *) |
|
51 |
by (strip_tac 1); |
|
52 |
by (etac (Gamma_mono RSN (2,induct)) 1); |
|
53 |
by (rewtac Gamma_def); |
|
1973 | 54 |
by (Fast_tac 1); |
1696 | 55 |
|
56 |
qed_spec_mp "com2"; |
|
57 |
||
58 |
||
59 |
(**** Proof of Equivalence ****) |
|
60 |
||
5069 | 61 |
Goal "(s,t) : C(c) = (<c,s> -c-> t)"; |
4089 | 62 |
by (fast_tac (claset() addEs [com2] addDs [com1]) 1); |
1696 | 63 |
qed "denotational_is_natural"; |