IOA/meta_theory/Solve.ML
changeset 252 a4dc62a46ee4
parent 251 f04b33ce250f
child 253 132634d24019
equal deleted inserted replaced
251:f04b33ce250f 252:a4dc62a46ee4
     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";