3807
|
1 |
(*
|
|
2 |
File: MemoryParameters.ML
|
|
3 |
Author: Stephan Merz
|
|
4 |
Copyright: 1997 University of Munich
|
|
5 |
|
|
6 |
RPC-Memory example: memory parameters (ML file)
|
|
7 |
*)
|
|
8 |
|
6255
|
9 |
(*
|
3807
|
10 |
val MP_simps = [BadArgNoMemVal,MemFailNoMemVal,InitValMemVal,NotAResultNotVal,
|
|
11 |
NotAResultNotOK, NotAResultNotBA, NotAResultNotMF]
|
|
12 |
@ (map (fn x => x RS not_sym)
|
|
13 |
[NotAResultNotOK, NotAResultNotBA, NotAResultNotMF]);
|
6255
|
14 |
*)
|
3807
|
15 |
|
6255
|
16 |
Addsimps ([BadArgNoMemVal,MemFailNoMemVal,InitValMemVal,NotAResultNotVal,
|
|
17 |
NotAResultNotOK, NotAResultNotBA, NotAResultNotMF]
|
|
18 |
@ (map (fn x => x RS not_sym)
|
|
19 |
[NotAResultNotOK, NotAResultNotBA, NotAResultNotMF]));
|
3807
|
20 |
|
|
21 |
(* Auxiliary rules *)
|
|
22 |
|
|
23 |
qed_goal "MemValNotAResultE" MemoryParameters.thy
|
6255
|
24 |
"[| x : MemVal; (x ~= NotAResult ==> P) |] ==> P"
|
|
25 |
(fn prems => [resolve_tac prems 1,
|
|
26 |
cut_facts_tac (NotAResultNotVal::prems) 1,
|
|
27 |
Force_tac 1
|
|
28 |
]);
|
3807
|
29 |
|