equal
deleted
inserted
replaced
|
1 (* Title: HOLCF/IOA/meta_theory/Simulations.ML |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 Copyright 1997 TU Muenchen |
|
5 |
|
6 Simulations in HOLCF/IOA |
|
7 *) |
|
8 |
|
9 |
|
10 |
|
11 goal thy "(A~={}) = (? x. x:A)"; |
|
12 by (safe_tac set_cs); |
|
13 auto(); |
|
14 qed"set_non_empty"; |
|
15 |
|
16 goal thy "(A Int B ~= {}) = (? x. x: A & x:B)"; |
|
17 by (simp_tac (simpset() addsimps [set_non_empty]) 1); |
|
18 qed"Int_non_empty"; |
|
19 |
|
20 |
|
21 goalw thy [Image_def] |
|
22 "(R^^{x} Int S ~= {}) = (? y. (x,y):R & y:S)"; |
|
23 by (simp_tac (simpset() addsimps [Int_non_empty]) 1); |
|
24 qed"Sim_start_convert"; |
|
25 |
|
26 Addsimps [Sim_start_convert]; |
|
27 |
|
28 |
|
29 goalw thy [is_ref_map_def,is_simulation_def] |
|
30 "!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A"; |
|
31 (* start states *) |
|
32 by (Asm_full_simp_tac 1); |
|
33 (* main case *) |
|
34 by (Blast_tac 1); |
|
35 qed"ref_map_is_simulation"; |
|
36 |
|
37 |
|
38 |
|
39 |