mueller@3078: (*  Title:      HOL/IOA/meta_theory/Solve.ML
mueller@3078:     ID:         $Id$
mueller@3078:     Author:     Tobias Nipkow & Konrad Slind
mueller@3078:     Copyright   1994  TU Muenchen
mueller@3078: 
mueller@3078: Weak possibilities mapping (abstraction)
mueller@3078: *)
mueller@3078: 
mueller@3078: open Solve; 
mueller@3078: 
mueller@3078: Addsimps [mk_trace_thm,trans_in_actions];
mueller@3078: 
mueller@3078: goalw Solve.thy [is_weak_pmap_def,traces_def]
mueller@3078:   "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \
mueller@3078: \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
mueller@3078: 
wenzelm@4089:   by (simp_tac(simpset() addsimps [has_trace_def])1);
paulson@4153:   by Safe_tac;
mueller@3078: 
mueller@3078:   (* choose same trace, therefore same NF *)
mueller@3078:   by (res_inst_tac[("x","mk_trace  C (fst ex)")] exI 1);
mueller@3078:   by (Asm_full_simp_tac 1);
mueller@3078: 
mueller@3078:   (* give execution of abstract automata *)
wenzelm@3842:   by (res_inst_tac[("x","(mk_trace A (fst ex),%i. f(snd ex i))")] bexI 1);
mueller@3078: 
mueller@3078:   (* Traces coincide *)
wenzelm@4089:   by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1);
mueller@3078: 
mueller@3078:   (* Use lemma *)
mueller@3078:   by (forward_tac [states_of_exec_reachable] 1);
mueller@3078: 
mueller@3078:   (* Now show that it's an execution *)
wenzelm@4089:   by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1);
paulson@4153:   by Safe_tac;
mueller@3078: 
mueller@3078:   (* Start states map to start states *)
mueller@3078:   by (dtac bspec 1);
mueller@3078:   by (atac 1);
mueller@3078: 
mueller@3078:   (* Show that it's an execution fragment *)
wenzelm@4089:   by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1);
paulson@4153:   by Safe_tac;
mueller@3078: 
mueller@3078:   by (eres_inst_tac [("x","snd ex n")] allE 1);
mueller@3078:   by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
mueller@3078:   by (eres_inst_tac [("x","a")] allE 1);
mueller@3078:   by (Asm_full_simp_tac 1);
mueller@3078: qed "trace_inclusion";
mueller@3078: 
mueller@3078: (* Lemmata *)
mueller@3078: 
mueller@3078: val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
paulson@4153:   by (fast_tac (claset() addDs prems) 1);
mueller@3078: val imp_conj_lemma = result();
mueller@3078: 
mueller@3078: 
mueller@3078: (* fist_order_tautology of externals_of_par *)
mueller@3078: goal IOA.thy "a:externals(asig_of(A1||A2)) =    \
mueller@3078: \  (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) |  \
mueller@3078: \  a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |  \
mueller@3078: \  a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))";
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1);
mueller@3078:  by (Fast_tac 1);
mueller@3078: val externals_of_par_extra = result(); 
mueller@3078: 
mueller@3078: goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
mueller@3078: by (etac bexE 1);
mueller@3078: by (res_inst_tac [("x",
wenzelm@3842:    "(filter_oseq (%a. a:actions(asig_of(C1))) \
mueller@3078: \                (fst ex),                                                \
wenzelm@3842: \    %i. fst (snd ex i))")]  bexI 1);
mueller@3078: (* fst(s) is in projected execution *)
mueller@3078:  by (Simp_tac 1);
mueller@3078:  by (Fast_tac 1);
mueller@3078: (* projected execution is indeed an execution *)
mueller@3078: by (asm_full_simp_tac
wenzelm@4089:       (simpset() addsimps [executions_def,is_execution_fragment_def,
mueller@3078:                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
nipkow@4071:                 addsplits [expand_if,split_option_case]) 1);
mueller@3078: qed"comp1_reachable";
mueller@3078: 
mueller@3078: 
mueller@3078: (* Exact copy of proof of comp1_reachable for the second 
mueller@3078:    component of a parallel composition.     *)
mueller@3078: goal Solve.thy "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
mueller@3078: by (etac bexE 1);
mueller@3078: by (res_inst_tac [("x",
wenzelm@3842:    "(filter_oseq (%a. a:actions(asig_of(C2)))\
mueller@3078: \                (fst ex),                                                \
wenzelm@3842: \    %i. snd (snd ex i))")]  bexI 1);
mueller@3078: (* fst(s) is in projected execution *)
mueller@3078:  by (Simp_tac 1);
mueller@3078:  by (Fast_tac 1);
mueller@3078: (* projected execution is indeed an execution *)
mueller@3078: by (asm_full_simp_tac
wenzelm@4089:       (simpset() addsimps [executions_def,is_execution_fragment_def,
mueller@3078:                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
nipkow@4071:                 addsplits [expand_if,split_option_case]) 1);
mueller@3078: qed"comp2_reachable";
mueller@3078: 
mueller@3078: 
mueller@3078: (* Composition of possibility-mappings *)
mueller@3078: 
mueller@3078: goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
mueller@3078: \               externals(asig_of(A1))=externals(asig_of(C1)) &\
mueller@3078: \               is_weak_pmap g C2 A2 &  \
mueller@3078: \               externals(asig_of(A2))=externals(asig_of(C2)) & \
mueller@3078: \               compat_ioas C1 C2 & compat_ioas A1 A2  |]     \
mueller@3078: \  ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
mueller@3078:  by (rtac conjI 1);
mueller@3078: (* start_states *)
wenzelm@4089:  by (asm_full_simp_tac (simpset() addsimps [par_def, starts_of_def]) 1);
mueller@3078: (* transitions *)
mueller@3078: by (REPEAT (rtac allI 1));
mueller@3078: by (rtac imp_conj_lemma 1);
mueller@3078: by (REPEAT(etac conjE 1));
wenzelm@4089: by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
wenzelm@4089: by (simp_tac (simpset() addsimps [par_def]) 1);
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
paulson@4153: by (stac expand_if 1);
mueller@3078: by (rtac conjI 1);
mueller@3078: by (rtac impI 1); 
mueller@3078: by (etac disjE 1);
mueller@3078: (* case 1      a:e(A1) | a:e(A2) *)
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
mueller@3078:                                     ext_is_act]) 1);
mueller@3078: by (etac disjE 1);
mueller@3078: (* case 2      a:e(A1) | a~:e(A2) *)
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
mueller@3078:              ext_is_act,ext1_ext2_is_not_act2]) 1);
mueller@3078: (* case 3      a:~e(A1) | a:e(A2) *)
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
mueller@3078:              ext_is_act,ext1_ext2_is_not_act1]) 1);
mueller@3078: (* case 4      a:~e(A1) | a~:e(A2) *)
mueller@3078: by (rtac impI 1);
mueller@3078: by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1);
mueller@3078: (* delete auxiliary subgoal *)
mueller@3078: by (Asm_full_simp_tac 2);
mueller@3078: by (Fast_tac 2);
wenzelm@4089: by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
nipkow@3919:                  addsplits [expand_if]) 1);
paulson@4153: by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
wenzelm@4089:         asm_full_simp_tac(simpset() addsimps[comp1_reachable,
mueller@3078:                                       comp2_reachable])1));
mueller@3078: qed"fxg_is_weak_pmap_of_product_IOA";
mueller@3078: 
mueller@3078: 
mueller@3078: goal Solve.thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
mueller@3078: by (etac bexE 1);
mueller@3078: by (res_inst_tac [("x",
mueller@3078:    "((%i. case (fst ex i) \
mueller@3078: \         of None => None\
mueller@3078: \          | Some(x) => g x) ,snd ex)")]  bexI 1);
mueller@3078: by (Simp_tac 1);
mueller@3078: (* execution is indeed an execution of C *)
mueller@3078: by (asm_full_simp_tac
wenzelm@4089:       (simpset() addsimps [executions_def,is_execution_fragment_def,
mueller@3078:                           par_def,starts_of_def,trans_of_def,rename_def]
nipkow@4071:                 addsplits [split_option_case]) 1);
wenzelm@4089: by (best_tac (claset() addSDs [spec] addDs [sym] addss (simpset())) 1);
mueller@3078: qed"reachable_rename_ioa";
mueller@3078: 
mueller@3078: 
mueller@3078: goal Solve.thy "!!f.[| is_weak_pmap f C A |]\
mueller@3078: \                      ==> (is_weak_pmap f (rename C g) (rename A g))";
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1);
mueller@3078: by (rtac conjI 1);
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [rename_def,starts_of_def]) 1);
mueller@3078: by (REPEAT (rtac allI 1));
mueller@3078: by (rtac imp_conj_lemma 1);
wenzelm@4089: by (simp_tac (simpset() addsimps [rename_def]) 1);
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
paulson@4153: by Safe_tac;
paulson@4153: by (stac expand_if 1);
mueller@3078:  by (rtac conjI 1);
mueller@3078:  by (rtac impI 1);
mueller@3078:  by (etac disjE 1);
mueller@3078:  by (etac exE 1);
mueller@3078: by (etac conjE 1);
mueller@3078: (* x is input *)
mueller@3078:  by (dtac sym 1);
mueller@3078:  by (dtac sym 1);
mueller@3078: by (Asm_full_simp_tac 1);
mueller@3078: by (REPEAT (hyp_subst_tac 1));
mueller@3078: by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
mueller@3078: by (assume_tac 1);
mueller@3078: by (Asm_full_simp_tac 1);
mueller@3078: (* x is output *)
mueller@3078:  by (etac exE 1);
mueller@3078: by (etac conjE 1);
mueller@3078:  by (dtac sym 1);
mueller@3078:  by (dtac sym 1);
mueller@3078: by (Asm_full_simp_tac 1);
mueller@3078: by (REPEAT (hyp_subst_tac 1));
mueller@3078: by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
mueller@3078: by (assume_tac 1);
mueller@3078: by (Asm_full_simp_tac 1);
mueller@3078: (* x is internal *)
wenzelm@4089: by (simp_tac (simpset() addsimps [de_Morgan_disj, de_Morgan_conj, not_ex] 
mueller@3078: 	               addcongs [conj_cong]) 1);
mueller@3078: by (rtac impI 1);
mueller@3078: by (etac conjE 1);
mueller@3078: by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
mueller@3078: by (Auto_tac());
mueller@3078: qed"rename_through_pmap";