converted to Isar theory format;
authorwenzelm
Tue Sep 06 19:03:39 2005 +0200 (2005-09-06)
changeset 17288aa3833fb7bee
parent 17287 bd49e10bbd24
child 17289 8608f7a881eb
converted to Isar theory format;
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
     1.1 --- a/src/HOL/IOA/Asig.ML	Tue Sep 06 18:49:25 2005 +0200
     1.2 +++ b/src/HOL/IOA/Asig.ML	Tue Sep 06 19:03:39 2005 +0200
     1.3 @@ -2,13 +2,9 @@
     1.4      ID:         $Id$
     1.5      Author:     Tobias Nipkow & Konrad Slind
     1.6      Copyright   1994  TU Muenchen
     1.7 -
     1.8 -Action signatures
     1.9  *)
    1.10  
    1.11 -open Asig;
    1.12 -
    1.13 -val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
    1.14 +bind_thms ("asig_projections", [asig_inputs_def, asig_outputs_def, asig_internals_def]);
    1.15  
    1.16  Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
    1.17  by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
     2.1 --- a/src/HOL/IOA/Asig.thy	Tue Sep 06 18:49:25 2005 +0200
     2.2 +++ b/src/HOL/IOA/Asig.thy	Tue Sep 06 19:03:39 2005 +0200
     2.3 @@ -2,44 +2,50 @@
     2.4      ID:         $Id$
     2.5      Author:     Tobias Nipkow & Konrad Slind
     2.6      Copyright   1994  TU Muenchen
     2.7 -
     2.8 -Action signatures
     2.9  *)
    2.10  
    2.11 -Asig = Main +
    2.12 +header {* Action signatures *}
    2.13  
    2.14 -types 
    2.15 +theory Asig
    2.16 +imports Main
    2.17 +begin
    2.18  
    2.19 -'a signature = "('a set * 'a set * 'a set)"
    2.20 +types
    2.21 +  'a signature = "('a set * 'a set * 'a set)"
    2.22  
    2.23  consts
    2.24 -  actions,inputs,outputs,internals,externals
    2.25 -                ::"'action signature => 'action set"
    2.26 +  "actions" :: "'action signature => 'action set"
    2.27 +  "inputs" :: "'action signature => 'action set"
    2.28 +  "outputs" :: "'action signature => 'action set"
    2.29 +  "internals" :: "'action signature => 'action set"
    2.30 +  externals :: "'action signature => 'action set"
    2.31 +
    2.32    is_asig       ::"'action signature => bool"
    2.33    mk_ext_asig   ::"'action signature => 'action signature"
    2.34  
    2.35  
    2.36  defs
    2.37  
    2.38 -asig_inputs_def    "inputs == fst"
    2.39 -asig_outputs_def   "outputs == (fst o snd)"
    2.40 -asig_internals_def "internals == (snd o snd)"
    2.41 +asig_inputs_def:    "inputs == fst"
    2.42 +asig_outputs_def:   "outputs == (fst o snd)"
    2.43 +asig_internals_def: "internals == (snd o snd)"
    2.44  
    2.45 -actions_def
    2.46 +actions_def:
    2.47     "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
    2.48  
    2.49 -externals_def
    2.50 +externals_def:
    2.51     "externals(asig) == (inputs(asig) Un outputs(asig))"
    2.52  
    2.53 -is_asig_def
    2.54 -  "is_asig(triple) ==            
    2.55 -      ((inputs(triple) Int outputs(triple) = {})    & 
    2.56 -       (outputs(triple) Int internals(triple) = {}) & 
    2.57 +is_asig_def:
    2.58 +  "is_asig(triple) ==
    2.59 +      ((inputs(triple) Int outputs(triple) = {})    &
    2.60 +       (outputs(triple) Int internals(triple) = {}) &
    2.61         (inputs(triple) Int internals(triple) = {}))"
    2.62  
    2.63  
    2.64 -mk_ext_asig_def
    2.65 +mk_ext_asig_def:
    2.66    "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
    2.67  
    2.68 +ML {* use_legacy_bindings (the_context ()) *}
    2.69  
    2.70 -end 
    2.71 +end
     3.1 --- a/src/HOL/IOA/IOA.ML	Tue Sep 06 18:49:25 2005 +0200
     3.2 +++ b/src/HOL/IOA/IOA.ML	Tue Sep 06 19:03:39 2005 +0200
     3.3 @@ -2,15 +2,13 @@
     3.4      ID:         $Id$
     3.5      Author:     Tobias Nipkow & Konrad Slind
     3.6      Copyright   1994  TU Muenchen
     3.7 -
     3.8 -The I/O automata of Lynch and Tuttle.
     3.9  *)
    3.10  
    3.11  Addsimps [Let_def];
    3.12  
    3.13 -val ioa_projections = [asig_of_def, starts_of_def, trans_of_def];
    3.14 +bind_thms ("ioa_projections", [asig_of_def, starts_of_def, trans_of_def]);
    3.15  
    3.16 -val exec_rws = [executions_def,is_execution_fragment_def];
    3.17 +bind_thms ("exec_rws", [executions_def,is_execution_fragment_def]);
    3.18  
    3.19  Goal
    3.20  "asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z";
    3.21 @@ -67,7 +65,7 @@
    3.22    by Auto_tac;
    3.23  qed "reachable_n";
    3.24  
    3.25 -val [p1,p2] = goalw IOA.thy [invariant_def]
    3.26 +val [p1,p2] = goalw (the_context ()) [invariant_def]
    3.27    "[| !!s. s:starts_of(A) ==> P(s);                                          \
    3.28  \     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
    3.29  \  ==> invariant A P";
    3.30 @@ -85,19 +83,19 @@
    3.31      by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
    3.32  qed "invariantI";
    3.33  
    3.34 -val [p1,p2] = goal IOA.thy
    3.35 +val [p1,p2] = goal (the_context ())
    3.36   "[| !!s. s : starts_of(A) ==> P(s); \
    3.37  \    !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
    3.38  \ |] ==> invariant A P";
    3.39    by (fast_tac (claset() addSIs [invariantI] addSDs [p1,p2]) 1);
    3.40  qed "invariantI1";
    3.41  
    3.42 -val [p1,p2] = goalw IOA.thy [invariant_def]
    3.43 +val [p1,p2] = goalw (the_context ()) [invariant_def]
    3.44  "[| invariant A P; reachable A s |] ==> P(s)";
    3.45     by (rtac (p2 RS (p1 RS spec RS mp)) 1);
    3.46  qed "invariantE";
    3.47  
    3.48 -Goal 
    3.49 +Goal
    3.50  "actions(asig_comp a b) = actions(a) Un actions(b)";
    3.51    by (simp_tac (simpset() addsimps
    3.52                 ([actions_def,asig_comp_def]@asig_projections)) 1);
    3.53 @@ -110,13 +108,13 @@
    3.54  qed "starts_of_par";
    3.55  
    3.56  (* Every state in an execution is reachable *)
    3.57 -Goalw [reachable_def] 
    3.58 +Goalw [reachable_def]
    3.59  "ex:executions(A) ==> !n. reachable A (snd ex n)";
    3.60    by (Fast_tac 1);
    3.61  qed "states_of_exec_reachable";
    3.62  
    3.63  
    3.64 -Goal 
    3.65 +Goal
    3.66  "(s,a,t) : trans_of(A || B || C || D) =                                      \
    3.67  \ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |  \
    3.68  \   a:actions(asig_of(D))) &                                                 \
    3.69 @@ -150,9 +148,9 @@
    3.70  Goal "externals(asig_of(A1||A2)) =    \
    3.71  \  (externals(asig_of(A1)) Un externals(asig_of(A2)))";
    3.72  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.73 -by (rtac set_ext 1); 
    3.74 +by (rtac set_ext 1);
    3.75  by (Fast_tac 1);
    3.76 -qed"externals_of_par"; 
    3.77 +qed"externals_of_par";
    3.78  
    3.79  Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
    3.80   "[| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
    3.81 @@ -168,4 +166,3 @@
    3.82  
    3.83  val ext1_ext2_is_not_act2 = ext1_is_not_int2 RS int_and_ext_is_act;
    3.84  val ext1_ext2_is_not_act1 = ext2_is_not_int1 RS int_and_ext_is_act;
    3.85 -
     4.1 --- a/src/HOL/IOA/IOA.thy	Tue Sep 06 18:49:25 2005 +0200
     4.2 +++ b/src/HOL/IOA/IOA.thy	Tue Sep 06 19:03:39 2005 +0200
     4.3 @@ -2,11 +2,13 @@
     4.4      ID:         $Id$
     4.5      Author:     Tobias Nipkow & Konrad Slind
     4.6      Copyright   1994  TU Muenchen
     4.7 -
     4.8 -The I/O automata of Lynch and Tuttle.
     4.9  *)
    4.10  
    4.11 -IOA = Asig + 
    4.12 +header {* The I/O automata of Lynch and Tuttle *}
    4.13 +
    4.14 +theory IOA
    4.15 +imports Asig
    4.16 +begin
    4.17  
    4.18  types
    4.19     'a seq            =   "nat => 'a"
    4.20 @@ -26,7 +28,7 @@
    4.21  
    4.22    (* Executions, schedules, and traces *)
    4.23  
    4.24 -  is_execution_fragment,
    4.25 +  is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool"
    4.26    has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
    4.27    executions    :: "('action,'state)ioa => ('action,'state)execution set"
    4.28    mk_trace  :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
    4.29 @@ -46,7 +48,7 @@
    4.30    compat_asigs ::"['action signature, 'action signature] => bool"
    4.31    asig_comp    ::"['action signature, 'action signature] => 'action signature"
    4.32    compat_ioas  ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
    4.33 -  "||"         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr 10)
    4.34 +  par         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
    4.35  
    4.36    (* Filtering and hiding *)
    4.37    filter_oseq  :: "('a => bool) => 'a oseq => 'a oseq"
    4.38 @@ -62,19 +64,19 @@
    4.39  
    4.40  defs
    4.41  
    4.42 -state_trans_def
    4.43 -  "state_trans asig R == 
    4.44 -     (!triple. triple:R --> fst(snd(triple)):actions(asig)) & 
    4.45 +state_trans_def:
    4.46 +  "state_trans asig R ==
    4.47 +     (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
    4.48       (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
    4.49  
    4.50  
    4.51 -asig_of_def   "asig_of == fst"
    4.52 -starts_of_def "starts_of == (fst o snd)"
    4.53 -trans_of_def  "trans_of == (snd o snd)"
    4.54 +asig_of_def:   "asig_of == fst"
    4.55 +starts_of_def: "starts_of == (fst o snd)"
    4.56 +trans_of_def:  "trans_of == (snd o snd)"
    4.57  
    4.58 -ioa_def
    4.59 -  "IOA(ioa) == (is_asig(asig_of(ioa))      &                            
    4.60 -                (~ starts_of(ioa) = {})    &                            
    4.61 +ioa_def:
    4.62 +  "IOA(ioa) == (is_asig(asig_of(ioa))      &
    4.63 +                (~ starts_of(ioa) = {})    &
    4.64                  state_trans (asig_of ioa) (trans_of ioa))"
    4.65  
    4.66  
    4.67 @@ -82,115 +84,117 @@
    4.68   * the first is the action options, the second the state sequence.
    4.69   * Finite executions have None actions from some point on.
    4.70   *******)
    4.71 -is_execution_fragment_def
    4.72 -  "is_execution_fragment A ex ==                                        
    4.73 -     let act = fst(ex); state = snd(ex)                                 
    4.74 -     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &              
    4.75 +is_execution_fragment_def:
    4.76 +  "is_execution_fragment A ex ==
    4.77 +     let act = fst(ex); state = snd(ex)
    4.78 +     in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
    4.79                (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
    4.80  
    4.81  
    4.82 -executions_def
    4.83 -  "executions(ioa) == {e. snd e 0:starts_of(ioa) &                      
    4.84 +executions_def:
    4.85 +  "executions(ioa) == {e. snd e 0:starts_of(ioa) &
    4.86                          is_execution_fragment ioa e}"
    4.87  
    4.88 -  
    4.89 -reachable_def
    4.90 +
    4.91 +reachable_def:
    4.92    "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
    4.93  
    4.94  
    4.95 -invariant_def "invariant A P == (!s. reachable A s --> P(s))"
    4.96 +invariant_def: "invariant A P == (!s. reachable A s --> P(s))"
    4.97  
    4.98  
    4.99  (* Restrict the trace to those members of the set s *)
   4.100 -filter_oseq_def
   4.101 -  "filter_oseq p s ==                                                   
   4.102 -   (%i. case s(i)                                                       
   4.103 -         of None => None                                               
   4.104 +filter_oseq_def:
   4.105 +  "filter_oseq p s ==
   4.106 +   (%i. case s(i)
   4.107 +         of None => None
   4.108            | Some(x) => if p x then Some x else None)"
   4.109  
   4.110  
   4.111 -mk_trace_def
   4.112 +mk_trace_def:
   4.113    "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
   4.114  
   4.115  
   4.116  (* Does an ioa have an execution with the given trace *)
   4.117 -has_trace_def
   4.118 -  "has_trace ioa b ==                                               
   4.119 +has_trace_def:
   4.120 +  "has_trace ioa b ==
   4.121       (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
   4.122  
   4.123 -normal_form_def
   4.124 -  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &   
   4.125 -                    (!j. j ~: range(f) --> nf(j)= None) &   
   4.126 +normal_form_def:
   4.127 +  "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
   4.128 +                    (!j. j ~: range(f) --> nf(j)= None) &
   4.129                      (!i. nf(i)=None --> (nf (Suc i)) = None)   "
   4.130 -  
   4.131 +
   4.132  (* All the traces of an ioa *)
   4.133  
   4.134 -  traces_def
   4.135 +  traces_def:
   4.136    "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
   4.137  
   4.138  (*
   4.139 -  traces_def
   4.140 +  traces_def:
   4.141    "traces(ioa) == {tr. has_trace ioa tr}"
   4.142  *)
   4.143 -  
   4.144 -compat_asigs_def
   4.145 -  "compat_asigs a1 a2 ==                                                
   4.146 -   (((outputs(a1) Int outputs(a2)) = {}) &                              
   4.147 -    ((internals(a1) Int actions(a2)) = {}) &                            
   4.148 +
   4.149 +compat_asigs_def:
   4.150 +  "compat_asigs a1 a2 ==
   4.151 +   (((outputs(a1) Int outputs(a2)) = {}) &
   4.152 +    ((internals(a1) Int actions(a2)) = {}) &
   4.153      ((internals(a2) Int actions(a1)) = {}))"
   4.154  
   4.155  
   4.156 -compat_ioas_def
   4.157 +compat_ioas_def:
   4.158    "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
   4.159  
   4.160  
   4.161 -asig_comp_def
   4.162 -  "asig_comp a1 a2 ==                                                   
   4.163 -      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),      
   4.164 -        (outputs(a1) Un outputs(a2)),                                   
   4.165 +asig_comp_def:
   4.166 +  "asig_comp a1 a2 ==
   4.167 +      (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
   4.168 +        (outputs(a1) Un outputs(a2)),
   4.169          (internals(a1) Un internals(a2))))"
   4.170  
   4.171  
   4.172 -par_def
   4.173 -  "(ioa1 || ioa2) ==                                                    
   4.174 -       (asig_comp (asig_of ioa1) (asig_of ioa2),                        
   4.175 -        {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},        
   4.176 -        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))        
   4.177 -             in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & 
   4.178 -                (if a:actions(asig_of(ioa1)) then                       
   4.179 -                   (fst(s),a,fst(t)):trans_of(ioa1)                     
   4.180 -                 else fst(t) = fst(s))                                  
   4.181 -                &                                                       
   4.182 -                (if a:actions(asig_of(ioa2)) then                       
   4.183 -                   (snd(s),a,snd(t)):trans_of(ioa2)                     
   4.184 +par_def:
   4.185 +  "(ioa1 || ioa2) ==
   4.186 +       (asig_comp (asig_of ioa1) (asig_of ioa2),
   4.187 +        {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
   4.188 +        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
   4.189 +             in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
   4.190 +                (if a:actions(asig_of(ioa1)) then
   4.191 +                   (fst(s),a,fst(t)):trans_of(ioa1)
   4.192 +                 else fst(t) = fst(s))
   4.193 +                &
   4.194 +                (if a:actions(asig_of(ioa2)) then
   4.195 +                   (snd(s),a,snd(t)):trans_of(ioa2)
   4.196                   else snd(t) = snd(s))})"
   4.197  
   4.198  
   4.199 -restrict_asig_def
   4.200 -  "restrict_asig asig actns ==                                          
   4.201 -    (inputs(asig) Int actns, outputs(asig) Int actns,                  
   4.202 +restrict_asig_def:
   4.203 +  "restrict_asig asig actns ==
   4.204 +    (inputs(asig) Int actns, outputs(asig) Int actns,
   4.205       internals(asig) Un (externals(asig) - actns))"
   4.206  
   4.207  
   4.208 -restrict_def
   4.209 -  "restrict ioa actns ==                                               
   4.210 +restrict_def:
   4.211 +  "restrict ioa actns ==
   4.212      (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
   4.213  
   4.214  
   4.215 -ioa_implements_def
   4.216 -  "ioa_implements ioa1 ioa2 ==   
   4.217 -  ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &   
   4.218 -     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &   
   4.219 +ioa_implements_def:
   4.220 +  "ioa_implements ioa1 ioa2 ==
   4.221 +  ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
   4.222 +     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &
   4.223        traces(ioa1) <= traces(ioa2))"
   4.224 - 
   4.225 -rename_def 
   4.226 -"rename ioa ren ==  
   4.227 -  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},         
   4.228 -    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},        
   4.229 -    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),     
   4.230 -              starts_of(ioa)   ,                                            
   4.231 -   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))    
   4.232 -        in                                                      
   4.233 +
   4.234 +rename_def:
   4.235 +"rename ioa ren ==
   4.236 +  (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
   4.237 +    {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
   4.238 +    {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
   4.239 +              starts_of(ioa)   ,
   4.240 +   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
   4.241 +        in
   4.242          ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
   4.243  
   4.244 -end 
   4.245 +ML {* use_legacy_bindings (the_context ()) *}
   4.246 +
   4.247 +end
     5.1 --- a/src/HOL/IOA/Solve.ML	Tue Sep 06 18:49:25 2005 +0200
     5.2 +++ b/src/HOL/IOA/Solve.ML	Tue Sep 06 19:03:39 2005 +0200
     5.3 @@ -2,12 +2,8 @@
     5.4      ID:         $Id$
     5.5      Author:     Tobias Nipkow & Konrad Slind
     5.6      Copyright   1994  TU Muenchen
     5.7 -
     5.8 -Weak possibilities mapping (abstraction)
     5.9  *)
    5.10  
    5.11 -open Solve; 
    5.12 -
    5.13  Addsimps [mk_trace_thm,trans_in_actions];
    5.14  
    5.15  Goalw [is_weak_pmap_def,traces_def]
    5.16 @@ -57,16 +53,16 @@
    5.17  
    5.18  
    5.19  (* fist_order_tautology of externals_of_par *)
    5.20 -goal IOA.thy "a:externals(asig_of(A1||A2)) =    \
    5.21 +goal (theory "IOA") "a:externals(asig_of(A1||A2)) =    \
    5.22  \  (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) |  \
    5.23  \  a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |  \
    5.24  \  a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))";
    5.25  by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1);
    5.26   by (Fast_tac 1);
    5.27 -val externals_of_par_extra = result(); 
    5.28 +val externals_of_par_extra = result();
    5.29  
    5.30  Goal "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
    5.31 -by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    5.32 +by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
    5.33  by (etac bexE 1);
    5.34  by (res_inst_tac [("x",
    5.35     "(filter_oseq (%a. a:actions(asig_of(C1))) \
    5.36 @@ -77,16 +73,16 @@
    5.37  (* projected execution is indeed an execution *)
    5.38  by (asm_full_simp_tac
    5.39        (simpset() delcongs [if_weak_cong]
    5.40 -		 addsimps [executions_def,is_execution_fragment_def,
    5.41 -			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
    5.42 +                 addsimps [executions_def,is_execution_fragment_def,
    5.43 +                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
    5.44                   addsplits [option.split]) 1);
    5.45  qed"comp1_reachable";
    5.46  
    5.47  
    5.48 -(* Exact copy of proof of comp1_reachable for the second 
    5.49 +(* Exact copy of proof of comp1_reachable for the second
    5.50     component of a parallel composition.     *)
    5.51  Goal "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
    5.52 -by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    5.53 +by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
    5.54  by (etac bexE 1);
    5.55  by (res_inst_tac [("x",
    5.56     "(filter_oseq (%a. a:actions(asig_of(C2)))\
    5.57 @@ -97,8 +93,8 @@
    5.58  (* projected execution is indeed an execution *)
    5.59  by (asm_full_simp_tac
    5.60        (simpset() delcongs [if_weak_cong]
    5.61 -		 addsimps [executions_def,is_execution_fragment_def,
    5.62 -			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
    5.63 +                 addsimps [executions_def,is_execution_fragment_def,
    5.64 +                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
    5.65                   addsplits [option.split]) 1);
    5.66  qed"comp2_reachable";
    5.67  
    5.68 @@ -124,7 +120,7 @@
    5.69  by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
    5.70  by (stac split_if 1);
    5.71  by (rtac conjI 1);
    5.72 -by (rtac impI 1); 
    5.73 +by (rtac impI 1);
    5.74  by (etac disjE 1);
    5.75  (* case 1      a:e(A1) | a:e(A2) *)
    5.76  by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
    5.77 @@ -145,13 +141,13 @@
    5.78  by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
    5.79                   addsplits [split_if]) 1);
    5.80  by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
    5.81 -	   asm_full_simp_tac(simpset() addsimps[comp1_reachable,
    5.82 -						comp2_reachable])1));
    5.83 +           asm_full_simp_tac(simpset() addsimps[comp1_reachable,
    5.84 +                                                comp2_reachable])1));
    5.85  qed"fxg_is_weak_pmap_of_product_IOA";
    5.86  
    5.87  
    5.88  Goal "[| reachable (rename C g) s |] ==> reachable C s";
    5.89 -by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    5.90 +by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
    5.91  by (etac bexE 1);
    5.92  by (res_inst_tac [("x",
    5.93     "((%i. case (fst ex i) \
    5.94 @@ -202,8 +198,8 @@
    5.95  by (assume_tac 1);
    5.96  by (Asm_full_simp_tac 1);
    5.97  (* x is internal *)
    5.98 -by (simp_tac (simpset() addsimps [de_Morgan_disj, de_Morgan_conj, not_ex] 
    5.99 -	               addcongs [conj_cong]) 1);
   5.100 +by (simp_tac (simpset() addsimps [de_Morgan_disj, de_Morgan_conj, not_ex]
   5.101 +                       addcongs [conj_cong]) 1);
   5.102  by (rtac impI 1);
   5.103  by (etac conjE 1);
   5.104  by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
     6.1 --- a/src/HOL/IOA/Solve.thy	Tue Sep 06 18:49:25 2005 +0200
     6.2 +++ b/src/HOL/IOA/Solve.thy	Tue Sep 06 19:03:39 2005 +0200
     6.3 @@ -2,21 +2,25 @@
     6.4      ID:         $Id$
     6.5      Author:     Tobias Nipkow & Konrad Slind
     6.6      Copyright   1994  TU Muenchen
     6.7 -
     6.8 -Weak possibilities mapping (abstraction)
     6.9  *)
    6.10  
    6.11 -Solve = IOA +
    6.12 +header {* Weak possibilities mapping (abstraction) *}
    6.13 +
    6.14 +theory Solve
    6.15 +imports IOA
    6.16 +begin
    6.17  
    6.18  constdefs
    6.19  
    6.20    is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
    6.21 -  "is_weak_pmap f C A ==                          
    6.22 -   (!s:starts_of(C). f(s):starts_of(A)) &        
    6.23 -   (!s t a. reachable C s &                      
    6.24 -            (s,a,t):trans_of(C)                  
    6.25 -            --> (if a:externals(asig_of(C)) then 
    6.26 -                   (f(s),a,f(t)):trans_of(A)     
    6.27 +  "is_weak_pmap f C A ==
    6.28 +   (!s:starts_of(C). f(s):starts_of(A)) &
    6.29 +   (!s t a. reachable C s &
    6.30 +            (s,a,t):trans_of(C)
    6.31 +            --> (if a:externals(asig_of(C)) then
    6.32 +                   (f(s),a,f(t)):trans_of(A)
    6.33                   else f(s)=f(t)))"
    6.34  
    6.35 +ML {* use_legacy_bindings (the_context ()) *}
    6.36 +
    6.37  end