src/HOLCF/IOA/meta_theory/CompoTraces.ML

 \      (case x of  \ 
 \        Undef => UU  \
 \      | Def y => \
 \         (if y:act A then \
 \             (if y:act B then \ 
-\                   ((Takewhile (%a.a:int A)`schA) \
-\                         @@(Takewhile (%a.a:int B)`schB) \
+\                   ((Takewhile (%a. a:int A)`schA) \
+\                         @@(Takewhile (%a. a:int B)`schB) \
 \                              @@(y>>(mksch A B`xs   \
-\                                       `(TL`(Dropwhile (%a.a:int A)`schA))  \
-\                                       `(TL`(Dropwhile (%a.a:int B)`schB))  \
+\                                       `(TL`(Dropwhile (%a. a:int A)`schA))  \
+\                                       `(TL`(Dropwhile (%a. a:int B)`schB))  \
 \                    )))   \
 \              else  \
-\                 ((Takewhile (%a.a:int A)`schA)  \
+\                 ((Takewhile (%a. a:int A)`schA)  \
 \                      @@ (y>>(mksch A B`xs  \
-\                              `(TL`(Dropwhile (%a.a:int A)`schA))  \
+\                              `(TL`(Dropwhile (%a. a:int A)`schA))  \
 \                              `schB)))  \
 \              )   \
 \          else    \
 \             (if y:act B then  \ 
-\                 ((Takewhile (%a.a:int B)`schB)  \
+\                 ((Takewhile (%a. a:int B)`schB)  \
 \                       @@ (y>>(mksch A B`xs   \
 \                              `schA   \
-\                              `(TL`(Dropwhile (%a.a:int B)`schB))  \
+\                              `(TL`(Dropwhile (%a. a:int B)`schB))  \
 \                              )))  \
 \             else  \
 \               UU  \
 \             )  \
 \         )  \

 by (Simp_tac 1);
 qed"mksch_nil";
 
 goal thy "!!x.[|x:act A;x~:act B|]  \
 \   ==> mksch A B`(x>>tr)`schA`schB = \
-\         (Takewhile (%a.a:int A)`schA) \
-\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
+\         (Takewhile (%a. a:int A)`schA) \
+\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
 \                             `schB))";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
 by (simp_tac (!simpset addsimps [Cons_def]) 1);
 qed"mksch_cons1";
 
 goal thy "!!x.[|x~:act A;x:act B|] \
 \   ==> mksch A B`(x>>tr)`schA`schB = \
-\        (Takewhile (%a.a:int B)`schB)  \
-\         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a.a:int B)`schB))  \
+\        (Takewhile (%a. a:int B)`schB)  \
+\         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a. a:int B)`schB))  \
 \                            ))";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
 by (simp_tac (!simpset addsimps [Cons_def]) 1);
 qed"mksch_cons2";
 
 goal thy "!!x.[|x:act A;x:act B|] \
 \   ==> mksch A B`(x>>tr)`schA`schB = \
-\            (Takewhile (%a.a:int A)`schA) \
-\         @@ ((Takewhile (%a.a:int B)`schB)  \
-\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
-\                            `(TL`(Dropwhile (%a.a:int B)`schB))))  \
+\            (Takewhile (%a. a:int A)`schA) \
+\         @@ ((Takewhile (%a. a:int B)`schB)  \
+\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
+\                            `(TL`(Dropwhile (%a. a:int B)`schB))))  \
 \             )";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
 by (simp_tac (!simpset addsimps [Cons_def]) 1);

 
 (* safe-tac makes too many case distinctions with this lemma in the next proof *)
 Delsimps [FiniteConc];
 
 goal thy "!! tr. [| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\   ! x y. Forall (%x.x:act A) x & Forall (%x.x:act B) y & \
+\   ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \
 \          Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
 \          Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
 \          Forall (%x. x:ext (A||B)) tr \
 \          --> Finite (mksch A B`tr`x`y)";
 

 
 (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
 Delsimps [FilterConc]; 
 
 goal thy " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
-\! y.Forall (%x.x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
+\! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
 \    Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
 \    --> (? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
 \                   Forall (%x. x:act B & x~:act A) y1 & \
 \                   Finite y1 & y = (y1 @@ y2) & \
 \                   Filter (%a. a:ext B)`y1 = bs)";

                    ("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
 by (assume_tac 1);
 Addsimps [FilterConc]; 
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
 (* apply IH *)
-by (eres_inst_tac [("x","TL`(Dropwhile (%a.a:int B)`y)")] allE 1);
+by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int B)`y)")] allE 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
 by (Asm_full_simp_tac 1); 
 (* for replacing IH in conclusion *)
 by (rotate_tac ~2 1); 
 by (Asm_full_simp_tac 1); 
 (* instantiate y1a and y2a *)
-by (res_inst_tac [("x","Takewhile (%a.a:int B)`y @@ a>>y1")] exI 1);
+by (res_inst_tac [("x","Takewhile (%a. a:int B)`y @@ a>>y1")] exI 1);
 by (res_inst_tac [("x","y2")] exI 1);
 (* elminate all obligations up to two depending on Conc_assoc *)
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
              int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1); 
 by (simp_tac (!simpset addsimps [Conc_assoc]) 1); 

 (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
 Delsimps [FilterConc]; 
 
 
 goal thy " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
-\! x.Forall (%x.x:act A) x & Forall (%x. x:act A & x~:act B) as &\
+\! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
 \    Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
 \    --> (? x1 x2.  (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
 \                   Forall (%x. x:act A & x~:act B) x1 & \
 \                   Finite x1 & x = (x1 @@ x2) & \
 \                   Filter (%a. a:ext A)`x1 = as)";

                    ("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
 by (assume_tac 1);
 Addsimps [FilterConc]; 
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
 (* apply IH *)
-by (eres_inst_tac [("x","TL`(Dropwhile (%a.a:int A)`x)")] allE 1);
+by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int A)`x)")] allE 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
 by (Asm_full_simp_tac 1); 
 (* for replacing IH in conclusion *)
 by (rotate_tac ~2 1); 
 by (Asm_full_simp_tac 1); 
 (* instantiate y1a and y2a *)
-by (res_inst_tac [("x","Takewhile (%a.a:int A)`x @@ a>>x1")] exI 1);
+by (res_inst_tac [("x","Takewhile (%a. a:int A)`x @@ a>>x1")] exI 1);
 by (res_inst_tac [("x","x2")] exI 1);
 (* elminate all obligations up to two depending on Conc_assoc *)
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
              int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1); 
 by (simp_tac (!simpset addsimps [Conc_assoc]) 1); 

 by (case_tac "aaa:act A" 2);
 by (case_tac "aaa:act B" 2);
 by (rotate_tac ~2 2);
 by (rotate_tac ~2 3);
 by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2);
-by (eres_inst_tac [("x","sb@@Takewhile (%a.a: int A)`a @@ Takewhile (%a.a:int B)`b@@(aaa>>nil)")] allE 2);
+by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)`a @@ Takewhile (%a. a:int B)`b@@(aaa>>nil)")] allE 2);
 by (eres_inst_tac [("x","sa")] allE 2);
 by (asm_full_simp_tac (!simpset addsimps [Conc_assoc])2);
 
 
 

   ------------------------------------------------------------------------------------- *)
 
 goal thy 
 "!! A B. [| compatible A B; compatible B A;\
 \           is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ ! schA schB. Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Filter (%a.a:act A)`tr << Filter (%a.a:ext A)`schA &\
-\ Filter (%a.a:act B)`tr << Filter (%a.a:ext B)`schB  \
-\ --> Filter (%a.a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
+\ ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Filter (%a. a:act A)`tr << Filter (%a. a:ext A)`schA &\
+\ Filter (%a. a:act B)`tr << Filter (%a. a:ext B)`schB  \
+\ --> Filter (%a. a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
 
 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
 
 (* main case *) 
 (* splitting into 4 cases according to a:A, a:B *)

                              take lemma
   --------------------------------------------------------------------------- *)
 
 goal thy "!! A B. [| compatible A B; compatible B A; \
 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
-\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
+\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
 \ LastActExtsch A schA & LastActExtsch B schB  \
-\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
+\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
 
 by (res_inst_tac [("Q","%x. x:act B & x~:act A"),("x","tr")] take_lemma_less_induct 1);
 by (REPEAT (etac conjE 1));
 
 by (case_tac "Finite s" 1);

 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac  1);
 
 (* eliminate the B-only prefix *)
 
-by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
 by (etac ForallQFilterPnil 2);
 by (assume_tac 2);
 by (Fast_tac 2);
 
 (* Now real recursive step follows (in y) *)

 
 
 
 goal thy "!! A B. [| compatible A B; compatible B A; \
 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
-\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
+\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
 \ LastActExtsch A schA & LastActExtsch B schB  \
-\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
+\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
 
 by (strip_tac 1);
 by (rtac seq.take_lemma 1);
 by (rtac mp 1);
 by (assume_tac 2);

 by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch1],
                            !simpset)) 1);
 (* second side: schA = nil *)
 by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
 by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPnil 1);
+by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPnil 1);
 by (assume_tac 1);
 by (Fast_tac 1);
 
 (* case ~ Finite s *)
 

                                             ForallBnAmksch],
                            !simpset)) 1);
 (* schA = UU *)
 by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
 by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPUU 1);
+by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPUU 1);
 by (assume_tac 1);
 by (Fast_tac 1);
 
 (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
 

 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac  1);
 
 (* eliminate the B-only prefix *)
 
-by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
 by (etac ForallQFilterPnil 2);
 by (assume_tac 2);
 by (Fast_tac 2);
 
 (* Now real recursive step follows (in y) *)

 by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
 by (assume_tac 1);
 
 (* assumption Forall schA *)
 by (dres_inst_tac [("s","schA"),
-                   ("P","Forall (%x.x:act A)")] subst 1);
+                   ("P","Forall (%x. x:act A)")] subst 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
 
 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
 

 
 
 
 goal thy "!! A B. [| compatible A B; compatible B A; \
 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
-\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
+\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
 \ LastActExtsch A schA & LastActExtsch B schB  \
-\ --> Filter (%a.a:act B)`(mksch A B`tr`schA`schB) = schB";
+\ --> Filter (%a. a:act B)`(mksch A B`tr`schA`schB) = schB";
 
 by (strip_tac 1);
 by (rtac seq.take_lemma 1);
 by (rtac mp 1);
 by (assume_tac 2);

 by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil,ForallAnBmksch,FiniteL_mksch1],
                            !simpset)) 1);
 (* second side: schA = nil *)
 by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
 by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPnil 1);
+by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPnil 1);
 by (assume_tac 1);
 by (Fast_tac 1);
 
 (* case ~ Finite tr *)
 

                                             ForallAnBmksch],
                            !simpset)) 1);
 (* schA = UU *)
 by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
 by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPUU 1);
+by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPUU 1);
 by (assume_tac 1);
 by (Fast_tac 1);
 
 (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
 

 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac  1);
 
 (* eliminate the A-only prefix *)
 
-by (subgoal_tac "(Filter (%a.a :act B)`x1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act B)`x1) = nil" 1);
 by (etac ForallQFilterPnil 2);
 by (assume_tac 2);
 by (Fast_tac 2);
 
 (* Now real recursive step follows (in x) *)

 by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
 by (assume_tac 1);
 
 (* assumption Forall schB *)
 by (dres_inst_tac [("s","schB"),
-                   ("P","Forall (%x.x:act B)")] subst 1);
+                   ("P","Forall (%x. x:act B)")] subst 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
 
 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
 

  
 goal thy 
 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
 \           is_asig(asig_of A); is_asig(asig_of B)|] \
 \       ==>  tr: traces(A||B) = \
-\            (Filter (%a.a:act A)`tr : traces A &\
-\             Filter (%a.a:act B)`tr : traces B &\
+\            (Filter (%a. a:act A)`tr : traces A &\
+\             Filter (%a. a:act B)`tr : traces B &\
 \             Forall (%x. x:ext(A||B)) tr)";
 
 by (simp_tac (!simpset addsimps [traces_def,has_trace_def]) 1);
 by (safe_tac set_cs);
  
 (* ==> *) 
 (* There is a schedule of A *)
-by (res_inst_tac [("x","Filter (%a.a:act A)`sch")] bexI 1);
+by (res_inst_tac [("x","Filter (%a. a:act A)`sch")] bexI 1);
 by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
 by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence1,
                   externals_of_par,ext1_ext2_is_not_act1]) 1);
 (* There is a schedule of B *)
-by (res_inst_tac [("x","Filter (%a.a:act B)`sch")] bexI 1);
+by (res_inst_tac [("x","Filter (%a. a:act B)`sch")] bexI 1);
 by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
 by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2,
                   externals_of_par,ext1_ext2_is_not_act2]) 1);
 (* Traces of A||B have only external actions from A or B *)  
 by (rtac ForallPFilterP 1);