src/HOL/IOA/Solve.ML
changeset 3078 984866a8f905
child 3842 b55686a7b22c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IOA/Solve.ML	Wed Apr 30 11:56:17 1997 +0200
     1.3 @@ -0,0 +1,209 @@
     1.4 +(*  Title:      HOL/IOA/meta_theory/Solve.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow & Konrad Slind
     1.7 +    Copyright   1994  TU Muenchen
     1.8 +
     1.9 +Weak possibilities mapping (abstraction)
    1.10 +*)
    1.11 +
    1.12 +open Solve; 
    1.13 +
    1.14 +Addsimps [mk_trace_thm,trans_in_actions];
    1.15 +
    1.16 +goalw Solve.thy [is_weak_pmap_def,traces_def]
    1.17 +  "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \
    1.18 +\          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
    1.19 +
    1.20 +  by (simp_tac(!simpset addsimps [has_trace_def])1);
    1.21 +  by (safe_tac (!claset));
    1.22 +
    1.23 +  (* choose same trace, therefore same NF *)
    1.24 +  by (res_inst_tac[("x","mk_trace  C (fst ex)")] exI 1);
    1.25 +  by (Asm_full_simp_tac 1);
    1.26 +
    1.27 +  (* give execution of abstract automata *)
    1.28 +  by (res_inst_tac[("x","(mk_trace A (fst ex),%i.f(snd ex i))")] bexI 1);
    1.29 +
    1.30 +  (* Traces coincide *)
    1.31 +  by (asm_simp_tac (!simpset addsimps [mk_trace_def,filter_oseq_idemp])1);
    1.32 +
    1.33 +  (* Use lemma *)
    1.34 +  by (forward_tac [states_of_exec_reachable] 1);
    1.35 +
    1.36 +  (* Now show that it's an execution *)
    1.37 +  by (asm_full_simp_tac(!simpset addsimps [executions_def]) 1);
    1.38 +  by (safe_tac (!claset));
    1.39 +
    1.40 +  (* Start states map to start states *)
    1.41 +  by (dtac bspec 1);
    1.42 +  by (atac 1);
    1.43 +
    1.44 +  (* Show that it's an execution fragment *)
    1.45 +  by (asm_full_simp_tac (!simpset addsimps [is_execution_fragment_def])1);
    1.46 +  by (safe_tac (!claset));
    1.47 +
    1.48 +  by (eres_inst_tac [("x","snd ex n")] allE 1);
    1.49 +  by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
    1.50 +  by (eres_inst_tac [("x","a")] allE 1);
    1.51 +  by (Asm_full_simp_tac 1);
    1.52 +qed "trace_inclusion";
    1.53 +
    1.54 +(* Lemmata *)
    1.55 +
    1.56 +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    1.57 +  by(fast_tac (!claset addDs prems) 1);
    1.58 +val imp_conj_lemma = result();
    1.59 +
    1.60 +
    1.61 +(* fist_order_tautology of externals_of_par *)
    1.62 +goal IOA.thy "a:externals(asig_of(A1||A2)) =    \
    1.63 +\  (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) |  \
    1.64 +\  a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |  \
    1.65 +\  a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))";
    1.66 +by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1);
    1.67 + by (Fast_tac 1);
    1.68 +val externals_of_par_extra = result(); 
    1.69 +
    1.70 +goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
    1.71 +by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); 
    1.72 +by (etac bexE 1);
    1.73 +by (res_inst_tac [("x",
    1.74 +   "(filter_oseq (%a.a:actions(asig_of(C1))) \
    1.75 +\                (fst ex),                                                \
    1.76 +\    %i.fst (snd ex i))")]  bexI 1);
    1.77 +(* fst(s) is in projected execution *)
    1.78 + by (Simp_tac 1);
    1.79 + by (Fast_tac 1);
    1.80 +(* projected execution is indeed an execution *)
    1.81 +by (asm_full_simp_tac
    1.82 +      (!simpset addsimps [executions_def,is_execution_fragment_def,
    1.83 +                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.84 +                setloop (split_tac[expand_if,expand_option_case])) 1);
    1.85 +qed"comp1_reachable";
    1.86 +
    1.87 +
    1.88 +(* Exact copy of proof of comp1_reachable for the second 
    1.89 +   component of a parallel composition.     *)
    1.90 +goal Solve.thy "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
    1.91 +by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); 
    1.92 +by (etac bexE 1);
    1.93 +by (res_inst_tac [("x",
    1.94 +   "(filter_oseq (%a.a:actions(asig_of(C2)))\
    1.95 +\                (fst ex),                                                \
    1.96 +\    %i.snd (snd ex i))")]  bexI 1);
    1.97 +(* fst(s) is in projected execution *)
    1.98 + by (Simp_tac 1);
    1.99 + by (Fast_tac 1);
   1.100 +(* projected execution is indeed an execution *)
   1.101 +by (asm_full_simp_tac
   1.102 +      (!simpset addsimps [executions_def,is_execution_fragment_def,
   1.103 +                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
   1.104 +                setloop (split_tac[expand_if,expand_option_case])) 1);
   1.105 +qed"comp2_reachable";
   1.106 +
   1.107 +
   1.108 +(* Composition of possibility-mappings *)
   1.109 +
   1.110 +goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
   1.111 +\               externals(asig_of(A1))=externals(asig_of(C1)) &\
   1.112 +\               is_weak_pmap g C2 A2 &  \
   1.113 +\               externals(asig_of(A2))=externals(asig_of(C2)) & \
   1.114 +\               compat_ioas C1 C2 & compat_ioas A1 A2  |]     \
   1.115 +\  ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
   1.116 + by (rtac conjI 1);
   1.117 +(* start_states *)
   1.118 + by (asm_full_simp_tac (!simpset addsimps [par_def, starts_of_def]) 1);
   1.119 +(* transitions *)
   1.120 +by (REPEAT (rtac allI 1));
   1.121 +by (rtac imp_conj_lemma 1);
   1.122 +by (REPEAT(etac conjE 1));
   1.123 +by (simp_tac (!simpset addsimps [externals_of_par_extra]) 1);
   1.124 +by (simp_tac (!simpset addsimps [par_def]) 1);
   1.125 +by (asm_full_simp_tac (!simpset addsimps [trans_of_def]) 1);
   1.126 +by (rtac (expand_if RS ssubst) 1);
   1.127 +by (rtac conjI 1);
   1.128 +by (rtac impI 1); 
   1.129 +by (etac disjE 1);
   1.130 +(* case 1      a:e(A1) | a:e(A2) *)
   1.131 +by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable,
   1.132 +                                    ext_is_act]) 1);
   1.133 +by (etac disjE 1);
   1.134 +(* case 2      a:e(A1) | a~:e(A2) *)
   1.135 +by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable,
   1.136 +             ext_is_act,ext1_ext2_is_not_act2]) 1);
   1.137 +(* case 3      a:~e(A1) | a:e(A2) *)
   1.138 +by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable,
   1.139 +             ext_is_act,ext1_ext2_is_not_act1]) 1);
   1.140 +(* case 4      a:~e(A1) | a~:e(A2) *)
   1.141 +by (rtac impI 1);
   1.142 +by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1);
   1.143 +(* delete auxiliary subgoal *)
   1.144 +by (Asm_full_simp_tac 2);
   1.145 +by (Fast_tac 2);
   1.146 +by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong]
   1.147 +                 setloop (split_tac [expand_if])) 1);
   1.148 +by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
   1.149 +        asm_full_simp_tac(!simpset addsimps[comp1_reachable,
   1.150 +                                      comp2_reachable])1));
   1.151 +qed"fxg_is_weak_pmap_of_product_IOA";
   1.152 +
   1.153 +
   1.154 +goal Solve.thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
   1.155 +by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); 
   1.156 +by (etac bexE 1);
   1.157 +by (res_inst_tac [("x",
   1.158 +   "((%i. case (fst ex i) \
   1.159 +\         of None => None\
   1.160 +\          | Some(x) => g x) ,snd ex)")]  bexI 1);
   1.161 +by (Simp_tac 1);
   1.162 +(* execution is indeed an execution of C *)
   1.163 +by (asm_full_simp_tac
   1.164 +      (!simpset addsimps [executions_def,is_execution_fragment_def,
   1.165 +                          par_def,starts_of_def,trans_of_def,rename_def]
   1.166 +                setloop (split_tac[expand_option_case])) 1);
   1.167 +by (best_tac (!claset addSDs [spec] addDs [sym] addss (!simpset)) 1);
   1.168 +qed"reachable_rename_ioa";
   1.169 +
   1.170 +
   1.171 +goal Solve.thy "!!f.[| is_weak_pmap f C A |]\
   1.172 +\                      ==> (is_weak_pmap f (rename C g) (rename A g))";
   1.173 +by (asm_full_simp_tac (!simpset addsimps [is_weak_pmap_def]) 1);
   1.174 +by (rtac conjI 1);
   1.175 +by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1);
   1.176 +by (REPEAT (rtac allI 1));
   1.177 +by (rtac imp_conj_lemma 1);
   1.178 +by (simp_tac (!simpset addsimps [rename_def]) 1);
   1.179 +by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
   1.180 +by (safe_tac (!claset));
   1.181 +by (rtac (expand_if RS ssubst) 1);
   1.182 + by (rtac conjI 1);
   1.183 + by (rtac impI 1);
   1.184 + by (etac disjE 1);
   1.185 + by (etac exE 1);
   1.186 +by (etac conjE 1);
   1.187 +(* x is input *)
   1.188 + by (dtac sym 1);
   1.189 + by (dtac sym 1);
   1.190 +by (Asm_full_simp_tac 1);
   1.191 +by (REPEAT (hyp_subst_tac 1));
   1.192 +by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
   1.193 +by (assume_tac 1);
   1.194 +by (Asm_full_simp_tac 1);
   1.195 +(* x is output *)
   1.196 + by (etac exE 1);
   1.197 +by (etac conjE 1);
   1.198 + by (dtac sym 1);
   1.199 + by (dtac sym 1);
   1.200 +by (Asm_full_simp_tac 1);
   1.201 +by (REPEAT (hyp_subst_tac 1));
   1.202 +by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
   1.203 +by (assume_tac 1);
   1.204 +by (Asm_full_simp_tac 1);
   1.205 +(* x is internal *)
   1.206 +by (simp_tac (!simpset addsimps [de_Morgan_disj, de_Morgan_conj, not_ex] 
   1.207 +	               addcongs [conj_cong]) 1);
   1.208 +by (rtac impI 1);
   1.209 +by (etac conjE 1);
   1.210 +by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
   1.211 +by (Auto_tac());
   1.212 +qed"rename_through_pmap";