Theory PreliminaryWork

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff
 *
 * This file       : Preliminary induction rules for set, multiset, nat
 *
 * 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 ‹Some Preliminary Work›

theory PreliminaryWork
  imports "HOL-Library.Multiset"
begin



section ‹Induction Rules for typ‹'α set››


lemma finite_subset_induct_singleton
      [consumes 3, case_names singleton insertion]:
  ‹⟦a ∈ A; finite F; F ⊆ A; P {a}; 
    ⋀x F. finite F ⟹ x ∈ A ⟹ x ∉ (insert a F) ⟹ P (insert a F)
          ⟹ P (insert x (insert a F))⟧ ⟹ P (insert a F)›
  apply (erule Finite_Set.finite_subset_induct, simp_all)
  by (metis insert_absorb2 insert_commute)


lemma finite_set_induct_nonempty
      [consumes 2, case_names singleton insertion]:
  assumes ‹A ≠ {}› and ‹finite A›
      and singleton: ‹⋀a. a ∈ A ⟹ P {a}›
      and insert: ‹⋀x F. ⟦F ≠ {}; finite F; x ∈ A; x ∉ F;  P F⟧ 
                          ⟹ P (insert x F)›
    shows ‹P A›
proof-
  obtain a A' where ‹a ∈ A› ‹finite A'› ‹A' ⊆ A› ‹A = insert a A'›
    using ‹A ≠ {}› ‹finite A› by fastforce
  show ‹P A›
    apply (subst ‹A = insert a A'›, rule finite_subset_induct_singleton[of a A])
    by (simp_all add: ‹a ∈ A› ‹finite A'› ‹A' ⊆ A› singleton insert)
qed


lemma finite_subset_induct_singleton'
      [consumes 3, case_names singleton insertion]:
  ‹⟦a ∈ A; finite F; F ⊆ A; P {a};
    ⋀x F. ⟦finite F; x ∈ A; insert a F ⊆ A; x ∉ insert a F; P (insert a F)⟧
           ⟹ P (insert x (insert a F))⟧
   ⟹ P (insert a F)›
  apply (erule Finite_Set.finite_subset_induct', simp_all)
  by (metis insert_absorb2 insert_commute)


lemma induct_subset_empty_single[consumes 1]:
  ‹⟦finite A; P {}; ∀a ∈ A. P {a}; 
    ⋀F a. ⟦a ∈ A; finite F; F ⊆ A; F ≠ {}; P F⟧ ⟹ P (insert a F)⟧ ⟹ P A›
  by (rule finite_subset_induct') auto



section ‹Induction Rules for typ‹'α multiset››

text ‹The following rule comes directly from theory‹HOL-Library.Multiset› but is written
      with ∗‹consumes 2› instead of ∗‹consumes 1›. I rewrite here a correct version.›
lemma msubset_induct [consumes 1, case_names empty add]:
  ‹⟦F ⊆# A; P {#}; ⋀a F. ⟦a ∈# A; P F⟧ ⟹ P (add_mset a F)⟧ ⟹ P F›
  by (fact multi_subset_induct)


lemma msubset_induct_singleton [consumes 2, case_names m_singleton add]:
  ‹⟦a ∈# A; F ⊆# A; P {#a#};
    ⋀x F. ⟦x ∈# A; P (add_mset a F)⟧ ⟹ P (add_mset x (add_mset a F))⟧
    ⟹ P (add_mset a F)›
  by (erule msubset_induct, simp_all add: add_mset_commute)


lemma mset_induct_nonempty [consumes 1, case_names m_singleton add]:
  assumes ‹A ≠ {#}›
      and m_singleton: ‹⋀a. a ∈# A ⟹ P {#a#}›
      and add: ‹⋀x F. ⟦F ≠ {#}; x ∈# A; P F⟧ ⟹ P (add_mset x F)›
    shows ‹P A›
proof-
  obtain a A' where ‹a ∈# A› ‹A' ⊆# A› ‹A = add_mset a A'›
    by (metis  ‹A ≠ {#}› diff_subset_eq_self insert_DiffM multiset_nonemptyE)
  show ‹P A›
    apply (subst ‹A = add_mset a A'›, rule msubset_induct_singleton[of a A])
    by (simp_all add: ‹a ∈# A› ‹A' ⊆# A› m_singleton add)
qed 


lemma msubset_induct' [consumes 2, case_names empty add]:
  assumes ‹F ⊆# A›
    and empty: ‹P {#}›
    and insert: ‹⋀a F. ⟦a ∈# A - F; F ⊆# A; P F⟧ ⟹ P (add_mset a F)›
  shows ‹P F›
proof -
  from ‹F ⊆# A›
  show ?thesis
  proof (induct F)
    show ‹P {#}› by (simp add: assms(2))
  next
    case (add x F)
    then show ‹P (add_mset x F)›
      using Diff_eq_empty_iff_mset add_diff_cancel_left add_diff_cancel_left'
            add_mset_add_single local.insert mset_subset_eq_insertD
            subset_mset.le_iff_add subset_mset.less_imp_le by fastforce
  qed
qed


lemma msubset_induct_singleton' [consumes 2, case_names m_singleton add]:
  ‹⟦a ∈# A - F; F ⊆# A; P {#a#};
    ⋀x F. ⟦x ∈# A - F; F ⊆# A; P (add_mset a F)⟧
           ⟹ P (add_mset x (add_mset a F))⟧
   ⟹ P (add_mset a F)›
  by (erule msubset_induct', simp_all add: add_mset_commute)


lemma msubset_induct_singleton'' [consumes 1, case_names m_singleton add]:
  ‹⟦add_mset a F ⊆# A; P {#a#};
    ⋀x F. ⟦add_mset x (add_mset a F) ⊆# A; P (add_mset a F)⟧
           ⟹ P (add_mset x (add_mset a F))⟧
   ⟹ P (add_mset a F)›
  apply (induct F, simp) 
  by (metis add_mset_commute diff_subset_eq_self subset_mset.trans union_single_eq_diff)


lemma mset_induct_nonempty' [consumes 1, case_names m_singleton add]:
  assumes nonempty: ‹A ≠ {#}› and m_singleton: ‹⋀a. a ∈# A ⟹ P {#a#}›
      and hyp: ‹⋀a x F. ⟦a ∈# A; x ∈# A - add_mset a F; add_mset a F ⊆# A;
                          P (add_mset a F)⟧ ⟹ P (add_mset x (add_mset a F))›
    shows ‹P A›
proof-
  obtain a A' where ‹A = add_mset a A'› ‹add_mset a A' ⊆# A›
    using nonempty multiset_cases subset_mset_def by auto
  show ‹P A›
    apply (subst ‹A = add_mset a A'›)
    using ‹add_mset a A' ⊆# A›
  proof (induct A' rule: msubset_induct_singleton'')
    show ‹P {#a#}› using ‹A = add_mset a A'› m_singleton by force
  next
    case (add x F)
    show ‹P (add_mset x (add_mset a F))›
      apply (subst hyp) 
          apply (simp add: ‹A = add_mset a A'›)
         apply (metis ‹add_mset x (add_mset a F) ⊆# A› add_mset_add_single
                      mset_subset_eq_insertD subset_mset.add_diff_inverse 
                      subset_mset.add_le_cancel_left subset_mset_def)
        apply (meson ‹add_mset x (add_mset a F) ⊆# A› mset_subset_eq_insertD
                     subset_mset.dual_order.strict_implies_order)
      by (simp_all add: ‹P (add_mset a F)›)
  qed
qed


lemma induct_subset_mset_empty_single:
  ‹⟦P {#}; ∀a ∈# M. P {#a#}; 
    ⋀N a. ⟦a ∈# M; N ⊆# M; N ≠ {#}; P N⟧ ⟹ P (add_mset a N)⟧ ⟹ P M›
  by (metis in_diffD mset_induct_nonempty')



section ‹Strong Induction for typ‹nat››

lemma strong_nat_induct[consumes 0, case_names 0 Suc]: 
  ‹⟦P 0; ⋀n. (⋀m. m ≤ n ⟹ P m) ⟹ P (Suc n)⟧ ⟹ P n›
  by (induct n rule: nat_less_induct) (metis gr0_implies_Suc gr_zeroI less_Suc_eq_le)

lemma strong_nat_induct_non_zero[consumes 1, case_names 1 Suc]: 
  ‹⟦0 < n; P 1; ⋀n. 0 < n ⟹ (⋀m. 0 < m ∧ m ≤ n ⟹ P m) ⟹ P (Suc n)⟧
   ⟹ P n›
  by (induct n rule: nat_less_induct) (metis One_nat_def gr0_implies_Suc gr_zeroI less_Suc_eq_le)



section ‹Preliminaries for Cartesian Product Results›

lemma prem_Multi_cartprod:
  ‹(λ(x, y). x @ y ) ` (A  × B ) = {s @ t  |s t. (s, t) ∈ A  × B }›
  ‹(λ(x, y). x # y ) ` (A' × B ) = {s # t  |s t. (s, t) ∈ A' × B }›
  ‹(λ(x, y). [x, y]) ` (A' × B') = {[s, t] |s t. (s, t) ∈ A' × B'}›
  by auto



end