diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/CompoExecs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,262 @@ +(* Title: HOLCF/IOA/meta_theory/CompoExecs.ML + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Compositionality on Execution level. +*) + +Delsimps (ex_simps @ all_simps); +Delsimps [split_paired_All]; + +(* ----------------------------------------------------------------------------------- *) + + +section "recursive equations of operators"; + + +(* ---------------------------------------------------------------- *) +(* ProjA2 *) +(* ---------------------------------------------------------------- *) + + +goal thy "ProjA2`UU = UU"; +by (simp_tac (!simpset addsimps [ProjA2_def]) 1); +qed"ProjA2_UU"; + +goal thy "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"; +by (simp_tac (!simpset addsimps [ProjA2_def]) 1); +qed"ProjA2_cons"; + + +(* ---------------------------------------------------------------- *) +(* ProjB2 *) +(* ---------------------------------------------------------------- *) + + +goal thy "ProjB2`UU = UU"; +by (simp_tac (!simpset addsimps [ProjB2_def]) 1); +qed"ProjB2_UU"; + +goal thy "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"; +by (simp_tac (!simpset addsimps [ProjB2_def]) 1); +qed"ProjB2_cons"; + + + +(* ---------------------------------------------------------------- *) +(* Filter_ex2 *) +(* ---------------------------------------------------------------- *) + + +goal thy "Filter_ex2 A`UU=UU"; +by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1); +qed"Filter_ex2_UU"; + +goal thy "Filter_ex2 A`nil=nil"; +by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1); +qed"Filter_ex2_nil"; + +goal thy "Filter_ex2 A`(at >> xs) = \ +\ (if (fst at:act A) \ +\ then at >> (Filter_ex2 A`xs) \ +\ else Filter_ex2 A`xs)"; + +by (asm_full_simp_tac (!simpset addsimps [Filter_ex2_def]) 1); +qed"Filter_ex2_cons"; + + +(* ---------------------------------------------------------------- *) +(* stutter2 *) +(* ---------------------------------------------------------------- *) + + +goal thy "stutter2 A = (LAM ex. (%s. case ex of \ +\ nil => TT \ +\ | x##xs => (flift1 \ +\ (%p.(If Def ((fst p)~:act A) \ +\ then Def (s=(snd p)) \ +\ else TT fi) \ +\ andalso (stutter2 A`xs) (snd p)) \ +\ `x) \ +\ ))"; +by (rtac trans 1); +br fix_eq2 1; +br stutter2_def 1; +br beta_cfun 1; +by (simp_tac (!simpset addsimps [flift1_def]) 1); +qed"stutter2_unfold"; + +goal thy "(stutter2 A`UU) s=UU"; +by (stac stutter2_unfold 1); +by (Simp_tac 1); +qed"stutter2_UU"; + +goal thy "(stutter2 A`nil) s = TT"; +by (stac stutter2_unfold 1); +by (Simp_tac 1); +qed"stutter2_nil"; + +goal thy "(stutter2 A`(at>>xs)) s = \ +\ ((if (fst at)~:act A then Def (s=snd at) else TT) \ +\ andalso (stutter2 A`xs) (snd at))"; +br trans 1; +by (stac stutter2_unfold 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1); +by (Simp_tac 1); +qed"stutter2_cons"; + + +Addsimps [stutter2_UU,stutter2_nil,stutter2_cons]; + + +(* ---------------------------------------------------------------- *) +(* stutter *) +(* ---------------------------------------------------------------- *) + +goal thy "stutter A (s, UU)"; +by (simp_tac (!simpset addsimps [stutter_def]) 1); +qed"stutter_UU"; + +goal thy "stutter A (s, nil)"; +by (simp_tac (!simpset addsimps [stutter_def]) 1); +qed"stutter_nil"; + +goal thy "stutter A (s, (a,t)>>ex) = \ +\ ((a~:act A --> (s=t)) & stutter A (t,ex))"; +by (simp_tac (!simpset addsimps [stutter_def] + setloop (split_tac [expand_if]) ) 1); +qed"stutter_cons"; + +(* ----------------------------------------------------------------------------------- *) + +Delsimps [stutter2_UU,stutter2_nil,stutter2_cons]; + +val compoex_simps = [ProjA2_UU,ProjA2_nil,ProjA2_cons, + ProjB2_UU,ProjB2_nil,ProjB2_cons, + Filter_ex2_UU,Filter_ex2_nil,Filter_ex2_cons, + stutter_UU,stutter_nil,stutter_cons]; + +Addsimps compoex_simps; + + + +(* ------------------------------------------------------------------ *) +(* The following lemmata aim for *) +(* COMPOSITIONALITY on EXECUTION Level *) +(* ------------------------------------------------------------------ *) + + +(* --------------------------------------------------------------------- *) +(* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *) +(* --------------------------------------------------------------------- *) + +goal thy "!s. is_execution_fragment (A||B) (s,xs) \ +\ --> is_execution_fragment A (fst s, Filter_ex2 A`(ProjA2`xs)) &\ +\ is_execution_fragment B (snd s, Filter_ex2 B`(ProjB2`xs))"; + +by (pair_induct_tac "xs" [is_execution_fragment_def] 1); +(* main case *) +ren "ss a t" 1; +by (safe_tac set_cs); +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 + setloop (split_tac [expand_if])) 1)); +qed"lemma_1_1a"; + + +(* --------------------------------------------------------------------- *) +(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *) +(* --------------------------------------------------------------------- *) + +goal thy "!s. is_execution_fragment (A||B) (s,xs) \ +\ --> stutter A (fst s,ProjA2`xs) &\ +\ stutter B (snd s,ProjB2`xs)"; + +by (pair_induct_tac "xs" [stutter_def,is_execution_fragment_def] 1); +(* main case *) +by (safe_tac set_cs); +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 + setloop (split_tac [expand_if])) 1)); +qed"lemma_1_1b"; + + +(* --------------------------------------------------------------------- *) +(* Lemma_1_1c : Executions of A||B have only A- or B-actions *) +(* --------------------------------------------------------------------- *) + +goal thy "!s. (is_execution_fragment (A||B) (s,xs) \ +\ --> Forall (%x.fst x:act (A||B)) xs)"; + +by (pair_induct_tac "xs" [Forall_def,sforall_def,is_execution_fragment_def] 1); +(* main case *) +by (safe_tac set_cs); +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @ + [actions_asig_comp,asig_of_par]) 1)); +qed"lemma_1_1c"; + + +(* ----------------------------------------------------------------------- *) +(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *) +(* ----------------------------------------------------------------------- *) + +goal thy +"!s. is_execution_fragment A (fst s,Filter_ex2 A`(ProjA2`xs)) &\ +\ is_execution_fragment B (snd s,Filter_ex2 B`(ProjB2`xs)) &\ +\ stutter A (fst s,(ProjA2`xs)) & \ +\ stutter B (snd s,(ProjB2`xs)) & \ +\ Forall (%x.fst x:act (A||B)) xs \ +\ --> is_execution_fragment (A||B) (s,xs)"; + +by (pair_induct_tac "xs" [Forall_def,sforall_def, + is_execution_fragment_def, stutter_def] 1); +(* main case *) +by (rtac allI 1); +ren "ss a t s" 1; +by (asm_full_simp_tac (!simpset addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par] + setloop (split_tac [expand_if])) 1); +by (safe_tac set_cs); +(* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *) +by (rotate_tac ~4 1); +by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); +by (rotate_tac ~4 1); +by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); +qed"lemma_1_2"; + + +(* ------------------------------------------------------------------ *) +(* COMPOSITIONALITY on EXECUTION Level *) +(* Main Theorem *) +(* ------------------------------------------------------------------ *) + + +goal thy +"ex:executions(A||B) =\ +\(Filter_ex A (ProjA ex) : executions A &\ +\ Filter_ex B (ProjB ex) : executions B &\ +\ stutter A (ProjA ex) & stutter B (ProjB ex) &\ +\ Forall (%x.fst x:act (A||B)) (snd ex))"; + +by (simp_tac (!simpset addsimps [executions_def,ProjB_def, + Filter_ex_def,ProjA_def,starts_of_par]) 1); +by (pair_tac "ex" 1); +by (rtac iffI 1); +(* ==> *) +by (REPEAT (etac conjE 1)); +by (asm_full_simp_tac (!simpset addsimps [lemma_1_1a RS spec RS mp, + lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1); +(* <== *) +by (REPEAT (etac conjE 1)); +by (asm_full_simp_tac (!simpset addsimps [lemma_1_2 RS spec RS mp]) 1); +qed"compositionality_ex"; + + + +