src/HOL/IOA/Solve.ML
author paulson
Thu Jul 08 13:42:31 1999 +0200 (1999-07-08)
changeset 6916 4957978b6f9e
parent 5184 9b8547a9496a
child 7499 23e090051cb8
permissions -rw-r--r--
tidied proofs to cope with default if_weak_cong
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
wenzelm@5069
    13
Goalw [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);
wenzelm@5132
    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
paulson@5143
    68
Goal "[| 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 *)
paulson@6916
    76
 by (Force_tac 1);
mueller@3078
    77
(* projected execution is indeed an execution *)
mueller@3078
    78
by (asm_full_simp_tac
paulson@6916
    79
      (simpset() delcongs [if_weak_cong]
paulson@6916
    80
		 addsimps [executions_def,is_execution_fragment_def,
paulson@6916
    81
			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
paulson@6916
    82
                 addsplits [option.split]) 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.     *)
paulson@5143
    88
Goal "[| 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 *)
paulson@6916
    96
 by (Force_tac 1);
mueller@3078
    97
(* projected execution is indeed an execution *)
mueller@3078
    98
by (asm_full_simp_tac
paulson@6916
    99
      (simpset() delcongs [if_weak_cong]
paulson@6916
   100
		 addsimps [executions_def,is_execution_fragment_def,
paulson@6916
   101
			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
paulson@6916
   102
                 addsplits [option.split]) 1);
mueller@3078
   103
qed"comp2_reachable";
mueller@3078
   104
paulson@6916
   105
Delsplits [split_if]; Delcongs [if_weak_cong];
mueller@3078
   106
paulson@6916
   107
(* THIS THEOREM IS NEVER USED (lcp)
paulson@6916
   108
   Composition of possibility-mappings *)
paulson@6916
   109
Goalw [is_weak_pmap_def]
paulson@6916
   110
     "[| is_weak_pmap f C1 A1; \
paulson@6916
   111
\        externals(asig_of(A1))=externals(asig_of(C1));\
paulson@6916
   112
\        is_weak_pmap g C2 A2;  \
paulson@6916
   113
\        externals(asig_of(A2))=externals(asig_of(C2)); \
paulson@6916
   114
\        compat_ioas C1 C2; compat_ioas A1 A2  |]     \
mueller@3078
   115
\  ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
mueller@3078
   116
 by (rtac conjI 1);
mueller@3078
   117
(* start_states *)
wenzelm@4089
   118
 by (asm_full_simp_tac (simpset() addsimps [par_def, starts_of_def]) 1);
mueller@3078
   119
(* transitions *)
mueller@3078
   120
by (REPEAT (rtac allI 1));
mueller@3078
   121
by (rtac imp_conj_lemma 1);
wenzelm@4089
   122
by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
wenzelm@4089
   123
by (simp_tac (simpset() addsimps [par_def]) 1);
wenzelm@4089
   124
by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
nipkow@4831
   125
by (stac split_if 1);
mueller@3078
   126
by (rtac conjI 1);
mueller@3078
   127
by (rtac impI 1); 
mueller@3078
   128
by (etac disjE 1);
mueller@3078
   129
(* case 1      a:e(A1) | a:e(A2) *)
wenzelm@4089
   130
by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
mueller@3078
   131
                                    ext_is_act]) 1);
mueller@3078
   132
by (etac disjE 1);
mueller@3078
   133
(* case 2      a:e(A1) | a~:e(A2) *)
wenzelm@4089
   134
by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
mueller@3078
   135
             ext_is_act,ext1_ext2_is_not_act2]) 1);
mueller@3078
   136
(* case 3      a:~e(A1) | a:e(A2) *)
wenzelm@4089
   137
by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
mueller@3078
   138
             ext_is_act,ext1_ext2_is_not_act1]) 1);
mueller@3078
   139
(* case 4      a:~e(A1) | a~:e(A2) *)
mueller@3078
   140
by (rtac impI 1);
mueller@3078
   141
by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1);
mueller@3078
   142
(* delete auxiliary subgoal *)
mueller@3078
   143
by (Asm_full_simp_tac 2);
mueller@3078
   144
by (Fast_tac 2);
wenzelm@4089
   145
by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
nipkow@4831
   146
                 addsplits [split_if]) 1);
paulson@4153
   147
by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
paulson@6916
   148
	   asm_full_simp_tac(simpset() addsimps[comp1_reachable,
paulson@6916
   149
						comp2_reachable])1));
mueller@3078
   150
qed"fxg_is_weak_pmap_of_product_IOA";
mueller@3078
   151
mueller@3078
   152
paulson@5143
   153
Goal "[| reachable (rename C g) s |] ==> reachable C s";
wenzelm@4089
   154
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
mueller@3078
   155
by (etac bexE 1);
mueller@3078
   156
by (res_inst_tac [("x",
mueller@3078
   157
   "((%i. case (fst ex i) \
mueller@3078
   158
\         of None => None\
mueller@3078
   159
\          | Some(x) => g x) ,snd ex)")]  bexI 1);
mueller@3078
   160
by (Simp_tac 1);
mueller@3078
   161
(* execution is indeed an execution of C *)
mueller@3078
   162
by (asm_full_simp_tac
wenzelm@4089
   163
      (simpset() addsimps [executions_def,is_execution_fragment_def,
mueller@3078
   164
                          par_def,starts_of_def,trans_of_def,rename_def]
berghofe@5184
   165
                addsplits [option.split]) 1);
wenzelm@4089
   166
by (best_tac (claset() addSDs [spec] addDs [sym] addss (simpset())) 1);
mueller@3078
   167
qed"reachable_rename_ioa";
mueller@3078
   168
mueller@3078
   169
paulson@5143
   170
Goal "[| is_weak_pmap f C A |]\
mueller@3078
   171
\                      ==> (is_weak_pmap f (rename C g) (rename A g))";
wenzelm@4089
   172
by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1);
mueller@3078
   173
by (rtac conjI 1);
wenzelm@4089
   174
by (asm_full_simp_tac (simpset() addsimps [rename_def,starts_of_def]) 1);
mueller@3078
   175
by (REPEAT (rtac allI 1));
mueller@3078
   176
by (rtac imp_conj_lemma 1);
wenzelm@4089
   177
by (simp_tac (simpset() addsimps [rename_def]) 1);
wenzelm@4089
   178
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
paulson@4153
   179
by Safe_tac;
nipkow@4831
   180
by (stac split_if 1);
mueller@3078
   181
 by (rtac conjI 1);
mueller@3078
   182
 by (rtac impI 1);
mueller@3078
   183
 by (etac disjE 1);
mueller@3078
   184
 by (etac exE 1);
mueller@3078
   185
by (etac conjE 1);
mueller@3078
   186
(* x is input *)
mueller@3078
   187
 by (dtac sym 1);
mueller@3078
   188
 by (dtac sym 1);
mueller@3078
   189
by (Asm_full_simp_tac 1);
mueller@3078
   190
by (REPEAT (hyp_subst_tac 1));
mueller@3078
   191
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
mueller@3078
   192
by (assume_tac 1);
mueller@3078
   193
by (Asm_full_simp_tac 1);
mueller@3078
   194
(* x is output *)
mueller@3078
   195
 by (etac exE 1);
mueller@3078
   196
by (etac conjE 1);
mueller@3078
   197
 by (dtac sym 1);
mueller@3078
   198
 by (dtac sym 1);
mueller@3078
   199
by (Asm_full_simp_tac 1);
mueller@3078
   200
by (REPEAT (hyp_subst_tac 1));
mueller@3078
   201
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
mueller@3078
   202
by (assume_tac 1);
mueller@3078
   203
by (Asm_full_simp_tac 1);
mueller@3078
   204
(* x is internal *)
wenzelm@4089
   205
by (simp_tac (simpset() addsimps [de_Morgan_disj, de_Morgan_conj, not_ex] 
mueller@3078
   206
	               addcongs [conj_cong]) 1);
mueller@3078
   207
by (rtac impI 1);
mueller@3078
   208
by (etac conjE 1);
mueller@3078
   209
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
paulson@4477
   210
by Auto_tac;
mueller@3078
   211
qed"rename_through_pmap";
nipkow@4681
   212
nipkow@4831
   213
Addsplits [split_if];
paulson@6916
   214
Addcongs  [if_weak_cong];