--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Dec 31 12:37:16 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,541 +0,0 @@
-(* Title: HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
- Author: Olaf Müller
-*)
-
-section \<open>Compositionality on Schedule level\<close>
-
-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))\<leadsto>
- (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
- else
- (case HD$exA of
- UU => UU
- | Def a =>
- (y,(snd a,t))\<leadsto>(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))\<leadsto>(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))\<leadsto>
- (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))\<leadsto>(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))\<leadsto>(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\<leadsto>sch)$exA$exB) s t =
- (x,snd a,t) \<leadsto> (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\<leadsto>sch)$exA$exB) s t =
- (x,s,snd b) \<leadsto> (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\<leadsto>sch)$exA$exB) s t =
- (x,snd a,snd b) \<leadsto>
- (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 \<open>mkex\<close>
-
-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\<leadsto>sch) (s,a\<leadsto>exA) (t,exB) =
- ((s,t), (x,snd a,t) \<leadsto> snd (mkex A B sch (snd a,exA) (t,exB)))"
-apply (simp (no_asm) add: mkex_def)
-apply (cut_tac exA = "a\<leadsto>exA" in mkex2_cons_1)
-apply auto
-done
-
-lemma mkex_cons_2: "[| x~:act A; x:act B |]
- ==> mkex A B (x\<leadsto>sch) (s,exA) (t,b\<leadsto>exB) =
- ((s,t), (x,s,snd b) \<leadsto> snd (mkex A B sch (s,exA) (snd b,exB)))"
-apply (simp (no_asm) add: mkex_def)
-apply (cut_tac exB = "b\<leadsto>exB" in mkex2_cons_2)
-apply auto
-done
-
-lemma mkex_cons_3: "[| x:act A; x:act B |]
- ==> mkex A B (x\<leadsto>sch) (s,a\<leadsto>exA) (t,b\<leadsto>exB) =
- ((s,t), (x,snd a,snd b) \<leadsto> snd (mkex A B sch (snd a,exA) (snd b,exB)))"
-apply (simp (no_asm) add: mkex_def)
-apply (cut_tac exB = "b\<leadsto>exB" and exA = "a\<leadsto>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 \<open>COMPOSITIONALITY on SCHEDULE Level\<close>
-
-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 \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
-done
-
-
-(* --------------------------------------------------------------------- *)
-(* Schedules of A\<parallel>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\<parallel>B) (s,xs)
- --> Forall (%x. x:act (A\<parallel>B)) (filter_act$xs)"
-
-apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
- @{thm sforall_def}] 1\<close>)
-(* 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\<parallel>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 \<open>Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
- @{thm sforall_def}, @{thm mkex_def}] 1\<close>)
-
-(* main case *)
-(* splitting into 4 cases according to a:A, a:B *)
-apply auto
-
-(* Case y:A, y:B *)
-apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
-(* 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\<leadsto>ss<< UU(nil), using theorems
- Cons_not_less_UU and Cons_not_less_nil *)
-apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
-(* Case exA=a\<leadsto>x, exB=b\<leadsto>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 \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
-apply simp
-
-(* Case y~:A, y:B *)
-apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
-apply simp
-
-(* Case y~:A, y~:B *)
-apply (simp add: asig_of_par actions_asig_comp)
-done
-
-
-(* generalizing the proof above to a proof method *)
-
-ML \<open>
-fun mkex_induct_tac ctxt sch exA exB =
- EVERY'[Seq_induct_tac ctxt sch @{thms Filter_def Forall_def sforall_def mkex_def stutter_def},
- asm_full_simp_tac ctxt,
- SELECT_GOAL
- (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
- Seq_case_simp_tac ctxt exA,
- Seq_case_simp_tac ctxt exB,
- asm_full_simp_tac ctxt,
- Seq_case_simp_tac ctxt exA,
- asm_full_simp_tac ctxt,
- Seq_case_simp_tac ctxt exB,
- asm_full_simp_tac ctxt,
- asm_full_simp_tac (ctxt addsimps @{thms asig_of_par actions_asig_comp})
- ]
-\<close>
-
-method_setup mkex_induct = \<open>
- Scan.lift (Args.name -- Args.name -- Args.name)
- >> (fn ((sch, exA), exB) => fn ctxt => SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
-\<close>
-
-
-(*---------------------------------------------------------------------------
- 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\<parallel>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))))"
- by (mkex_induct sch exA exB)
-
-lemma stutter_mkex_on_A: "[|
- Forall (%x. x:act (A\<parallel>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\<parallel>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))))"
- by (mkex_induct sch exA exB)
-
-
-lemma stutter_mkex_on_B: "[|
- Forall (%x. x:act (A\<parallel>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\<parallel>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)"
- by (mkex_induct sch exB exA)
-
-(*---------------------------------------------------------------------------
- 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 \<open>Seq_induct_tac @{context} "y" [] 1\<close>)
-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\<parallel>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 \<open>pair_tac @{context} "exA" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
-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\<parallel>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 *)
- by (mkex_induct sch exA exB)
-
-
-(*---------------------------------------------------------------------------
- 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\<parallel>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 \<open>pair_tac @{context} "exA" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
-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 \<parallel> 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 \<parallel>B))
- (snd (mkex A B sch (s,exA) (t,exB)))"
- by (mkex_induct sch exA exB)
-
-
-(* ------------------------------------------------------------------ *)
-(* COMPOSITIONALITY on SCHEDULE Level *)
-(* Main Theorem *)
-(* ------------------------------------------------------------------ *)
-
-lemma compositionality_sch:
-"(sch : schedules (A\<parallel>B)) =
- (Filter (%a. a:act A)$sch : schedules A &
- Filter (%a. a:act B)$sch : schedules B &
- Forall (%x. x:act (A\<parallel>B)) sch)"
-apply (simp 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 \<open>pair_tac @{context} "ex" 1\<close>)
-apply (erule conjE)
-apply (simp add: sch_actions_in_AorB)
-
-(* <== *)
-
-(* mkex is exactly the construction of exA\<parallel>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 \<open>pair_tac @{context} "exA" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
-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 \<open>pair_tac @{context} "exA" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
-apply (simp add: mkex_actions_in_AorB)
-done
-
-
-subsection \<open>COMPOSITIONALITY on SCHEDULE Level -- for Modules\<close>
-
-lemma compositionality_sch_modules:
- "Scheds (A\<parallel>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