| author | clasohm |
| Fri, 19 Jan 1996 12:49:36 +0100 | |
| changeset 253 | 132634d24019 |
| permissions | -rw-r--r-- |
|
253
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
1 |
(* Title: HOL/IMP/Denotation.ML |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
4 |
Copyright 1994 TUM |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
5 |
*) |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
6 |
|
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
7 |
open Denotation; |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
8 |
|
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
9 |
(**** Rewrite Rules for A,B,C ****) |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
10 |
|
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
11 |
val A_simps = |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
12 |
[A_nat,A_loc,A_op1,A_op2]; |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
13 |
|
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
14 |
val B_simps = map (fn t => t RS eq_reflection) |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
15 |
[B_true,B_false,B_op,B_not,B_and,B_or] |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
16 |
|
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
17 |
val C_simps = map (fn t => t RS eq_reflection) |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
18 |
[C_skip,C_assign,C_comp,C_if,C_while]; |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
19 |
|
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
20 |
(**** mono (Gamma(b,c)) ****) |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
21 |
|
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
22 |
qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def] |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
23 |
"mono(Gamma(b,c))" |
|
132634d24019
accidentally deleted these files from the repository; now adding them and
clasohm
parents:
diff
changeset
|
24 |
(fn _ => [(best_tac comp_cs 1)]); |