src/HOL/IOA/Solve.ML
author nipkow
Mon Apr 27 16:45:27 1998 +0200 (1998-04-27)
changeset 4831 dae4d63a1318
parent 4828 ee3317896a47
child 4838 196100237656
permissions -rw-r--r--
Renamed expand_const -> split_const.
oheimb@4530
     1
(*  Title:      HOL/IOA/Solve.ML
mueller@3078
     2
    ID:         $Id$
mueller@3078
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@3078
     4
    Copyright   1994  TU Muenchen
mueller@3078
     5
mueller@3078
     6
Weak possibilities mapping (abstraction)
mueller@3078
     7
*)
mueller@3078
     8
mueller@3078
     9
open Solve; 
mueller@3078
    10
mueller@3078
    11
Addsimps [mk_trace_thm,trans_in_actions];
mueller@3078
    12
mueller@3078
    13
goalw Solve.thy [is_weak_pmap_def,traces_def]
mueller@3078
    14
  "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \
mueller@3078
    15
\          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
mueller@3078
    16
wenzelm@4089
    17
  by (simp_tac(simpset() addsimps [has_trace_def])1);
oheimb@4828
    18
  by (Safe_tac);
oheimb@4828
    19
  by (rename_tac "ex1 ex2" 1);
mueller@3078
    20
mueller@3078
    21
  (* choose same trace, therefore same NF *)
oheimb@4772
    22
  by (res_inst_tac[("x","mk_trace  C ex1")] exI 1);
mueller@3078
    23
  by (Asm_full_simp_tac 1);
mueller@3078
    24
mueller@3078
    25
  (* give execution of abstract automata *)
oheimb@4772
    26
  by (res_inst_tac[("x","(mk_trace A ex1,%i. f (ex2 i))")] bexI 1);
mueller@3078
    27
mueller@3078
    28
  (* Traces coincide *)
oheimb@4772
    29
   by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1);
mueller@3078
    30
mueller@3078
    31
  (* Use lemma *)
mueller@3078
    32
  by (forward_tac [states_of_exec_reachable] 1);
mueller@3078
    33
mueller@3078
    34
  (* Now show that it's an execution *)
wenzelm@4089
    35
  by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1);
paulson@4153
    36
  by Safe_tac;
mueller@3078
    37
mueller@3078
    38
  (* Start states map to start states *)
mueller@3078
    39
  by (dtac bspec 1);
mueller@3078
    40
  by (atac 1);
mueller@3078
    41
mueller@3078
    42
  (* Show that it's an execution fragment *)
wenzelm@4089
    43
  by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1);
paulson@4153
    44
  by Safe_tac;
mueller@3078
    45
oheimb@4772
    46
  by (eres_inst_tac [("x","ex2 n")] allE 1);
oheimb@4772
    47
  by (eres_inst_tac [("x","ex2 (Suc n)")] allE 1);
mueller@3078
    48
  by (eres_inst_tac [("x","a")] allE 1);
mueller@3078
    49
  by (Asm_full_simp_tac 1);
mueller@3078
    50
qed "trace_inclusion";
mueller@3078
    51
mueller@3078
    52
(* Lemmata *)
mueller@3078
    53
mueller@3078
    54
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
paulson@4153
    55
  by (fast_tac (claset() addDs prems) 1);
mueller@3078
    56
val imp_conj_lemma = result();
mueller@3078
    57
mueller@3078
    58
mueller@3078
    59
(* fist_order_tautology of externals_of_par *)
mueller@3078
    60
goal IOA.thy "a:externals(asig_of(A1||A2)) =    \
mueller@3078
    61
\  (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) |  \
mueller@3078
    62
\  a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |  \
mueller@3078
    63
\  a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))";
wenzelm@4089
    64
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1);
mueller@3078
    65
 by (Fast_tac 1);
mueller@3078
    66
val externals_of_par_extra = result(); 
mueller@3078
    67
mueller@3078
    68
goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
wenzelm@4089
    69
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
mueller@3078
    70
by (etac bexE 1);
mueller@3078
    71
by (res_inst_tac [("x",
wenzelm@3842
    72
   "(filter_oseq (%a. a:actions(asig_of(C1))) \
mueller@3078
    73
\                (fst ex),                                                \
wenzelm@3842
    74
\    %i. fst (snd ex i))")]  bexI 1);
mueller@3078
    75
(* fst(s) is in projected execution *)
mueller@3078
    76
 by (Simp_tac 1);
oheimb@4799
    77
 by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
mueller@3078
    78
(* projected execution is indeed an execution *)
mueller@3078
    79
by (asm_full_simp_tac
wenzelm@4089
    80
      (simpset() addsimps [executions_def,is_execution_fragment_def,
mueller@3078
    81
                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
oheimb@4799
    82
                addsplits [split_option_case]) 1);
mueller@3078
    83
qed"comp1_reachable";
mueller@3078
    84
mueller@3078
    85
mueller@3078
    86
(* Exact copy of proof of comp1_reachable for the second 
mueller@3078
    87
   component of a parallel composition.     *)
mueller@3078
    88
goal Solve.thy "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
wenzelm@4089
    89
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
mueller@3078
    90
by (etac bexE 1);
mueller@3078
    91
by (res_inst_tac [("x",
wenzelm@3842
    92
   "(filter_oseq (%a. a:actions(asig_of(C2)))\
mueller@3078
    93
\                (fst ex),                                                \
wenzelm@3842
    94
\    %i. snd (snd ex i))")]  bexI 1);
mueller@3078
    95
(* fst(s) is in projected execution *)
mueller@3078
    96
 by (Simp_tac 1);
oheimb@4799
    97
 by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
mueller@3078
    98
(* projected execution is indeed an execution *)
mueller@3078
    99
by (asm_full_simp_tac
wenzelm@4089
   100
      (simpset() addsimps [executions_def,is_execution_fragment_def,
mueller@3078
   101
                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
oheimb@4799
   102
                addsplits [split_option_case]) 1);
mueller@3078
   103
qed"comp2_reachable";
mueller@3078
   104
nipkow@4831
   105
Delsplits [split_if];
mueller@3078
   106
mueller@3078
   107
(* Composition of possibility-mappings *)
mueller@3078
   108
goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
mueller@3078
   109
\               externals(asig_of(A1))=externals(asig_of(C1)) &\
mueller@3078
   110
\               is_weak_pmap g C2 A2 &  \
mueller@3078
   111
\               externals(asig_of(A2))=externals(asig_of(C2)) & \
mueller@3078
   112
\               compat_ioas C1 C2 & compat_ioas A1 A2  |]     \
mueller@3078
   113
\  ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
mueller@3078
   114
 by (rtac conjI 1);
mueller@3078
   115
(* start_states *)
wenzelm@4089
   116
 by (asm_full_simp_tac (simpset() addsimps [par_def, starts_of_def]) 1);
mueller@3078
   117
(* transitions *)
mueller@3078
   118
by (REPEAT (rtac allI 1));
mueller@3078
   119
by (rtac imp_conj_lemma 1);
mueller@3078
   120
by (REPEAT(etac conjE 1));
wenzelm@4089
   121
by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
wenzelm@4089
   122
by (simp_tac (simpset() addsimps [par_def]) 1);
wenzelm@4089
   123
by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
nipkow@4831
   124
by (stac split_if 1);
mueller@3078
   125
by (rtac conjI 1);
mueller@3078
   126
by (rtac impI 1); 
mueller@3078
   127
by (etac disjE 1);
mueller@3078
   128
(* case 1      a:e(A1) | a:e(A2) *)
wenzelm@4089
   129
by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
mueller@3078
   130
                                    ext_is_act]) 1);
mueller@3078
   131
by (etac disjE 1);
mueller@3078
   132
(* case 2      a:e(A1) | a~:e(A2) *)
wenzelm@4089
   133
by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
mueller@3078
   134
             ext_is_act,ext1_ext2_is_not_act2]) 1);
mueller@3078
   135
(* case 3      a:~e(A1) | a:e(A2) *)
wenzelm@4089
   136
by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
mueller@3078
   137
             ext_is_act,ext1_ext2_is_not_act1]) 1);
mueller@3078
   138
(* case 4      a:~e(A1) | a~:e(A2) *)
mueller@3078
   139
by (rtac impI 1);
mueller@3078
   140
by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1);
mueller@3078
   141
(* delete auxiliary subgoal *)
mueller@3078
   142
by (Asm_full_simp_tac 2);
mueller@3078
   143
by (Fast_tac 2);
wenzelm@4089
   144
by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
nipkow@4831
   145
                 addsplits [split_if]) 1);
paulson@4153
   146
by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
wenzelm@4089
   147
        asm_full_simp_tac(simpset() addsimps[comp1_reachable,
mueller@3078
   148
                                      comp2_reachable])1));
mueller@3078
   149
qed"fxg_is_weak_pmap_of_product_IOA";
mueller@3078
   150
mueller@3078
   151
mueller@3078
   152
goal Solve.thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
wenzelm@4089
   153
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
mueller@3078
   154
by (etac bexE 1);
mueller@3078
   155
by (res_inst_tac [("x",
mueller@3078
   156
   "((%i. case (fst ex i) \
mueller@3078
   157
\         of None => None\
mueller@3078
   158
\          | Some(x) => g x) ,snd ex)")]  bexI 1);
mueller@3078
   159
by (Simp_tac 1);
mueller@3078
   160
(* execution is indeed an execution of C *)
mueller@3078
   161
by (asm_full_simp_tac
wenzelm@4089
   162
      (simpset() addsimps [executions_def,is_execution_fragment_def,
mueller@3078
   163
                          par_def,starts_of_def,trans_of_def,rename_def]
nipkow@4071
   164
                addsplits [split_option_case]) 1);
wenzelm@4089
   165
by (best_tac (claset() addSDs [spec] addDs [sym] addss (simpset())) 1);
mueller@3078
   166
qed"reachable_rename_ioa";
mueller@3078
   167
mueller@3078
   168
mueller@3078
   169
goal Solve.thy "!!f.[| is_weak_pmap f C A |]\
mueller@3078
   170
\                      ==> (is_weak_pmap f (rename C g) (rename A g))";
wenzelm@4089
   171
by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1);
mueller@3078
   172
by (rtac conjI 1);
wenzelm@4089
   173
by (asm_full_simp_tac (simpset() addsimps [rename_def,starts_of_def]) 1);
mueller@3078
   174
by (REPEAT (rtac allI 1));
mueller@3078
   175
by (rtac imp_conj_lemma 1);
wenzelm@4089
   176
by (simp_tac (simpset() addsimps [rename_def]) 1);
wenzelm@4089
   177
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
paulson@4153
   178
by Safe_tac;
nipkow@4831
   179
by (stac split_if 1);
mueller@3078
   180
 by (rtac conjI 1);
mueller@3078
   181
 by (rtac impI 1);
mueller@3078
   182
 by (etac disjE 1);
mueller@3078
   183
 by (etac exE 1);
mueller@3078
   184
by (etac conjE 1);
mueller@3078
   185
(* x is input *)
mueller@3078
   186
 by (dtac sym 1);
mueller@3078
   187
 by (dtac sym 1);
mueller@3078
   188
by (Asm_full_simp_tac 1);
mueller@3078
   189
by (REPEAT (hyp_subst_tac 1));
mueller@3078
   190
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
mueller@3078
   191
by (assume_tac 1);
mueller@3078
   192
by (Asm_full_simp_tac 1);
mueller@3078
   193
(* x is output *)
mueller@3078
   194
 by (etac exE 1);
mueller@3078
   195
by (etac conjE 1);
mueller@3078
   196
 by (dtac sym 1);
mueller@3078
   197
 by (dtac sym 1);
mueller@3078
   198
by (Asm_full_simp_tac 1);
mueller@3078
   199
by (REPEAT (hyp_subst_tac 1));
mueller@3078
   200
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
mueller@3078
   201
by (assume_tac 1);
mueller@3078
   202
by (Asm_full_simp_tac 1);
mueller@3078
   203
(* x is internal *)
wenzelm@4089
   204
by (simp_tac (simpset() addsimps [de_Morgan_disj, de_Morgan_conj, not_ex] 
mueller@3078
   205
	               addcongs [conj_cong]) 1);
mueller@3078
   206
by (rtac impI 1);
mueller@3078
   207
by (etac conjE 1);
mueller@3078
   208
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
paulson@4477
   209
by Auto_tac;
mueller@3078
   210
qed"rename_through_pmap";
nipkow@4681
   211
nipkow@4831
   212
Addsplits [split_if];