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