--- 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";
--- 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
--- 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<n then ex1 i \
-\ else (if i=n then Some a else None), \
-\ %i. if i<Suc n then ex2 i else t)")] bexI 1);
- by (res_inst_tac [("x","Suc n")] exI 1);
- by (Simp_tac 1);
- by (Asm_full_simp_tac 1);
- by (rtac allI 1);
- by (cut_inst_tac [("m","na"),("n","n")] less_linear 1);
- by Auto_tac;
-qed "reachable_n";
-
-val [p1,p2] = goalw (the_context ()) [invariant_def]
- "[| !!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 (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;
--- 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<n then ex1 i else (if i=n then Some a else None) , %i. if i<Suc n then ex2 i else t)" in bexI)
+ apply (rule_tac x = "Suc n" in exI)
+ apply (simp (no_asm))
+ apply simp
+ apply (rule allI)
+ apply (cut_tac m = "na" and n = "n" in less_linear)
+ apply auto
+ done
+
+
+lemma invariantI:
+ assumes p1: "!!s. s:starts_of(A) ==> 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
--- 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];
--- 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
--- 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