src/HOL/IOA/Solve.thy
author wenzelm
Mon Mar 22 20:58:52 2010 +0100 (2010-03-22)
changeset 35898 c890a3835d15
parent 35416 d8d7d1b785af
child 36862 952b2b102a0a
permissions -rw-r--r--
recovered header;
     1 (*  Title:      HOL/IOA/Solve.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  TU Muenchen
     5 *)
     6 
     7 header {* Weak possibilities mapping (abstraction) *}
     8 
     9 theory Solve
    10 imports IOA
    11 begin
    12 
    13 definition is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool" where
    14   "is_weak_pmap f C A ==
    15    (!s:starts_of(C). f(s):starts_of(A)) &
    16    (!s t a. reachable C s &
    17             (s,a,t):trans_of(C)
    18             --> (if a:externals(asig_of(C)) then
    19                    (f(s),a,f(t)):trans_of(A)
    20                  else f(s)=f(t)))"
    21 
    22 declare mk_trace_thm [simp] trans_in_actions [simp]
    23 
    24 lemma trace_inclusion: 
    25   "[| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A));  
    26            is_weak_pmap f C A |] ==> traces(C) <= traces(A)"
    27   apply (unfold is_weak_pmap_def traces_def)
    28 
    29   apply (simp (no_asm) add: has_trace_def)
    30   apply safe
    31   apply (rename_tac ex1 ex2)
    32 
    33   (* choose same trace, therefore same NF *)
    34   apply (rule_tac x = "mk_trace C ex1" in exI)
    35   apply simp
    36 
    37   (* give execution of abstract automata *)
    38   apply (rule_tac x = "(mk_trace A ex1,%i. f (ex2 i))" in bexI)
    39 
    40   (* Traces coincide *)
    41    apply (simp (no_asm_simp) add: mk_trace_def filter_oseq_idemp)
    42 
    43   (* Use lemma *)
    44   apply (frule states_of_exec_reachable)
    45 
    46   (* Now show that it's an execution *)
    47   apply (simp add: executions_def)
    48   apply safe
    49 
    50   (* Start states map to start states *)
    51   apply (drule bspec)
    52   apply assumption
    53 
    54   (* Show that it's an execution fragment *)
    55   apply (simp add: is_execution_fragment_def)
    56   apply safe
    57 
    58   apply (erule_tac x = "ex2 n" in allE)
    59   apply (erule_tac x = "ex2 (Suc n)" in allE)
    60   apply (erule_tac x = a in allE)
    61   apply simp
    62   done
    63 
    64 (* Lemmata *)
    65 
    66 lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R"
    67   by blast
    68 
    69 
    70 (* fist_order_tautology of externals_of_par *)
    71 lemma externals_of_par_extra:
    72   "a:externals(asig_of(A1||A2)) =     
    73    (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) |   
    74    a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |   
    75    a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))"
    76   apply (auto simp add: externals_def asig_of_par asig_comp_def asig_inputs_def asig_outputs_def)
    77   done
    78 
    79 lemma comp1_reachable: "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)"
    80   apply (simp add: reachable_def)
    81   apply (erule bexE)
    82   apply (rule_tac x =
    83     "(filter_oseq (%a. a:actions (asig_of (C1))) (fst ex) , %i. fst (snd ex i))" in bexI)
    84 (* fst(s) is in projected execution *)
    85   apply force
    86 (* projected execution is indeed an execution *)
    87   apply (simp cong del: if_weak_cong
    88     add: executions_def is_execution_fragment_def par_def starts_of_def
    89       trans_of_def filter_oseq_def
    90     split add: option.split)
    91   done
    92 
    93 
    94 (* Exact copy of proof of comp1_reachable for the second
    95    component of a parallel composition.     *)
    96 lemma comp2_reachable: "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)"
    97   apply (simp add: reachable_def)
    98   apply (erule bexE)
    99   apply (rule_tac x =
   100     "(filter_oseq (%a. a:actions (asig_of (C2))) (fst ex) , %i. snd (snd ex i))" in bexI)
   101 (* fst(s) is in projected execution *)
   102   apply force
   103 (* projected execution is indeed an execution *)
   104   apply (simp cong del: if_weak_cong
   105     add: executions_def is_execution_fragment_def par_def starts_of_def
   106     trans_of_def filter_oseq_def
   107     split add: option.split)
   108   done
   109 
   110 declare split_if [split del] if_weak_cong [cong del]
   111 
   112 (*Composition of possibility-mappings *)
   113 lemma fxg_is_weak_pmap_of_product_IOA: 
   114      "[| is_weak_pmap f C1 A1;  
   115          externals(asig_of(A1))=externals(asig_of(C1)); 
   116          is_weak_pmap g C2 A2;   
   117          externals(asig_of(A2))=externals(asig_of(C2));  
   118          compat_ioas C1 C2; compat_ioas A1 A2  |]      
   119    ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)"
   120   apply (unfold is_weak_pmap_def)
   121   apply (rule conjI)
   122 (* start_states *)
   123   apply (simp add: par_def starts_of_def)
   124 (* transitions *)
   125   apply (rule allI)+
   126   apply (rule imp_conj_lemma)
   127   apply (simp (no_asm) add: externals_of_par_extra)
   128   apply (simp (no_asm) add: par_def)
   129   apply (simp add: trans_of_def)
   130   apply (simplesubst split_if)
   131   apply (rule conjI)
   132   apply (rule impI)
   133   apply (erule disjE)
   134 (* case 1      a:e(A1) | a:e(A2) *)
   135   apply (simp add: comp1_reachable comp2_reachable ext_is_act)
   136   apply (erule disjE)
   137 (* case 2      a:e(A1) | a~:e(A2) *)
   138   apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act2)
   139 (* case 3      a:~e(A1) | a:e(A2) *)
   140   apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act1)
   141 (* case 4      a:~e(A1) | a~:e(A2) *)
   142   apply (rule impI)
   143   apply (subgoal_tac "a~:externals (asig_of (A1)) & a~:externals (asig_of (A2))")
   144 (* delete auxiliary subgoal *)
   145   prefer 2
   146   apply force
   147   apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
   148   apply (tactic {*
   149     REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
   150       asm_full_simp_tac(@{simpset} addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *})
   151   done
   152 
   153 
   154 lemma reachable_rename_ioa: "[| reachable (rename C g) s |] ==> reachable C s"
   155   apply (simp add: reachable_def)
   156   apply (erule bexE)
   157   apply (rule_tac x = "((%i. case (fst ex i) of None => None | Some (x) => g x) ,snd ex)" in bexI)
   158   apply (simp (no_asm))
   159 (* execution is indeed an execution of C *)
   160   apply (simp add: executions_def is_execution_fragment_def par_def
   161     starts_of_def trans_of_def rename_def split add: option.split)
   162   apply force
   163   done
   164 
   165 
   166 lemma rename_through_pmap: "[| is_weak_pmap f C A |] 
   167                        ==> (is_weak_pmap f (rename C g) (rename A g))"
   168   apply (simp add: is_weak_pmap_def)
   169   apply (rule conjI)
   170   apply (simp add: rename_def starts_of_def)
   171   apply (rule allI)+
   172   apply (rule imp_conj_lemma)
   173   apply (simp (no_asm) add: rename_def)
   174   apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
   175   apply safe
   176   apply (simplesubst split_if)
   177   apply (rule conjI)
   178   apply (rule impI)
   179   apply (erule disjE)
   180   apply (erule exE)
   181   apply (erule conjE)
   182 (* x is input *)
   183   apply (drule sym)
   184   apply (drule sym)
   185   apply simp
   186   apply hypsubst+
   187   apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
   188   apply assumption
   189   apply simp
   190 (* x is output *)
   191   apply (erule exE)
   192   apply (erule conjE)
   193   apply (drule sym)
   194   apply (drule sym)
   195   apply simp
   196   apply hypsubst+
   197   apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
   198   apply assumption
   199   apply simp
   200 (* x is internal *)
   201   apply (simp (no_asm) add: de_Morgan_disj de_Morgan_conj not_ex cong add: conj_cong)
   202   apply (rule impI)
   203   apply (erule conjE)
   204   apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
   205   apply auto
   206   done
   207 
   208 declare split_if [split] if_weak_cong [cong]
   209 
   210 end