src/HOLCF/IOA/meta_theory/Automata.ML
author oheimb
Thu, 08 Jan 1998 18:09:47 +0100
changeset 4536 74f7c556fd90
parent 4477 b3e5857d8d99
child 4814 0277a026f99d
permissions -rw-r--r--
added split_paired_Ex to the implicit simpset
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     1
(*  Title:      HOLCF/IOA/meta_theory/Automata.ML
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
     2
    ID:         $Id$
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     3
    Author:     Olaf Mueller, Tobias Nipkow, Konrad Slind
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     4
    Copyright   1994, 1996  TU Muenchen
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     5
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     6
The I/O automata of Lynch and Tuttle.
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     7
*)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     8
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     9
(* Has been removed from HOL-simpset, who knows why? *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    10
Addsimps [Let_def];
4536
74f7c556fd90 added split_paired_Ex to the implicit simpset
oheimb
parents: 4477
diff changeset
    11
Delsimps [split_paired_Ex];
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    12
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    13
open reachable;
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    14
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    15
val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def];
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    16
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    17
(* ----------------------------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    18
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    19
section "asig_of, starts_of, trans_of";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    20
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    21
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    22
goal thy
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    23
 "((asig_of (x,y,z,w,s)) = x)   & \
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    24
\ ((starts_of (x,y,z,w,s)) = y) & \
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    25
\ ((trans_of (x,y,z,w,s)) = z)  & \
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    26
\ ((wfair_of (x,y,z,w,s)) = w) & \
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    27
\ ((sfair_of (x,y,z,w,s)) = s)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
    28
  by (simp_tac (simpset() addsimps ioa_projections) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    29
qed "ioa_triple_proj";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    30
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    31
goalw thy [is_trans_of_def,actions_def, is_asig_def]
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    32
  "!!A. [| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    33
  by (REPEAT(etac conjE 1));
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    34
  by (EVERY1[etac allE, etac impE, atac]);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    35
  by (Asm_full_simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    36
qed "trans_in_actions";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    37
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    38
goal thy
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    39
"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
    40
  by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    41
qed "starts_of_par";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    42
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    43
goal thy
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    44
"trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \       
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    45
\            in (a:act A | a:act B) & \
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    46
\               (if a:act A then       \                
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    47
\                  (fst(s),a,fst(t)):trans_of(A) \                    
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    48
\                else fst(t) = fst(s))            \                      
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    49
\               &                                  \                     
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    50
\               (if a:act B then                    \   
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    51
\                  (snd(s),a,snd(t)):trans_of(B)     \                
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    52
\                else snd(t) = snd(s))}";
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    53
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
    54
by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    55
qed "trans_of_par";
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
    56
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    57
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    58
(* ----------------------------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    59
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    60
section "actions and par";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    61
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    62
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    63
goal thy 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    64
"actions(asig_comp a b) = actions(a) Un actions(b)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
    65
  by (simp_tac (simpset() addsimps
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    66
               ([actions_def,asig_comp_def]@asig_projections)) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    67
  by (fast_tac (set_cs addSIs [equalityI]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    68
qed "actions_asig_comp";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    69
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    70
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    71
goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
    72
  by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    73
qed "asig_of_par";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    74
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    75
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    76
goal thy "ext (A1||A2) =    \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    77
\  (ext A1) Un (ext A2)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
    78
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    79
      asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    80
by (rtac set_ext 1); 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    81
by (fast_tac set_cs 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    82
qed"externals_of_par"; 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    83
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    84
goal thy "act (A1||A2) =    \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    85
\  (act A1) Un (act A2)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
    86
by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    87
      asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    88
by (rtac set_ext 1); 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    89
by (fast_tac set_cs 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    90
qed"actions_of_par"; 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    91
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    92
goal thy "inp (A1||A2) =\
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    93
\         ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
    94
by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    95
      asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    96
qed"inputs_of_par";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    97
  
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    98
goal thy "out (A1||A2) =\
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    99
\         (out A1) Un (out A2)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   100
by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   101
      asig_outputs_def,Un_def,set_diff_def]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   102
qed"outputs_of_par";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   103
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   104
goal thy "int (A1||A2) =\
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   105
\         (int A1) Un (int A2)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   106
by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   107
      asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   108
qed"internals_of_par";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   109
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   110
(* ---------------------------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   111
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   112
section "actions and compatibility"; 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   113
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   114
goal thy"compatible A B = compatible B A";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   115
by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   116
by Auto_tac;
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   117
qed"compat_commute";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   118
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   119
goalw thy [externals_def,actions_def,compatible_def]
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   120
 "!! a. [| compatible A1 A2; a:ext A1|] ==> a~:int A2";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   121
by (Asm_full_simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   122
by (best_tac (set_cs addEs [equalityCE]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   123
qed"ext1_is_not_int2";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   124
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   125
(* just commuting the previous one: better commute compatible *)
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   126
goalw thy [externals_def,actions_def,compatible_def]
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   127
 "!! a. [| compatible A2 A1 ; a:ext A1|] ==> a~:int A2";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   128
by (Asm_full_simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   129
by (best_tac (set_cs addEs [equalityCE]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   130
qed"ext2_is_not_int1";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   131
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   132
bind_thm("ext1_ext2_is_not_act2",ext1_is_not_int2 RS int_and_ext_is_act);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   133
bind_thm("ext1_ext2_is_not_act1",ext2_is_not_int1 RS int_and_ext_is_act);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   134
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   135
goalw thy  [externals_def,actions_def,compatible_def]
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   136
 "!! x. [| compatible A B; x:int A |] ==> x~:ext B";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   137
by (Asm_full_simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   138
by (best_tac (set_cs addEs [equalityCE]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   139
qed"intA_is_not_extB";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   140
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   141
goalw thy [externals_def,actions_def,compatible_def,is_asig_def,asig_of_def]
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   142
"!! a. [| compatible A B; a:int A |] ==> a ~: act B";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   143
by (Asm_full_simp_tac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   144
by (best_tac (set_cs addEs [equalityCE]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   145
qed"intA_is_not_actB";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   146
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   147
(* the only one that needs disjointness of outputs and of internals and _all_ acts *)
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   148
goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   149
    compatible_def,is_asig_def,asig_of_def]
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   150
"!! a. [| compatible A B; a:out A ;a:act B|] ==> a : inp B";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   151
by (Asm_full_simp_tac 1);
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   152
by (best_tac (set_cs addEs [equalityCE]) 1);
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   153
qed"outAactB_is_inpB";
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   154
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   155
(* needed for propagation of input_enabledness from A,B to A||B *)
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   156
goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   157
    compatible_def,is_asig_def,asig_of_def]
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   158
"!! a. [| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B";
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   159
by (Asm_full_simp_tac 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   160
by (best_tac (set_cs addEs [equalityCE]) 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   161
qed"inpAAactB_is_inpBoroutB";
3433
2de17c994071 added deadlock freedom, polished definitions and proofs
mueller
parents: 3275
diff changeset
   162
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   163
(* ---------------------------------------------------------------------------------- *)
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   164
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   165
section "input_enabledness and par";  
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   166
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   167
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   168
(* ugly case distinctions. Heart of proof: 
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   169
     1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   170
     2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   171
goalw thy [input_enabled_def] 
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   172
"!!A. [| compatible A B; input_enabled A; input_enabled B|] \
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   173
\     ==> input_enabled (A||B)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   174
by (asm_full_simp_tac (simpset() addsimps [inputs_of_par,trans_of_par]) 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   175
by (safe_tac set_cs);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   176
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   177
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 2);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   178
(* a: inp A *)
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   179
by (case_tac "a:act B" 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   180
(* a:act B *)
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   181
by (eres_inst_tac [("x","a")] allE 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   182
by (Asm_full_simp_tac 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   183
by (dtac inpAAactB_is_inpBoroutB 1);
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   184
by (assume_tac 1);
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   185
by (assume_tac 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   186
by (eres_inst_tac [("x","a")] allE 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   187
by (Asm_full_simp_tac 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   188
by (eres_inst_tac [("x","aa")] allE 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   189
by (eres_inst_tac [("x","b")] allE 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   190
by (etac exE 1);
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   191
by (etac exE 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   192
by (res_inst_tac [("x","(s2,s2a)")] exI 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   193
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   194
(* a~: act B*)
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   195
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   196
by (eres_inst_tac [("x","a")] allE 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   197
by (Asm_full_simp_tac 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   198
by (eres_inst_tac [("x","aa")] allE 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   199
by (etac exE 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   200
by (res_inst_tac [("x","(s2,b)")] exI 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   201
by (Asm_full_simp_tac 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   202
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   203
(* a:inp B *)
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   204
by (case_tac "a:act A" 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   205
(* a:act A *)
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   206
by (eres_inst_tac [("x","a")] allE 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   207
by (eres_inst_tac [("x","a")] allE 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   208
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
4473
803d1e302af1 Decremented subscript because of change to iffD1
paulson
parents: 4423
diff changeset
   209
by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   210
by (dtac inpAAactB_is_inpBoroutB 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   211
back();
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   212
by (assume_tac 1);
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   213
by (assume_tac 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   214
by (Asm_full_simp_tac 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   215
by (rotate_tac ~1 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   216
by (Asm_full_simp_tac 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   217
by (eres_inst_tac [("x","aa")] allE 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   218
by (eres_inst_tac [("x","b")] allE 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   219
by (etac exE 1);
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   220
by (etac exE 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   221
by (res_inst_tac [("x","(s2,s2a)")] exI 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   222
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   223
(* a~: act B*)
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   224
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   225
by (eres_inst_tac [("x","a")] allE 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   226
by (Asm_full_simp_tac 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   227
by (eres_inst_tac [("x","a")] allE 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   228
by (Asm_full_simp_tac 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   229
by (eres_inst_tac [("x","b")] allE 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   230
by (etac exE 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   231
by (res_inst_tac [("x","(aa,s2)")] exI 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   232
by (Asm_full_simp_tac 1);
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   233
qed"input_enabled_par";
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   234
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   235
(* ---------------------------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   236
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   237
section "invariants";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   238
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   239
val [p1,p2] = goalw thy [invariant_def]
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   240
  "[| !!s. s:starts_of(A) ==> P(s);     \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   241
\     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   242
\  ==> invariant A P";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   243
by (rtac allI 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   244
by (rtac impI 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   245
by (res_inst_tac [("za","s")] reachable.induct 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   246
by (atac 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   247
by (etac p1 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   248
by (eres_inst_tac [("s1","sa")] (p2 RS mp) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   249
by (REPEAT (atac 1));
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   250
qed"invariantI";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   251
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   252
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   253
val [p1,p2] = goal thy
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   254
 "[| !!s. s : starts_of(A) ==> P(s); \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   255
\   !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   256
\ |] ==> invariant A P";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   257
  by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   258
qed "invariantI1";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   259
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   260
val [p1,p2] = goalw thy [invariant_def]
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   261
"[| invariant A P; reachable A s |] ==> P(s)";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   262
   br(p2 RS (p1 RS spec RS mp))1;
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   263
qed "invariantE";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   264
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   265
(* ---------------------------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   266
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   267
section "restrict";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   268
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   269
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   270
goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   271
\         trans_of(restrict ioa acts) = trans_of(ioa)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   272
by (simp_tac (simpset() addsimps ([restrict_def]@ioa_projections)) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   273
qed "cancel_restrict_a";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   274
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   275
goal thy "reachable (restrict ioa acts) s = reachable ioa s";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   276
by (rtac iffI 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   277
by (etac reachable.induct 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   278
by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a,reachable_0]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   279
by (etac reachable_n 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   280
by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   281
(* <--  *)
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   282
by (etac reachable.induct 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   283
by (rtac reachable_0 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   284
by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   285
by (etac reachable_n 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   286
by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   287
qed "cancel_restrict_b";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   288
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   289
goal thy "act (restrict A acts) = act A";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   290
by (simp_tac (simpset() addsimps [actions_def,asig_internals_def,
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   291
        asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def,
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   292
        restrict_asig_def]) 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   293
by Auto_tac;
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   294
qed"acts_restrict";
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   295
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   296
goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   297
\         trans_of(restrict ioa acts) = trans_of(ioa) & \
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   298
\         reachable (restrict ioa acts) s = reachable ioa s & \
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   299
\         act (restrict A acts) = act A";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   300
  by (simp_tac (simpset() addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   301
qed"cancel_restrict";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   302
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   303
(* ---------------------------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   304
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   305
section "rename";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   306
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   307
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   308
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   309
goal thy "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   310
by (asm_full_simp_tac (simpset() addsimps [Let_def,rename_def,trans_of_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   311
qed"trans_rename";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   312
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   313
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   314
goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   315
by (etac reachable.induct 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   316
by (rtac reachable_0 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   317
by (asm_full_simp_tac (simpset() addsimps [rename_def]@ioa_projections) 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   318
by (dtac trans_rename 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   319
by (etac exE 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   320
by (etac conjE 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   321
by (etac reachable_n 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3433
diff changeset
   322
by (assume_tac 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   323
qed"reachable_rename";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   324
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   325
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   326
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   327
(* ---------------------------------------------------------------------------------- *)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   328
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   329
section "trans_of(A||B)";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   330
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   331
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   332
goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   333
\             ==> (fst s,a,fst t):trans_of A";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   334
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   335
qed"trans_A_proj";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   336
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   337
goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   338
\             ==> (snd s,a,snd t):trans_of B";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   339
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   340
qed"trans_B_proj";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   341
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   342
goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   343
\             ==> fst s = fst t";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   344
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   345
qed"trans_A_proj2";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   346
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   347
goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   348
\             ==> snd s = snd t";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   349
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   350
qed"trans_B_proj2";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   351
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   352
goal thy "!!A.(s,a,t):trans_of (A||B) \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   353
\              ==> a :act A | a :act B";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   354
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   355
qed"trans_AB_proj";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   356
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   357
goal thy "!!A. [|a:act A;a:act B;\
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   358
\      (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]\
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   359
\  ==> (s,a,t):trans_of (A||B)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   360
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   361
qed"trans_AB";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   362
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   363
goal thy "!!A. [|a:act A;a~:act B;\
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   364
\      (fst s,a,fst t):trans_of A;snd s=snd t|]\
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   365
\  ==> (s,a,t):trans_of (A||B)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   366
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   367
qed"trans_A_notB";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   368
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   369
goal thy "!!A. [|a~:act A;a:act B;\
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   370
\      (snd s,a,snd t):trans_of B;fst s=fst t|]\
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   371
\  ==> (s,a,t):trans_of (A||B)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   372
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   373
qed"trans_notA_B";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   374
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   375
val trans_of_defs1 = [trans_AB,trans_A_notB,trans_notA_B];
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   376
val trans_of_defs2 = [trans_A_proj,trans_B_proj,trans_A_proj2,
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   377
                      trans_B_proj2,trans_AB_proj];
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   378
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   379
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   380
goal thy 
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   381
"(s,a,t) : trans_of(A || B || C || D) =                                      \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   382
\ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |  \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   383
\   a:actions(asig_of(D))) &                                                 \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   384
\  (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)              \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   385
\   else fst t=fst s) &                                                      \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   386
\  (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)    \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   387
\   else fst(snd(t))=fst(snd(s))) &                                          \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   388
\  (if a:actions(asig_of(C)) then                                            \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   389
\     (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)                      \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   390
\   else fst(snd(snd(t)))=fst(snd(snd(s)))) &                                \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   391
\  (if a:actions(asig_of(D)) then                                            \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   392
\     (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                      \
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   393
\   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   394
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   395
  by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   396
                            ioa_projections)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   397
                  setloop (split_tac [expand_if])) 1);
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   398
qed "trans_of_par4";
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   399
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   400
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   401
(* ---------------------------------------------------------------------------------- *)
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
   402
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   403
section "proof obligation generator for IOA requirements";  
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   404
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   405
(* without assumptions on A and B because is_trans_of is also incorporated in ||def *)
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   406
goalw thy [is_trans_of_def] 
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   407
"is_trans_of (A||B)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   408
by (simp_tac (simpset() addsimps [actions_of_par,trans_of_par]) 1);
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   409
qed"is_trans_of_par";
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   410
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   411
goalw thy [is_trans_of_def] 
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   412
"!!A. is_trans_of A ==> is_trans_of (restrict A acts)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   413
by (asm_simp_tac (simpset() addsimps [cancel_restrict,acts_restrict])1);
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   414
qed"is_trans_of_restrict";
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   415
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   416
goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   417
"!!A. is_trans_of A ==> is_trans_of (rename A f)";
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   418
by (asm_full_simp_tac
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   419
    (simpset() addsimps [actions_def,trans_of_def, asig_internals_def,
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   420
			 asig_outputs_def,asig_inputs_def,externals_def,
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   421
			 asig_of_def,rename_def,rename_set_def]) 1);
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   422
by (Blast_tac 1);
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   423
qed"is_trans_of_rename";
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   424
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   425
goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|]  \
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   426
\         ==> is_asig_of (A||B)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   427
by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,asig_of_par,
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   428
       asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   429
     asig_inputs_def,actions_def,is_asig_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   430
by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   431
by Auto_tac;
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   432
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   433
qed"is_asig_of_par";
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   434
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   435
goalw thy [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def,
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   436
           asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] 
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   437
"!! A. is_asig_of A ==> is_asig_of (restrict A f)";
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   438
by (Asm_full_simp_tac 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   439
by Auto_tac;
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   440
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   441
qed"is_asig_of_restrict";
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   442
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   443
goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   444
by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   445
     rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   446
     asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   447
by Auto_tac; 
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   448
by (dres_inst_tac [("s","Some xb")] sym 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   449
by (rotate_tac ~1 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   450
by (Asm_full_simp_tac 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   451
by (best_tac (set_cs addEs [equalityCE]) 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   452
by (dres_inst_tac [("s","Some xb")] sym 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   453
by (rotate_tac ~1 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   454
by (Asm_full_simp_tac 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   455
by (best_tac (set_cs addEs [equalityCE]) 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   456
by (dres_inst_tac [("s","Some xb")] sym 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   457
by (rotate_tac ~1 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   458
by (Asm_full_simp_tac 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   459
by (best_tac (set_cs addEs [equalityCE]) 1);
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   460
qed"is_asig_of_rename";
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   461
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   462
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   463
Addsimps [is_asig_of_par,is_asig_of_restrict,is_asig_of_rename,
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   464
          is_trans_of_par,is_trans_of_restrict,is_trans_of_rename];
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   465
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   466
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   467
goalw thy [compatible_def]
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   468
"!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   469
by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   470
   outputs_of_par,actions_of_par]) 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   471
by Auto_tac;
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   472
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   473
qed"compatible_par";
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   474
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   475
(* FIX: better derive by previous one and compat_commute *)
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   476
goalw thy [compatible_def]
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   477
"!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   478
by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   479
   outputs_of_par,actions_of_par]) 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4473
diff changeset
   480
by Auto_tac;
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   481
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   482
qed"compatible_par2";
3521
bdc51b4c6050 changes needed for adding fairness
mueller
parents: 3457
diff changeset
   483
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   484
goalw thy [compatible_def]
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   485
"!! A. [| compatible A B; (ext B - S) Int ext A = {}|] \
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   486
\     ==> compatible A (restrict B S)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   487
by (asm_full_simp_tac (simpset() addsimps [ioa_triple_proj,asig_triple_proj,
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   488
          externals_def,restrict_def,restrict_asig_def,actions_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3662
diff changeset
   489
by (auto_tac (claset() addEs [equalityCE],simpset()));
3656
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   490
qed"compatible_restrict";
2df8a2bc3ee2 some minor changes;
mueller
parents: 3521
diff changeset
   491