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