--- a/src/HOLCF/IOA/meta_theory/Asig.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Asig.ML Wed May 21 15:08:52 1997 +0200
@@ -31,8 +31,14 @@
by (best_tac (set_cs addEs [equalityCE]) 1);
qed"not_ext_is_int";
+goal thy "!!S. is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,is_asig_def,externals_def]) 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"not_ext_is_int_or_not_act";
+
goalw thy [externals_def,actions_def,is_asig_def]
"!! x. [| is_asig (S); x:internals S |] ==> x~:externals S";
by (Asm_full_simp_tac 1);
by (best_tac (set_cs addEs [equalityCE]) 1);
-qed"int_is_not_ext";
\ No newline at end of file
+qed"int_is_not_ext";
+
--- a/src/HOLCF/IOA/meta_theory/Asig.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Asig.thy Wed May 21 15:08:52 1997 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/IOA/meta_theory/Asig.thy
ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ Author: Olaf Mueller, Tobias Nipkow & Konrad Slind
+ Copyright 1994, 1996 TU Muenchen
Action signatures
*)
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Automata.ML
- ID: $$
+ ID: $Id$
Author: Olaf Mueller, Tobias Nipkow, Konrad Slind
Copyright 1994, 1996 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Automata.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller, Konrad Slind, Tobias Nipkow
Copyright 1995, 1996 TU Muenchen
@@ -82,8 +82,8 @@
state_trans_def
"state_trans asig R ==
- (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
- (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
+ (!triple. triple:R --> fst(snd(triple)):actions(asig))"
+(* & (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" *)
asig_of_def "asig_of == fst"
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/CompoExecs.ML
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/CompoExecs.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/CompoScheds.ML
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/CompoScheds.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Wed May 21 15:08:52 1997 +0200
@@ -2,27 +2,20 @@
ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
-
+
Compositionality on Trace level.
*)
-(* FIX:Proof and add in Sequence.ML *)
-Addsimps [Finite_Conc];
-
-
-(*
-Addsimps [forall_cons];
-
-Addsimps [(* LastActExtsmall1, LastActExtsmall2, looping !! *) ext_and_act];
-*)
fun thin_tac' j =
rotate_tac (j - 1) THEN'
- etac thin_rl THEN'
+ etac thin_rl THEN'
rotate_tac (~ (j - 1));
+
+
(* ---------------------------------------------------------------- *)
section "mksch rewrite rules";
(* ---------------------------------------------------------------- *)
@@ -122,7 +115,7 @@
(* ---------------------------------------------------------------------------- *)
-(* Specifics for "==>" *)
+ section"Lemmata for ==>";
(* ---------------------------------------------------------------------------- *)
(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of
@@ -143,27 +136,22 @@
qed"compatibility_consequence2";
-goal thy "!!x. [| x = nil; y = z|] ==> (x @@ y) = z";
-auto();
-qed"nil_and_tconc";
-
-(* FIX: should be easy to get out of lemma before *)
-goal thy "!!x. [| x = nil; f`y = f`z|] ==> f`(x @@ y) = f`z";
-auto();
-qed"nil_and_tconc_f";
-
-(* FIX: should be something like subst: or better improve simp_tac so that these lemmat are
- superfluid *)
-goal thy "!!x. [| x1 = x2; f`(x2 @@ y) = f`z|] ==> f`(x1 @@ y) = f`z";
-auto();
-qed"tconcf";
+(* ---------------------------------------------------------------------------- *)
+ section"Lemmata for <==";
+(* ---------------------------------------------------------------------------- *)
-
-(*
+(* Lemma for substitution of looping assumption in another specific assumption *)
+val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
+by (cut_facts_tac [p1] 1);
+be (p2 RS subst) 1;
+qed"subst_lemma1";
-
-(* -------------------------------------------------------------------------------- *)
+(* Lemma for substitution of looping assumption in another specific assumption *)
+val [p1,p2] = goal thy "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g";
+by (cut_facts_tac [p1] 1);
+be (p2 RS subst) 1;
+qed"subst_lemma2";
goal thy "!!A B. compat_ioas A B ==> \
@@ -177,34 +165,39 @@
(* a:A, a:B *)
by (Asm_full_simp_tac 1);
br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
(* a:A,a~:B *)
by (Asm_full_simp_tac 1);
br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
by (case_tac "a:act B" 1);
(* a~:A, a:B *)
by (Asm_full_simp_tac 1);
br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
(* a~:A,a~:B *)
auto();
-qed"ForallAorB_mksch";
+qed"ForallAorB_mksch1";
+bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp);
-goal thy "!!A B. compat_ioas A B ==> \
+goal thy "!!A B. compat_ioas B A ==> \
\ ! schA schB. (Forall (%x. x:act B & x~:act A) tr \
\ --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))";
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
by (safe_tac set_cs);
br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
+ intA_is_not_actB,int_is_act]) 1);
qed"ForallBnA_mksch";
-goal thy "!!A B. compat_ioas B A ==> \
+bind_thm ("ForallBnAmksch",ForallBnA_mksch RS spec RS spec RS mp);
+
+
+goal thy "!!A B. compat_ioas A B ==> \
\ ! schA schB. (Forall (%x. x:act A & x~:act B) tr \
\ --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))";
@@ -212,15 +205,19 @@
by (safe_tac set_cs);
by (Asm_full_simp_tac 1);
br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
+ intA_is_not_actB,int_is_act]) 1);
qed"ForallAnB_mksch";
+bind_thm ("ForallAnBmksch",ForallAnB_mksch RS spec RS spec RS mp);
+
-(* ------------------------------------------------------------------------------------ *)
+(* safe-tac makes too many case distinctions with this lemma in the next proof *)
+Delsimps [FiniteConc];
-(*
-goal thy "!! tr. Finite tr ==> \
-\ ! x y. Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
+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 & \
+\ 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)";
@@ -230,55 +227,188 @@
(* main case *)
by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (safe_tac set_cs);
-by (Asm_full_simp_tac 1);
+
+(* a: act A; a: act B *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+back();
+by (REPEAT (etac conjE 1));
+(* Finite (tw iA x) and Finite (tw iB y) *)
+by (asm_full_simp_tac (!simpset addsimps
+ [not_ext_is_int_or_not_act,FiniteConc]) 1);
+(* now for conclusion IH applicable, but assumptions have to be transformed *)
+by (dres_inst_tac [("x","x"),
+ ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
+ba 1;
+by (dres_inst_tac [("x","y"),
+ ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
+ba 1;
+(* IH *)
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+ FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
+
+(* a: act B; a~: act A *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+(* Finite (tw iB y) *)
+by (asm_full_simp_tac (!simpset addsimps
+ [not_ext_is_int_or_not_act,FiniteConc]) 1);
+(* now for conclusion IH applicable, but assumptions have to be transformed *)
+by (dres_inst_tac [("x","y"),
+ ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
+ba 1;
+(* IH *)
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+ FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
+(* a~: act B; a: act A *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+(* Finite (tw iA x) *)
+by (asm_full_simp_tac (!simpset addsimps
+ [not_ext_is_int_or_not_act,FiniteConc]) 1);
+(* now for conclusion IH applicable, but assumptions have to be transformed *)
+by (dres_inst_tac [("x","x"),
+ ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
+ba 1;
+(* IH *)
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+ FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
+
+(* a~: act B; a~: act A *)
+by (fast_tac (!claset addSIs [ext_is_act]
+ addss (!simpset addsimps [externals_of_par]) ) 1);
qed"FiniteL_mksch";
-goal thy " !!bs. Finite bs ==> \
-\ 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)";
+bind_thm("FiniteL_mksch1", FiniteL_mksch RS spec RS spec RS mp);
+
+Addsimps [FiniteConc];
+
+
+(* 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);compat_ioas A B|] ==> \
+\! 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)";
+by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
be Seq_Finite_ind 1;
+by (REPEAT (rtac allI 1));
by (rtac impI 1);
by (res_inst_tac [("x","nil")] exI 1);
by (res_inst_tac [("x","y")] exI 1);
by (Asm_full_simp_tac 1);
(* main case *)
+by (REPEAT (rtac allI 1));
by (rtac impI 1);
by (Asm_full_simp_tac 1);
by (REPEAT (etac conjE 1));
+by (Asm_full_simp_tac 1);
+(* divide_Seq on s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+(* transform assumption f eB y = f B (s@z) *)
+by (dres_inst_tac [("x","y"),
+ ("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
+ba 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 (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","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);
+qed"reduceA_mksch1";
+
+bind_thm("reduceA_mksch",conjI RSN (6,conjI RSN (5,reduceA_mksch1 RS spec RS mp)));
+
+
+
+(* 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);compat_ioas A B|] ==> \
+\! 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)";
+by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
+be Seq_Finite_ind 1;
+by (REPEAT (rtac allI 1));
+by (rtac impI 1);
+by (res_inst_tac [("x","nil")] exI 1);
+by (res_inst_tac [("x","x")] exI 1);
+by (Asm_full_simp_tac 1);
+(* main case *)
+by (REPEAT (rtac allI 1));
+by (rtac impI 1);
+by (Asm_full_simp_tac 1);
+by (REPEAT (etac conjE 1));
+by (Asm_full_simp_tac 1);
+(* divide_Seq on s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+(* transform assumption f eA x = f A (s@z) *)
+by (dres_inst_tac [("x","x"),
+ ("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
+ba 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 (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","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);
+qed"reduceB_mksch1";
+
+bind_thm("reduceB_mksch",conjI RSN (6,conjI RSN (5,reduceB_mksch1 RS spec RS mp)));
-qed"reduce_mksch";
-
-*)
-
-
-(* Lemma for substitution of looping assumption in another specific assumption *)
-val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
-by (cut_facts_tac [p1] 1);
-be (p2 RS subst) 1;
-qed"subst_lemma1";
-
-
-
-(*---------------------------------------------------------------------------
- Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr
- structural induction
- --------------------------------------------------------------------------- *)
+(*------------------------------------------------------------------------------------- *)
+ section"Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr";
+(* structural induction
+ ------------------------------------------------------------------------------------- *)
-goal thy "! schA schB. compat_ioas A B & compat_ioas B A &\
-\ is_asig(asig_of A) & is_asig(asig_of B) &\
+goal thy
+"!! A B. [| compat_ioas A B; compat_ioas 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 \
@@ -296,373 +426,544 @@
by (forward_tac [divide_Seq] 1);
back();
by (REPEAT (etac conjE 1));
-(* filtering internals of A is nil *)
-br nil_and_tconc 1;
-br FilterPTakewhileQnil 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
- intA_is_not_extB,int_is_not_ext]) 1);
-(* end*)
-(* filtering internals of B is nil *)
-(* FIX: should be done by simp_tac and claset combined until end*)
-br nil_and_tconc 1;
-br FilterPTakewhileQnil 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
- intA_is_not_extB,int_is_not_ext]) 1);
-(* end*)
+(* filtering internals of A in schA and of B in schB 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);
(* conclusion of IH ok, but assumptions of IH have to be transformed *)
by (dres_inst_tac [("x","schA")] subst_lemma1 1);
ba 1;
by (dres_inst_tac [("x","schB")] subst_lemma1 1);
ba 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1);
-
+(* IH *)
+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 *)
-(* FIX: should be done by simp_tac and claset combined until end*)
-br nil_and_tconc 1;
-br FilterPTakewhileQnil 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
- intA_is_not_extB,int_is_not_ext]) 1);
-(* end*)
+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","schB")] subst_lemma1 1);
back();
ba 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 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 *)
-(* FIX: should be done by simp_tac and claset combined until end*)
-br nil_and_tconc 1;
-br FilterPTakewhileQnil 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
- intA_is_not_extB,int_is_not_ext]) 1);
-(* end*)
+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);
ba 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 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";
-
+qed"FilterA_mksch_is_tr";
-goal thy "!!x y. [|x=UU; y=UU|] ==> x=y";
-auto();
-qed"both_UU";
-
-goal thy "!!x y. [|x=nil; y=nil|] ==> x=y";
-auto();
-qed"both_nil";
+(*--------------------------------------------------------------------------- *)
-
-(* FIX: does it exist already? *)
-(* To eliminate representation a##xs, if only ~=UU & ~=nil is needed *)
-goal thy "!!tr. [|tr=a##xs; a~=UU |] ==> tr~=UU & tr~=nil";
- by (Asm_full_simp_tac 1);
-qed"yields_not_UU_or_nil";
-
-
+ section" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof";
+
+(* --------------------------------------------------------------------------- *)
-(*---------------------------------------------------------------------------
- Filter of mksch(tr,schA,schB) to A is schA
- take lemma
- --------------------------------------------------------------------------- *)
-
-goal thy "compat_ioas A B & compat_ioas B A &\
+goal thy "!! A B. [| compat_ioas A B; compat_ioas 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 &\
-\ LastActExtsch schA & LastActExtsch schB \
+\ LastActExtsch A schA & LastActExtsch B schB \
\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
+by (strip_tac 1);
+br seq.take_lemma 1;
+br mp 1;
+ba 2;
+back();back();back();back();
+by (res_inst_tac [("x","schA")] spec 1);
+by (res_inst_tac [("x","schB")] spec 1);
+by (res_inst_tac [("x","tr")] spec 1);
+by (thin_tac' 5 1);
+br less_induct 1;
+by (REPEAT (rtac allI 1));
+ren "tr schB schA" 1;
+by (strip_tac 1);
+by (REPEAT (etac conjE 1));
-by (res_inst_tac [("Q","%x. x:act B & x~:act A")] take_lemma_less_induct 1);
+by (case_tac "Forall (%x. x:act B & x~:act A) tr" 1);
+
+br (seq_take_lemma RS iffD2 RS spec) 1;
+by (thin_tac' 5 1);
-(*---------------------------------------------------------------------------
- Filter of mksch(tr,schA,schB) to A is schA
- take lemma
- --------------------------------------------------------------------------- *)
-
-goal thy "! schA schB tr. compat_ioas A B & compat_ioas B A &\
-\ forall (plift (%x.x:externals(asig_of (A||B)))) tr & \
-\ tfilter`(plift (%a.a:externals(asig_of A)))`schA = tfilter`(plift (%a.a:actions(asig_of A)))`tr &\
-\ tfilter`(plift (%a.a:externals(asig_of B)))`schB = tfilter`(plift (%a.a:actions(asig_of B)))`tr &\
-\ LastActExtsch schA & LastActExtsch schB \
-\ --> trace_take n`(tfilter`(plift (%a.a:actions(asig_of A)))`(mksch A B`tr`schA`schB)) = trace_take n`schA";
-
-by (res_inst_tac[("n","n")] less_induct 1);
-by (REPEAT(rtac allI 1));
-br impI 1;
-by (REPEAT (etac conjE 1));
-by (res_inst_tac [("x","tr")] trace.cases 1);
-
-(* tr = UU *)
-by (rotate_tac ~1 1);
-by (Asm_full_simp_tac 1);
-by (dtac LastActExtimplUU 1);
-ba 1;
-by (Asm_simp_tac 1);
+by (case_tac "Finite tr" 1);
-(* tr = nil *)
-by (rotate_tac ~1 1);
-by (Asm_full_simp_tac 1);
-by (dtac LastActExtimplnil 1);
-ba 1;
+(* both sides of this equation are nil *)
+by (subgoal_tac "schA=nil" 1);
by (Asm_simp_tac 1);
-
-(* tr = t##ts *)
-
-(* just to delete tr=a##xs, as we do not make induction on a but on an element in
- xs we find later *)
-by (dtac yields_not_UU_or_nil 1);
-ba 1;
-by (REPEAT (etac conjE 1));
-
-(* FIX: or use equality "hd(f ~P x)=UU = fa P x" to make distinction on that *)
-by (case_tac "forall (plift (%x.x:actions(asig_of B) & x~:actions(asig_of A))) tr" 1);
-(* This case holds for whole streams, not only for takes *)
-br (trace_take_lemma RS iffD2 RS spec) 1;
-
-by (case_tac "tr : tfinite" 1);
-
-(* FIX: Check if new trace lemmata with ==> instead of --> allow for simplifiaction instead
- of ares_tac in the following *)
-br both_nil 1;
-(* mksch = nil *)
-by (REPEAT (ares_tac [forallQfilterPnil,forallBnA_mksch,finiteL_mksch] 1));
-by (Fast_tac 1);
-(* schA = nil *)
+(* first side: mksch = nil *)
+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);
-br forallQfilterPnil 1;
-ba 1;
-back();
-ba 1;
-by (Fast_tac 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil],
+ !simpset)) 1);
+
+(* case ~ Finite s *)
-(* case tr~:tfinite *)
-
-br both_UU 1;
-(* mksch = UU *)
-by (REPEAT (ares_tac [forallQfilterPUU,(finiteR_mksch RS mp COMP rev_contrapos),
- forallBnA_mksch] 1));
-by (Fast_tac 1);
+(* both sides of this equation are UU *)
+by (subgoal_tac "schA=UU" 1);
+by (Asm_simp_tac 1);
+(* first side: mksch = UU *)
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU,
+ (finiteR_mksch RS mp COMP rev_contrapos),
+ ForallBnAmksch],
+ !simpset)) 1);
(* schA = UU *)
by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
by (Asm_simp_tac 1);
-br forallQfilterPUU 1;
-by (REPEAT (atac 1));
-back();
-by (Fast_tac 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU],
+ !simpset)) 1);
+
+(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
+
+bd divide_Seq3 1;
-(* case" ~ forall (plift (%x.x:actions(asig_of B) & x~:actions(asig_of A))) tr" *)
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+by (hyp_subst_tac 1);
-by (dtac divide_trace3 1);
+(* bring in lemma reduceA_mksch *)
+by (forw_inst_tac [("x","schB"),("xa","schA"),("A","A"),("B","B")] reduceA_mksch 1);
by (REPEAT (atac 1));
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
-(* rewrite assuption for tr *)
-by (hyp_subst_tac 1);
-(* bring in lemma reduce_mksch *)
-by (forw_inst_tac [("y","schB"),("x","schA")] reduce_mksch 1);
-ba 1;
-by (asm_simp_tac HOL_min_ss 1);
-by (REPEAT (etac exE 1));
-by (REPEAT (etac conjE 1));
-
-(* use reduce_mksch to rewrite conclusion *)
+(* use reduceA_mksch to rewrite conclusion *)
by (hyp_subst_tac 1);
by (Asm_full_simp_tac 1);
(* eliminate the B-only prefix *)
-(* FIX: Cannot be done by
- by (asm_full_simp_tac (HOL_min_ss addsimps [forallQfilterPnil]) 1);
- as P&Q --> Q is looping. Perhaps forall (and other) operations not on predicates but on
- sets because of this reason ?????? *)
-br nil_and_tconc_f 1;
-be forallQfilterPnil 1;
-ba 1;
-by (Fast_tac 1);
+
+by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
+be ForallQFilterPnil 2;
+ba 2;
+by (Fast_tac 2);
+
+(* Now real recursive step follows (in y) *)
-(* Now real recursive step follows (in Def x) *)
-
-by (case_tac "x:actions(asig_of A)" 1);
-by (case_tac "x~:actions(asig_of B)" 1);
+by (Asm_full_simp_tac 1);
+by (case_tac "x:act A" 1);
+by (case_tac "x~:act B" 1);
by (rotate_tac ~2 1);
-by (asm_full_simp_tac (!simpset addsimps [filter_rep]) 1);
+by (Asm_full_simp_tac 1);
-(* same problem as above for the B-onlu prefix *)
-(* FIX: eliminate generated subgoal immeadiately ! (as in case below x:A & x: B *)
-by (subgoal_tac "tfilter`(plift (%a. a : actions (asig_of A) & a : externals (asig_of B)))`y1=nil" 1);
+by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
(* eliminate introduced subgoal 2 *)
-be forallQfilterPnil 2;
+be ForallQFilterPnil 2;
ba 2;
by (Fast_tac 2);
-(* f A (tw iA) = tw iA *)
-by (simp_tac (HOL_min_ss addsimps [filterPtakewhileQ,int_is_act]) 1);
+(* bring in divide Seq for s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+
+(* subst divide_Seq in conclusion, but only at the righest occurence *)
+by (res_inst_tac [("t","schA")] ssubst 1);
+back();
+back();
+back();
+ba 1;
+
+(* reduce trace_takes from n to strictly smaller k *)
+br take_reduction 1;
+
+(* f A (tw iA) = tw ~eA *)
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+ not_ext_is_int_or_not_act]) 1);
+br refl 1;
+by (asm_full_simp_tac (!simpset addsimps [int_is_act,
+ not_ext_is_int_or_not_act]) 1);
+by (rotate_tac ~11 1);
+
+(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
-by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace] 1);
-(* subst divide_trace in conlcusion, but only at the righest occurence *)
+(* assumption Forall tr *)
+by (asm_full_simp_tac (!simpset addsimps [Forall_Conc]) 1);
+(* assumption schB *)
+by (asm_full_simp_tac (!simpset addsimps [Forall_Conc,ext_and_act]) 1);
+by (REPEAT (etac conjE 1));
+(* assumption schA *)
+by (dres_inst_tac [("x","schA"),
+ ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
+by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
+by (forw_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
+ba 1;
+
+(* assumption Forall schA *)
+by (dres_inst_tac [("s","schA"),
+ ("P","Forall (%x.x:act A)")] subst 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
+
+(* case x:actions(asig_of A) & x: actions(asig_of B) *)
+
+
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac 1);
+
+by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+(* eliminate introduced subgoal 2 *)
+be ForallQFilterPnil 2;
+ba 2;
+by (Fast_tac 2);
+
+(* bring in divide Seq for s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+
+(* subst divide_Seq in conclusion, but only at the righest occurence *)
by (res_inst_tac [("t","schA")] ssubst 1);
back();
back();
back();
ba 1;
-by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite] 1);
+
+(* f A (tw iA) = tw ~eA *)
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+ not_ext_is_int_or_not_act]) 1);
+(* rewrite assumption forall and schB *)
+by (rotate_tac 13 1);
+by (asm_full_simp_tac (!simpset addsimps [ext_and_act]) 1);
+
+(* divide_Seq for schB2 *)
+by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
by (REPEAT (etac conjE 1));
-(* reduce trace_takes from n to strictly smaller k *)
-by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext]) 1);
-br take_reduction 1;
-ba 1;
-(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
-by (rotate_tac ~10 1);
-(* assumption forall and schB *)
-by (asm_full_simp_tac (!simpset addsimps [tconc_cong,forall_cons,forall_tconc,ext_and_act]) 1);
(* assumption schA *)
by (dres_inst_tac [("x","schA"),
- ("g","tfilter`(plift (%a. a : actions (asig_of A)))`rs")] lemma22 1);
+ ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+
+(* f A (tw iB schB2) = nil *)
+by (asm_full_simp_tac (!simpset addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
+ FilterPTakewhileQnil,intA_is_not_actB]) 1);
+
+
+(* reduce trace_takes from n to strictly smaller k *)
+br take_reduction 1;
+br refl 1;
+br refl 1;
+
+(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
+
+(* assumption schB *)
+by (dres_inst_tac [("x","y2"),
+ ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
ba 1;
-by (asm_full_simp_tac (!simpset addsimps [tfiltertconc,not_int_is_ext,tfilterPtakewhileQ]) 1);
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
+
+(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
+by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
+by (forw_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
+ba 1;
+by (dres_inst_tac [("sch","y2"),("P","%a. a:int B")] LastActExtsmall1 1);
+
+(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
+by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile]) 1);
+
+(* case x~:A & x:B *)
+(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
+by (case_tac "x:act B" 1);
+by (Fast_tac 1);
+
+(* case x~:A & x~:B *)
+(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
+by (rotate_tac ~9 1);
+(* reduce forall assumption from tr to (x>>rs) *)
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
by (REPEAT (etac conjE 1));
-(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
-by (dres_inst_tac [("sch","schA"),("P","plift (%a. a : internals (asig_of A))")] LastActExtsmall1 1);
-by (dres_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
-ba 1;
+by (fast_tac (!claset addSIs [ext_is_act]) 1);
+
+qed"FilterAmksch_is_schA";
+
+
+
+(*--------------------------------------------------------------------------- *)
+
+ section" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof";
+
+(* --------------------------------------------------------------------------- *)
+
+
+
+goal thy "!! A B. [| compat_ioas A B; compat_ioas 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 &\
+\ LastActExtsch A schA & LastActExtsch B schB \
+\ --> Filter (%a.a:act B)`(mksch A B`tr`schA`schB) = schB";
+
+by (strip_tac 1);
+br seq.take_lemma 1;
+br mp 1;
+ba 2;
+back();back();back();back();
+by (res_inst_tac [("x","schA")] spec 1);
+by (res_inst_tac [("x","schB")] spec 1);
+by (res_inst_tac [("x","tr")] spec 1);
+by (thin_tac' 5 1);
+br less_induct 1;
+by (REPEAT (rtac allI 1));
+ren "tr schB schA" 1;
+by (strip_tac 1);
+by (REPEAT (etac conjE 1));
+
+by (case_tac "Forall (%x. x:act A & x~:act B) tr" 1);
+
+br (seq_take_lemma RS iffD2 RS spec) 1;
+by (thin_tac' 5 1);
+
+
+by (case_tac "Finite tr" 1);
+
+(* both sides of this equation are nil *)
+by (subgoal_tac "schB=nil" 1);
+by (Asm_simp_tac 1);
+(* first side: mksch = nil *)
+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 (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil],
+ !simpset)) 1);
+
+(* case ~ Finite tr *)
+
+(* both sides of this equation are UU *)
+by (subgoal_tac "schB=UU" 1);
+by (Asm_simp_tac 1);
+(* first side: mksch = UU *)
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU,
+ (finiteR_mksch RS mp COMP rev_contrapos),
+ ForallAnBmksch],
+ !simpset)) 1);
+(* schA = UU *)
+by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
+by (Asm_simp_tac 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU],
+ !simpset)) 1);
+
+(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
+
+bd divide_Seq3 1;
+
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+by (hyp_subst_tac 1);
+
+(* bring in lemma reduceB_mksch *)
+by (forw_inst_tac [("y","schB"),("x","schA"),("A","A"),("B","B")] reduceB_mksch 1);
+by (REPEAT (atac 1));
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+
+(* use reduceB_mksch to rewrite conclusion *)
+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);
+be ForallQFilterPnil 2;
+ba 2;
+by (Fast_tac 2);
+
+(* Now real recursive step follows (in x) *)
+
+by (Asm_full_simp_tac 1);
+by (case_tac "x:act B" 1);
+by (case_tac "x~:act A" 1);
+by (rotate_tac ~2 1);
by (Asm_full_simp_tac 1);
-(* case x:actions(asig_of A) & x: actions(asig_of B) *)
-by (rotate_tac ~2 1);
-by (asm_full_simp_tac (!simpset addsimps [filter_rep]) 1);
-by (subgoal_tac "tfilter`(plift (%a. a : actions (asig_of A) & a : externals (asig_of B)))`y1=nil" 1);
+by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1);
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
-by (thin_tac' 1 1);
(* eliminate introduced subgoal 2 *)
-be forallQfilterPnil 2;
+be ForallQFilterPnil 2;
ba 2;
by (Fast_tac 2);
-(* f A (tw iA) = tw iA *)
-by (simp_tac (HOL_min_ss addsimps [filterPtakewhileQ,int_is_act]) 1);
+(* bring in divide Seq for s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
-by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace] 1);
-(* subst divide_trace in conlcusion, but only at the righest occurence *)
-by (res_inst_tac [("t","schA")] ssubst 1);
+(* subst divide_Seq in conclusion, but only at the righest occurence *)
+by (res_inst_tac [("t","schB")] ssubst 1);
back();
back();
back();
ba 1;
-by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite] 1);
+
+(* reduce trace_takes from n to strictly smaller k *)
+br take_reduction 1;
+
+(* f B (tw iB) = tw ~eB *)
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+ not_ext_is_int_or_not_act]) 1);
+br refl 1;
+by (asm_full_simp_tac (!simpset addsimps [int_is_act,
+ not_ext_is_int_or_not_act]) 1);
+by (rotate_tac ~11 1);
+
+(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
+
+(* assumption Forall tr *)
+by (asm_full_simp_tac (!simpset addsimps [Forall_Conc]) 1);
+(* assumption schA *)
+by (asm_full_simp_tac (!simpset addsimps [Forall_Conc,ext_and_act]) 1);
by (REPEAT (etac conjE 1));
-(* tidy up *)
-by (thin_tac' 12 1);
-by (thin_tac' 12 1);
-by (thin_tac' 14 1);
-by (thin_tac' 14 1);
-by (rotate_tac ~8 1);
-(* rewrite assumption forall and schB *)
-by (asm_full_simp_tac (!simpset addsimps [tconc_cong,forall_cons,forall_tconc,ext_and_act]) 1);
-(* divide_trace for schB2 *)
-by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_trace) 1);
-by (forw_inst_tac [("y","y2")](sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite) 1);
+(* assumption schB *)
+by (dres_inst_tac [("x","schB"),
+ ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
+by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
+by (forw_inst_tac [("sch1.0","x1")] LastActExtsmall2 1);
+ba 1;
+
+(* assumption Forall schB *)
+by (dres_inst_tac [("s","schB"),
+ ("P","Forall (%x.x:act B)")] subst 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
+
+(* case x:actions(asig_of A) & x: actions(asig_of B) *)
+
+
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac 1);
+
+by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+(* eliminate introduced subgoal 2 *)
+be ForallQFilterPnil 2;
+ba 2;
+by (Fast_tac 2);
+
+(* bring in divide Seq for s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
by (REPEAT (etac conjE 1));
-by (rotate_tac ~6 1);
-(* assumption schA *)
-by (dres_inst_tac [("x","schA"),
- ("g","tfilter`(plift (%a. a : actions (asig_of A)))`rs")] lemma22 1);
-ba 1;
-by (asm_full_simp_tac (!simpset addsimps [tfiltertconc,not_int_is_ext,tfilterPtakewhileQ]) 1);
-by (REPEAT (etac conjE 1));
-(* f A (tw iB schB2) = nil *)
-(* good luck: intAisnotextB is not looping *)
-by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext,tfilterPtakewhileQ,intAisnotextB]) 1);
-(* reduce trace_takes from n to strictly smaller k *)
-by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext]) 1);
-br take_reduction 1;
+(* subst divide_Seq in conclusion, but only at the righest occurence *)
+by (res_inst_tac [("t","schB")] ssubst 1);
+back();
+back();
+back();
ba 1;
-(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
-(* assumption schB *)
-by (dres_inst_tac [("x","y2"),
- ("g","tfilter`(plift (%a. a : actions (asig_of B)))`rs")] lemma22 1);
+
+(* f B (tw iB) = tw ~eB *)
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+ not_ext_is_int_or_not_act]) 1);
+
+(* rewrite assumption forall and schB *)
+by (rotate_tac 13 1);
+by (asm_full_simp_tac (!simpset addsimps [ext_and_act]) 1);
+
+(* divide_Seq for schB2 *)
+by (forw_inst_tac [("y","x2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
+by (REPEAT (etac conjE 1));
+(* assumption schA *)
+by (dres_inst_tac [("x","schB"),
+ ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
ba 1;
-(* FIX: hey wonder: why does loopin rule for y2 here rewrites !!!!!!!!!!!!!!!!!!!!!!!!*)
-by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext,tfilterPtakewhileQ,intAisnotextB]) 1);
-by (REPEAT (etac conjE 1));
-(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
-by (dres_inst_tac [("sch","schA"),("P","plift (%a. a : internals (asig_of A))")] LastActExtsmall1 1);
-by (dres_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+
+(* f B (tw iA schA2) = nil *)
+by (asm_full_simp_tac (!simpset addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
+ FilterPTakewhileQnil,intA_is_not_actB]) 1);
+
+
+(* reduce trace_takes from n to strictly smaller k *)
+br take_reduction 1;
+br refl 1;
+br refl 1;
+
+(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
+
+(* assumption schA *)
+by (dres_inst_tac [("x","x2"),
+ ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
ba 1;
-by (dres_inst_tac [("sch","y2"),("P","plift (%a. a : internals (asig_of B))")] LastActExtsmall1 1);
-by (Asm_full_simp_tac 1);
-
-(* case x~:A & x:B *)
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
+
+(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
+by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
+by (forw_inst_tac [("sch1.0","x1")] LastActExtsmall2 1);
+ba 1;
+by (dres_inst_tac [("sch","x2"),("P","%a. a:int A")] LastActExtsmall1 1);
+
+(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
+by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile]) 1);
+
+(* case x~:B & x:A *)
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
-by (case_tac "x:actions(asig_of B)" 1);
+by (case_tac "x:act A" 1);
by (Fast_tac 1);
-(* case x~:A & x~:B *)
-(* cannot occur because of assumption: forall (a:ext A | a:ext B) *)
-by (rotate_tac ~8 1);
-(* reduce forall assumption from tr to (Def x ## rs) *)
-by (asm_full_simp_tac (!simpset addsimps [forall_cons,forall_tconc]) 1);
+(* case x~:B & x~:A *)
+(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
+by (rotate_tac ~9 1);
+(* reduce forall assumption from tr to (x>>rs) *)
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
by (REPEAT (etac conjE 1));
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
by (fast_tac (!claset addSIs [ext_is_act]) 1);
-qed"filterAmksch_is_schA";
-
-
-goal thy "!! tr. [|compat_ioas A B ; compat_ioas B A ;\
-\ forall (plift (%x.x:externals(asig_of (A||B)))) tr ; \
-\ tfilter`(plift (%a.a:externals(asig_of A)))`schA = tfilter`(plift (%a.a:actions(asig_of A)))`tr ;\
-\ tfilter`(plift (%a.a:externals(asig_of B)))`schB = tfilter`(plift (%a.a:actions(asig_of B)))`tr ;\
-\ LastActExtsch schA ; LastActExtsch schB |] \
-\ ==> tfilter`(plift (%a.a:actions(asig_of A)))`(mksch A B`tr`schA`schB) = schA";
-
-br trace.take_lemma 1;
-by (asm_simp_tac (!simpset addsimps [filterAmksch_is_schA]) 1);
-qed"filterAmkschschA";
+qed"FilterBmksch_is_schB";
(* ------------------------------------------------------------------ *)
-(* COMPOSITIONALITY on TRACE Level *)
-(* Main Theorem *)
+ section"COMPOSITIONALITY on TRACE Level -- Main Theorem";
(* ------------------------------------------------------------------ *)
goal thy
-"!! A B. [| compat_ioas A B; compat_ioas B A; \
+"!! A B. [| IOA A; IOA B; compat_ioas A B; compat_ioas B A; \
\ is_asig(asig_of A); is_asig(asig_of B)|] \
-\ ==> traces(A||B) = \
-\ { tr.(Filter (%a.a:act A)`tr : traces A &\
-\ Filter (%a.a:act B)`tr : traces B &\
-\ Forall (%x. x:ext(A||B)) tr) }";
+\ ==> tr: traces(A||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);
-br set_ext 1;
by (safe_tac set_cs);
(* ==> *)
@@ -681,54 +982,40 @@
(* <== *)
-(* replace schA and schB by cutsch(schA) and cutsch(schB) *)
+(* replace schA and schB by Cut(schA) and Cut(schB) *)
by (dtac exists_LastActExtsch 1);
ba 1;
by (dtac exists_LastActExtsch 1);
ba 1;
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
+(* Schedules of A(B) have only actions of A(B) *)
+bd scheds_in_sig 1;
+ba 1;
+bd scheds_in_sig 1;
+ba 1;
+ren "h1 h2 schA schB" 1;
(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
we need here *)
-by (res_inst_tac [("x","mksch A B`tr`schb`schc")] bexI 1);
+by (res_inst_tac [("x","mksch A B`tr`schA`schB")] bexI 1);
(* External actions of mksch are just the oracle *)
-by (asm_full_simp_tac (!simpset addsimps [filterA_mksch_is_tr]) 1);
+by (asm_full_simp_tac (!simpset addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1);
(* mksch is a schedule -- use compositionality on sch-level *)
by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 1);
-
- das hier loopt: ForallPForallQ, ext_is_act,ForallAorB_mksch]) 1);
+by (asm_full_simp_tac (!simpset addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
+be ForallAorB_mksch 1;
+be ForallPForallQ 1;
+be ext_is_act 1;
+qed"compositionality_tr";
-*)
-(* -------------------------------------------------------------------------------
- Other useful things
- -------------------------------------------------------------------------------- *)
-
-
-(* Lemmata not needed yet
-goal Trace.thy "!!x. nil<<x ==> nil=x";
-by (res_inst_tac [("x","x")] trace.cases 1);
-by (hyp_subst_tac 1);
-by (etac antisym_less 1);
-by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
-qed"nil_less_is_nil";
-
-
-*)
-
-
-
-
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/CompoTraces.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
@@ -53,38 +53,11 @@
rules
-(* FIX: x:actions S is further assumption, see Asig.ML: how to fulfill this in proofs ? *)
-not_ext_is_int_FIX
- "[|is_asig S|] ==> (x~:externals S) = (x: internals S)"
-
-(* FIX: should be more general , something like subst *)
-lemma12
-"[| f << (g x) ; (x= (h x)) |] ==> f << g (h x)"
-
-(* FIX: as above, should be done more intelligent *)
-lemma22
-"[| (f x) = y >> g ; x = h x |] ==> (f (h x)) = y >> g"
-
-Finite_Conc
- "Finite (x @@ y) = (Finite x & Finite y)"
finiteR_mksch
"Finite (mksch A B`tr`x`y) --> Finite tr"
-finiteL_mksch
- "[| Finite tr;
- Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr;
- Filter (%a. a:ext B)`y = Filter (%a. a:actB)`tr;
- Forall (%x. x:ext (A||B)) tr |]
- ==> Finite (mksch A B`tr`x`y)"
-reduce_mksch
- "[| Finite bs; 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"
end
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Compositionality.ML
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1997 TU Muenchen
@@ -7,17 +7,80 @@
*)
+
+goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
+auto();
+qed"compatibility_consequence3";
+
+
+goal thy
+"!! A B. [| compat_ioas A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
+\ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
+br ForallPFilterQR 1;
+ba 2;
+br compatibility_consequence3 1;
+by (REPEAT (asm_full_simp_tac (!simpset
+ addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
+qed"Filter_actAisFilter_extA";
+
+
+(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A)
+ or even better A||B= B||A, FIX *)
+
+goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
+auto();
+qed"compatibility_consequence4";
+
+goal thy
+"!! A B. [| compat_ioas A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
+\ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
+br ForallPFilterQR 1;
+ba 2;
+br compatibility_consequence4 1;
+by (REPEAT (asm_full_simp_tac (!simpset
+ addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
+qed"Filter_actAisFilter_extA2";
+
+
+(* -------------------------------------------------------------------------- *)
+ section " Main Compositionality Theorem ";
+(* -------------------------------------------------------------------------- *)
+
+
+
goal thy "!! A1 A2 B1 B2. \
-\ [| is_asig (asig_of A1); is_asig (asig_of A2); \
+\ [| IOA A1; IOA A2; IOA B1; IOA B2;\
+\ is_asig (asig_of A1); is_asig (asig_of A2); \
\ is_asig (asig_of B1); is_asig (asig_of B2); \
-\ compat_ioas A1 B1; compat_ioas B1 A1; compat_ioas A2 B2; compat_ioas B2 A2; \
+\ compat_ioas A1 B1; compat_ioas A2 B2; \
\ A1 =<| A2; \
\ B1 =<| B2 |] \
\ ==> (A1 || B1) =<| (A2 || B2)";
+
+by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1);
+by (forw_inst_tac [("A2","A2")] (compat_commute RS iffD1) 1);
by (asm_full_simp_tac (!simpset addsimps [ioa_implements_def,
- inputs_of_par,outputs_of_par]) 1);
+ inputs_of_par,outputs_of_par,externals_of_par]) 1);
+by (safe_tac set_cs);
+by (asm_full_simp_tac (!simpset addsimps [compositionality_tr]) 1);
+by (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2" 1);
+by (asm_full_simp_tac (!simpset addsimps [externals_def]) 2);
+by (REPEAT (etac conjE 1));
+(* rewrite with proven subgoal *)
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
+by (safe_tac set_cs);
+
+(* 2 goals, the 3rd has been solved automatically *)
+(* 1: Filter A2 x : traces A2 *)
+by (dres_inst_tac [("A","traces A1")] subsetD 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA]) 1);
+(* 2: Filter B2 x : traces B2 *)
+by (dres_inst_tac [("A","traces B1")] subsetD 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA2]) 1);
+qed"compositionality";
-by (safe_tac set_cs);
-by (asm_full_simp_tac (!simpset addsimps [compotraces]) 1);
+
--- a/src/HOLCF/IOA/meta_theory/Compositionality.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy Wed May 21 15:08:52 1997 +0200
@@ -1,21 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Compositionality.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1997 TU Muenchen
Compositionality of I/O automata
*)
-Compositionality = CompoTraces +
-
-rules
-
-compotraces
-"[| compat_ioas A B; compat_ioas B A;
- is_asig(asig_of A); is_asig(asig_of B)|]
- ==> traces(A||B) =
- {tr. (Filter (%a.a:act A)`tr : traces A &
- Filter (%a.a:act B)`tr : traces B &
- Forall (%x. x:ext(A||B)) tr)}"
-
-end
\ No newline at end of file
+Compositionality = Automata + Traces + CompoTraces
--- a/src/HOLCF/IOA/meta_theory/IOA.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/IOA.ML Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/IOA.thy
- ID:
+ ID: $Id$
Author: Olaf Mueller
Copyright 1996,1997 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/IOA.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/IOA.thy Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/IOA.thy
- ID:
+ ID: $Id$
Author: Olaf Mueller
Copyright 1996,1997 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/RefCorrectness.ML
- ID: $$
+ ID: $Id$
Author: Olaf Mueller
Copyright 1996 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy
- ID: $$
+ ID: $Id$
Author: Olaf Mueller
Copyright 1996 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/RefMappings.ML
- ID: $$
+ ID: $Id$
Author: Olaf Mueller
Copyright 1996 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/RefMappings.thy
- ID: $$
+ ID: $Id$
Author: Olaf Mueller
Copyright 1996 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/Seq.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Seq.ML
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
@@ -16,6 +16,9 @@
Addsimps [UU_neq_nil];
+
+
+
(* ------------------------------------------------------------------------------------- *)
@@ -224,7 +227,7 @@
by (REPEAT (Asm_full_simp_tac 1));
qed"sconc_cons";
-Addsimps [sconc_nil, sconc_UU,sconc_cons];
+Addsimps [sconc_nil,sconc_UU,sconc_cons];
(* ----------------------------------------------------------- *)
@@ -311,7 +314,7 @@
(* ------------------------------------------------------------------------------------- *)
-section "scons";
+section "scons, nil";
goal thy
"!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
@@ -320,6 +323,15 @@
auto();
qed"scons_inject_eq";
+goal thy "!!x. nil<<x ==> nil=x";
+by (res_inst_tac [("x","x")] seq.cases 1);
+by (hyp_subst_tac 1);
+by (etac antisym_less 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac 1);
+qed"nil_less_is_nil";
(* ------------------------------------------------------------------------------------- *)
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Seq.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Sequence.ML
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
@@ -67,13 +67,6 @@
(* Conc *)
(* ---------------------------------------------------------------- *)
-goal thy "UU @@ y =UU";
-by (Simp_tac 1);
-qed"Conc_UU";
-
-goal thy "nil @@ y =y";
-by (Simp_tac 1);
-qed"Conc_nil";
goal thy "(x>>xs) @@ y = x>>(xs @@y)";
by (simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -215,7 +208,7 @@
Map_UU,Map_nil,Map_cons,
Forall_UU,Forall_nil,Forall_cons,
Last_UU,Last_nil,Last_cons,
- Conc_UU,Conc_nil,Conc_cons,
+ Conc_cons,
Takewhile_UU, Takewhile_nil, Takewhile_cons,
Dropwhile_UU, Dropwhile_nil, Dropwhile_cons,
Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons];
@@ -281,6 +274,7 @@
br Def_not_UU 1;
qed"Cons_not_UU";
+
goal thy "~(a>>x) << UU";
by (rtac notI 1);
by (dtac antisym_less 1);
@@ -299,6 +293,10 @@
by (resolve_tac seq.rews 1);
qed"Cons_not_nil";
+goal thy "nil ~= a>>s";
+by (simp_tac (!simpset addsimps [Cons_def2]) 1);
+qed"Cons_not_nil2";
+
goal thy "(a>>s = b>>t) = (a = b & s = t)";
by (simp_tac (HOL_ss addsimps [Cons_def2]) 1);
by (stac (hd lift.inject RS sym) 1);
@@ -325,9 +323,17 @@
by (simp_tac (!simpset addsimps [Cons_def]) 1);
qed"seq_take_Cons";
-Addsimps [Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
+Addsimps [Cons_not_nil2,Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil];
+(* Instead of adding UU_neq_Cons every equation UU~=x could be changed to x~=UU *)
+goal thy "UU ~= x>>xs";
+by (res_inst_tac [("s1","UU"),("t1","x>>xs")] (sym RS rev_contrapos) 1);
+by (REPEAT (Simp_tac 1));
+qed"UU_neq_Cons";
+
+Addsimps [UU_neq_Cons];
+
(* ----------------------------------------------------------------------------------- *)
@@ -399,6 +405,61 @@
qed"Finite_Cons";
Addsimps [Finite_Cons];
+goal thy "!! x. Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
+by (Seq_Finite_induct_tac 1);
+qed"FiniteConc_1";
+
+goal thy "!! z. Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
+by (Seq_Finite_induct_tac 1);
+(* nil*)
+by (strip_tac 1);
+by (Seq_case_simp_tac "x" 1);
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+(* cons *)
+by (strip_tac 1);
+by (Seq_case_simp_tac "x" 1);
+by (Seq_case_simp_tac "y" 1);
+by (SELECT_GOAL (auto_tac (!claset,!simpset))1);
+by (eres_inst_tac [("x","sa")] allE 1);
+by (eres_inst_tac [("x","y")] allE 1);
+by (Asm_full_simp_tac 1);
+qed"FiniteConc_2";
+
+goal thy "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)";
+by (rtac iffI 1);
+be (FiniteConc_2 RS spec RS spec RS mp) 1;
+br refl 1;
+br (FiniteConc_1 RS mp) 1;
+auto();
+qed"FiniteConc";
+
+Addsimps [FiniteConc];
+
+
+goal thy "!! s. Finite s ==> Finite (Map f`s)";
+by (Seq_Finite_induct_tac 1);
+qed"FiniteMap1";
+
+goal thy "!! s. Finite s ==> ! t. (s = Map f`t) --> Finite t";
+by (Seq_Finite_induct_tac 1);
+by (strip_tac 1);
+by (Seq_case_simp_tac "t" 1);
+by (Asm_full_simp_tac 1);
+(* main case *)
+auto();
+by (Seq_case_simp_tac "t" 1);
+by (Asm_full_simp_tac 1);
+qed"FiniteMap2";
+
+goal thy "Finite (Map f`s) = Finite s";
+auto();
+be (FiniteMap2 RS spec RS mp) 1;
+br refl 1;
+be FiniteMap1 1;
+qed"Map2Finite";
+
(* ------------------------------------------------------------------------------------ *)
@@ -408,6 +469,21 @@
by (Seq_Finite_induct_tac 1);
qed"Conc_cong";
+goal thy "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z";
+by (Seq_induct_tac "x" [] 1);
+qed"Conc_assoc";
+
+goal thy "s@@ nil = s";
+by (res_inst_tac[("x","s")] seq.ind 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed"nilConc";
+
+Addsimps [nilConc];
+
+
(* ------------------------------------------------------------------------------------ *)
section "Last";
@@ -456,10 +532,33 @@
by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
qed"MapFilter";
+goal thy "nil = (Map f`s) --> s= nil";
+by (Seq_case_simp_tac "s" 1);
+qed"nilMap";
+
+goal thy "Forall P (Map f`s) --> Forall (P o f) s";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+auto();
+qed"ForallMap1";
+
+
+goal thy "Forall (P o f) s --> Forall P (Map f`s) ";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+auto();
+qed"ForallMap2";
+
+(* FIX: should be proved directly. Therefore adm lemma for equalitys on _bools_ has
+ to be added to !simpset *)
+goal thy "Forall P (Map f`s) = Forall (P o f) s";
+auto();
+be (ForallMap1 RS mp) 1;
+be (ForallMap2 RS mp) 1;
+qed"ForallMap";
+
(* ------------------------------------------------------------------------------------ *)
-section "Forall, Conc";
+section "Forall";
goal thy "Forall P ys & (! x. P x --> Q x) \
@@ -477,6 +576,46 @@
by (Seq_Finite_induct_tac 1);
qed"Forall_Conc";
+Addsimps [Forall_Conc];
+
+goal thy "Forall P s --> Forall P (TL`s)";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+qed"ForallTL1";
+
+bind_thm ("ForallTL",ForallTL1 RS mp);
+
+goal thy "Forall P s --> Forall P (Dropwhile Q`s)";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+qed"ForallDropwhile1";
+
+bind_thm ("ForallDropwhile",ForallDropwhile1 RS mp);
+
+
+(* only admissible in t, not if done in s *)
+
+goal thy "! s. Forall P s --> t<<s --> Forall P t";
+by (Seq_induct_tac "t" [Forall_def,sforall_def] 1);
+by (strip_tac 1);
+by (Seq_case_simp_tac "sa" 1);
+by (Asm_full_simp_tac 1);
+auto();
+qed"Forall_prefix";
+
+bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
+
+
+goal thy "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
+auto();
+qed"Forall_postfixclosed";
+
+
+goal thy "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q`tr = Filter R`tr";
+by (Seq_induct_tac "tr" [Forall_def,sforall_def] 1);
+qed"ForallPFilterQR1";
+
+bind_thm("ForallPFilterQR",allI RS (conjI RS (ForallPFilterQR1 RS mp)));
+
(* ------------------------------------------------------------------------------------- *)
@@ -487,38 +626,29 @@
by (simp_tac (!simpset addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
qed"ForallPFilterP";
-(* FIX: holds also in other direction, then equal to forallPfilterP *)
+(* holds also in other direction, then equal to forallPfilterP *)
goal thy "Forall P x --> Filter P`x = x";
by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
qed"ForallPFilterPid1";
-val ForallPFilterPid = standard (ForallPFilterPid1 RS mp);
+bind_thm(" ForallPFilterPid",ForallPFilterPid1 RS mp);
-(* holds also in <-- direction. FIX: prove that also *)
-
-goal thy "!! P. Finite ys & Forall (%x. ~P x) ys \
-\ --> Filter P`ys = nil ";
-by (res_inst_tac[("x","ys")] Seq_induct 1);
-(* adm *)
-(* FIX: cont tfinite behandeln *)
-br adm_all 1;
-(* base cases *)
-by (Simp_tac 1);
-by (Simp_tac 1);
-(* main case *)
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+(* holds also in other direction *)
+goal thy "!! ys . Finite ys ==> \
+\ Forall (%x. ~P x) ys --> Filter P`ys = nil ";
+by (Seq_Finite_induct_tac 1);
qed"ForallnPFilterPnil1";
-val ForallnPFilterPnil = standard (conjI RS (ForallnPFilterPnil1 RS mp));
+bind_thm ("ForallnPFilterPnil",ForallnPFilterPnil1 RS mp);
-(* FIX: holds also in <== direction *)
+(* holds also in other direction *)
goal thy "!! P. ~Finite ys & Forall (%x. ~P x) ys \
\ --> Filter P`ys = UU ";
by (res_inst_tac[("x","ys")] Seq_induct 1);
(* adm *)
-(* FIX: cont ~tfinite behandeln *)
+(* FIX: cont ~Finite behandeln *)
br adm_all 1;
(* base cases *)
by (Simp_tac 1);
@@ -527,7 +657,43 @@
by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
qed"ForallnPFilterPUU1";
-val ForallnPFilterPUU = standard (conjI RS (ForallnPFilterPUU1 RS mp));
+bind_thm ("ForallnPFilterPUU",conjI RS (ForallnPFilterPUU1 RS mp));
+
+
+(* inverse of ForallnPFilterPnil *)
+
+goal thy "!! ys . Filter P`ys = nil --> \
+\ (Forall (%x. ~P x) ys & Finite ys)";
+by (res_inst_tac[("x","ys")] Seq_induct 1);
+(* adm *)
+(* FIX: cont Finite behandeln *)
+br adm_all 1;
+(* base cases *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"FilternPnilForallP1";
+
+bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp);
+
+(* inverse of ForallnPFilterPUU *)
+(* FIX: will not be admissable, search other way of proof *)
+
+goal thy "!! P. Filter P`ys = UU --> \
+\ (Forall (%x. ~P x) ys & ~Finite ys)";
+by (res_inst_tac[("x","ys")] Seq_induct 1);
+(* adm *)
+(* FIX: cont ~Finite behandeln *)
+br adm_all 1;
+(* base cases *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"FilternPUUForallP1";
+
+bind_thm ("FilternPUUForallP",FilternPUUForallP1 RS mp);
goal thy "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
@@ -582,7 +748,33 @@
Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
FilterPTakewhileQnil,FilterPTakewhileQid];
+goal thy "Takewhile P`(Takewhile P`s) = Takewhile P`s";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+qed"Takewhile_idempotent";
+goal thy "Forall P s --> Takewhile (%x.Q x | (~P x))`s = Takewhile Q`s";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+qed"ForallPTakewhileQnP";
+
+goal thy "Forall P s --> Dropwhile (%x.Q x | (~P x))`s = Dropwhile Q`s";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+qed"ForallPDropwhileQnP";
+
+Addsimps [ForallPTakewhileQnP RS mp, ForallPDropwhileQnP RS mp];
+
+
+goal thy "Forall P s --> Takewhile P`(s @@ t) = s @@ (Takewhile P`t)";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+qed"TakewhileConc1";
+
+bind_thm("TakewhileConc",TakewhileConc1 RS mp);
+
+goal thy "!! s.Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
+by (Seq_Finite_induct_tac 1);
+qed"DropwhileConc1";
+
+bind_thm("DropwhileConc",DropwhileConc1 RS mp);
(* ----------------------------------------------------------------------------------- *)
@@ -590,7 +782,7 @@
(*
section "admissibility";
-goal thy "adm(%x.~Finite x)";
+goal thy "adm(%x.Finite x)";
br admI 1;
bd spec 1;
be contrapos 1;
@@ -662,7 +854,7 @@
auto();
qed"divide_Seq3";
-Addsimps [FilterPQ,FilterConc,Conc_cong,Forall_Conc];
+Addsimps [FilterPQ,FilterConc,Conc_cong];
(* ------------------------------------------------------------------------------------- *)
@@ -676,22 +868,24 @@
auto();
qed"seq_take_lemma";
-(*
-
-goal thy "Finite x & (! k. k < n --> seq_take k`y1 = seq_take k`y2) \
-\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2))";
-br less_induct 1;
+goal thy
+" ! n. ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \
+\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2)))";
+by (Seq_induct_tac "x" [] 1);
+by (strip_tac 1);
+by (res_inst_tac [("n","n")] natE 1);
+auto();
+by (res_inst_tac [("n","n")] natE 1);
+auto();
+qed"take_reduction1";
-goal thy "!!x. Finite x ==> \
-\ ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \
-\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2)))";
-by (Seq_Finite_induct_tac 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+goal thy "!! n.[| x=y; s=t;!! k.k<n ==> seq_take k`y1 = seq_take k`y2|] \
+\ ==> seq_take n`(x @@ (s>>y1)) = seq_take n`(y @@ (t>>y2))";
-
+by (auto_tac (!claset addSIs [take_reduction1 RS spec RS mp],!simpset));
qed"take_reduction";
-*)
+
goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
\ !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
@@ -763,6 +957,62 @@
by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
qed"take_lemma_less_induct";
+
+(*
+
+goal thy
+"!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \
+\ !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m`(f t h1 h2) = seq_take m`(g t h1 h2);\
+\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) h1 h2|] \
+\ ==> seq_take n`(f (s1 @@ y>>s2) h1 h2) \
+\ = seq_take n`(g (s1 @@ y>>s2) h1 h2) |] \
+\ ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)";
+by (strip_tac 1);
+br seq.take_lemma 1;
+br mp 1;
+ba 2;
+by (res_inst_tac [("x","h2a")] spec 1);
+by (res_inst_tac [("x","h1a")] spec 1);
+by (res_inst_tac [("x","x")] spec 1);
+br less_induct 1;
+br allI 1;
+by (case_tac "Forall Q xa" 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
+ !simpset)) 1);
+by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+qed"take_lemma_less_induct";
+
+
+
+goal thy
+"!! Q. [|!! s. Forall Q s ==> P ((f s) = (g s)) ; \
+\ !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m`(f t) = seq_take m`(g t));\
+\ Forall Q s1; Finite s1; ~ Q y|] \
+\ ==> P (seq_take n`(f (s1 @@ y>>s2)) \
+\ = seq_take n`(g (s1 @@ y>>s2))) |] \
+\ ==> P ((f x)=(g x))";
+
+by (res_inst_tac [("t","f x = g x"),
+ ("s","!n. seq_take n`(f x) = seq_take n`(g x)")] subst 1);
+br seq_take_lemma 1;
+
+wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden.....
+
+
+FIX
+
+br less_induct 1;
+br allI 1;
+by (case_tac "Forall Q xa" 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
+ !simpset)) 1);
+by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+qed"take_lemma_less_induct";
+
+
+*)
+
+
goal thy
"!! Q. [| A UU ==> (f UU) = (g UU) ; \
\ A nil ==> (f nil) = (g nil) ; \
@@ -822,10 +1072,8 @@
goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
by (res_inst_tac [("A1","%x.True")
- ,("Q1","%x.~(P x & Q x)")]
+ ,("Q1","%x.~(P x & Q x)"),("x1","s")]
(take_lemma_induct RS mp) 1);
-(* FIX: rule always needs a back: eliminate *)
-back();
(* FIX: better support for A = %.True *)
by (Fast_tac 3);
by (asm_full_simp_tac (!simpset addsimps [Filter_lemma1]) 1);
@@ -840,12 +1088,11 @@
(* Alternative Proof of MapConc *)
(* --------------------------------------------------------------- *)
-Delsimps [MapConc];
+
goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
by (res_inst_tac [("A1","%x.True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
auto();
qed"MapConc_takelemma";
-Addsimps [MapConc];
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Sequence.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
@@ -83,9 +83,4 @@
adm_all "adm f"
-take_reduction
- "[| Finite x; !! k. k < n ==> seq_take k`y1 = seq_take k`y2 |]
- ==> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2))"
-
-
end
\ No newline at end of file
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Wed May 21 15:08:52 1997 +0200
@@ -1,11 +1,214 @@
(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1997 TU Muenchen
-Some properties about cut(ex), defined as follows:
+Some properties about (Cut ex), defined as follows:
-For every execution ex there is another shorter execution cut(ex)
+For every execution ex there is another shorter execution (Cut ex)
that has the same trace as ex, but its schedule ends with an external action.
-*)
\ No newline at end of file
+*)
+
+
+
+
+(* ---------------------------------------------------------------- *)
+ section "oraclebuild rewrite rules";
+(* ---------------------------------------------------------------- *)
+
+
+bind_thm ("oraclebuild_unfold", fix_prover2 thy oraclebuild_def
+"oraclebuild P = (LAM s t. case t of \
+\ nil => nil\
+\ | x##xs => \
+\ (case x of\
+\ Undef => UU\
+\ | Def y => (Takewhile (%a.~ P a)`s)\
+\ @@ (y>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`xs))\
+\ )\
+\ )");
+
+goal thy "oraclebuild P`sch`UU = UU";
+by (stac oraclebuild_unfold 1);
+by (Simp_tac 1);
+qed"oraclebuild_UU";
+
+goal thy "oraclebuild P`sch`nil = nil";
+by (stac oraclebuild_unfold 1);
+by (Simp_tac 1);
+qed"oraclebuild_nil";
+
+goal thy "oraclebuild P`s`(x>>t) = \
+\ (Takewhile (%a.~ P a)`s) \
+\ @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";
+br trans 1;
+by (stac oraclebuild_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"oraclebuild_cons";
+
+
+
+
+(* ---------------------------------------------------------------- *)
+ section "Cut rewrite rules";
+(* ---------------------------------------------------------------- *)
+
+goalw thy [Cut_def]
+"!! s. [| Forall (%a.~ P a) s; Finite s|] \
+\ ==> Cut P s =nil";
+by (subgoal_tac "Filter P`s = nil" 1);
+by (asm_simp_tac (!simpset addsimps [oraclebuild_nil]) 1);
+br ForallQFilterPnil 1;
+by (REPEAT (atac 1));
+qed"Cut_nil";
+
+goalw thy [Cut_def]
+"!! s. [| Forall (%a.~ P a) s; ~Finite s|] \
+\ ==> Cut P s =UU";
+by (subgoal_tac "Filter P`s= UU" 1);
+by (asm_simp_tac (!simpset addsimps [oraclebuild_UU]) 1);
+br ForallQFilterPUU 1;
+by (REPEAT (atac 1));
+qed"Cut_UU";
+
+goalw thy [Cut_def]
+"!! s. [| P t; Forall (%x.~ P x) ss; Finite ss|] \
+\ ==> Cut P (ss @@ (t>> rs)) \
+\ = ss @@ (t >> Cut P rs)";
+
+by (asm_full_simp_tac (!simpset addsimps [ForallQFilterPnil,oraclebuild_cons,
+ TakewhileConc,DropwhileConc]) 1);
+qed"Cut_Cons";
+
+
+(* ---------------------------------------------------------------- *)
+ section "Cut lemmas for main theorem";
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "Filter P`s = Filter P`(Cut P s)";
+
+by (res_inst_tac [("A1","%x.True")
+ ,("Q1","%x.~ P x"), ("x1","s")]
+ (take_lemma_induct RS mp) 1);
+by (Fast_tac 3);
+by (case_tac "Finite s" 1);
+by (asm_full_simp_tac (!simpset addsimps [Cut_nil,
+ ForallQFilterPnil]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Cut_UU,
+ ForallQFilterPUU]) 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
+auto();
+qed"FilterCut";
+
+
+goal thy "Cut P (Cut P s) = (Cut P s)";
+
+by (res_inst_tac [("A1","%x.True")
+ ,("Q1","%x.~ P x"), ("x1","s")]
+ (take_lemma_less_induct RS mp) 1);
+by (Fast_tac 3);
+by (case_tac "Finite s" 1);
+by (asm_full_simp_tac (!simpset addsimps [Cut_nil,
+ ForallQFilterPnil]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Cut_UU,
+ ForallQFilterPUU]) 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
+br take_reduction 1;
+auto();
+qed"Cut_idemp";
+
+
+goal thy "Map f`(Cut (P o f) s) = Cut P (Map f`s)";
+
+by (res_inst_tac [("A1","%x.True")
+ ,("Q1","%x.~ P (f x)"), ("x1","s")]
+ (take_lemma_less_induct RS mp) 1);
+by (Fast_tac 3);
+by (case_tac "Finite s" 1);
+by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1);
+br (Cut_nil RS sym) 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
+(* csae ~ Finite s *)
+by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
+br (Cut_UU RS sym) 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,MapConc,
+ ForallMap,FiniteMap1,o_def]) 1);
+br take_reduction 1;
+auto();
+qed"MapCut";
+
+
+
+
+(* ---------------------------------------------------------------- *)
+ section "Main Cut Theorem";
+(* ---------------------------------------------------------------- *)
+
+
+
+goalw thy [schedules_def,has_schedule_def]
+ "!! sch. [|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|] \
+\ ==> ? sch. sch : schedules A & \
+\ tr = Filter (%a.a:ext A)`sch &\
+\ LastActExtsch A sch";
+
+by (safe_tac set_cs);
+by (res_inst_tac [("x","filter_act`(Cut (%a.fst a:ext A) (snd ex))")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (pair_tac "ex" 1);
+by (safe_tac set_cs);
+by (res_inst_tac [("x","(x,Cut (%a.fst a:ext A) y)")] exI 1);
+by (Asm_simp_tac 1);
+
+(* Subgoal 1: Lemma: propagation of execution through Cut *)
+
+by (asm_full_simp_tac (!simpset addsimps [execThruCut]) 1);
+
+(* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *)
+
+by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
+br (rewrite_rule [o_def] MapCut) 2;
+by (asm_full_simp_tac (!simpset addsimps [FilterCut RS sym]) 1);
+
+(* Subgoal 3: Lemma: Cut idempotent *)
+
+by (simp_tac (!simpset addsimps [LastActExtsch_def,filter_act_def]) 1);
+by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
+br (rewrite_rule [o_def] MapCut) 2;
+by (asm_full_simp_tac (!simpset addsimps [Cut_idemp]) 1);
+qed"exists_LastActExtsch";
+
+
+(* ---------------------------------------------------------------- *)
+ section "Further Cut lemmas";
+(* ---------------------------------------------------------------- *)
+
+goalw thy [LastActExtsch_def]
+ "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = nil |] \
+\ ==> sch=nil";
+bd FilternPnilForallP 1;
+be conjE 1;
+bd Cut_nil 1;
+ba 1;
+by (Asm_full_simp_tac 1);
+qed"LastActExtimplnil";
+
+goalw thy [LastActExtsch_def]
+ "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = UU |] \
+\ ==> sch=UU";
+bd FilternPUUForallP 1;
+be conjE 1;
+bd Cut_UU 1;
+ba 1;
+by (Asm_full_simp_tac 1);
+qed"LastActExtimplUU";
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed May 21 15:08:52 1997 +0200
@@ -1,11 +1,11 @@
(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1997 TU Muenchen
-Some properties about cut(ex), defined as follows:
+Some properties about (Cut ex), defined as follows:
-For every execution ex there is another shorter execution cut(ex)
+For every execution ex there is another shorter execution (Cut ex)
that has the same trace as ex, but its schedule ends with an external action.
*)
@@ -15,40 +15,48 @@
consts
- LastActExtsch ::"'a Seq => bool"
- cutsch ::"'a Seq => 'a Seq"
+ LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"
+ LastActExtsch ::"('a,'s)ioa => 'a Seq => bool"
+ Cut ::"('a => bool) => 'a Seq => 'a Seq"
+
+ oraclebuild ::"('a => bool) => 'a Seq -> 'a Seq -> 'a Seq"
defs
LastActExtsch_def
- "LastActExtsch sch == (cutsch sch = sch)"
+ "LastActExtsch A sch == (Cut (%x.x: ext A) sch = sch)"
+
+LastActExtex_def
+ "LastActExtex A ex == LastActExtsch A (filter_act`ex)"
+
+Cut_def
+ "Cut P s == oraclebuild P`s`(Filter P`s)"
+
+oraclebuild_def
+ "oraclebuild P == (fix`(LAM h s t. case t of
+ nil => nil
+ | x##xs =>
+ (case x of
+ Undef => UU
+ | Def y => (Takewhile (%x.~P x)`s)
+ @@ (y>>(h`(TL`(Dropwhile (%x.~ P x)`s))`xs))
+ )
+ ))"
+
+
rules
-exists_LastActExtsch
- "[|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|]
- ==> ? sch. sch : schedules A &
- tr = Filter (%a.a:ext A)`sch &
- LastActExtsch sch"
-
-(* FIX: 1. LastActExtsch should have argument A also?
- 2. use equality: (I) f P x =UU <-> (II) (fa ~P x) & ~finite(x) to prove it for (II) instead *)
-LastActExtimplUU
- "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = UU |]
- ==> sch=UU"
-
-(* FIX: see above *)
-LastActExtimplnil
- "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = nil |]
- ==> sch=nil"
+execThruCut
+ "is_execution_fragment A (s,ex) ==> is_execution_fragment A (s,Cut P ex)"
LastActExtsmall1
- "LastActExtsch sch ==> LastActExtsch (TL`(Dropwhile P`sch))"
+ "LastActExtsch A sch ==> LastActExtsch A (TL`(Dropwhile P`sch))"
LastActExtsmall2
- "[| Finite sch1; LastActExtsch (sch1 @@ sch2) |] ==> LastActExtsch (sch2)"
+ "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
end
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Wed May 21 15:08:52 1997 +0200
@@ -1,12 +1,12 @@
(* Title: HOLCF/IOA/meta_theory/Traces.ML
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
Theorems about Executions and Traces of I/O automata in HOLCF.
*)
-
+Delsimps (ex_simps @ all_simps);
val exec_rws = [executions_def,is_execution_fragment_def];
@@ -150,3 +150,58 @@
by (REPEAT (Asm_simp_tac 1));
qed"has_trace_def2";
+
+(* -------------------------------------------------------------------------------- *)
+
+section "signatures and executions, schedules";
+
+
+(* All executions of A have only actions of A. This is only true because of the
+ predicate state_trans (part of the predicate IOA): We have no dependent types.
+ For executions of parallel automata this assumption is not needed, as in par_def
+ this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
+
+goal thy
+ "!! A. IOA A ==> \
+\ ! s. is_execution_fragment A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)";
+
+by (pair_induct_tac "xs" [is_execution_fragment_def,Forall_def,sforall_def] 1);
+(* main case *)
+ren "ss a t" 1;
+by (safe_tac set_cs);
+by (REPEAT (asm_full_simp_tac (!simpset addsimps [ioa_def,state_trans_def]) 1));
+qed"execfrag_in_sig";
+
+goal thy
+ "!! A.[| IOA A; x:executions A |] ==> \
+\ Forall (%a.a:act A) (filter_act`(snd x))";
+
+by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (pair_tac "x" 1);
+br (execfrag_in_sig RS spec RS mp) 1;
+auto();
+qed"exec_in_sig";
+
+goalw thy [schedules_def,has_schedule_def]
+ "!! A.[| IOA A; x:schedules A |] ==> \
+\ Forall (%a.a:act A) x";
+
+by (fast_tac (!claset addSIs [exec_in_sig]) 1);
+qed"scheds_in_sig";
+
+
+(* -------------------------------------------------------------------------------- *)
+
+section "executions are prefix closed";
+
+(* only admissible in y, not if done in x !! *)
+goal thy "!x s. is_execution_fragment A (s,x) & y<<x --> is_execution_fragment A (s,y)";
+by (pair_induct_tac "y" [is_execution_fragment_def] 1);
+by (strip_tac 1);
+by (Seq_case_simp_tac "xa" 1);
+by (pair_tac "a" 1);
+auto();
+qed"execfrag_prefixclosed";
+
+bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
+
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
(* Title: HOLCF/IOA/meta_theory/Traces.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1996 TU Muenchen
@@ -7,7 +7,7 @@
*)
-Traces = Automata + Sequence +
+Traces = Sequence + Automata +
default term