# HG changeset patch # User wenzelm # Date 1149634634 -7200 # Node ID b2af2549efd1146fc4621006975cccbcbbbefc4a # Parent 5f764272183eed838e683629df25a0d38daff2bb removed obsolete ML files; diff -r 5f764272183e -r b2af2549efd1 src/HOL/IOA/Asig.ML --- a/src/HOL/IOA/Asig.ML Tue Jun 06 20:47:12 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: HOL/IOA/Asig.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen -*) - -bind_thms ("asig_projections", [asig_inputs_def, asig_outputs_def, asig_internals_def]); - -Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"; -by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1); -qed"int_and_ext_is_act"; - -Goal "[|a:externals(S)|] ==> a:actions(S)"; -by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1); -qed"ext_is_act"; diff -r 5f764272183e -r b2af2549efd1 src/HOL/IOA/Asig.thy --- a/src/HOL/IOA/Asig.thy Tue Jun 06 20:47:12 2006 +0200 +++ b/src/HOL/IOA/Asig.thy Wed Jun 07 00:57:14 2006 +0200 @@ -46,6 +46,15 @@ mk_ext_asig_def: "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})" -ML {* use_legacy_bindings (the_context ()) *} + +lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def + +lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)" + apply (simp add: externals_def actions_def) + done + +lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)" + apply (simp add: externals_def actions_def) + done end diff -r 5f764272183e -r b2af2549efd1 src/HOL/IOA/IOA.ML --- a/src/HOL/IOA/IOA.ML Tue Jun 06 20:47:12 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,168 +0,0 @@ -(* Title: HOL/IOA/IOA.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen -*) - -Addsimps [Let_def]; - -bind_thms ("ioa_projections", [asig_of_def, starts_of_def, trans_of_def]); - -bind_thms ("exec_rws", [executions_def,is_execution_fragment_def]); - -Goal -"asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z"; - by (simp_tac (simpset() addsimps ioa_projections) 1); - qed "ioa_triple_proj"; - -Goalw [ioa_def,state_trans_def,actions_def, is_asig_def] - "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"; - by (REPEAT(etac conjE 1)); - by (EVERY1[etac allE, etac impE, atac]); - by (Asm_full_simp_tac 1); -qed "trans_in_actions"; - - -Goal "filter_oseq p (filter_oseq p s) = filter_oseq p s"; - by (simp_tac (simpset() addsimps [filter_oseq_def]) 1); - by (rtac ext 1); - by (case_tac "s(i)" 1); - by (Asm_simp_tac 1); - by (Asm_simp_tac 1); -qed "filter_oseq_idemp"; - -Goalw [mk_trace_def,filter_oseq_def] -"(mk_trace A s n = None) = \ -\ (s(n)=None | (? a. s(n)=Some(a) & a ~: externals(asig_of(A)))) \ -\ & \ -\ (mk_trace A s n = Some(a)) = \ -\ (s(n)=Some(a) & a : externals(asig_of(A)))"; - by (case_tac "s(n)" 1); - by (ALLGOALS Asm_simp_tac); - by (Fast_tac 1); -qed "mk_trace_thm"; - -Goalw [reachable_def] "s:starts_of(A) ==> reachable A s"; - by (res_inst_tac [("x","(%i. None,%i. s)")] bexI 1); - by (Simp_tac 1); - by (asm_simp_tac (simpset() addsimps exec_rws) 1); -qed "reachable_0"; - -Goalw (reachable_def::exec_rws) -"!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"; - by (asm_full_simp_tac (simpset() delsimps bex_simps) 1); - by (split_all_tac 1); - by Safe_tac; - by (rename_tac "ex1 ex2 n" 1); - by (res_inst_tac [("x","(%i. if i P(s); \ -\ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \ -\ ==> invariant A P"; - by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); - by Safe_tac; - by (rename_tac "ex1 ex2 n" 1); - by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1); - by (Asm_full_simp_tac 1); - by (induct_tac "n" 1); - by (fast_tac (claset() addIs [p1,reachable_0]) 1); - by (eres_inst_tac[("x","na")] allE 1); - by (case_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac); - by Safe_tac; - by (etac (p2 RS mp) 1); - by (ALLGOALS(fast_tac(claset() addDs [reachable_n]))); -qed "invariantI"; - -val [p1,p2] = goal (the_context ()) - "[| !!s. s : starts_of(A) ==> P(s); \ -\ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \ -\ |] ==> invariant A P"; - by (fast_tac (claset() addSIs [invariantI] addSDs [p1,p2]) 1); -qed "invariantI1"; - -val [p1,p2] = goalw (the_context ()) [invariant_def] -"[| invariant A P; reachable A s |] ==> P(s)"; - by (rtac (p2 RS (p1 RS spec RS mp)) 1); -qed "invariantE"; - -Goal -"actions(asig_comp a b) = actions(a) Un actions(b)"; - by (simp_tac (simpset() addsimps - ([actions_def,asig_comp_def]@asig_projections)) 1); - by (Fast_tac 1); -qed "actions_asig_comp"; - -Goal -"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; - by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1); -qed "starts_of_par"; - -(* Every state in an execution is reachable *) -Goalw [reachable_def] -"ex:executions(A) ==> !n. reachable A (snd ex n)"; - by (Fast_tac 1); -qed "states_of_exec_reachable"; - - -Goal -"(s,a,t) : trans_of(A || B || C || D) = \ -\ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | \ -\ a:actions(asig_of(D))) & \ -\ (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) \ -\ else fst t=fst s) & \ -\ (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B) \ -\ else fst(snd(t))=fst(snd(s))) & \ -\ (if a:actions(asig_of(C)) then \ -\ (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) \ -\ else fst(snd(snd(t)))=fst(snd(snd(s)))) & \ -\ (if a:actions(asig_of(D)) then \ -\ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \ -\ else snd(snd(snd(t)))=snd(snd(snd(s)))))"; - (*SLOW*) - by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq] - @ ioa_projections)) 1); -qed "trans_of_par4"; - -Goal "starts_of(restrict ioa acts) = starts_of(ioa) & \ -\ trans_of(restrict ioa acts) = trans_of(ioa) & \ -\ reachable (restrict ioa acts) s = reachable ioa s"; -by (simp_tac (simpset() addsimps ([is_execution_fragment_def,executions_def, - reachable_def,restrict_def]@ioa_projections)) 1); -qed "cancel_restrict"; - -Goal "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"; - by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1); -qed "asig_of_par"; - - -Goal "externals(asig_of(A1||A2)) = \ -\ (externals(asig_of(A1)) Un 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,Un_def,set_diff_def]) 1); -by (rtac set_ext 1); -by (Fast_tac 1); -qed"externals_of_par"; - -Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def] - "[| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; -by (Asm_full_simp_tac 1); -by (Best_tac 1); -qed"ext1_is_not_int2"; - -Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def] - "[| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; -by (Asm_full_simp_tac 1); -by (Best_tac 1); -qed"ext2_is_not_int1"; - -val ext1_ext2_is_not_act2 = ext1_is_not_int2 RS int_and_ext_is_act; -val ext1_ext2_is_not_act1 = ext2_is_not_int1 RS int_and_ext_is_act; diff -r 5f764272183e -r b2af2549efd1 src/HOL/IOA/IOA.thy --- a/src/HOL/IOA/IOA.thy Tue Jun 06 20:47:12 2006 +0200 +++ b/src/HOL/IOA/IOA.thy Wed Jun 07 00:57:14 2006 +0200 @@ -195,6 +195,167 @@ in ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})" -ML {* use_legacy_bindings (the_context ()) *} + +declare Let_def [simp] + +lemmas ioa_projections = asig_of_def starts_of_def trans_of_def + and exec_rws = executions_def is_execution_fragment_def + +lemma ioa_triple_proj: + "asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z" + apply (simp add: ioa_projections) + done + +lemma trans_in_actions: + "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))" + apply (unfold ioa_def state_trans_def actions_def is_asig_def) + apply (erule conjE)+ + apply (erule allE, erule impE, assumption) + apply simp + done + + +lemma filter_oseq_idemp: "filter_oseq p (filter_oseq p s) = filter_oseq p s" + apply (simp add: filter_oseq_def) + apply (rule ext) + apply (case_tac "s i") + apply simp_all + done + +lemma mk_trace_thm: +"(mk_trace A s n = None) = + (s(n)=None | (? a. s(n)=Some(a) & a ~: externals(asig_of(A)))) + & + (mk_trace A s n = Some(a)) = + (s(n)=Some(a) & a : externals(asig_of(A)))" + apply (unfold mk_trace_def filter_oseq_def) + apply (case_tac "s n") + apply auto + done + +lemma reachable_0: "s:starts_of(A) ==> reachable A s" + apply (unfold reachable_def) + apply (rule_tac x = "(%i. None, %i. s)" in bexI) + apply simp + apply (simp add: exec_rws) + done + +lemma reachable_n: + "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t" + apply (unfold reachable_def exec_rws) + apply (simp del: bex_simps) + apply (simp (no_asm_simp) only: split_tupled_all) + apply safe + apply (rename_tac ex1 ex2 n) + apply (rule_tac x = "(%i. if i P(s)" + and p2: "!!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t)" + shows "invariant A P" + apply (unfold invariant_def reachable_def Let_def exec_rws) + apply safe + apply (rename_tac ex1 ex2 n) + apply (rule_tac Q = "reachable A (ex2 n) " in conjunct1) + apply simp + apply (induct_tac n) + apply (fast intro: p1 reachable_0) + apply (erule_tac x = na in allE) + apply (case_tac "ex1 na", simp_all) + apply safe + apply (erule p2 [THEN mp]) + apply (fast dest: reachable_n)+ + done + +lemma invariantI1: + "[| !!s. s : starts_of(A) ==> P(s); + !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) + |] ==> invariant A P" + apply (blast intro!: invariantI) + done + +lemma invariantE: + "[| invariant A P; reachable A s |] ==> P(s)" + apply (unfold invariant_def) + apply blast + done + +lemma actions_asig_comp: + "actions(asig_comp a b) = actions(a) Un actions(b)" + apply (auto simp add: actions_def asig_comp_def asig_projections) + done + +lemma starts_of_par: + "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}" + apply (simp add: par_def ioa_projections) + done + +(* Every state in an execution is reachable *) +lemma states_of_exec_reachable: + "ex:executions(A) ==> !n. reachable A (snd ex n)" + apply (unfold reachable_def) + apply fast + done + + +lemma trans_of_par4: +"(s,a,t) : trans_of(A || B || C || D) = + ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | + a:actions(asig_of(D))) & + (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) + else fst t=fst s) & + (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B) + else fst(snd(t))=fst(snd(s))) & + (if a:actions(asig_of(C)) then + (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) + else fst(snd(snd(t)))=fst(snd(snd(s)))) & + (if a:actions(asig_of(D)) then + (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) + else snd(snd(snd(t)))=snd(snd(snd(s)))))" + (*SLOW*) + apply (simp (no_asm) add: par_def actions_asig_comp Pair_fst_snd_eq ioa_projections) + done + +lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) & + trans_of(restrict ioa acts) = trans_of(ioa) & + reachable (restrict ioa acts) s = reachable ioa s" + apply (simp add: is_execution_fragment_def executions_def + reachable_def restrict_def ioa_projections) + done + +lemma asig_of_par: "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)" + apply (simp add: par_def ioa_projections) + done + + +lemma externals_of_par: "externals(asig_of(A1||A2)) = + (externals(asig_of(A1)) Un externals(asig_of(A2)))" + apply (simp add: externals_def asig_of_par asig_comp_def + asig_inputs_def asig_outputs_def Un_def set_diff_def) + apply blast + done + +lemma ext1_is_not_int2: + "[| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))" + apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def) + apply auto + done + +lemma ext2_is_not_int1: + "[| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))" + apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def) + apply auto + done + +lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act] + and ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act] end diff -r 5f764272183e -r b2af2549efd1 src/HOL/IOA/Solve.ML --- a/src/HOL/IOA/Solve.ML Tue Jun 06 20:47:12 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,210 +0,0 @@ -(* Title: HOL/IOA/Solve.ML - ID: $Id$ - 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]; diff -r 5f764272183e -r b2af2549efd1 src/HOL/IOA/Solve.thy --- a/src/HOL/IOA/Solve.thy Tue Jun 06 20:47:12 2006 +0200 +++ b/src/HOL/IOA/Solve.thy Wed Jun 07 00:57:14 2006 +0200 @@ -21,6 +21,192 @@ (f(s),a,f(t)):trans_of(A) else f(s)=f(t)))" -ML {* use_legacy_bindings (the_context ()) *} +declare mk_trace_thm [simp] trans_in_actions [simp] + +lemma trace_inclusion: + "[| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); + is_weak_pmap f C A |] ==> traces(C) <= traces(A)" + apply (unfold is_weak_pmap_def traces_def) + + apply (simp (no_asm) add: has_trace_def) + apply safe + apply (rename_tac ex1 ex2) + + (* choose same trace, therefore same NF *) + apply (rule_tac x = "mk_trace C ex1" in exI) + apply simp + + (* give execution of abstract automata *) + apply (rule_tac x = "(mk_trace A ex1,%i. f (ex2 i))" in bexI) + + (* Traces coincide *) + apply (simp (no_asm_simp) add: mk_trace_def filter_oseq_idemp) + + (* Use lemma *) + apply (frule states_of_exec_reachable) + + (* Now show that it's an execution *) + apply (simp add: executions_def) + apply safe + + (* Start states map to start states *) + apply (drule bspec) + apply assumption + + (* Show that it's an execution fragment *) + apply (simp add: is_execution_fragment_def) + apply safe + + apply (erule_tac x = "ex2 n" in allE) + apply (erule_tac x = "ex2 (Suc n)" in allE) + apply (erule_tac x = a in allE) + apply simp + done + +(* Lemmata *) + +lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R" + by blast + + +(* fist_order_tautology of externals_of_par *) +lemma externals_of_par_extra: + "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)))" + apply (auto simp add: externals_def asig_of_par asig_comp_def asig_inputs_def asig_outputs_def) + done + +lemma comp1_reachable: "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)" + apply (simp add: reachable_def) + apply (erule bexE) + apply (rule_tac x = + "(filter_oseq (%a. a:actions (asig_of (C1))) (fst ex) , %i. fst (snd ex i))" in bexI) +(* fst(s) is in projected execution *) + apply force +(* projected execution is indeed an execution *) + apply (simp cong del: if_weak_cong + add: executions_def is_execution_fragment_def par_def starts_of_def + trans_of_def filter_oseq_def + split add: option.split) + done + + +(* Exact copy of proof of comp1_reachable for the second + component of a parallel composition. *) +lemma comp2_reachable: "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)" + apply (simp add: reachable_def) + apply (erule bexE) + apply (rule_tac x = + "(filter_oseq (%a. a:actions (asig_of (C2))) (fst ex) , %i. snd (snd ex i))" in bexI) +(* fst(s) is in projected execution *) + apply force +(* projected execution is indeed an execution *) + apply (simp cong del: if_weak_cong + add: executions_def is_execution_fragment_def par_def starts_of_def + trans_of_def filter_oseq_def + split add: option.split) + done + +declare split_if [split del] if_weak_cong [cong del] + +(*Composition of possibility-mappings *) +lemma fxg_is_weak_pmap_of_product_IOA: + "[| 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)" + apply (unfold is_weak_pmap_def) + apply (rule conjI) +(* start_states *) + apply (simp add: par_def starts_of_def) +(* transitions *) + apply (rule allI)+ + apply (rule imp_conj_lemma) + apply (simp (no_asm) add: externals_of_par_extra) + apply (simp (no_asm) add: par_def) + apply (simp add: trans_of_def) + apply (simplesubst split_if) + apply (rule conjI) + apply (rule impI) + apply (erule disjE) +(* case 1 a:e(A1) | a:e(A2) *) + apply (simp add: comp1_reachable comp2_reachable ext_is_act) + apply (erule disjE) +(* case 2 a:e(A1) | a~:e(A2) *) + apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act2) +(* case 3 a:~e(A1) | a:e(A2) *) + apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act1) +(* case 4 a:~e(A1) | a~:e(A2) *) + apply (rule impI) + apply (subgoal_tac "a~:externals (asig_of (A1)) & a~:externals (asig_of (A2))") +(* delete auxiliary subgoal *) + prefer 2 + apply force + apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if) + apply (tactic {* + REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN + asm_full_simp_tac(simpset() addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *}) + done + + +lemma reachable_rename_ioa: "[| reachable (rename C g) s |] ==> reachable C s" + apply (simp add: reachable_def) + apply (erule bexE) + apply (rule_tac x = "((%i. case (fst ex i) of None => None | Some (x) => g x) ,snd ex)" in bexI) + apply (simp (no_asm)) +(* execution is indeed an execution of C *) + apply (simp add: executions_def is_execution_fragment_def par_def + starts_of_def trans_of_def rename_def split add: option.split) + apply force + done + + +lemma rename_through_pmap: "[| is_weak_pmap f C A |] + ==> (is_weak_pmap f (rename C g) (rename A g))" + apply (simp add: is_weak_pmap_def) + apply (rule conjI) + apply (simp add: rename_def starts_of_def) + apply (rule allI)+ + apply (rule imp_conj_lemma) + apply (simp (no_asm) add: rename_def) + apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def) + apply safe + apply (simplesubst split_if) + apply (rule conjI) + apply (rule impI) + apply (erule disjE) + apply (erule exE) + apply (erule conjE) +(* x is input *) + apply (drule sym) + apply (drule sym) + apply simp + apply hypsubst+ + apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa) + apply assumption + apply simp +(* x is output *) + apply (erule exE) + apply (erule conjE) + apply (drule sym) + apply (drule sym) + apply simp + apply hypsubst+ + apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa) + apply assumption + apply simp +(* x is internal *) + apply (simp (no_asm) add: de_Morgan_disj de_Morgan_conj not_ex cong add: conj_cong) + apply (rule impI) + apply (erule conjE) + apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa) + apply auto + done + +declare split_if [split] if_weak_cong [cong] end diff -r 5f764272183e -r b2af2549efd1 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jun 06 20:47:12 2006 +0200 +++ b/src/HOL/IsaMakefile Wed Jun 07 00:57:14 2006 +0200 @@ -599,8 +599,8 @@ HOL-IOA: HOL $(LOG)/HOL-IOA.gz -$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.ML IOA/Asig.thy IOA/IOA.ML \ - IOA/IOA.thy IOA/ROOT.ML IOA/Solve.ML IOA/Solve.thy +$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy \ + IOA/ROOT.ML IOA/Solve.thy @$(ISATOOL) usedir $(OUT)/HOL IOA