src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy

isabelle update_cartouches -c -t;

(*  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>

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 =
  EVERY'[Seq_induct_tac ctxt sch defs,
         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 asigs)
        ]

end
\<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 (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 \<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