Theory Induct_CSP_Rules

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : More Fixpoint and k-Induction Schemata
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * Copyright (c) 2025 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 ‹ Advanced Induction Schemata ›

(*<*)
theory  Induct_CSP_Rules
  imports HOLCF
begin

default_sort type
  (*>*)

section ‹k-fixpoint-induction›

lemma nat_k_induct [case_names base step]:
  ‹P n› if ‹∀i<k. P i› and ‹∀n⇩0. (∀i<k. P (n⇩0 + i)) ⟶ P (n⇩0 + k)› for k n :: nat
proof (induct rule: nat_less_induct)
  fix n assume ‹∀m<n. P m›
  show ‹P n›
  proof (cases ‹n < k›)
    from that(1) show ‹n < k ⟹ P n› by blast
  next
    from ‹∀m<n. P m› that(2)[rule_format, of ‹n - k›]
    show ‹¬ n < k ⟹ P n› by auto
  qed
qed

thm fix_ind fix_ind2 

lemma fix_ind_k [case_names admissibility base_k_steps step]:
  assumes adm : ‹adm P›
    and base_k_steps : ‹∀i<k. P (iterate i⋅f⋅⊥)›
    and step : ‹⋀X. (∀i<k. P (iterate i⋅f⋅X)) ⟹ P (iterate k⋅f⋅X)›
  shows ‹P (fix⋅f)›
proof (unfold fix_def2, rule admD [OF adm chain_iterate])
  show ‹P (iterate i⋅f⋅⊥)› for i
  proof (induct i rule : nat_k_induct[of k])
    show ‹∀i<k. P (iterate i⋅f⋅⊥)› by (fact base_k_steps)
  next
    show ‹∀n⇩0. (∀i<k. P (iterate (n⇩0 + i)⋅f⋅⊥)) ⟶ P (iterate (n⇩0 + k)⋅f⋅⊥)›
      by (metis add.commute iterate_iterate step)
  qed
qed


lemma nat_k_skip_induct [case_names lower_bound base_k step]:
  ‹P n› if ‹1 ≤ k› and ‹∀i<k. P i› and ‹∀n⇩0. P n⇩0 ⟶ P (n⇩0 + k)› for k n :: nat
proof (induct n rule: nat_less_induct)
  fix n assume ‹∀m<n. P m›
  show ‹P n›
  proof (cases ‹n < k›)
    from that(2) show ‹n < k ⟹ P n› by blast
  next
    from ‹∀m<n. P m› ‹1 ≤ k› that(3)[rule_format, of ‹n - k›]
    show ‹¬ n < k ⟹ P n› by auto
  qed
qed

lemma fix_ind_k_skip [case_names lower_bound admissibility base_k_steps step]:
  assumes k_1 : ‹1 ≤ k›
    and adm : ‹adm P›
    and base_k_steps : ‹∀i<k. P (iterate i⋅f⋅⊥)›
    and step : ‹⋀X. P X ⟹ P (iterate k⋅f⋅X)›
  shows ‹P (fix⋅f)›
proof (unfold fix_def2, rule admD [OF adm chain_iterate])
  show ‹P (iterate i⋅f⋅⊥)› for i
  proof (induct i rule : nat_k_skip_induct[of k])
    show ‹1 ≤ k› by (fact ‹1 ≤ k›)
  next
    show ‹∀i<k. P (iterate i⋅f⋅⊥)› by (fact base_k_steps)
  next
    show ‹∀n⇩0. P (iterate n⇩0⋅f⋅⊥) ⟶ P (iterate (n⇩0 + k)⋅f⋅⊥)›
      by (metis add.commute iterate_iterate step)
  qed
qed



section‹Parallel fixpoint-induction›

lemma parallel_fix_ind_inc[case_names admissibility base_fst base_snd step]:
  assumes adm: ‹adm (λX. P (fst X) (snd X))›
    and base_fst: ‹⋀Y. P ⊥ Y› and base_snd: ‹⋀X. P X ⊥›
    and step: ‹⋀X Y. P X Y ⟹ P (G⋅X) Y ⟹ P X (H⋅Y) ⟹ P (G⋅X) (H⋅Y)›
  shows ‹P (fix⋅G) (fix⋅H)›
proof -
  from adm have adm': ‹adm (case_prod P)›
    unfolding split_def .
  have ‹P (iterate i⋅G⋅⊥) (iterate j⋅H⋅⊥)› for i j
  proof (induct ‹i + j› arbitrary: i j rule: nat_less_induct)
    case 1
    { fix i' j'
      assume i: ‹i = Suc i'› and j: ‹j = Suc j'›
      have ‹P (iterate i'⋅G⋅⊥) (iterate j'⋅H⋅⊥)›
        using "1.hyps" add_strict_mono i j by blast
      moreover have ‹P (iterate i'⋅G⋅⊥) (iterate j⋅H⋅⊥)›
        using "1.hyps" i by auto
      moreover have ‹P (iterate i⋅G⋅⊥) (iterate j'⋅H⋅⊥)›
        using "1.hyps" j by auto
      ultimately have ?case by (simp add: i j step)
    }
    thus ?case by (cases i; cases j; simp add: base_fst base_snd)
  qed
  hence ‹case_prod P (iterate i⋅G⋅⊥, iterate i⋅H⋅⊥)› for i by simp
  hence ‹case_prod P (⨆i. (iterate i⋅G⋅⊥, iterate i⋅H⋅⊥))›
    by - (rule admD [OF adm'], simp, assumption)
  hence ‹P (⨆i. iterate i⋅G⋅⊥) (⨆i. iterate i⋅H⋅⊥)›
    by (simp add: lub_Pair)  
  thus ‹P (fix⋅G) (fix⋅H)› by (simp add: fix_def2)
qed

(*<*)
end
  (*>*)