author | clasohm |
Fri, 03 Mar 1995 12:04:16 +0100 | |
changeset 924 | 806721cfbf46 |
child 1266 | 3ae9fe3c0f68 |
permissions | -rw-r--r-- |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
1 |
(* Title: HOL/IMP/Denotation.ML |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM |
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 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
9 |
(**** Rewrite Rules for A,B,C ****) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
10 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
11 |
val A_simps = |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
12 |
[A_nat,A_loc,A_op1,A_op2]; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
13 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
14 |
val B_simps = map (fn t => t RS eq_reflection) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
15 |
[B_true,B_false,B_op,B_not,B_and,B_or] |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
16 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
17 |
val C_simps = map (fn t => t RS eq_reflection) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
18 |
[C_skip,C_assign,C_comp,C_if,C_while]; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
19 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
20 |
(**** mono (Gamma(b,c)) ****) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
21 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
22 |
qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def] |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
23 |
"mono (Gamma b c)" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
24 |
(fn _ => [(best_tac comp_cs 1)]); |