--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Sat Nov 27 16:08:10 2010 -0800
@@ -0,0 +1,553 @@
+(* Title: HOLCF/IOA/meta_theory/CompoScheds.thy
+ Author: Olaf Müller
+*)
+
+header {* Compositionality on Schedule level *}
+
+theory CompoScheds
+imports CompoExecs
+begin
+
+definition
+ mkex2 :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
+ ('a,'s)pairs -> ('a,'t)pairs ->
+ ('s => 't => ('a,'s*'t)pairs)" where
+ "mkex2 A B = (fix$(LAM h sch exA exB. (%s t. case sch of
+ nil => nil
+ | x##xs =>
+ (case x of
+ UU => UU
+ | Def y =>
+ (if y:act A then
+ (if y:act B then
+ (case HD$exA of
+ UU => UU
+ | Def a => (case HD$exB of
+ UU => UU
+ | Def b =>
+ (y,(snd a,snd b))>>
+ (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
+ else
+ (case HD$exA of
+ UU => UU
+ | Def a =>
+ (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t)
+ )
+ else
+ (if y:act B then
+ (case HD$exB of
+ UU => UU
+ | Def b =>
+ (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b))
+ else
+ UU
+ )
+ )
+ ))))"
+
+definition
+ mkex :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
+ ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" where
+ "mkex A B sch exA exB =
+ ((fst exA,fst exB),
+ (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
+
+definition
+ par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module" where
+ "par_scheds SchedsA SchedsB =
+ (let schA = fst SchedsA; sigA = snd SchedsA;
+ schB = fst SchedsB; sigB = snd SchedsB
+ in
+ ( {sch. Filter (%a. a:actions sigA)$sch : schA}
+ Int {sch. Filter (%a. a:actions sigB)$sch : schB}
+ Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
+ asig_comp sigA sigB))"
+
+
+subsection "mkex rewrite rules"
+
+
+lemma mkex2_unfold:
+"mkex2 A B = (LAM sch exA exB. (%s t. case sch of
+ nil => nil
+ | x##xs =>
+ (case x of
+ UU => UU
+ | Def y =>
+ (if y:act A then
+ (if y:act B then
+ (case HD$exA of
+ UU => UU
+ | Def a => (case HD$exB of
+ UU => UU
+ | Def b =>
+ (y,(snd a,snd b))>>
+ (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
+ else
+ (case HD$exA of
+ UU => UU
+ | Def a =>
+ (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t)
+ )
+ else
+ (if y:act B then
+ (case HD$exB of
+ UU => UU
+ | Def b =>
+ (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b))
+ else
+ UU
+ )
+ )
+ )))"
+apply (rule trans)
+apply (rule fix_eq2)
+apply (simp only: mkex2_def)
+apply (rule beta_cfun)
+apply simp
+done
+
+lemma mkex2_UU: "(mkex2 A B$UU$exA$exB) s t = UU"
+apply (subst mkex2_unfold)
+apply simp
+done
+
+lemma mkex2_nil: "(mkex2 A B$nil$exA$exB) s t= nil"
+apply (subst mkex2_unfold)
+apply simp
+done
+
+lemma mkex2_cons_1: "[| x:act A; x~:act B; HD$exA=Def a|]
+ ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
+ (x,snd a,t) >> (mkex2 A B$sch$(TL$exA)$exB) (snd a) t"
+apply (rule trans)
+apply (subst mkex2_unfold)
+apply (simp add: Consq_def If_and_if)
+apply (simp add: Consq_def)
+done
+
+lemma mkex2_cons_2: "[| x~:act A; x:act B; HD$exB=Def b|]
+ ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
+ (x,s,snd b) >> (mkex2 A B$sch$exA$(TL$exB)) s (snd b)"
+apply (rule trans)
+apply (subst mkex2_unfold)
+apply (simp add: Consq_def If_and_if)
+apply (simp add: Consq_def)
+done
+
+lemma mkex2_cons_3: "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|]
+ ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
+ (x,snd a,snd b) >>
+ (mkex2 A B$sch$(TL$exA)$(TL$exB)) (snd a) (snd b)"
+apply (rule trans)
+apply (subst mkex2_unfold)
+apply (simp add: Consq_def If_and_if)
+apply (simp add: Consq_def)
+done
+
+declare mkex2_UU [simp] mkex2_nil [simp] mkex2_cons_1 [simp]
+ mkex2_cons_2 [simp] mkex2_cons_3 [simp]
+
+
+subsection {* mkex *}
+
+lemma mkex_UU: "mkex A B UU (s,exA) (t,exB) = ((s,t),UU)"
+apply (simp add: mkex_def)
+done
+
+lemma mkex_nil: "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)"
+apply (simp add: mkex_def)
+done
+
+lemma mkex_cons_1: "[| x:act A; x~:act B |]
+ ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) =
+ ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))"
+apply (simp (no_asm) add: mkex_def)
+apply (cut_tac exA = "a>>exA" in mkex2_cons_1)
+apply auto
+done
+
+lemma mkex_cons_2: "[| x~:act A; x:act B |]
+ ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =
+ ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))"
+apply (simp (no_asm) add: mkex_def)
+apply (cut_tac exB = "b>>exB" in mkex2_cons_2)
+apply auto
+done
+
+lemma mkex_cons_3: "[| x:act A; x:act B |]
+ ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) =
+ ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))"
+apply (simp (no_asm) add: mkex_def)
+apply (cut_tac exB = "b>>exB" and exA = "a>>exA" in mkex2_cons_3)
+apply auto
+done
+
+declare mkex2_UU [simp del] mkex2_nil [simp del]
+ mkex2_cons_1 [simp del] mkex2_cons_2 [simp del] mkex2_cons_3 [simp del]
+
+lemmas composch_simps = mkex_UU mkex_nil mkex_cons_1 mkex_cons_2 mkex_cons_3
+
+declare composch_simps [simp]
+
+
+subsection {* COMPOSITIONALITY on SCHEDULE Level *}
+
+subsubsection "Lemmas for ==>"
+
+(* --------------------------------------------------------------------- *)
+(* Lemma_2_1 : tfilter(ex) and filter_act are commutative *)
+(* --------------------------------------------------------------------- *)
+
+lemma lemma_2_1a:
+ "filter_act$(Filter_ex2 (asig_of A)$xs)=
+ Filter (%a. a:act A)$(filter_act$xs)"
+
+apply (unfold filter_act_def Filter_ex2_def)
+apply (simp (no_asm) add: MapFilter o_def)
+done
+
+
+(* --------------------------------------------------------------------- *)
+(* Lemma_2_2 : State-projections do not affect filter_act *)
+(* --------------------------------------------------------------------- *)
+
+lemma lemma_2_1b:
+ "filter_act$(ProjA2$xs) =filter_act$xs &
+ filter_act$(ProjB2$xs) =filter_act$xs"
+apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
+done
+
+
+(* --------------------------------------------------------------------- *)
+(* Schedules of A||B have only A- or B-actions *)
+(* --------------------------------------------------------------------- *)
+
+(* very similar to lemma_1_1c, but it is not checking if every action element of
+ an ex is in A or B, but after projecting it onto the action schedule. Of course, this
+ is the same proposition, but we cannot change this one, when then rather lemma_1_1c *)
+
+lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs)
+ --> Forall (%x. x:act (A||B)) (filter_act$xs)"
+
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
+ @{thm sforall_def}] 1 *})
+(* main case *)
+apply auto
+apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
+done
+
+
+subsubsection "Lemmas for <=="
+
+(*---------------------------------------------------------------------------
+ Filtering actions out of mkex(sch,exA,exB) yields the oracle sch
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+lemma Mapfst_mkex_is_sch: "! exA exB s t.
+ Forall (%x. x:act (A||B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
+ --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"
+
+apply (tactic {* Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
+ @{thm sforall_def}, @{thm mkex_def}] 1 *})
+
+(* main case *)
+(* splitting into 4 cases according to a:A, a:B *)
+apply auto
+
+(* Case y:A, y:B *)
+apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
+(* Case exA=UU, Case exA=nil*)
+(* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA
+ is used! --> to generate a contradiction using ~a>>ss<< UU(nil), using theorems
+ Cons_not_less_UU and Cons_not_less_nil *)
+apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
+(* Case exA=a>>x, exB=b>>y *)
+(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case,
+ as otherwise mkex_cons_3 would not be rewritten without use of rotate_tac: then tactic
+ would not be generally applicable *)
+apply simp
+
+(* Case y:A, y~:B *)
+apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
+apply simp
+
+(* Case y~:A, y:B *)
+apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
+apply simp
+
+(* Case y~:A, y~:B *)
+apply (simp add: asig_of_par actions_asig_comp)
+done
+
+
+(* generalizing the proof above to a tactic *)
+
+ML {*
+
+local
+ val defs = [@{thm Filter_def}, @{thm Forall_def}, @{thm sforall_def}, @{thm mkex_def},
+ @{thm stutter_def}]
+ val asigs = [@{thm asig_of_par}, @{thm actions_asig_comp}]
+in
+
+fun mkex_induct_tac ctxt sch exA exB =
+ let val ss = simpset_of ctxt in
+ EVERY1[Seq_induct_tac ctxt sch defs,
+ asm_full_simp_tac ss,
+ SELECT_GOAL (safe_tac (global_claset_of @{theory Fun})),
+ Seq_case_simp_tac ctxt exA,
+ Seq_case_simp_tac ctxt exB,
+ asm_full_simp_tac ss,
+ Seq_case_simp_tac ctxt exA,
+ asm_full_simp_tac ss,
+ Seq_case_simp_tac ctxt exB,
+ asm_full_simp_tac ss,
+ asm_full_simp_tac (ss addsimps asigs)
+ ]
+ end
+
+end
+*}
+
+
+(*---------------------------------------------------------------------------
+ Projection of mkex(sch,exA,exB) onto A stutters on A
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+lemma stutterA_mkex: "! exA exB s t.
+ Forall (%x. x:act (A||B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
+ --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
+
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
+done
+
+
+lemma stutter_mkex_on_A: "[|
+ Forall (%x. x:act (A||B)) sch ;
+ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
+ Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
+ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))"
+
+apply (cut_tac stutterA_mkex)
+apply (simp add: stutter_def ProjA_def mkex_def)
+apply (erule allE)+
+apply (drule mp)
+prefer 2 apply (assumption)
+apply simp
+done
+
+
+(*---------------------------------------------------------------------------
+ Projection of mkex(sch,exA,exB) onto B stutters on B
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+lemma stutterB_mkex: "! exA exB s t.
+ Forall (%x. x:act (A||B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
+ --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
+done
+
+
+lemma stutter_mkex_on_B: "[|
+ Forall (%x. x:act (A||B)) sch ;
+ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
+ Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
+ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))"
+apply (cut_tac stutterB_mkex)
+apply (simp add: stutter_def ProjB_def mkex_def)
+apply (erule allE)+
+apply (drule mp)
+prefer 2 apply (assumption)
+apply simp
+done
+
+
+(*---------------------------------------------------------------------------
+ Filter of mkex(sch,exA,exB) to A after projection onto A is exA
+ -- using zip$(proj1$exA)$(proj2$exA) instead of exA --
+ -- because of admissibility problems --
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+lemma filter_mkex_is_exA_tmp: "! exA exB s t.
+ Forall (%x. x:act (A||B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
+ --> 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)"
+apply (tactic {* mkex_induct_tac @{context} "sch" "exB" "exA" *})
+done
+
+(*---------------------------------------------------------------------------
+ zip$(proj1$y)$(proj2$y) = y (using the lift operations)
+ lemma for admissibility problems
+ --------------------------------------------------------------------------- *)
+
+lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
+apply (tactic {* Seq_induct_tac @{context} "y" [] 1 *})
+done
+
+
+(*---------------------------------------------------------------------------
+ filter A$sch = proj1$ex --> zip$(filter A$sch)$(proj2$ex) = ex
+ lemma for eliminating non admissible equations in assumptions
+ --------------------------------------------------------------------------- *)
+
+lemma trick_against_eq_in_ass: "!! sch ex.
+ Filter (%a. a:act AB)$sch = filter_act$ex
+ ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)"
+apply (simp add: filter_act_def)
+apply (rule Zip_Map_fst_snd [symmetric])
+done
+
+(*---------------------------------------------------------------------------
+ Filter of mkex(sch,exA,exB) to A after projection onto A is exA
+ using the above trick
+ --------------------------------------------------------------------------- *)
+
+
+lemma filter_mkex_is_exA: "!!sch exA exB.
+ [| Forall (%a. a:act (A||B)) sch ;
+ Filter (%a. a:act A)$sch = filter_act$(snd exA) ;
+ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
+ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
+apply (simp add: ProjA_def Filter_ex_def)
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (rule conjI)
+apply (simp (no_asm) add: mkex_def)
+apply (simplesubst trick_against_eq_in_ass)
+back
+apply assumption
+apply (simp add: filter_mkex_is_exA_tmp)
+done
+
+
+(*---------------------------------------------------------------------------
+ Filter of mkex(sch,exA,exB) to B after projection onto B is exB
+ -- using zip$(proj1$exB)$(proj2$exB) instead of exB --
+ -- because of admissibility problems --
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+lemma filter_mkex_is_exB_tmp: "! exA exB s t.
+ Forall (%x. x:act (A||B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
+ --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =
+ Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
+
+(* notice necessary change of arguments exA and exB *)
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
+done
+
+
+(*---------------------------------------------------------------------------
+ Filter of mkex(sch,exA,exB) to A after projection onto B is exB
+ using the above trick
+ --------------------------------------------------------------------------- *)
+
+
+lemma filter_mkex_is_exB: "!!sch exA exB.
+ [| Forall (%a. a:act (A||B)) sch ;
+ Filter (%a. a:act A)$sch = filter_act$(snd exA) ;
+ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
+ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
+apply (simp add: ProjB_def Filter_ex_def)
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (rule conjI)
+apply (simp (no_asm) add: mkex_def)
+apply (simplesubst trick_against_eq_in_ass)
+back
+apply assumption
+apply (simp add: filter_mkex_is_exB_tmp)
+done
+
+(* --------------------------------------------------------------------- *)
+(* mkex has only A- or B-actions *)
+(* --------------------------------------------------------------------- *)
+
+
+lemma mkex_actions_in_AorB: "!s t exA exB.
+ Forall (%x. x : act (A || B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
+ --> Forall (%x. fst x : act (A ||B))
+ (snd (mkex A B sch (s,exA) (t,exB)))"
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
+done
+
+
+(* ------------------------------------------------------------------ *)
+(* COMPOSITIONALITY on SCHEDULE Level *)
+(* Main Theorem *)
+(* ------------------------------------------------------------------ *)
+
+lemma compositionality_sch:
+"(sch : schedules (A||B)) =
+ (Filter (%a. a:act A)$sch : schedules A &
+ Filter (%a. a:act B)$sch : schedules B &
+ Forall (%x. x:act (A||B)) sch)"
+apply (simp (no_asm) add: schedules_def has_schedule_def)
+apply auto
+(* ==> *)
+apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex) " in bexI)
+prefer 2
+apply (simp add: compositionality_ex)
+apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b)
+apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex) " in bexI)
+prefer 2
+apply (simp add: compositionality_ex)
+apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
+apply (simp add: executions_def)
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (erule conjE)
+apply (simp add: sch_actions_in_AorB)
+
+(* <== *)
+
+(* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
+ we need here *)
+apply (rename_tac exA exB)
+apply (rule_tac x = "mkex A B sch exA exB" in bexI)
+(* mkex actions are just the oracle *)
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (simp add: Mapfst_mkex_is_sch)
+
+(* mkex is an execution -- use compositionality on ex-level *)
+apply (simp add: compositionality_ex)
+apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (simp add: mkex_actions_in_AorB)
+done
+
+
+subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *}
+
+lemma compositionality_sch_modules:
+ "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)"
+
+apply (unfold Scheds_def par_scheds_def)
+apply (simp add: asig_of_par)
+apply (rule set_eqI)
+apply (simp add: compositionality_sch actions_of_par)
+done
+
+
+declare compoex_simps [simp del]
+declare composch_simps [simp del]
+
+end