966
|
1 |
(* Title: HOL/IOA/meta_theory/Solve.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow & Konrad Slind
|
|
4 |
Copyright 1994 TU Muenchen
|
|
5 |
|
|
6 |
Weak possibilities mapping (abstraction)
|
|
7 |
*)
|
|
8 |
|
|
9 |
open Solve;
|
|
10 |
|
|
11 |
val SS = SS addsimps [mk_behaviour_thm,trans_in_actions];
|
|
12 |
|
|
13 |
goalw Solve.thy [is_weak_pmap_def,behaviours_def]
|
|
14 |
"!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \
|
|
15 |
\ is_weak_pmap f C A |] ==> behaviours(C) <= behaviours(A)";
|
|
16 |
|
|
17 |
by (simp_tac(SS addsimps [has_behaviour_def])1);
|
|
18 |
by (safe_tac set_cs);
|
|
19 |
|
|
20 |
(* give execution of abstract automata *)
|
|
21 |
by (res_inst_tac[("x","<mk_behaviour A (fst ex),%i.f(snd ex i)>")] bexI 1);
|
|
22 |
|
|
23 |
(* Behaviours coincide *)
|
|
24 |
by (asm_simp_tac (SS addsimps [mk_behaviour_def,filter_oseq_idemp])1);
|
|
25 |
|
|
26 |
(* Use lemma *)
|
|
27 |
by (forward_tac [states_of_exec_reachable] 1);
|
|
28 |
|
|
29 |
(* Now show that it's an execution *)
|
|
30 |
by (asm_full_simp_tac(SS addsimps [executions_def]) 1);
|
|
31 |
by (safe_tac set_cs);
|
|
32 |
|
|
33 |
(* Start states map to start states *)
|
|
34 |
by (dtac bspec 1);
|
|
35 |
by (atac 1);
|
|
36 |
|
|
37 |
(* Show that it's an execution fragment *)
|
|
38 |
by (asm_full_simp_tac (SS addsimps [is_execution_fragment_def])1);
|
|
39 |
by (safe_tac HOL_cs);
|
|
40 |
|
|
41 |
by (eres_inst_tac [("x","snd ex n")] allE 1);
|
|
42 |
by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
|
|
43 |
by (eres_inst_tac [("x","a")] allE 1);
|
|
44 |
by (asm_full_simp_tac SS 1);
|
|
45 |
qed "trace_inclusion";
|