# HG changeset patch # User wenzelm # Date 884177754 -3600 # Node ID d430a1b349282d855455d95c84ff3f0aa737eaf9 # Parent 055f2067d3734f7e1d7e8cb4c9eab15ddc297046 adapted to new split order; diff -r 055f2067d373 -r d430a1b34928 src/HOLCF/IOA/meta_theory/CompoScheds.ML --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Wed Jan 07 13:55:29 1998 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Wed Jan 07 13:55:54 1998 +0100 @@ -233,11 +233,11 @@ by (Asm_full_simp_tac 1); (* Case y:A, y~:B *) -by (Seq_case_simp_tac "exB" 1); +by (Seq_case_simp_tac "exA" 1); by (Asm_full_simp_tac 1); (* Case y~:A, y:B *) -by (Seq_case_simp_tac "exA" 1); +by (Seq_case_simp_tac "exB" 1); by (Asm_full_simp_tac 1); (* Case y~:A, y~:B *) @@ -254,9 +254,9 @@ Seq_case_simp_tac exA, Seq_case_simp_tac exB, Asm_full_simp_tac, - Seq_case_simp_tac exB, + Seq_case_simp_tac exA, Asm_full_simp_tac, - Seq_case_simp_tac exA, + Seq_case_simp_tac exB, Asm_full_simp_tac, asm_full_simp_tac (simpset() addsimps [asig_of_par,actions_asig_comp]) ]; @@ -340,7 +340,7 @@ \ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) = \ \ Zip`(Filter (%a. a:act A)`sch)`(Map snd`exA)"; -by (mkex_induct_tac "sch" "exA" "exB"); +by (mkex_induct_tac "sch" "exB" "exA"); qed"filter_mkex_is_exA_tmp"; @@ -359,15 +359,6 @@ lemma for eliminating non admissible equations in assumptions --------------------------------------------------------------------------- *) -(* Versuich -goal thy "(y~= nil & Map fst`x < x= Zip`y`(Map snd`x)"; -by (Seq_induct_tac "x" [] 1); -by (Seq_case_simp_tac "y" 2); -by (pair_tac "a" 1); -by Auto_tac; - -*) - goal thy "!! sch ex. \ \ Filter (%a. a:act AB)`sch = filter_act`ex \ \ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)"; @@ -414,7 +405,7 @@ \ Zip`(Filter (%a. a:act B)`sch)`(Map snd`exB)"; (* notice necessary change of arguments exA and exB *) -by (mkex_induct_tac "sch" "exB" "exA"); +by (mkex_induct_tac "sch" "exA" "exB"); qed"filter_mkex_is_exB_tmp"; @@ -523,4 +514,4 @@ Delsimps compoex_simps; -Delsimps composch_simps; \ No newline at end of file +Delsimps composch_simps; diff -r 055f2067d373 -r d430a1b34928 src/HOLCF/IOA/meta_theory/CompoTraces.ML --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Wed Jan 07 13:55:29 1998 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Wed Jan 07 13:55:54 1998 +0100 @@ -511,8 +511,20 @@ (* IH *) by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1); + +(* Case a:A, a~:B *) +by (forward_tac [divide_Seq] 1); +by (REPEAT (etac conjE 1)); +(* filtering internals of A is nil *) +by (asm_full_simp_tac (simpset() addsimps + [FilterPTakewhileQnil,not_ext_is_int_or_not_act, + externals_of_par, intA_is_not_extB,int_is_not_ext]) 1); +by (dres_inst_tac [("x","schA")] subst_lemma1 1); +by (assume_tac 1); +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, + FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1); + (* Case a:B, a~:A *) - by (forward_tac [divide_Seq] 1); by (REPEAT (etac conjE 1)); (* filtering internals of A is nil *) @@ -524,20 +536,8 @@ by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1); -(* Case a:A, a~:B *) -by (forward_tac [divide_Seq] 1); -by (REPEAT (etac conjE 1)); -(* filtering internals of A is nil *) -by (asm_full_simp_tac (simpset() addsimps - [FilterPTakewhileQnil,not_ext_is_int_or_not_act, - externals_of_par, intA_is_not_extB,int_is_not_ext]) 1); -by (dres_inst_tac [("x","schA")] subst_lemma1 1); -by (assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, - FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1); (* Case a~:A, a~:B *) - by (fast_tac (claset() addSIs [ext_is_act] addss (simpset() addsimps [externals_of_par]) ) 1); qed"FilterA_mksch_is_tr";