author | nipkow |
Wed, 11 Oct 2000 09:09:06 +0200 | |
changeset 10186 | 499637e8f2c6 |
parent 5223 | 4cb05273f764 |
child 10202 | 9e8b4bebc940 |
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 |
(**** mono (Gamma(b,c)) ****) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
8 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
9 |
qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def] |
1465 | 10 |
"mono (Gamma b c)" |
1973 | 11 |
(fn _ => [Fast_tac 1]); |
1481 | 12 |
|
1696 | 13 |
|
5069 | 14 |
Goal "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"; |
2031 | 15 |
by (Simp_tac 1); |
10186 | 16 |
by (EVERY[stac (Gamma_mono RS lfp_unfold) 1, |
1696 | 17 |
stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong) 1, |
2031 | 18 |
Simp_tac 1, |
19 |
IF_UNSOLVED no_tac]); |
|
1481 | 20 |
qed "C_While_If"; |
21 |
||
1696 | 22 |
|
23 |
(* Operational Semantics implies Denotational Semantics *) |
|
24 |
||
5117 | 25 |
Goal "<c,s> -c-> t ==> (s,t) : C(c)"; |
1696 | 26 |
|
27 |
(* start with rule induction *) |
|
1731 | 28 |
by (etac evalc.induct 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4089
diff
changeset
|
29 |
by Auto_tac; |
1696 | 30 |
(* while *) |
2031 | 31 |
by (rewtac Gamma_def); |
10186 | 32 |
by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_unfold)) 1); |
1973 | 33 |
by (Fast_tac 1); |
10186 | 34 |
by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_unfold)) 1); |
1973 | 35 |
by (Fast_tac 1); |
1696 | 36 |
|
1731 | 37 |
qed "com1"; |
1696 | 38 |
|
39 |
(* Denotational Semantics implies Operational Semantics *) |
|
40 |
||
5069 | 41 |
Goal "!s t. (s,t):C(c) --> <c,s> -c-> t"; |
5183 | 42 |
by (induct_tac "c" 1); |
1973 | 43 |
|
2031 | 44 |
by (ALLGOALS Full_simp_tac); |
45 |
by (ALLGOALS (TRY o Fast_tac)); |
|
1696 | 46 |
|
47 |
(* while *) |
|
48 |
by (strip_tac 1); |
|
49 |
by (etac (Gamma_mono RSN (2,induct)) 1); |
|
50 |
by (rewtac Gamma_def); |
|
1973 | 51 |
by (Fast_tac 1); |
1696 | 52 |
|
53 |
qed_spec_mp "com2"; |
|
54 |
||
55 |
||
56 |
(**** Proof of Equivalence ****) |
|
57 |
||
5069 | 58 |
Goal "(s,t) : C(c) = (<c,s> -c-> t)"; |
4089 | 59 |
by (fast_tac (claset() addEs [com2] addDs [com1]) 1); |
1696 | 60 |
qed "denotational_is_natural"; |