|
1 open Solve IOA Asig; |
|
2 |
|
3 val SS = SS addsimps [mk_behaviour_thm,trans_in_actions]; |
|
4 |
|
5 goalw Solve.thy [is_weak_pmap_def,behaviours_def] |
|
6 "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \ |
|
7 \ is_weak_pmap(f,C,A) |] ==> behaviours(C) <= behaviours(A)"; |
|
8 |
|
9 by (simp_tac(SS addsimps [has_behaviour_def])1); |
|
10 by (safe_tac set_cs); |
|
11 |
|
12 (* give execution of abstract automata *) |
|
13 by (res_inst_tac[("x","<mk_behaviour(A,fst(ex)),%i.f(snd(ex,i))>")] bexI 1); |
|
14 |
|
15 (* Behaviours coincide *) |
|
16 by (asm_simp_tac (SS addsimps [mk_behaviour_def,filter_oseq_idemp])1); |
|
17 |
|
18 (* Use lemma *) |
|
19 by (forward_tac [states_of_exec_reachable] 1); |
|
20 |
|
21 (* Now show that it's an execution *) |
|
22 by (asm_full_simp_tac(SS addsimps [executions_def]) 1); |
|
23 by (safe_tac set_cs); |
|
24 |
|
25 (* Start states map to start states *) |
|
26 by (dtac bspec 1); |
|
27 by (atac 1); |
|
28 |
|
29 (* Show that it's an execution fragment *) |
|
30 by (asm_full_simp_tac (SS addsimps [is_execution_fragment_def])1); |
|
31 by (safe_tac HOL_cs); |
|
32 |
|
33 (* Cases on whether action is external or not (basically) *) |
|
34 (* 1 *) |
|
35 by (eres_inst_tac [("x","snd(ex,n)")] allE 1); |
|
36 by (eres_inst_tac [("x","snd(ex,Suc(n))")] allE 1); |
|
37 by (eres_inst_tac [("x","aa")] allE 1); |
|
38 by (asm_full_simp_tac SS 1); |
|
39 |
|
40 (* 2 *) |
|
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 val trace_inclusion = result(); |