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"; |
|