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