Theory MultiDet

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff
 *
 * This file       : Multi-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 MultiDet Operator›

theory MultiDet
  imports Patch PreliminaryWork
begin



section ‹Definition›


definition  MultiDet :: ‹['a set, 'a ⇒ 'b process] ⇒ 'b process›
  where    ‹MultiDet A P = Finite_Set.fold (λa r. r □ P a) STOP A›

(* Unfortunately, we don't have a big □ in jedit *)
syntax "_MultiDet" :: ‹[pttrn, 'a set, 'b process] ⇒ 'b process›  (‹(3❙□_∈_. / _)› 75)
syntax_consts "_MultiDet" ⇌ MultiDet
translations "❙□ p ∈ A. P"  ⇌  "CONST MultiDet A (λp. P)"



section ‹First Properties›

lemma MultiDet_rec0[simp]: ‹(❙□ p ∈ {}. P p) = STOP›
  by(simp add: MultiDet_def)

lemma MultiDet_rec1[simp]: ‹(❙□ p ∈ {a}. P p) = P a›
  unfolding MultiDet_def
  apply (subst comp_fun_commute_on.fold_insert_remove[where S = ‹{a}›])
  by (simp_all add: comp_fun_commute_on_def
                    Det_commute[of ‹STOP›, simplified Det_STOP])


lemma MultiDet_in_id[simp]:
  ‹a ∈ A ⟹ (❙□ p ∈ insert a A. P p) = ❙□ p ∈ A. P p›
  unfolding MultiDet_def by (simp add: insert_absorb)


lemma MultiDet_insert[simp]:
  ‹finite A ⟹ (❙□ p ∈ insert a A. P p) = P a □ (❙□ p ∈ A - {a}. P p)›
  unfolding MultiDet_def
  apply (subst comp_fun_commute_on.fold_insert_remove[where S = ‹insert a A›])
  unfolding comp_fun_commute_on_def comp_def
     apply (metis Det_assoc Det_commute)
  by (auto simp: comp_fun_commute_on_def Det_commute Det_assoc comp_def)


lemma MultiDet_insert'[simp]:
  ‹finite A ⟹ (❙□ p ∈ insert a A. P p) = (P a □ (❙□ p ∈ A. P p))›
  by (cases ‹a ∈ A›, metis MultiDet_insert Det_assoc Det_id insert_absorb, simp)


lemma mono_MultiDet_eq:
  ‹finite A ⟹ ∀x ∈ A. P x = Q x ⟹ MultiDet A P = MultiDet A Q›
  by (induct A rule: induct_subset_empty_single, simp, simp)
     (metis MultiDet_insert' insertCI)



section ‹Some Tests›

lemma test_MultiDet: ‹(❙□ 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: Det_assoc)
qed


lemma test_MultiDet':
  ‹(❙□ 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 MultiDet_cont[simp]:
  ‹⟦finite A; ∀x ∈ A. cont (P x)⟧ ⟹ cont (λy. ❙□ z∈A. P z y)›
  by (rule Finite_Set.finite_subset_induct[of A A], simp+)



section ‹Factorization of \<^const>‹Det› in front of \<^const>‹MultiDet››

lemma MultiDet_factorization_union:
  ‹⟦finite A; finite B⟧ ⟹ (❙□ p ∈ A. P p) □ (❙□ p ∈ B. P p) = ❙□ p ∈ A ∪ B . P p›
  apply (erule finite_induct, simp_all)
  by (metis Det_commute Det_STOP)
     (metis MultiDet_insert MultiDet_insert' Det_assoc finite_UnI)



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

lemma MultiDet_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 Det_commute MultiDet_insert' Det_BOT fin insert_absorb)


lemma MultiDet_is_BOT_iff:
  ‹finite A ⟹ MultiDet A P = ⊥ ⟷ (∃a ∈ A. P a = ⊥)›
  by (induct A rule: finite_induct) (auto simp add: STOP_neq_BOT Det_is_BOT_iff)



section ‹First Properties›

lemma MultiDet_id: ‹A ≠ {} ⟹ finite A ⟹ (❙□p ∈ A. P) = P›
  by (erule finite_set_induct_nonempty, simp_all add: Det_id)


lemma MultiDet_STOP_id: ‹finite A ⟹ (❙□p ∈ A. STOP) = STOP› 
  by (cases ‹A = {}›) (simp_all add: MultiDet_id)


lemma MultiDet_STOP_neutral:
  ‹finite A ⟹ P a = STOP ⟹ (❙□ z ∈ insert a A. P z) = ❙□ z ∈ A. P z›
  by (metis Det_commute MultiDet_insert' Det_STOP)


lemma MultiDet_is_STOP_iff:
  ‹finite A ⟹ (❙□ a ∈ A. P a) = STOP ⟷ A = {} ∨ (∀a ∈ A. P a = STOP)›
  by (induct rule: finite_induct) (auto simp add: Det_is_STOP_iff)



section ‹Behaviour of \<^const>‹MultiDet› with \<^const>‹Det››

lemma MultiDet_Det:
  ‹finite A ⟹ (❙□ a ∈ A. P a) □ (❙□ a ∈ A. Q a) = ❙□ a ∈ A. P a □ Q a›
proof (induct A rule: finite_induct)
  case empty show ?case by (simp add: Det_id)
next
  case (insert x F)
  hence ‹MultiDet (insert x F) P □ MultiDet (insert x F) Q =
         P x □ MultiDet F P □ Q x □ MultiDet F Q› by (simp add: Det_assoc)
  also have ‹… = (P x □ Q x) □ (❙□ a∈F.  P a □ Q a)›
    by (metis (no_types, lifting) Det_assoc Det_commute insert.hyps(3))
  ultimately show ‹MultiDet (insert x F) P □ MultiDet (insert x F) Q = 
                   (❙□ a∈insert x F.  P a □ Q a)›
    by (simp add: ‹finite F› ‹x ∉ F›)
qed



section ‹Commutativity›

lemma MultiDet_sets_commute:
  ‹⟦finite A; finite B⟧ ⟹ (❙□ a ∈ A. ❙□ b ∈ B. P a b) = ❙□ b ∈ B. ❙□ a ∈ A. P a b›
  by (induct A rule: finite_induct) (simp_all add: MultiDet_STOP_id MultiDet_Det)



section ‹Behaviour with Injectivity›

lemma inj_on_mapping_over_MultiDet:
  ‹⟦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)
  case 1
  thus ?case by force
next
  case 2
  thus ?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 del: MultiDet_insert)
    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_MultiDet_eq, simp add: "3.hyps"(2))
    using "3.prems" by fastforce
qed



section ‹The Projections›

lemma D_MultiDet: ‹finite A ⟹ 𝒟 (❙□ x ∈ A. P x) = (⋃ p ∈ A. 𝒟 (P p))›
  by (induct rule: finite_induct) (simp_all add: D_Det D_STOP)

lemma T_MultiDet:
  ‹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_Det T_STOP)



section ‹Cartesian Product Results›

lemma MultiDet_cartprod_σs_set_σs_set:
  (*we can't remove hypothesis on len⇩1 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_MultiDet[where f = ‹λ (s, t). s @ t›],
         simp_all add: inj_on_def)
  apply (subst prem_Multi_cartprod(1)[simplified, symmetric])
  apply (rule mono_MultiDet_eq, simp add: finite_image_set2)
  by (metis (no_types, lifting) case_prod_unfold f_inv_into_f)


lemma MultiDet_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_MultiDet[where f = ‹λ (s, t). s # t›],
         simp_all add: inj_on_def) 
  apply (subst prem_Multi_cartprod(2)[simplified, symmetric])
  apply (rule mono_MultiDet_eq, simp add: finite_image_set2)
  by (metis (no_types, lifting) case_prod_unfold f_inv_into_f)


lemma MultiDet_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_MultiDet[where f = ‹λ (s, t). [s, t]›],
         simp_all add: inj_on_def) 
  apply (subst prem_Multi_cartprod(3)[simplified, symmetric])
  apply (rule mono_MultiDet_eq, simp add: finite_image_set2)
  by (metis (no_types, lifting) case_prod_unfold f_inv_into_f)


lemma MultiDet_cartprod: 
  ‹finite A ⟹ finite B ⟹ (❙□ (s, t) ∈ A × B. P s t) = ❙□ s∈A. ❙□ t∈B. P s t›
  supply arg_cong_Det = arg_cong[where f = ‹λQ. _ □ Q›]
  supply MultiDet_insert[simp del]
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.  MultiDet B (P s)›
  proof cases
    show ‹A = {} ⟹ (❙□(x, y)∈A × B. P x y) = ❙□s∈A. MultiDet B (P s)›
      by simp
  next
    show ‹B = {} ⟹ (❙□(x, y)∈A × B. P x y) = ❙□s∈A. MultiDet B (P s)›
      by (simp add: MultiDet_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'› unfolding image_def by blast
    show ‹(❙□(x, y)∈A × B.  P x y) = ❙□s∈A.  MultiDet B (P s)›
      using "*"(1, 2) ‹finite A› ‹finite B› apply simp
      apply (subst MultiDet_factorization_union[symmetric], simp_all)
      apply (subst "1"(1)[rule_format, OF "*"(5, 3)], simp_all)
      apply (simp add: MultiDet_Det[symmetric])
      apply (subst Det_assoc, rule arg_cong_Det)
      apply (subst (3) Det_commute, rule arg_cong_Det)
      apply (subst inj_on_mapping_over_MultiDet[of B' ‹λb. (a, b)›],
             simp_all add: inj_on_def "**")
      apply (rule mono_MultiDet_eq)
       apply (simp; fail)
      by (metis "**" case_prod_conv f_inv_into_f)
  qed
qed



end