src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 61999 89291b5d0ede
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/IOA/meta_theory/Compositionality.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 section {* Compositionality of I/O automata *}
     6 theory Compositionality
     7 imports CompoTraces
     8 begin
     9 
    10 lemma compatibility_consequence3: "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA"
    11 apply auto
    12 done
    13 
    14 
    15 lemma Filter_actAisFilter_extA: 
    16 "!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==>  
    17             Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"
    18 apply (rule ForallPFilterQR)
    19 (* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *)
    20 prefer 2 apply (assumption)
    21 apply (rule compatibility_consequence3)
    22 apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
    23 done
    24 
    25 
    26 (* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *)
    27 
    28 lemma compatibility_consequence4: "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA"
    29 apply auto
    30 done
    31 
    32 lemma Filter_actAisFilter_extA2: "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==>  
    33             Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"
    34 apply (rule ForallPFilterQR)
    35 prefer 2 apply (assumption)
    36 apply (rule compatibility_consequence4)
    37 apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
    38 done
    39 
    40 
    41 subsection " Main Compositionality Theorem "
    42 
    43 lemma compositionality: "[| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2; 
    44              is_asig_of A1; is_asig_of A2;  
    45              is_asig_of B1; is_asig_of B2;  
    46              compatible A1 B1; compatible A2 B2;  
    47              A1 =<| A2;  
    48              B1 =<| B2 |]  
    49          ==> (A1 || B1) =<| (A2 || B2)"
    50 apply (simp add: is_asig_of_def)
    51 apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1])
    52 apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1])
    53 apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par)
    54 apply auto
    55 apply (simp add: compositionality_tr)
    56 apply (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2")
    57 prefer 2
    58 apply (simp add: externals_def)
    59 apply (erule conjE)+
    60 (* rewrite with proven subgoal *)
    61 apply (simp add: externals_of_par)
    62 apply auto
    63 
    64 (* 2 goals, the 3rd has been solved automatically *)
    65 (* 1: Filter A2 x : traces A2 *)
    66 apply (drule_tac A = "traces A1" in subsetD)
    67 apply assumption
    68 apply (simp add: Filter_actAisFilter_extA)
    69 (* 2: Filter B2 x : traces B2 *)
    70 apply (drule_tac A = "traces B1" in subsetD)
    71 apply assumption
    72 apply (simp add: Filter_actAisFilter_extA2)
    73 done
    74 
    75 end