src/HOLCF/IOA/meta_theory/CompoExecs.ML

 (* ---------------------------------------------------------------- *)
 (*                               ProjA2                             *)
 (* ---------------------------------------------------------------- *)
 
 
-goal thy  "ProjA2`UU = UU";
+Goal  "ProjA2`UU = UU";
 by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
 qed"ProjA2_UU";
 
-goal thy  "ProjA2`nil = nil";
+Goal  "ProjA2`nil = nil";
 by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
 qed"ProjA2_nil";
 
-goal thy "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs";
+Goal "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs";
 by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
 qed"ProjA2_cons";
 
 
 (* ---------------------------------------------------------------- *)
 (*                               ProjB2                             *)
 (* ---------------------------------------------------------------- *)
 
 
-goal thy  "ProjB2`UU = UU";
+Goal  "ProjB2`UU = UU";
 by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
 qed"ProjB2_UU";
 
-goal thy  "ProjB2`nil = nil";
+Goal  "ProjB2`nil = nil";
 by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
 qed"ProjB2_nil";
 
-goal thy "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs";
+Goal "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs";
 by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
 qed"ProjB2_cons";
 
 
 
 (* ---------------------------------------------------------------- *)
 (*                             Filter_ex2                           *)
 (* ---------------------------------------------------------------- *)
 
 
-goal thy "Filter_ex2 sig`UU=UU";
+Goal "Filter_ex2 sig`UU=UU";
 by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
 qed"Filter_ex2_UU";
 
-goal thy "Filter_ex2 sig`nil=nil";
+Goal "Filter_ex2 sig`nil=nil";
 by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
 qed"Filter_ex2_nil";
 
-goal thy "Filter_ex2 sig`(at >> xs) =    \
+Goal "Filter_ex2 sig`(at >> xs) =    \
 \            (if (fst at:actions sig)    \       
 \                 then at >> (Filter_ex2 sig`xs) \   
 \                 else        Filter_ex2 sig`xs)";
 
 by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1);

 (* ---------------------------------------------------------------- *)
 (*                             stutter2                             *)
 (* ---------------------------------------------------------------- *)
 
 
-goal thy "stutter2 sig = (LAM ex. (%s. case ex of \
+Goal "stutter2 sig = (LAM ex. (%s. case ex of \
 \      nil => TT \
 \    | x##xs => (flift1 \ 
 \            (%p.(If Def ((fst p)~:actions sig) \
 \                 then Def (s=(snd p)) \
 \                 else TT fi) \

 by (rtac stutter2_def 1);
 by (rtac beta_cfun 1);
 by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"stutter2_unfold";
 
-goal thy "(stutter2 sig`UU) s=UU";
+Goal "(stutter2 sig`UU) s=UU";
 by (stac stutter2_unfold 1);
 by (Simp_tac 1);
 qed"stutter2_UU";
 
-goal thy "(stutter2 sig`nil) s = TT";
+Goal "(stutter2 sig`nil) s = TT";
 by (stac stutter2_unfold 1);
 by (Simp_tac 1);
 qed"stutter2_nil";
 
-goal thy "(stutter2 sig`(at>>xs)) s = \
+Goal "(stutter2 sig`(at>>xs)) s = \
 \              ((if (fst at)~:actions sig then Def (s=snd at) else TT) \
 \                andalso (stutter2 sig`xs) (snd at))"; 
 by (rtac trans 1);
 by (stac stutter2_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def,If_and_if]) 1);

 
 (* ---------------------------------------------------------------- *)
 (*                             stutter                              *)
 (* ---------------------------------------------------------------- *)
 
-goal thy "stutter sig (s, UU)";
+Goal "stutter sig (s, UU)";
 by (simp_tac (simpset() addsimps [stutter_def]) 1);
 qed"stutter_UU";
 
-goal thy "stutter sig (s, nil)";
+Goal "stutter sig (s, nil)";
 by (simp_tac (simpset() addsimps [stutter_def]) 1);
 qed"stutter_nil";
 
-goal thy "stutter sig (s, (a,t)>>ex) = \
+Goal "stutter sig (s, (a,t)>>ex) = \
 \     ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
 by (simp_tac (simpset() addsimps [stutter_def]) 1);
 qed"stutter_cons";
 
 (* ----------------------------------------------------------------------------------- *)

 
 (* --------------------------------------------------------------------- *)
 (*  Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B    *)
 (* --------------------------------------------------------------------- *)
 
-goal thy "!s. is_exec_frag (A||B) (s,xs) \
+Goal "!s. is_exec_frag (A||B) (s,xs) \
 \      -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)`(ProjA2`xs)) &\
 \           is_exec_frag B (snd s, Filter_ex2 (asig_of B)`(ProjB2`xs))";
 
 by (pair_induct_tac "xs" [is_exec_frag_def] 1);
 (* main case *)

 
 (* --------------------------------------------------------------------- *)
 (*  Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections       *)
 (* --------------------------------------------------------------------- *)
 
-goal thy "!s. is_exec_frag (A||B) (s,xs) \
+Goal "!s. is_exec_frag (A||B) (s,xs) \
 \      --> stutter (asig_of A) (fst s,ProjA2`xs)  &\
 \          stutter (asig_of B) (snd s,ProjB2`xs)"; 
 
 by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
 (* main case *)

 
 (* --------------------------------------------------------------------- *)
 (*  Lemma_1_1c : Executions of A||B have only  A- or B-actions           *)
 (* --------------------------------------------------------------------- *)
 
-goal thy "!s. (is_exec_frag (A||B) (s,xs) \
+Goal "!s. (is_exec_frag (A||B) (s,xs) \
 \  --> Forall (%x. fst x:act (A||B)) xs)";
 
 by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1);
 (* main case *)
 by (safe_tac set_cs);

 
 (* ----------------------------------------------------------------------- *)
 (*  Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B)   *)
 (* ----------------------------------------------------------------------- *)
 
-goal thy 
+Goal 
 "!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)`(ProjA2`xs)) &\
 \    is_exec_frag B (snd s,Filter_ex2 (asig_of B)`(ProjB2`xs)) &\
 \    stutter (asig_of A) (fst s,(ProjA2`xs)) & \
 \    stutter (asig_of B) (snd s,(ProjB2`xs)) & \
 \    Forall (%x. fst x:act (A||B)) xs \

 (*           COMPOSITIONALITY   on    EXECUTION     Level             *)
 (*                          Main Theorem                              *)
 (* ------------------------------------------------------------------ *)
 
 
-goal thy 
+Goal 
 "ex:executions(A||B) =\
 \(Filter_ex (asig_of A) (ProjA ex) : executions A &\
 \ Filter_ex (asig_of B) (ProjB ex) : executions B &\
 \ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
 \ Forall (%x. fst x:act (A||B)) (snd ex))";

 (* ------------------------------------------------------------------ *)
 (*           COMPOSITIONALITY   on    EXECUTION     Level             *)
 (*                            For Modules                             *)
 (* ------------------------------------------------------------------ *)
 
-goalw thy [Execs_def,par_execs_def]
+Goalw [Execs_def,par_execs_def]
 
 "Execs (A||B) = par_execs (Execs A) (Execs B)";
 
 by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
 by (rtac set_ext 1);