src/HOLCF/IOA/meta_theory/CompoScheds.thy

maintain PolyML.Compiler.printInAlphabeticalOrder in polyml.ML;

(*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
    ID:         $Id$
    Author:     Olaf Müller
*)

header {* Compositionality on Schedule level *}

theory CompoScheds
imports CompoExecs
begin

consts

 mkex     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
              ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution"
 mkex2    ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
              ('a,'s)pairs -> ('a,'t)pairs ->
              ('s => 't => ('a,'s*'t)pairs)"
 par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module"


defs

mkex_def:
  "mkex A B sch exA exB ==
       ((fst exA,fst exB),
        (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"

mkex2_def:
  "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
             )
         )
       ))))"

par_scheds_def:
  "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)"


declare surjective_pairing [symmetric, simp]


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 (rule 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 "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 "xs" [thm "is_exec_frag_def", thm "Forall_def",
  thm "sforall_def"] 1 *})
(* main case *)
apply (tactic "safe_tac set_cs")
apply (auto 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 "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 (tactic "safe_tac set_cs")

(* Case y:A, y:B *)
apply (tactic {* Seq_case_simp_tac "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 "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 "exA" 1 *})
apply simp

(* Case y~:A, y:B *)
apply (tactic {* Seq_case_simp_tac "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 sch exA exB =
    EVERY1[Seq_induct_tac sch defs,
           SIMPSET' asm_full_simp_tac,
           SELECT_GOAL (safe_tac set_cs),
           Seq_case_simp_tac exA,
           Seq_case_simp_tac exB,
           SIMPSET' asm_full_simp_tac,
           Seq_case_simp_tac exA,
           SIMPSET' asm_full_simp_tac,
           Seq_case_simp_tac exB,
           SIMPSET' asm_full_simp_tac,
           SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps asigs))
          ]

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 "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 "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 "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 "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 "exA" 1 *})
apply (tactic {* pair_tac "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 "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 "exA" 1 *})
apply (tactic {* pair_tac "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 "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 (tactic "safe_tac set_cs")
(* ==> *)
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 "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 "exA" 1 *})
apply (tactic {* pair_tac "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 "exA" 1 *})
apply (tactic {* pair_tac "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_ext)
apply (simp add: compositionality_sch actions_of_par)
done


declare compoex_simps [simp del]
declare composch_simps [simp del]

end