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