Theory MultiNdet

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff
 *
 * This file       : Multi-non-deterministic choice
 *
 * Copyright (c) 2023 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)


chapter ‹The MultiNdet Operator›

theory MultiNdet
  imports Patch PreliminaryWork
begin



section ‹Definition›



text ‹Defining the multi operator of \<^const>‹Ndet› requires more work than with \<^const>‹Det›
      since there is no neutral element. 
      We will first build a version on \<^typ>‹'α list› that we will generalize to \<^typ>‹'α set›.›

fun MultiNdet_list :: ‹['a list, 'a ⇒ 'b process] ⇒ 'b process›
  where ‹MultiNdet_list   []    P = STOP›
  |     ‹MultiNdet_list (a # l) P = fold (λx r. r ⊓ P x) l (P a)› 


syntax       "_MultiNdet_list" :: ‹[pttrn,'a set,'b process] ⇒ 'b process›
                                  (‹(3⨅⇩l _∈_. / _)› 76)
translations  "⨅⇩l p ∈ l. P "  ⇌ "CONST MultiNdet_list l (λp. P)"


interpretation MultiNdet: comp_fun_idem where f=‹λx r. r ⊓ P x›
  unfolding comp_fun_idem_def comp_fun_commute_def
            comp_fun_idem_axioms_def comp_def
  by (metis Ndet_commute Ndet_assoc Ndet_id)


lemma MultiNdet_list_set:
  ‹set L = set L' ⟹ MultiNdet_list L P = MultiNdet_list L' P› 
  apply (cases L, simp_all)
proof -
  fix a  l
  assume * : ‹insert a (set l) = set L'› and  ** : ‹L = a # l› 
  then obtain a' l' where *** : ‹L' = a' # l'› by (metis insertI1 list.set_cases)
  note * = *[simplified ***, simplified]
  have a0: ‹MultiNdet_list L P =
            Finite_Set.fold (λx r. r ⊓ P x) (P a) (set L - {a})›
    by (metis ** List.finite_set MultiNdet.fold_fun_left_comm
              MultiNdet.fold_insert_idem2 MultiNdet.fold_rec
              MultiNdet.fold_set_fold MultiNdet_list.simps(2)
              insert_iff list.simps(15) Ndet_id set_removeAll)
  have a11: ‹a' ∈ set L›
   and a12: ‹a ≠ a' ⟹ insert a' (set L - {a, a'}) = set L - {a}›
    by (auto simp add: * **)
  hence a2: ‹Finite_Set.fold (λx r. r ⊓ P x) (P a) (insert a' (set L - {a, a'})) = 
             Finite_Set.fold (λx r. r ⊓ P x) (P a ⊓ P a') (set L - {a, a'})› 
    by (subst MultiNdet.fold_insert_idem2, simp_all)
  have a3:‹MultiNdet_list L' P =
           Finite_Set.fold (λx r. r ⊓ P x) (P a') (set L' - {a'})› 
    by (metis *** List.finite_set MultiNdet.fold_fun_left_comm
              MultiNdet.fold_insert_idem2 MultiNdet.fold_rec
              MultiNdet.fold_set_fold MultiNdet_list.simps(2)
              insert_iff list.simps(15) Ndet_id set_removeAll)
  have a41: ‹a ∈ set L'›
   and a42: ‹a ≠ a' ⟹ insert a (set L' - {a, a'}) = set L' - {a'}› 
    using * *** by auto
  hence a5: ‹Finite_Set.fold (λx r. r ⊓ P x) (P a') (insert a (set L' - {a, a'}))
           = Finite_Set.fold (λx r. r ⊓ P x) (P a ⊓ P a') (set L' - {a, a'})›
    by (subst MultiNdet.fold_insert_idem2, simp_all add: Ndet_commute)
  have a6: ‹(set L - {a, a'}) = (set L' - {a, a'})›
    using * ** *** by force
  from  * ** *** a0 a11 a12 a2 a3 a41 a42 a5 a6 
  show ‹fold (λx r. r ⊓ P x) l (P a) = MultiNdet_list L' P›
    by (metis MultiNdet_list.simps(2) list.simps(15))
qed


definition MultiNdet :: ‹['a set, 'a ⇒ 'b process] ⇒ 'b process›
  where    ‹MultiNdet A P = MultiNdet_list (SOME L. set L = A) P› 


syntax "_MultiNdet" :: ‹[pttrn, 'a set, 'b process] ⇒ 'b process› (‹(3⨅ _∈_. / _)› 76)
translations "⨅ p ∈ A. P" ⇌ "CONST MultiNdet A (λp. P)"



section ‹First Properties›

lemma MultiNdet_rec0[simp]: ‹(⨅ p ∈ {}. P p) = STOP›
  by(simp add: MultiNdet_def)


lemma MultiNdet_rec1[simp]: ‹(⨅ p ∈ {a}. P p) = P a›
  unfolding MultiNdet_def apply (rule someI2[of _ ‹[a]›], simp)
  by (rule MultiNdet_list_set[where L' = ‹[a]›, simplified])

  
lemma MultiNdet_in_id[simp]:
  ‹a ∈ A ⟹ (⨅ p ∈ insert a A. P p) = ⨅ p ∈ A. P p›
  unfolding MultiNdet_def by (simp add: insert_absorb)


lemma MultiNdet_insert[simp]:
  assumes fin: ‹finite A› and notempty: ‹A ≠ {}› and notin: ‹a ∉ A›
  shows ‹(⨅ p ∈ insert a A. P p) = P a ⊓ (⨅ p ∈ A. P p)›
  unfolding MultiNdet_def
  apply (rule someI2_ex, simp add: fin finite_list)+
proof-
  fix l l'
  assume ‹set l = A› and ‹set l' = insert a A›
  from notempty and ‹set l = A› have ‹l ≠ []› by fastforce
  then have ‹MultiNdet_list (a # l) P = P a ⊓ MultiNdet_list l P›
    proof(induct l rule: List.list_nonempty_induct)
    case (single x)
    show ‹MultiNdet_list [a, x] P = P a ⊓ MultiNdet_list [x] P› by simp
  next
    case (cons x xs)
    have ‹MultiNdet_list (a # x # xs) P = P a ⊓ ((MultiNdet_list xs P) ⊓ P x)›
      by (metis List.finite_set MultiNdet.fold_insert_idem MultiNdet.fold_set_fold
                MultiNdet_list.simps(2) cons.hyps(2) list.simps(15) Ndet_assoc)
    thus ‹MultiNdet_list (a # x # xs) P = P a ⊓ MultiNdet_list (x # xs) P›
    proof -
      have f1: ‹MultiNdet_list (a # x # xs) P =
                Finite_Set.fold (λa p. p ⊓ P a) (P x ⊓ P a) (set xs)›
        by (simp add: MultiNdet.fold_set_fold Ndet_commute)
      have ‹MultiNdet_list (x # xs) P =
            Finite_Set.fold (λa p. p ⊓ P a) (P x) (set xs)›
        by (simp add: MultiNdet.fold_set_fold)
      hence ‹MultiNdet_list (a # x # xs) P = MultiNdet_list (x # xs) P ⊓ P a›
        using f1 by (simp add: MultiNdet.fold_fun_left_comm)
      thus ‹MultiNdet_list (a # x # xs) P = P a ⊓ MultiNdet_list (x # xs) P›
        by (simp add: Ndet_commute)
    qed
  qed
  moreover have ‹set l' = set (a # l)›
    by (simp add: ‹set l = A› ‹set l' = insert a A›)
  ultimately show ‹MultiNdet_list l' P = P a ⊓ MultiNdet_list l P›
    by (metis MultiNdet_list_set)
qed


lemma MultiNdet_insert'[simp]:
  ‹⟦finite A; A ≠ {}⟧ ⟹ (⨅ p ∈ insert a A. P p) = P a ⊓ (⨅ p ∈ A. P p)›
  apply (cases ‹a ∈ A›, subst Set.insert_absorb, simp_all)
  apply (cases ‹A = {a}›, simp add: Ndet_id)
proof -
  assume ‹finite A› and ‹a ∈ A› and ‹A ≠ {a}›
  then obtain A' where ‹A' ≠ {}› ‹A = insert a A'› ‹a ∉ A'› ‹finite A'›
    by (metis Set.set_insert finite_insert)
  hence ‹MultiNdet A P = P a ⊓ MultiNdet A' P› by simp
  hence ‹MultiNdet A P = P a ⊓ P a ⊓ MultiNdet A' P› by (simp add: Ndet_id)
  thus ‹MultiNdet A P = P a ⊓ MultiNdet A P› by (metis Ndet_id Ndet_assoc)
qed


lemma mono_MultiNdet_eq:
  ‹finite A ⟹ ∀x ∈ A. P x = Q x ⟹ MultiNdet A P = MultiNdet A Q›
  by (induct A rule: induct_subset_empty_single; simp)



section ‹Some Tests›

lemma ‹(⨅⇩l p ∈ []. P p) = STOP› 
  and ‹(⨅⇩l p ∈ [a]. P p) = P a› 
  and ‹(⨅⇩l p ∈ [a, b]. P p) = P a ⊓ P b›    
  and ‹(⨅⇩l p ∈ [a, b, c]. P p) = P a ⊓ P b ⊓ P c›   
  by auto


lemma ‹(⨅ p ∈ {}. P p) = STOP› 
  and ‹(⨅ p ∈ {a}. P p) = P a› 
  and ‹(⨅ p ∈ {a, b}. P p) = P a ⊓ P b›    
  and ‹(⨅ p ∈ {a, b, c}. P p) = P a ⊓ P b ⊓ P c›   
  by (simp add: Ndet_assoc)+


lemma test_MultiNdet: ‹(⨅ p ∈ {1::int .. 3}. P p) = P 1 ⊓ P 2 ⊓ P 3›
proof -
  have ‹{1::int .. 3} = insert 1 (insert 2 (insert 3 {}))› by fastforce
  thus ‹(⨅ p ∈ {1::int .. 3}. P p) = P 1 ⊓ P 2 ⊓ P 3› by (simp add: Ndet_assoc)
qed


lemma test_MultiNdet':
  ‹(⨅ p ∈ {0::nat .. a}. P p) = (⨅ p ∈ {a} ∪ {1 .. a} ∪ {0} . P p)›
  by (metis Un_insert_right atMost_atLeast0 boolean_algebra_cancel.sup0
            image_Suc_lessThan insert_absorb2 insert_is_Un lessThan_Suc 
            lessThan_Suc_atMost lessThan_Suc_eq_insert_0)



section ‹Continuity›

lemma MultiNdet_cont[simp]:
  ‹⟦finite A; ∀x ∈ A. cont (P x)⟧ ⟹ cont (λy. ⨅ z∈A. P z y)›
  by (cases ‹A = {}›, simp, erule finite_set_induct_nonempty; simp)



section ‹Factorization of \<^const>‹Ndet› in front of \<^const>‹MultiNdet››

lemma MultiNdet_factorization_union:
  ‹⟦A ≠ {}; finite A; B ≠ {}; finite B⟧ ⟹
   (⨅ p ∈ A. P p) ⊓ (⨅ p ∈ B. P p) = ⨅ p ∈ A ∪ B . P p›
  by (erule finite_set_induct_nonempty, simp_all add: Ndet_assoc)



section ‹\<^term>‹⊥› Absorbance›

lemma MultiNdet_BOT_absorb:
  assumes fin: ‹finite A› and bot: ‹P a = ⊥› and dom: ‹a ∈ A› 
    shows ‹(⨅ x ∈ A. P x) = ⊥›
  apply(rule rev_mp[OF dom], rule rev_mp[OF bot])
  by (metis MultiNdet_insert MultiNdet_rec1 Ndet_commute fin
            finite_insert mk_disjoint_insert Ndet_BOT) 


lemma MultiNdet_is_BOT_iff:
  ‹finite A ⟹ (⨅ p ∈ A. P p) = ⊥ ⟷ (∃a ∈ A. P a = ⊥)›
  apply (cases ‹A = {}›, simp add: STOP_neq_BOT)
  by (rotate_tac, induct A rule: finite_set_induct_nonempty) (simp_all add: Ndet_is_BOT_iff)




section ‹First Properties›

lemma MultiNdet_id: ‹A ≠ {} ⟹ finite A ⟹ (⨅ p ∈ A. P) = P›
  by (erule finite_set_induct_nonempty, (simp_all add: Ndet_id))


lemma MultiNdet_STOP_id: ‹finite A ⟹ (⨅ p ∈ A. STOP) = STOP›
  by (cases ‹A = {}›) (simp_all add: MultiNdet_id)


lemma MultiNdet_is_STOP_iff:
  ‹finite A ⟹ (⨅ p ∈ A. P p) = STOP ⟷ A = {} ∨ (∀a ∈ A. P a = STOP)›
  apply (cases ‹A = {}›, simp)
  by (rotate_tac, induct A rule: finite_set_induct_nonempty) (simp_all add: Ndet_is_STOP_iff)



section ‹Behaviour of \<^const>‹MultiNdet› with \<^const>‹Ndet››

lemma MultiNdet_Ndet:
  ‹finite A ⟹ (⨅ a ∈ A. P a) ⊓ (⨅ a ∈ A. Q a) = ⨅ a ∈ A. P a ⊓ Q a›
  apply (cases ‹A = {}›, simp add: Ndet_id)
  apply (rotate_tac, induct A rule: finite_set_induct_nonempty)
  by simp_all (metis (no_types, lifting) Ndet_commute Ndet_assoc)



section ‹Commutativity›

lemma MultiNdet_sets_commute: 
  ‹⟦finite A; finite B⟧ ⟹
   (⨅ a ∈ A. ⨅ b ∈ B. P a b) = ⨅ b ∈ B. ⨅ a ∈ A. P a b›
proof (cases ‹A = {}›)
  show ‹finite A ⟹ finite B ⟹ A = {} ⟹ 
        (⨅ a∈A.  MultiNdet B (P a)) = ⨅ b∈B.  ⨅ a∈A.  P a b›
    by (simp add: MultiNdet_STOP_id)
next 
  assume ‹A ≠ {}› and ‹finite A› and ‹finite B›
  thus ‹(⨅ a∈A.  MultiNdet B (P a)) = ⨅ b∈B.  ⨅ a∈A.  P a b›
    apply (induct A rule: finite_set_induct_nonempty)
    by (simp_all add: MultiNdet_Ndet)
qed



section ‹Behaviour with Injectivity›

lemma inj_on_mapping_over_MultiNdet:
  ‹⟦finite A; inj_on f A⟧ ⟹ (⨅ x ∈ A. P x) = ⨅ x ∈ f ` A. P (inv_into A f x)›
proof (induct A rule: induct_subset_empty_single)
  show ‹MultiNdet {} P = ⨅ x∈f ` {}.  P (inv_into {} f x)› by force
next
  case 2
  show ?case by force
next
  case (3 F a)
  hence f1: ‹inv_into (insert a F) f (f a) = a› by force
  show ?case
    apply (simp add: "3.hyps"(2) "3.hyps"(4) f1)
    apply (rule arg_cong[where f = ‹λx. P a ⊓ x›])
    apply (subst "3.hyps"(5), rule inj_on_subset[OF "3.prems" subset_insertI])
    apply (rule mono_MultiNdet_eq, simp add: "3.hyps"(2))
    using "3.prems" by fastforce
qed



section ‹The Projections›

lemma D_MultiNdet: ‹finite A ⟹ 𝒟 (⨅ x ∈ A. P x) = (⋃ p ∈ A. 𝒟 (P p))›
  apply (cases ‹A = {}›, simp add: D_STOP, rotate_tac)
  by (induct rule: finite_set_induct_nonempty) (simp_all add: D_Ndet)

lemma F_MultiNdet:
  ‹finite A ⟹ ℱ (⨅ x ∈ A. P x) =
                (if A = {} then {(s, X). s = []} else ⋃ p ∈ A. ℱ (P p))›
  apply (simp add: F_STOP, intro impI, rotate_tac)
  by (induct rule: finite_set_induct_nonempty) (simp_all add: F_Ndet)

lemma T_MultiNdet:
  ‹finite A ⟹ 𝒯 (⨅ x ∈ A. P x) =
                (if A = {} then {[]} else ⋃ p ∈ A. 𝒯 (P p))›
  apply (simp add: T_STOP, intro impI, rotate_tac)
  by (induct rule: finite_set_induct_nonempty) (simp_all add: T_Ndet)



section ‹Cartesian Product Results›

lemma MultiNdet_cartprod_σs_set_σs_set:
  (*we can't remove hypothesis on len⇩1 in this proof for injectivity*)
  ‹⟦finite A; finite B; ∀s ∈ A. length s = len⇩1⟧ ⟹ 
   (⨅ (s, t) ∈ A × B. P (s @ t)) = ⨅ u ∈ {s @ t |s t. (s, t) ∈ A × B}. P u›
  apply (subst inj_on_mapping_over_MultiNdet[where f = ‹λ (s, t). s @ t›],
         simp_all add: inj_on_def)
  apply (subst prem_Multi_cartprod(1)[simplified, symmetric])
  apply (rule mono_MultiNdet_eq, simp add: finite_image_set2)
  by (metis (no_types, lifting) case_prod_unfold f_inv_into_f)


lemma MultiNdet_cartprod_s_set_σs_set:
  ‹⟦finite A; finite B⟧ ⟹
   (⨅ (s, t) ∈ A × B. P (s # t)) = ⨅ u ∈ {s # t |s t. (s, t) ∈ A × B}. P u›
  apply (subst inj_on_mapping_over_MultiNdet[where f = ‹λ (s, t). s # t›],
         simp_all add: inj_on_def) 
  apply (subst prem_Multi_cartprod(2)[simplified, symmetric])
  apply (rule mono_MultiNdet_eq, simp add: finite_image_set2)
  by (metis (no_types, lifting) case_prod_unfold f_inv_into_f)


lemma MultiNdet_cartprod_s_set_s_set:
  ‹⟦finite A; finite B⟧ ⟹
   (⨅ (s, t) ∈ A × B. P [s, t]) = ⨅ u ∈ {[s, t] |s t. (s, t) ∈ A × B}. P u›
  apply (subst inj_on_mapping_over_MultiNdet[where f = ‹λ (s, t). [s, t]›],
         simp_all add: inj_on_def) 
  apply (subst prem_Multi_cartprod(3)[simplified, symmetric])
  apply (rule mono_MultiNdet_eq, simp add: finite_image_set2)
  by (metis (no_types, lifting) case_prod_unfold f_inv_into_f)


lemma MultiNdet_cartprod: 
  ‹⟦finite A; finite B⟧ ⟹ (⨅ (s, t) ∈ A × B. P s t) = ⨅ s∈A. ⨅ t∈B. P s t›
  supply arg_cong_Ndet = arg_cong[where f = ‹λQ. _ ⊓ Q›]
proof (induct ‹card A› arbitrary: A B rule: nat_less_induct)
  case (1 A B)
  from ‹finite A› ‹finite B› consider ‹A = {}› | ‹B = {}› | 
      ‹∃mA mB a b A' B'. A = insert a A' ∧ B = insert b B' ∧ mA = card A' ∧ 
                         mB = card B' ∧ mA < card A ∧ mB < card B› 
    by (metis card_Diff1_less_iff ex_in_conv insert_Diff)
  thus ‹(⨅(x, y) ∈ A × B.  P x y) = ⨅ s∈A.  MultiNdet B (P s)›
  proof cases
    show ‹A = {} ⟹ (⨅ (x, y)∈A × B. P x y) = ⨅ s∈A. MultiNdet B (P s)›
      by simp
  next 
    show ‹B = {} ⟹ (⨅ (x, y)∈A × B. P x y) = ⨅ s∈A. MultiNdet B (P s)›
      by (simp add: MultiNdet_STOP_id[OF "1.prems"(1)])
  next
    assume ‹∃mA mB a b A' B'. A = insert a A' ∧ B = insert b B' ∧ 
            mA = card A' ∧ mB = card B' ∧ mA < card A ∧ mB < card B›
    then obtain mA mB a b A' B'
      where * : ‹A = insert a A'› ‹B = insert b B'› ‹mA = card A'›
                ‹mB = card B'› ‹mA < card A› ‹mB < card B› by blast
    have **  : ‹Pair a ` B' = {a} × B'›
     and *** : ‹(λa. (a, b)) ` A' = A' × {b}› unfolding image_def by blast+
    show ‹(⨅(x, y) ∈ A × B.  P x y) = ⨅ s∈A.  MultiNdet B (P s)›
      using "*"(1, 2) ‹finite A› ‹finite B›
      apply (cases ‹A' = {}›; cases ‹B' = {}›; simp_all)
        apply (rule arg_cong_Ndet)
        apply (subst inj_on_mapping_over_MultiNdet[of B' ‹λb. (a, b)›],
               simp_all add: inj_on_def "**")
        apply (rule mono_MultiNdet_eq, simp_all)
        apply (metis Pair_inject f_inv_into_f image_eqI)
       apply (rule arg_cong_Ndet)
       apply (subst inj_on_mapping_over_MultiNdet[of A' ‹λa. (a, b)›],
              simp_all add: inj_on_def "***")
       apply (rule mono_MultiNdet_eq, simp_all)
       apply (metis (no_types, lifting) f_inv_into_f image_eqI prod.inject)

      apply (subst MultiNdet_factorization_union[symmetric], simp_all)
      apply (subst "1"(1)[rule_format, OF "*"(5, 3)], simp_all)
      apply (simp add: MultiNdet_Ndet[symmetric])
      apply (subst Ndet_assoc, rule arg_cong_Ndet)
      apply (subst (3) Ndet_commute, rule arg_cong_Ndet)
      apply (subst inj_on_mapping_over_MultiNdet[of B' ‹λb. (a, b)›],
             simp_all add: inj_on_def "**")
      apply (rule mono_MultiNdet_eq)
       apply (simp; fail)
      by (metis "**" case_prod_conv f_inv_into_f)
  qed
qed



end