equal
deleted
inserted
replaced
1 (* Title: HOLCF/IOA/meta_theory/Simulations.ML |
1 (* Title: HOLCF/IOA/meta_theory/Simulations.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Müller |
3 Author: Olaf Müller |
4 |
|
5 Simulations in HOLCF/IOA. |
|
6 *) |
4 *) |
7 |
|
8 |
|
9 |
5 |
10 Goal "(A~={}) = (? x. x:A)"; |
6 Goal "(A~={}) = (? x. x:A)"; |
11 by (safe_tac set_cs); |
7 by (safe_tac set_cs); |
12 by Auto_tac; |
8 by Auto_tac; |
13 qed"set_non_empty"; |
9 qed"set_non_empty"; |
27 |
23 |
28 Goalw [is_ref_map_def,is_simulation_def] |
24 Goalw [is_ref_map_def,is_simulation_def] |
29 "!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A"; |
25 "!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A"; |
30 by (Asm_full_simp_tac 1); |
26 by (Asm_full_simp_tac 1); |
31 qed"ref_map_is_simulation"; |
27 qed"ref_map_is_simulation"; |
32 |
|
33 |
|
34 |
|
35 |
|