4565
|
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 |
|
5068
|
11 |
Goal "(A~={}) = (? x. x:A)";
|
4565
|
12 |
by (safe_tac set_cs);
|
|
13 |
auto();
|
|
14 |
qed"set_non_empty";
|
|
15 |
|
5068
|
16 |
Goal "(A Int B ~= {}) = (? x. x: A & x:B)";
|
4565
|
17 |
by (simp_tac (simpset() addsimps [set_non_empty]) 1);
|
|
18 |
qed"Int_non_empty";
|
|
19 |
|
|
20 |
|
5068
|
21 |
Goalw [Image_def]
|
4565
|
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 |
|
5068
|
29 |
Goalw [is_ref_map_def,is_simulation_def]
|
4565
|
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 |
|