src/HOLCF/IOA/meta_theory/Compositionality.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12218 6597093b77e7
child 17233 41eee2e7b465
permissions -rw-r--r--
Merged in license change from Isabelle2004
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/Compositionality.ML
mueller@3275
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
mueller@3071
     4
mueller@3071
     5
Compositionality of I/O automata
mueller@3071
     6
*) 
mueller@3071
     7
mueller@3071
     8
mueller@3275
     9
paulson@6161
    10
Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
paulson@4477
    11
by Auto_tac;
mueller@3275
    12
qed"compatibility_consequence3";
mueller@3275
    13
mueller@3275
    14
wenzelm@5068
    15
Goal 
mueller@3433
    16
"!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
nipkow@10835
    17
\           Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr";
paulson@3457
    18
by (rtac ForallPFilterQR 1);
nipkow@10835
    19
(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *)
paulson@3457
    20
by (assume_tac 2);
paulson@3457
    21
by (rtac compatibility_consequence3 1);
wenzelm@4098
    22
by (REPEAT (asm_full_simp_tac (simpset() 
mueller@3275
    23
                  addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
mueller@3275
    24
qed"Filter_actAisFilter_extA";
mueller@3275
    25
mueller@3275
    26
mueller@5976
    27
(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *)
mueller@3275
    28
paulson@6161
    29
Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
paulson@4477
    30
by Auto_tac;
mueller@3275
    31
qed"compatibility_consequence4";
mueller@3275
    32
paulson@6161
    33
Goal "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
nipkow@10835
    34
\           Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr";
paulson@3457
    35
by (rtac ForallPFilterQR 1);
paulson@3457
    36
by (assume_tac 2);
paulson@3457
    37
by (rtac compatibility_consequence4 1);
wenzelm@4098
    38
by (REPEAT (asm_full_simp_tac (simpset() 
mueller@3275
    39
                  addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
mueller@3275
    40
qed"Filter_actAisFilter_extA2";
mueller@3275
    41
mueller@3275
    42
mueller@3275
    43
(* -------------------------------------------------------------------------- *)
mueller@3275
    44
                     section " Main Compositionality Theorem ";
mueller@3275
    45
(* -------------------------------------------------------------------------- *)
mueller@3275
    46
mueller@3275
    47
mueller@3275
    48
paulson@6161
    49
Goal "[| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2;\
mueller@3521
    50
\            is_asig_of A1; is_asig_of A2; \
mueller@3521
    51
\            is_asig_of B1; is_asig_of B2; \
mueller@3433
    52
\            compatible A1 B1; compatible A2 B2; \
mueller@3071
    53
\            A1 =<| A2; \
mueller@3071
    54
\            B1 =<| B2 |] \
mueller@3071
    55
\        ==> (A1 || B1) =<| (A2 || B2)";
mueller@3275
    56
wenzelm@4098
    57
by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def]) 1);
paulson@4473
    58
by (forw_inst_tac [("A1","A1")] (compat_commute RS iffD1) 1);
paulson@4473
    59
by (forw_inst_tac [("A1","A2")] (compat_commute RS iffD1) 1);
wenzelm@4098
    60
by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def,
mueller@3275
    61
          inputs_of_par,outputs_of_par,externals_of_par]) 1);
mueller@3275
    62
by (safe_tac set_cs);
wenzelm@4098
    63
by (asm_full_simp_tac (simpset() addsimps [compositionality_tr]) 1);
mueller@3275
    64
by (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2" 1);
wenzelm@4098
    65
by (asm_full_simp_tac (simpset() addsimps [externals_def]) 2);
mueller@3275
    66
by (REPEAT (etac conjE 1));
mueller@3275
    67
(* rewrite with proven subgoal *)
wenzelm@4098
    68
by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
mueller@3275
    69
by (safe_tac set_cs);
mueller@3275
    70
mueller@3275
    71
(* 2 goals, the 3rd has been solved automatically *)
mueller@3275
    72
(* 1: Filter A2 x : traces A2 *)
mueller@3275
    73
by (dres_inst_tac [("A","traces A1")] subsetD 1);
paulson@3457
    74
by (assume_tac 1);
wenzelm@4098
    75
by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA]) 1);
mueller@3275
    76
(* 2: Filter B2 x : traces B2 *)
mueller@3275
    77
by (dres_inst_tac [("A","traces B1")] subsetD 1);
paulson@3457
    78
by (assume_tac 1);
wenzelm@4098
    79
by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA2]) 1);
mueller@3275
    80
qed"compositionality";
mueller@3071
    81
mueller@3071
    82
mueller@3071
    83
mueller@3275
    84