removed obsolete ML files;
authorwenzelm
Wed Jun 07 00:57:14 2006 +0200 (2006-06-07)
changeset 19801b2af2549efd1
parent 19800 5f764272183e
child 19802 c2860c37e574
removed obsolete ML files;
src/HOL/IOA/Asig.ML
src/HOL/IOA/Asig.thy
src/HOL/IOA/IOA.ML
src/HOL/IOA/IOA.thy
src/HOL/IOA/Solve.ML
src/HOL/IOA/Solve.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IOA/Asig.ML	Tue Jun 06 20:47:12 2006 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,15 +0,0 @@
     1.4 -(*  Title:      HOL/IOA/Asig.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow & Konrad Slind
     1.7 -    Copyright   1994  TU Muenchen
     1.8 -*)
     1.9 -
    1.10 -bind_thms ("asig_projections", [asig_inputs_def, asig_outputs_def, asig_internals_def]);
    1.11 -
    1.12 -Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
    1.13 -by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
    1.14 -qed"int_and_ext_is_act";
    1.15 -
    1.16 -Goal "[|a:externals(S)|] ==> a:actions(S)";
    1.17 -by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
    1.18 -qed"ext_is_act";
     2.1 --- a/src/HOL/IOA/Asig.thy	Tue Jun 06 20:47:12 2006 +0200
     2.2 +++ b/src/HOL/IOA/Asig.thy	Wed Jun 07 00:57:14 2006 +0200
     2.3 @@ -46,6 +46,15 @@
     2.4  mk_ext_asig_def:
     2.5    "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
     2.6  
     2.7 -ML {* use_legacy_bindings (the_context ()) *}
     2.8 +
     2.9 +lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
    2.10 +
    2.11 +lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"
    2.12 +  apply (simp add: externals_def actions_def)
    2.13 +  done
    2.14 +
    2.15 +lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)"
    2.16 +  apply (simp add: externals_def actions_def)
    2.17 +  done
    2.18  
    2.19  end
     3.1 --- a/src/HOL/IOA/IOA.ML	Tue Jun 06 20:47:12 2006 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,168 +0,0 @@
     3.4 -(*  Title:      HOL/IOA/IOA.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Tobias Nipkow & Konrad Slind
     3.7 -    Copyright   1994  TU Muenchen
     3.8 -*)
     3.9 -
    3.10 -Addsimps [Let_def];
    3.11 -
    3.12 -bind_thms ("ioa_projections", [asig_of_def, starts_of_def, trans_of_def]);
    3.13 -
    3.14 -bind_thms ("exec_rws", [executions_def,is_execution_fragment_def]);
    3.15 -
    3.16 -Goal
    3.17 -"asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z";
    3.18 -  by (simp_tac (simpset() addsimps ioa_projections) 1);
    3.19 -  qed "ioa_triple_proj";
    3.20 -
    3.21 -Goalw [ioa_def,state_trans_def,actions_def, is_asig_def]
    3.22 -  "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))";
    3.23 -  by (REPEAT(etac conjE 1));
    3.24 -  by (EVERY1[etac allE, etac impE, atac]);
    3.25 -  by (Asm_full_simp_tac 1);
    3.26 -qed "trans_in_actions";
    3.27 -
    3.28 -
    3.29 -Goal "filter_oseq p (filter_oseq p s) = filter_oseq p s";
    3.30 -  by (simp_tac (simpset() addsimps [filter_oseq_def]) 1);
    3.31 -  by (rtac ext 1);
    3.32 -  by (case_tac "s(i)" 1);
    3.33 -  by (Asm_simp_tac 1);
    3.34 -  by (Asm_simp_tac 1);
    3.35 -qed "filter_oseq_idemp";
    3.36 -
    3.37 -Goalw [mk_trace_def,filter_oseq_def]
    3.38 -"(mk_trace A s n = None) =                                        \
    3.39 -\  (s(n)=None | (? a. s(n)=Some(a) & a ~: externals(asig_of(A)))) \
    3.40 -\  &                                                              \
    3.41 -\  (mk_trace A s n = Some(a)) =                                   \
    3.42 -\   (s(n)=Some(a) & a : externals(asig_of(A)))";
    3.43 -  by (case_tac "s(n)" 1);
    3.44 -  by (ALLGOALS Asm_simp_tac);
    3.45 -  by (Fast_tac 1);
    3.46 -qed "mk_trace_thm";
    3.47 -
    3.48 -Goalw [reachable_def] "s:starts_of(A) ==> reachable A s";
    3.49 -  by (res_inst_tac [("x","(%i. None,%i. s)")] bexI 1);
    3.50 -  by (Simp_tac 1);
    3.51 -  by (asm_simp_tac (simpset() addsimps exec_rws) 1);
    3.52 -qed "reachable_0";
    3.53 -
    3.54 -Goalw (reachable_def::exec_rws)
    3.55 -"!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
    3.56 -  by (asm_full_simp_tac (simpset() delsimps bex_simps) 1);
    3.57 -  by (split_all_tac 1);
    3.58 -  by Safe_tac;
    3.59 -  by (rename_tac "ex1 ex2 n" 1);
    3.60 -  by (res_inst_tac [("x","(%i. if i<n then ex1 i                    \
    3.61 -\                            else (if i=n then Some a else None),    \
    3.62 -\                         %i. if i<Suc n then ex2 i else t)")] bexI 1);
    3.63 -   by (res_inst_tac [("x","Suc n")] exI 1);
    3.64 -   by (Simp_tac 1);
    3.65 -  by (Asm_full_simp_tac 1);
    3.66 -  by (rtac allI 1);
    3.67 -  by (cut_inst_tac [("m","na"),("n","n")] less_linear 1);
    3.68 -  by Auto_tac;
    3.69 -qed "reachable_n";
    3.70 -
    3.71 -val [p1,p2] = goalw (the_context ()) [invariant_def]
    3.72 -  "[| !!s. s:starts_of(A) ==> P(s);                                          \
    3.73 -\     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
    3.74 -\  ==> invariant A P";
    3.75 -  by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
    3.76 -  by Safe_tac;
    3.77 -  by (rename_tac "ex1 ex2 n" 1);
    3.78 -  by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1);
    3.79 -  by (Asm_full_simp_tac 1);
    3.80 -  by (induct_tac "n" 1);
    3.81 -   by (fast_tac (claset() addIs [p1,reachable_0]) 1);
    3.82 -  by (eres_inst_tac[("x","na")] allE 1);
    3.83 -  by (case_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac);
    3.84 -  by Safe_tac;
    3.85 -   by (etac (p2 RS mp) 1);
    3.86 -    by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
    3.87 -qed "invariantI";
    3.88 -
    3.89 -val [p1,p2] = goal (the_context ())
    3.90 - "[| !!s. s : starts_of(A) ==> P(s); \
    3.91 -\    !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
    3.92 -\ |] ==> invariant A P";
    3.93 -  by (fast_tac (claset() addSIs [invariantI] addSDs [p1,p2]) 1);
    3.94 -qed "invariantI1";
    3.95 -
    3.96 -val [p1,p2] = goalw (the_context ()) [invariant_def]
    3.97 -"[| invariant A P; reachable A s |] ==> P(s)";
    3.98 -   by (rtac (p2 RS (p1 RS spec RS mp)) 1);
    3.99 -qed "invariantE";
   3.100 -
   3.101 -Goal
   3.102 -"actions(asig_comp a b) = actions(a) Un actions(b)";
   3.103 -  by (simp_tac (simpset() addsimps
   3.104 -               ([actions_def,asig_comp_def]@asig_projections)) 1);
   3.105 -  by (Fast_tac 1);
   3.106 -qed "actions_asig_comp";
   3.107 -
   3.108 -Goal
   3.109 -"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
   3.110 -  by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
   3.111 -qed "starts_of_par";
   3.112 -
   3.113 -(* Every state in an execution is reachable *)
   3.114 -Goalw [reachable_def]
   3.115 -"ex:executions(A) ==> !n. reachable A (snd ex n)";
   3.116 -  by (Fast_tac 1);
   3.117 -qed "states_of_exec_reachable";
   3.118 -
   3.119 -
   3.120 -Goal
   3.121 -"(s,a,t) : trans_of(A || B || C || D) =                                      \
   3.122 -\ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |  \
   3.123 -\   a:actions(asig_of(D))) &                                                 \
   3.124 -\  (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)              \
   3.125 -\   else fst t=fst s) &                                                      \
   3.126 -\  (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)    \
   3.127 -\   else fst(snd(t))=fst(snd(s))) &                                          \
   3.128 -\  (if a:actions(asig_of(C)) then                                            \
   3.129 -\     (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)                      \
   3.130 -\   else fst(snd(snd(t)))=fst(snd(snd(s)))) &                                \
   3.131 -\  (if a:actions(asig_of(D)) then                                            \
   3.132 -\     (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                      \
   3.133 -\   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
   3.134 -  (*SLOW*)
   3.135 -  by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]
   3.136 -                                    @ ioa_projections)) 1);
   3.137 -qed "trans_of_par4";
   3.138 -
   3.139 -Goal "starts_of(restrict ioa acts) = starts_of(ioa) &     \
   3.140 -\             trans_of(restrict ioa acts) = trans_of(ioa) &       \
   3.141 -\             reachable (restrict ioa acts) s = reachable ioa s";
   3.142 -by (simp_tac (simpset() addsimps ([is_execution_fragment_def,executions_def,
   3.143 -                           reachable_def,restrict_def]@ioa_projections)) 1);
   3.144 -qed "cancel_restrict";
   3.145 -
   3.146 -Goal "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
   3.147 -  by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
   3.148 -qed "asig_of_par";
   3.149 -
   3.150 -
   3.151 -Goal "externals(asig_of(A1||A2)) =    \
   3.152 -\  (externals(asig_of(A1)) Un externals(asig_of(A2)))";
   3.153 -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);
   3.154 -by (rtac set_ext 1);
   3.155 -by (Fast_tac 1);
   3.156 -qed"externals_of_par";
   3.157 -
   3.158 -Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
   3.159 - "[| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
   3.160 -by (Asm_full_simp_tac 1);
   3.161 -by (Best_tac 1);
   3.162 -qed"ext1_is_not_int2";
   3.163 -
   3.164 -Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
   3.165 - "[| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
   3.166 -by (Asm_full_simp_tac 1);
   3.167 -by (Best_tac 1);
   3.168 -qed"ext2_is_not_int1";
   3.169 -
   3.170 -val ext1_ext2_is_not_act2 = ext1_is_not_int2 RS int_and_ext_is_act;
   3.171 -val ext1_ext2_is_not_act1 = ext2_is_not_int1 RS int_and_ext_is_act;
     4.1 --- a/src/HOL/IOA/IOA.thy	Tue Jun 06 20:47:12 2006 +0200
     4.2 +++ b/src/HOL/IOA/IOA.thy	Wed Jun 07 00:57:14 2006 +0200
     4.3 @@ -195,6 +195,167 @@
     4.4          in
     4.5          ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
     4.6  
     4.7 -ML {* use_legacy_bindings (the_context ()) *}
     4.8 +
     4.9 +declare Let_def [simp]
    4.10 +
    4.11 +lemmas ioa_projections = asig_of_def starts_of_def trans_of_def
    4.12 +  and exec_rws = executions_def is_execution_fragment_def
    4.13 +
    4.14 +lemma ioa_triple_proj:
    4.15 +    "asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z"
    4.16 +  apply (simp add: ioa_projections)
    4.17 +  done
    4.18 +
    4.19 +lemma trans_in_actions:
    4.20 +  "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"
    4.21 +  apply (unfold ioa_def state_trans_def actions_def is_asig_def)
    4.22 +  apply (erule conjE)+
    4.23 +  apply (erule allE, erule impE, assumption)
    4.24 +  apply simp
    4.25 +  done
    4.26 +
    4.27 +
    4.28 +lemma filter_oseq_idemp: "filter_oseq p (filter_oseq p s) = filter_oseq p s"
    4.29 +  apply (simp add: filter_oseq_def)
    4.30 +  apply (rule ext)
    4.31 +  apply (case_tac "s i")
    4.32 +  apply simp_all
    4.33 +  done
    4.34 +
    4.35 +lemma mk_trace_thm:
    4.36 +"(mk_trace A s n = None) =
    4.37 +   (s(n)=None | (? a. s(n)=Some(a) & a ~: externals(asig_of(A))))
    4.38 +   &
    4.39 +   (mk_trace A s n = Some(a)) =
    4.40 +    (s(n)=Some(a) & a : externals(asig_of(A)))"
    4.41 +  apply (unfold mk_trace_def filter_oseq_def)
    4.42 +  apply (case_tac "s n")
    4.43 +  apply auto
    4.44 +  done
    4.45 +
    4.46 +lemma reachable_0: "s:starts_of(A) ==> reachable A s"
    4.47 +  apply (unfold reachable_def)
    4.48 +  apply (rule_tac x = "(%i. None, %i. s)" in bexI)
    4.49 +  apply simp
    4.50 +  apply (simp add: exec_rws)
    4.51 +  done
    4.52 +
    4.53 +lemma reachable_n:
    4.54 +  "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"
    4.55 +  apply (unfold reachable_def exec_rws)
    4.56 +  apply (simp del: bex_simps)
    4.57 +  apply (simp (no_asm_simp) only: split_tupled_all)
    4.58 +  apply safe
    4.59 +  apply (rename_tac ex1 ex2 n)
    4.60 +  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)
    4.61 +   apply (rule_tac x = "Suc n" in exI)
    4.62 +   apply (simp (no_asm))
    4.63 +  apply simp
    4.64 +  apply (rule allI)
    4.65 +  apply (cut_tac m = "na" and n = "n" in less_linear)
    4.66 +  apply auto
    4.67 +  done
    4.68 +
    4.69 +
    4.70 +lemma invariantI:
    4.71 +  assumes p1: "!!s. s:starts_of(A) ==> P(s)"
    4.72 +    and p2: "!!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t)"
    4.73 +  shows "invariant A P"
    4.74 +  apply (unfold invariant_def reachable_def Let_def exec_rws)
    4.75 +  apply safe
    4.76 +  apply (rename_tac ex1 ex2 n)
    4.77 +  apply (rule_tac Q = "reachable A (ex2 n) " in conjunct1)
    4.78 +  apply simp
    4.79 +  apply (induct_tac n)
    4.80 +   apply (fast intro: p1 reachable_0)
    4.81 +  apply (erule_tac x = na in allE)
    4.82 +  apply (case_tac "ex1 na", simp_all)
    4.83 +  apply safe
    4.84 +   apply (erule p2 [THEN mp])
    4.85 +    apply (fast dest: reachable_n)+
    4.86 +  done
    4.87 +
    4.88 +lemma invariantI1:
    4.89 + "[| !!s. s : starts_of(A) ==> P(s);
    4.90 +     !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t)
    4.91 +  |] ==> invariant A P"
    4.92 +  apply (blast intro!: invariantI)
    4.93 +  done
    4.94 +
    4.95 +lemma invariantE:
    4.96 +  "[| invariant A P; reachable A s |] ==> P(s)"
    4.97 +  apply (unfold invariant_def)
    4.98 +  apply blast
    4.99 +  done
   4.100 +
   4.101 +lemma actions_asig_comp:
   4.102 +  "actions(asig_comp a b) = actions(a) Un actions(b)"
   4.103 +  apply (auto simp add: actions_def asig_comp_def asig_projections)
   4.104 +  done
   4.105 +
   4.106 +lemma starts_of_par:
   4.107 +  "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"
   4.108 +  apply (simp add: par_def ioa_projections)
   4.109 +  done
   4.110 +
   4.111 +(* Every state in an execution is reachable *)
   4.112 +lemma states_of_exec_reachable:
   4.113 +  "ex:executions(A) ==> !n. reachable A (snd ex n)"
   4.114 +  apply (unfold reachable_def)
   4.115 +  apply fast
   4.116 +  done
   4.117 +
   4.118 +
   4.119 +lemma trans_of_par4:
   4.120 +"(s,a,t) : trans_of(A || B || C || D) =
   4.121 +  ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |
   4.122 +    a:actions(asig_of(D))) &
   4.123 +   (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)
   4.124 +    else fst t=fst s) &
   4.125 +   (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)
   4.126 +    else fst(snd(t))=fst(snd(s))) &
   4.127 +   (if a:actions(asig_of(C)) then
   4.128 +      (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)
   4.129 +    else fst(snd(snd(t)))=fst(snd(snd(s)))) &
   4.130 +   (if a:actions(asig_of(D)) then
   4.131 +      (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)
   4.132 +    else snd(snd(snd(t)))=snd(snd(snd(s)))))"
   4.133 +  (*SLOW*)
   4.134 +  apply (simp (no_asm) add: par_def actions_asig_comp Pair_fst_snd_eq ioa_projections)
   4.135 +  done
   4.136 +
   4.137 +lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) &
   4.138 +              trans_of(restrict ioa acts) = trans_of(ioa) &
   4.139 +              reachable (restrict ioa acts) s = reachable ioa s"
   4.140 +  apply (simp add: is_execution_fragment_def executions_def
   4.141 +    reachable_def restrict_def ioa_projections)
   4.142 +  done
   4.143 +
   4.144 +lemma asig_of_par: "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"
   4.145 +  apply (simp add: par_def ioa_projections)
   4.146 +  done
   4.147 +
   4.148 +
   4.149 +lemma externals_of_par: "externals(asig_of(A1||A2)) =
   4.150 +   (externals(asig_of(A1)) Un externals(asig_of(A2)))"
   4.151 +  apply (simp add: externals_def asig_of_par asig_comp_def
   4.152 +    asig_inputs_def asig_outputs_def Un_def set_diff_def)
   4.153 +  apply blast
   4.154 +  done
   4.155 +
   4.156 +lemma ext1_is_not_int2:
   4.157 +  "[| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"
   4.158 +  apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def)
   4.159 +  apply auto
   4.160 +  done
   4.161 +
   4.162 +lemma ext2_is_not_int1:
   4.163 + "[| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"
   4.164 +  apply (unfold externals_def actions_def compat_ioas_def compat_asigs_def)
   4.165 +  apply auto
   4.166 +  done
   4.167 +
   4.168 +lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act]
   4.169 +  and ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act]
   4.170  
   4.171  end
     5.1 --- a/src/HOL/IOA/Solve.ML	Tue Jun 06 20:47:12 2006 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,210 +0,0 @@
     5.4 -(*  Title:      HOL/IOA/Solve.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Tobias Nipkow & Konrad Slind
     5.7 -    Copyright   1994  TU Muenchen
     5.8 -*)
     5.9 -
    5.10 -Addsimps [mk_trace_thm,trans_in_actions];
    5.11 -
    5.12 -Goalw [is_weak_pmap_def,traces_def]
    5.13 -  "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \
    5.14 -\          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
    5.15 -
    5.16 -  by (simp_tac(simpset() addsimps [has_trace_def])1);
    5.17 -  by Safe_tac;
    5.18 -  by (rename_tac "ex1 ex2" 1);
    5.19 -
    5.20 -  (* choose same trace, therefore same NF *)
    5.21 -  by (res_inst_tac[("x","mk_trace  C ex1")] exI 1);
    5.22 -  by (Asm_full_simp_tac 1);
    5.23 -
    5.24 -  (* give execution of abstract automata *)
    5.25 -  by (res_inst_tac[("x","(mk_trace A ex1,%i. f (ex2 i))")] bexI 1);
    5.26 -
    5.27 -  (* Traces coincide *)
    5.28 -   by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1);
    5.29 -
    5.30 -  (* Use lemma *)
    5.31 -  by (ftac states_of_exec_reachable 1);
    5.32 -
    5.33 -  (* Now show that it's an execution *)
    5.34 -  by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1);
    5.35 -  by Safe_tac;
    5.36 -
    5.37 -  (* Start states map to start states *)
    5.38 -  by (dtac bspec 1);
    5.39 -  by (atac 1);
    5.40 -
    5.41 -  (* Show that it's an execution fragment *)
    5.42 -  by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1);
    5.43 -  by Safe_tac;
    5.44 -
    5.45 -  by (eres_inst_tac [("x","ex2 n")] allE 1);
    5.46 -  by (eres_inst_tac [("x","ex2 (Suc n)")] allE 1);
    5.47 -  by (eres_inst_tac [("x","a")] allE 1);
    5.48 -  by (Asm_full_simp_tac 1);
    5.49 -qed "trace_inclusion";
    5.50 -
    5.51 -(* Lemmata *)
    5.52 -
    5.53 -val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    5.54 -  by (fast_tac (claset() addDs prems) 1);
    5.55 -val imp_conj_lemma = result();
    5.56 -
    5.57 -
    5.58 -(* fist_order_tautology of externals_of_par *)
    5.59 -goal (theory "IOA") "a:externals(asig_of(A1||A2)) =    \
    5.60 -\  (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) |  \
    5.61 -\  a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |  \
    5.62 -\  a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))";
    5.63 -by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1);
    5.64 - by (Fast_tac 1);
    5.65 -val externals_of_par_extra = result();
    5.66 -
    5.67 -Goal "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
    5.68 -by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
    5.69 -by (etac bexE 1);
    5.70 -by (res_inst_tac [("x",
    5.71 -   "(filter_oseq (%a. a:actions(asig_of(C1))) \
    5.72 -\                (fst ex),                                                \
    5.73 -\    %i. fst (snd ex i))")]  bexI 1);
    5.74 -(* fst(s) is in projected execution *)
    5.75 - by (Force_tac 1);
    5.76 -(* projected execution is indeed an execution *)
    5.77 -by (asm_full_simp_tac
    5.78 -      (simpset() delcongs [if_weak_cong]
    5.79 -                 addsimps [executions_def,is_execution_fragment_def,
    5.80 -                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
    5.81 -                 addsplits [option.split]) 1);
    5.82 -qed"comp1_reachable";
    5.83 -
    5.84 -
    5.85 -(* Exact copy of proof of comp1_reachable for the second
    5.86 -   component of a parallel composition.     *)
    5.87 -Goal "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
    5.88 -by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
    5.89 -by (etac bexE 1);
    5.90 -by (res_inst_tac [("x",
    5.91 -   "(filter_oseq (%a. a:actions(asig_of(C2)))\
    5.92 -\                (fst ex),                                                \
    5.93 -\    %i. snd (snd ex i))")]  bexI 1);
    5.94 -(* fst(s) is in projected execution *)
    5.95 - by (Force_tac 1);
    5.96 -(* projected execution is indeed an execution *)
    5.97 -by (asm_full_simp_tac
    5.98 -      (simpset() delcongs [if_weak_cong]
    5.99 -                 addsimps [executions_def,is_execution_fragment_def,
   5.100 -                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
   5.101 -                 addsplits [option.split]) 1);
   5.102 -qed"comp2_reachable";
   5.103 -
   5.104 -Delsplits [split_if]; Delcongs [if_weak_cong];
   5.105 -
   5.106 -(* THIS THEOREM IS NEVER USED (lcp)
   5.107 -   Composition of possibility-mappings *)
   5.108 -Goalw [is_weak_pmap_def]
   5.109 -     "[| is_weak_pmap f C1 A1; \
   5.110 -\        externals(asig_of(A1))=externals(asig_of(C1));\
   5.111 -\        is_weak_pmap g C2 A2;  \
   5.112 -\        externals(asig_of(A2))=externals(asig_of(C2)); \
   5.113 -\        compat_ioas C1 C2; compat_ioas A1 A2  |]     \
   5.114 -\  ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
   5.115 - by (rtac conjI 1);
   5.116 -(* start_states *)
   5.117 - by (asm_full_simp_tac (simpset() addsimps [par_def, starts_of_def]) 1);
   5.118 -(* transitions *)
   5.119 -by (REPEAT (rtac allI 1));
   5.120 -by (rtac imp_conj_lemma 1);
   5.121 -by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
   5.122 -by (simp_tac (simpset() addsimps [par_def]) 1);
   5.123 -by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
   5.124 -by (stac split_if 1);
   5.125 -by (rtac conjI 1);
   5.126 -by (rtac impI 1);
   5.127 -by (etac disjE 1);
   5.128 -(* case 1      a:e(A1) | a:e(A2) *)
   5.129 -by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
   5.130 -                                    ext_is_act]) 1);
   5.131 -by (etac disjE 1);
   5.132 -(* case 2      a:e(A1) | a~:e(A2) *)
   5.133 -by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
   5.134 -             ext_is_act,ext1_ext2_is_not_act2]) 1);
   5.135 -(* case 3      a:~e(A1) | a:e(A2) *)
   5.136 -by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
   5.137 -             ext_is_act,ext1_ext2_is_not_act1]) 1);
   5.138 -(* case 4      a:~e(A1) | a~:e(A2) *)
   5.139 -by (rtac impI 1);
   5.140 -by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1);
   5.141 -(* delete auxiliary subgoal *)
   5.142 -by (Asm_full_simp_tac 2);
   5.143 -by (Fast_tac 2);
   5.144 -by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
   5.145 -                 addsplits [split_if]) 1);
   5.146 -by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
   5.147 -           asm_full_simp_tac(simpset() addsimps[comp1_reachable,
   5.148 -                                                comp2_reachable])1));
   5.149 -qed"fxg_is_weak_pmap_of_product_IOA";
   5.150 -
   5.151 -
   5.152 -Goal "[| reachable (rename C g) s |] ==> reachable C s";
   5.153 -by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
   5.154 -by (etac bexE 1);
   5.155 -by (res_inst_tac [("x",
   5.156 -   "((%i. case (fst ex i) \
   5.157 -\         of None => None\
   5.158 -\          | Some(x) => g x) ,snd ex)")]  bexI 1);
   5.159 -by (Simp_tac 1);
   5.160 -(* execution is indeed an execution of C *)
   5.161 -by (asm_full_simp_tac
   5.162 -      (simpset() addsimps [executions_def,is_execution_fragment_def,
   5.163 -                          par_def,starts_of_def,trans_of_def,rename_def]
   5.164 -                addsplits [option.split]) 1);
   5.165 -by (best_tac (claset() addSDs [spec] addDs [sym] addss (simpset())) 1);
   5.166 -qed"reachable_rename_ioa";
   5.167 -
   5.168 -
   5.169 -Goal "[| is_weak_pmap f C A |]\
   5.170 -\                      ==> (is_weak_pmap f (rename C g) (rename A g))";
   5.171 -by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1);
   5.172 -by (rtac conjI 1);
   5.173 -by (asm_full_simp_tac (simpset() addsimps [rename_def,starts_of_def]) 1);
   5.174 -by (REPEAT (rtac allI 1));
   5.175 -by (rtac imp_conj_lemma 1);
   5.176 -by (simp_tac (simpset() addsimps [rename_def]) 1);
   5.177 -by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
   5.178 -by Safe_tac;
   5.179 -by (stac split_if 1);
   5.180 - by (rtac conjI 1);
   5.181 - by (rtac impI 1);
   5.182 - by (etac disjE 1);
   5.183 - by (etac exE 1);
   5.184 -by (etac conjE 1);
   5.185 -(* x is input *)
   5.186 - by (dtac sym 1);
   5.187 - by (dtac sym 1);
   5.188 -by (Asm_full_simp_tac 1);
   5.189 -by (REPEAT (hyp_subst_tac 1));
   5.190 -by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
   5.191 -by (assume_tac 1);
   5.192 -by (Asm_full_simp_tac 1);
   5.193 -(* x is output *)
   5.194 - by (etac exE 1);
   5.195 -by (etac conjE 1);
   5.196 - by (dtac sym 1);
   5.197 - by (dtac sym 1);
   5.198 -by (Asm_full_simp_tac 1);
   5.199 -by (REPEAT (hyp_subst_tac 1));
   5.200 -by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
   5.201 -by (assume_tac 1);
   5.202 -by (Asm_full_simp_tac 1);
   5.203 -(* x is internal *)
   5.204 -by (simp_tac (simpset() addsimps [de_Morgan_disj, de_Morgan_conj, not_ex]
   5.205 -                       addcongs [conj_cong]) 1);
   5.206 -by (rtac impI 1);
   5.207 -by (etac conjE 1);
   5.208 -by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
   5.209 -by Auto_tac;
   5.210 -qed"rename_through_pmap";
   5.211 -
   5.212 -Addsplits [split_if];
   5.213 -Addcongs  [if_weak_cong];
     6.1 --- a/src/HOL/IOA/Solve.thy	Tue Jun 06 20:47:12 2006 +0200
     6.2 +++ b/src/HOL/IOA/Solve.thy	Wed Jun 07 00:57:14 2006 +0200
     6.3 @@ -21,6 +21,192 @@
     6.4                     (f(s),a,f(t)):trans_of(A)
     6.5                   else f(s)=f(t)))"
     6.6  
     6.7 -ML {* use_legacy_bindings (the_context ()) *}
     6.8 +declare mk_trace_thm [simp] trans_in_actions [simp]
     6.9 +
    6.10 +lemma trace_inclusion: 
    6.11 +  "[| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A));  
    6.12 +           is_weak_pmap f C A |] ==> traces(C) <= traces(A)"
    6.13 +  apply (unfold is_weak_pmap_def traces_def)
    6.14 +
    6.15 +  apply (simp (no_asm) add: has_trace_def)
    6.16 +  apply safe
    6.17 +  apply (rename_tac ex1 ex2)
    6.18 +
    6.19 +  (* choose same trace, therefore same NF *)
    6.20 +  apply (rule_tac x = "mk_trace C ex1" in exI)
    6.21 +  apply simp
    6.22 +
    6.23 +  (* give execution of abstract automata *)
    6.24 +  apply (rule_tac x = "(mk_trace A ex1,%i. f (ex2 i))" in bexI)
    6.25 +
    6.26 +  (* Traces coincide *)
    6.27 +   apply (simp (no_asm_simp) add: mk_trace_def filter_oseq_idemp)
    6.28 +
    6.29 +  (* Use lemma *)
    6.30 +  apply (frule states_of_exec_reachable)
    6.31 +
    6.32 +  (* Now show that it's an execution *)
    6.33 +  apply (simp add: executions_def)
    6.34 +  apply safe
    6.35 +
    6.36 +  (* Start states map to start states *)
    6.37 +  apply (drule bspec)
    6.38 +  apply assumption
    6.39 +
    6.40 +  (* Show that it's an execution fragment *)
    6.41 +  apply (simp add: is_execution_fragment_def)
    6.42 +  apply safe
    6.43 +
    6.44 +  apply (erule_tac x = "ex2 n" in allE)
    6.45 +  apply (erule_tac x = "ex2 (Suc n)" in allE)
    6.46 +  apply (erule_tac x = a in allE)
    6.47 +  apply simp
    6.48 +  done
    6.49 +
    6.50 +(* Lemmata *)
    6.51 +
    6.52 +lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R"
    6.53 +  by blast
    6.54 +
    6.55 +
    6.56 +(* fist_order_tautology of externals_of_par *)
    6.57 +lemma externals_of_par_extra:
    6.58 +  "a:externals(asig_of(A1||A2)) =     
    6.59 +   (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) |   
    6.60 +   a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |   
    6.61 +   a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))"
    6.62 +  apply (auto simp add: externals_def asig_of_par asig_comp_def asig_inputs_def asig_outputs_def)
    6.63 +  done
    6.64 +
    6.65 +lemma comp1_reachable: "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)"
    6.66 +  apply (simp add: reachable_def)
    6.67 +  apply (erule bexE)
    6.68 +  apply (rule_tac x =
    6.69 +    "(filter_oseq (%a. a:actions (asig_of (C1))) (fst ex) , %i. fst (snd ex i))" in bexI)
    6.70 +(* fst(s) is in projected execution *)
    6.71 +  apply force
    6.72 +(* projected execution is indeed an execution *)
    6.73 +  apply (simp cong del: if_weak_cong
    6.74 +    add: executions_def is_execution_fragment_def par_def starts_of_def
    6.75 +      trans_of_def filter_oseq_def
    6.76 +    split add: option.split)
    6.77 +  done
    6.78 +
    6.79 +
    6.80 +(* Exact copy of proof of comp1_reachable for the second
    6.81 +   component of a parallel composition.     *)
    6.82 +lemma comp2_reachable: "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)"
    6.83 +  apply (simp add: reachable_def)
    6.84 +  apply (erule bexE)
    6.85 +  apply (rule_tac x =
    6.86 +    "(filter_oseq (%a. a:actions (asig_of (C2))) (fst ex) , %i. snd (snd ex i))" in bexI)
    6.87 +(* fst(s) is in projected execution *)
    6.88 +  apply force
    6.89 +(* projected execution is indeed an execution *)
    6.90 +  apply (simp cong del: if_weak_cong
    6.91 +    add: executions_def is_execution_fragment_def par_def starts_of_def
    6.92 +    trans_of_def filter_oseq_def
    6.93 +    split add: option.split)
    6.94 +  done
    6.95 +
    6.96 +declare split_if [split del] if_weak_cong [cong del]
    6.97 +
    6.98 +(*Composition of possibility-mappings *)
    6.99 +lemma fxg_is_weak_pmap_of_product_IOA: 
   6.100 +     "[| is_weak_pmap f C1 A1;  
   6.101 +         externals(asig_of(A1))=externals(asig_of(C1)); 
   6.102 +         is_weak_pmap g C2 A2;   
   6.103 +         externals(asig_of(A2))=externals(asig_of(C2));  
   6.104 +         compat_ioas C1 C2; compat_ioas A1 A2  |]      
   6.105 +   ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)"
   6.106 +  apply (unfold is_weak_pmap_def)
   6.107 +  apply (rule conjI)
   6.108 +(* start_states *)
   6.109 +  apply (simp add: par_def starts_of_def)
   6.110 +(* transitions *)
   6.111 +  apply (rule allI)+
   6.112 +  apply (rule imp_conj_lemma)
   6.113 +  apply (simp (no_asm) add: externals_of_par_extra)
   6.114 +  apply (simp (no_asm) add: par_def)
   6.115 +  apply (simp add: trans_of_def)
   6.116 +  apply (simplesubst split_if)
   6.117 +  apply (rule conjI)
   6.118 +  apply (rule impI)
   6.119 +  apply (erule disjE)
   6.120 +(* case 1      a:e(A1) | a:e(A2) *)
   6.121 +  apply (simp add: comp1_reachable comp2_reachable ext_is_act)
   6.122 +  apply (erule disjE)
   6.123 +(* case 2      a:e(A1) | a~:e(A2) *)
   6.124 +  apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act2)
   6.125 +(* case 3      a:~e(A1) | a:e(A2) *)
   6.126 +  apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act1)
   6.127 +(* case 4      a:~e(A1) | a~:e(A2) *)
   6.128 +  apply (rule impI)
   6.129 +  apply (subgoal_tac "a~:externals (asig_of (A1)) & a~:externals (asig_of (A2))")
   6.130 +(* delete auxiliary subgoal *)
   6.131 +  prefer 2
   6.132 +  apply force
   6.133 +  apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
   6.134 +  apply (tactic {*
   6.135 +    REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
   6.136 +      asm_full_simp_tac(simpset() addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *})
   6.137 +  done
   6.138 +
   6.139 +
   6.140 +lemma reachable_rename_ioa: "[| reachable (rename C g) s |] ==> reachable C s"
   6.141 +  apply (simp add: reachable_def)
   6.142 +  apply (erule bexE)
   6.143 +  apply (rule_tac x = "((%i. case (fst ex i) of None => None | Some (x) => g x) ,snd ex)" in bexI)
   6.144 +  apply (simp (no_asm))
   6.145 +(* execution is indeed an execution of C *)
   6.146 +  apply (simp add: executions_def is_execution_fragment_def par_def
   6.147 +    starts_of_def trans_of_def rename_def split add: option.split)
   6.148 +  apply force
   6.149 +  done
   6.150 +
   6.151 +
   6.152 +lemma rename_through_pmap: "[| is_weak_pmap f C A |] 
   6.153 +                       ==> (is_weak_pmap f (rename C g) (rename A g))"
   6.154 +  apply (simp add: is_weak_pmap_def)
   6.155 +  apply (rule conjI)
   6.156 +  apply (simp add: rename_def starts_of_def)
   6.157 +  apply (rule allI)+
   6.158 +  apply (rule imp_conj_lemma)
   6.159 +  apply (simp (no_asm) add: rename_def)
   6.160 +  apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
   6.161 +  apply safe
   6.162 +  apply (simplesubst split_if)
   6.163 +  apply (rule conjI)
   6.164 +  apply (rule impI)
   6.165 +  apply (erule disjE)
   6.166 +  apply (erule exE)
   6.167 +  apply (erule conjE)
   6.168 +(* x is input *)
   6.169 +  apply (drule sym)
   6.170 +  apply (drule sym)
   6.171 +  apply simp
   6.172 +  apply hypsubst+
   6.173 +  apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
   6.174 +  apply assumption
   6.175 +  apply simp
   6.176 +(* x is output *)
   6.177 +  apply (erule exE)
   6.178 +  apply (erule conjE)
   6.179 +  apply (drule sym)
   6.180 +  apply (drule sym)
   6.181 +  apply simp
   6.182 +  apply hypsubst+
   6.183 +  apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
   6.184 +  apply assumption
   6.185 +  apply simp
   6.186 +(* x is internal *)
   6.187 +  apply (simp (no_asm) add: de_Morgan_disj de_Morgan_conj not_ex cong add: conj_cong)
   6.188 +  apply (rule impI)
   6.189 +  apply (erule conjE)
   6.190 +  apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
   6.191 +  apply auto
   6.192 +  done
   6.193 +
   6.194 +declare split_if [split] if_weak_cong [cong]
   6.195  
   6.196  end
     7.1 --- a/src/HOL/IsaMakefile	Tue Jun 06 20:47:12 2006 +0200
     7.2 +++ b/src/HOL/IsaMakefile	Wed Jun 07 00:57:14 2006 +0200
     7.3 @@ -599,8 +599,8 @@
     7.4  
     7.5  HOL-IOA: HOL $(LOG)/HOL-IOA.gz
     7.6  
     7.7 -$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.ML IOA/Asig.thy IOA/IOA.ML \
     7.8 -  IOA/IOA.thy IOA/ROOT.ML IOA/Solve.ML IOA/Solve.thy
     7.9 +$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy \
    7.10 +  IOA/ROOT.ML IOA/Solve.thy
    7.11  	@$(ISATOOL) usedir $(OUT)/HOL IOA
    7.12  
    7.13