src/HOLCF/IOA/meta_theory/CompoExecs.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 7229 6773ba0c36d5
child 11655 923e4d0d36d5
permissions -rw-r--r--
` -> $
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/CompoExecs.ML
mueller@3275
     2
    ID:         $Id$
mueller@3071
     3
    Author:     Olaf M"uller
mueller@3071
     4
    Copyright   1996  TU Muenchen
mueller@3071
     5
mueller@3071
     6
Compositionality on Execution level.
mueller@3071
     7
*)  
mueller@3071
     8
mueller@3071
     9
Delsimps (ex_simps @ all_simps); 
mueller@3071
    10
Delsimps [split_paired_All];
mueller@3071
    11
mueller@3071
    12
(* ----------------------------------------------------------------------------------- *)
mueller@3071
    13
mueller@3071
    14
mueller@3071
    15
section "recursive equations of operators";
mueller@3071
    16
mueller@3071
    17
mueller@3071
    18
(* ---------------------------------------------------------------- *)
mueller@3071
    19
(*                               ProjA2                             *)
mueller@3071
    20
(* ---------------------------------------------------------------- *)
mueller@3071
    21
mueller@3071
    22
nipkow@10835
    23
Goal  "ProjA2$UU = UU";
wenzelm@4098
    24
by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
mueller@3071
    25
qed"ProjA2_UU";
mueller@3071
    26
nipkow@10835
    27
Goal  "ProjA2$nil = nil";
wenzelm@4098
    28
by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
mueller@3071
    29
qed"ProjA2_nil";
mueller@3071
    30
nipkow@10835
    31
Goal "ProjA2$((a,t)>>xs) = (a,fst t) >> ProjA2$xs";
wenzelm@4098
    32
by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
mueller@3071
    33
qed"ProjA2_cons";
mueller@3071
    34
mueller@3071
    35
mueller@3071
    36
(* ---------------------------------------------------------------- *)
mueller@3071
    37
(*                               ProjB2                             *)
mueller@3071
    38
(* ---------------------------------------------------------------- *)
mueller@3071
    39
mueller@3071
    40
nipkow@10835
    41
Goal  "ProjB2$UU = UU";
wenzelm@4098
    42
by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
mueller@3071
    43
qed"ProjB2_UU";
mueller@3071
    44
nipkow@10835
    45
Goal  "ProjB2$nil = nil";
wenzelm@4098
    46
by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
mueller@3071
    47
qed"ProjB2_nil";
mueller@3071
    48
nipkow@10835
    49
Goal "ProjB2$((a,t)>>xs) = (a,snd t) >> ProjB2$xs";
wenzelm@4098
    50
by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
mueller@3071
    51
qed"ProjB2_cons";
mueller@3071
    52
mueller@3071
    53
mueller@3071
    54
mueller@3071
    55
(* ---------------------------------------------------------------- *)
mueller@3071
    56
(*                             Filter_ex2                           *)
mueller@3071
    57
(* ---------------------------------------------------------------- *)
mueller@3071
    58
mueller@3071
    59
nipkow@10835
    60
Goal "Filter_ex2 sig$UU=UU";
wenzelm@4098
    61
by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
mueller@3071
    62
qed"Filter_ex2_UU";
mueller@3071
    63
nipkow@10835
    64
Goal "Filter_ex2 sig$nil=nil";
wenzelm@4098
    65
by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
mueller@3071
    66
qed"Filter_ex2_nil";
mueller@3071
    67
nipkow@10835
    68
Goal "Filter_ex2 sig$(at >> xs) =    \
mueller@3521
    69
\            (if (fst at:actions sig)    \       
nipkow@10835
    70
\                 then at >> (Filter_ex2 sig$xs) \   
nipkow@10835
    71
\                 else        Filter_ex2 sig$xs)";
mueller@3071
    72
wenzelm@4098
    73
by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
mueller@3071
    74
qed"Filter_ex2_cons";
mueller@3071
    75
mueller@3071
    76
mueller@3071
    77
(* ---------------------------------------------------------------- *)
mueller@3071
    78
(*                             stutter2                             *)
mueller@3071
    79
(* ---------------------------------------------------------------- *)
mueller@3071
    80
mueller@3071
    81
wenzelm@5068
    82
Goal "stutter2 sig = (LAM ex. (%s. case ex of \
mueller@3071
    83
\      nil => TT \
mueller@3071
    84
\    | x##xs => (flift1 \ 
mueller@3521
    85
\            (%p.(If Def ((fst p)~:actions sig) \
mueller@3071
    86
\                 then Def (s=(snd p)) \
mueller@3071
    87
\                 else TT fi) \
nipkow@10835
    88
\                andalso (stutter2 sig$xs) (snd p))  \
nipkow@10835
    89
\             $x) \
mueller@3071
    90
\           ))";
mueller@3071
    91
by (rtac trans 1);
paulson@3457
    92
by (rtac fix_eq2 1);
paulson@3457
    93
by (rtac stutter2_def 1);
paulson@3457
    94
by (rtac beta_cfun 1);
wenzelm@4098
    95
by (simp_tac (simpset() addsimps [flift1_def]) 1);
mueller@3071
    96
qed"stutter2_unfold";
mueller@3071
    97
nipkow@10835
    98
Goal "(stutter2 sig$UU) s=UU";
mueller@3071
    99
by (stac stutter2_unfold 1);
mueller@3071
   100
by (Simp_tac 1);
mueller@3071
   101
qed"stutter2_UU";
mueller@3071
   102
nipkow@10835
   103
Goal "(stutter2 sig$nil) s = TT";
mueller@3071
   104
by (stac stutter2_unfold 1);
mueller@3071
   105
by (Simp_tac 1);
mueller@3071
   106
qed"stutter2_nil";
mueller@3071
   107
nipkow@10835
   108
Goal "(stutter2 sig$(at>>xs)) s = \
mueller@3521
   109
\              ((if (fst at)~:actions sig then Def (s=snd at) else TT) \
nipkow@10835
   110
\                andalso (stutter2 sig$xs) (snd at))"; 
wenzelm@4423
   111
by (rtac trans 1);
mueller@3071
   112
by (stac stutter2_unfold 1);
wenzelm@7229
   113
by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1);
mueller@3071
   114
by (Simp_tac 1);
mueller@3071
   115
qed"stutter2_cons";
mueller@3071
   116
mueller@3071
   117
mueller@3071
   118
Addsimps [stutter2_UU,stutter2_nil,stutter2_cons];
mueller@3071
   119
mueller@3071
   120
mueller@3071
   121
(* ---------------------------------------------------------------- *)
mueller@3071
   122
(*                             stutter                              *)
mueller@3071
   123
(* ---------------------------------------------------------------- *)
mueller@3071
   124
wenzelm@5068
   125
Goal "stutter sig (s, UU)";
wenzelm@4098
   126
by (simp_tac (simpset() addsimps [stutter_def]) 1);
mueller@3071
   127
qed"stutter_UU";
mueller@3071
   128
wenzelm@5068
   129
Goal "stutter sig (s, nil)";
wenzelm@4098
   130
by (simp_tac (simpset() addsimps [stutter_def]) 1);
mueller@3071
   131
qed"stutter_nil";
mueller@3071
   132
wenzelm@5068
   133
Goal "stutter sig (s, (a,t)>>ex) = \
mueller@3521
   134
\     ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
nipkow@4833
   135
by (simp_tac (simpset() addsimps [stutter_def]) 1);
mueller@3071
   136
qed"stutter_cons";
mueller@3071
   137
mueller@3071
   138
(* ----------------------------------------------------------------------------------- *)
mueller@3071
   139
mueller@3071
   140
Delsimps [stutter2_UU,stutter2_nil,stutter2_cons];
mueller@3071
   141
mueller@3071
   142
val compoex_simps = [ProjA2_UU,ProjA2_nil,ProjA2_cons,
mueller@3071
   143
                     ProjB2_UU,ProjB2_nil,ProjB2_cons,
mueller@3071
   144
                     Filter_ex2_UU,Filter_ex2_nil,Filter_ex2_cons,
mueller@3071
   145
                     stutter_UU,stutter_nil,stutter_cons];
mueller@3071
   146
mueller@3071
   147
Addsimps compoex_simps;
mueller@3071
   148
mueller@3071
   149
mueller@3071
   150
mueller@3071
   151
(* ------------------------------------------------------------------ *)
mueller@3071
   152
(*                      The following lemmata aim for                 *)
mueller@3071
   153
(*             COMPOSITIONALITY   on    EXECUTION     Level           *)
mueller@3071
   154
(* ------------------------------------------------------------------ *)
mueller@3071
   155
mueller@3071
   156
mueller@3071
   157
(* --------------------------------------------------------------------- *)
mueller@3071
   158
(*  Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B    *)
mueller@3071
   159
(* --------------------------------------------------------------------- *)
mueller@3071
   160
wenzelm@5068
   161
Goal "!s. is_exec_frag (A||B) (s,xs) \
nipkow@10835
   162
\      -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &\
nipkow@10835
   163
\           is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))";
mueller@3071
   164
mueller@3433
   165
by (pair_induct_tac "xs" [is_exec_frag_def] 1);
mueller@3071
   166
(* main case *)
mueller@3071
   167
ren "ss a t" 1;
mueller@3071
   168
by (safe_tac set_cs);
nipkow@4833
   169
by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
mueller@3071
   170
qed"lemma_1_1a";
mueller@3071
   171
mueller@3071
   172
mueller@3071
   173
(* --------------------------------------------------------------------- *)
mueller@3071
   174
(*  Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections       *)
mueller@3071
   175
(* --------------------------------------------------------------------- *)
mueller@3071
   176
wenzelm@5068
   177
Goal "!s. is_exec_frag (A||B) (s,xs) \
nipkow@10835
   178
\      --> stutter (asig_of A) (fst s,ProjA2$xs)  &\
nipkow@10835
   179
\          stutter (asig_of B) (snd s,ProjB2$xs)"; 
mueller@3071
   180
mueller@3433
   181
by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
mueller@3071
   182
(* main case *)
mueller@3071
   183
by (safe_tac set_cs);
nipkow@4833
   184
by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
mueller@3071
   185
qed"lemma_1_1b";
mueller@3071
   186
mueller@3071
   187
mueller@3071
   188
(* --------------------------------------------------------------------- *)
mueller@3071
   189
(*  Lemma_1_1c : Executions of A||B have only  A- or B-actions           *)
mueller@3071
   190
(* --------------------------------------------------------------------- *)
mueller@3071
   191
wenzelm@5068
   192
Goal "!s. (is_exec_frag (A||B) (s,xs) \
wenzelm@3842
   193
\  --> Forall (%x. fst x:act (A||B)) xs)";
mueller@3071
   194
mueller@3433
   195
by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1);
mueller@3071
   196
(* main case *)
mueller@3071
   197
by (safe_tac set_cs);
wenzelm@4098
   198
by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ 
mueller@3071
   199
                                [actions_asig_comp,asig_of_par]) 1));
mueller@3071
   200
qed"lemma_1_1c";
mueller@3071
   201
mueller@3071
   202
mueller@3071
   203
(* ----------------------------------------------------------------------- *)
mueller@3071
   204
(*  Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B)   *)
mueller@3071
   205
(* ----------------------------------------------------------------------- *)
mueller@3071
   206
wenzelm@5068
   207
Goal 
nipkow@10835
   208
"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &\
nipkow@10835
   209
\    is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &\
nipkow@10835
   210
\    stutter (asig_of A) (fst s,(ProjA2$xs)) & \
nipkow@10835
   211
\    stutter (asig_of B) (snd s,(ProjB2$xs)) & \
wenzelm@3842
   212
\    Forall (%x. fst x:act (A||B)) xs \
mueller@3433
   213
\    --> is_exec_frag (A||B) (s,xs)";
mueller@3071
   214
mueller@3071
   215
by (pair_induct_tac "xs" [Forall_def,sforall_def,
mueller@3433
   216
         is_exec_frag_def, stutter_def] 1);
nipkow@4681
   217
by (asm_full_simp_tac (simpset() addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]) 1);
mueller@3071
   218
by (safe_tac set_cs);
mueller@3071
   219
(* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *)
mueller@3071
   220
by (rotate_tac ~4 1);
nipkow@4681
   221
by (Asm_full_simp_tac 1);
mueller@3071
   222
by (rotate_tac ~4 1);
nipkow@4681
   223
by (Asm_full_simp_tac 1);
mueller@3071
   224
qed"lemma_1_2";
mueller@3071
   225
mueller@3071
   226
mueller@3071
   227
(* ------------------------------------------------------------------ *)
mueller@3071
   228
(*           COMPOSITIONALITY   on    EXECUTION     Level             *)
mueller@3071
   229
(*                          Main Theorem                              *)
mueller@3071
   230
(* ------------------------------------------------------------------ *)
mueller@3071
   231
mueller@3071
   232
wenzelm@5068
   233
Goal 
mueller@3071
   234
"ex:executions(A||B) =\
mueller@3521
   235
\(Filter_ex (asig_of A) (ProjA ex) : executions A &\
mueller@3521
   236
\ Filter_ex (asig_of B) (ProjB ex) : executions B &\
mueller@3521
   237
\ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
wenzelm@3842
   238
\ Forall (%x. fst x:act (A||B)) (snd ex))";
mueller@3071
   239
wenzelm@4098
   240
by (simp_tac (simpset() addsimps [executions_def,ProjB_def,
mueller@3071
   241
                                 Filter_ex_def,ProjA_def,starts_of_par]) 1);
mueller@3071
   242
by (pair_tac "ex" 1);
mueller@3071
   243
by (rtac iffI 1);
mueller@3071
   244
(* ==>  *)
mueller@3071
   245
by (REPEAT (etac conjE 1));
wenzelm@4098
   246
by (asm_full_simp_tac (simpset() addsimps [lemma_1_1a RS spec RS mp,
mueller@3071
   247
               lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1);
mueller@3071
   248
(* <==  *)
mueller@3071
   249
by (REPEAT (etac conjE 1));
wenzelm@4098
   250
by (asm_full_simp_tac (simpset() addsimps [lemma_1_2 RS spec RS mp]) 1);
mueller@3071
   251
qed"compositionality_ex";
mueller@3071
   252
mueller@3071
   253
mueller@3521
   254
(* ------------------------------------------------------------------ *)
mueller@3521
   255
(*           COMPOSITIONALITY   on    EXECUTION     Level             *)
mueller@3521
   256
(*                            For Modules                             *)
mueller@3521
   257
(* ------------------------------------------------------------------ *)
mueller@3521
   258
wenzelm@5068
   259
Goalw [Execs_def,par_execs_def]
mueller@3521
   260
mueller@3521
   261
"Execs (A||B) = par_execs (Execs A) (Execs B)";
mueller@3521
   262
wenzelm@4098
   263
by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
wenzelm@4423
   264
by (rtac set_ext 1);
wenzelm@4098
   265
by (asm_full_simp_tac (simpset() addsimps [compositionality_ex,actions_of_par]) 1);
mueller@3521
   266
qed"compositionality_ex_modules";
mueller@3071
   267
mueller@3071
   268
mueller@3521
   269
mueller@3521
   270
mueller@3521
   271
mueller@3521
   272
mueller@3521
   273