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