Theory CSP_Induct

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *
 * This file       : More Fixpoint and k-Induction Schemata
 *
 * Copyright (c) 2020 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  CSP_Induct

imports HOLCF

begin


default_sort type

section ‹k-fixpoint-induction›

lemma nat_k_induct [case_names base step]: 
  fixes k::nat
  assumes "∀i<k. P i" and "∀n⇩0. (∀i<k. P (n⇩0+i)) ⟶ P (n⇩0+k)"
  shows "P (n::nat)"
proof (induct rule: nat_less_induct)
  case (1 n)
  then show ?case 
    apply(cases "n < k") 
     using assms(1) apply blast
    using assms(2)[rule_format, of "n-k"] by auto
qed

thm fix_ind fix_ind2 

lemma fix_ind_k [case_names admissibility base_k_steps step]:
  fixes k::nat
  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)"
  unfolding fix_def2 apply (rule admD [OF adm chain_iterate])
  apply(rule nat_k_induct[of k], simp add: base_k_steps) 
  using step by (subst (1 2) add.commute, unfold iterate_iterate[symmetric]) blast 

lemma nat_k_skip_induct [case_names lower_bound base_k step]:
  fixes k::nat
  assumes "k ≥ 1" and "∀i<k. P i" and "∀n⇩0. P (n⇩0) ⟶ P (n⇩0+k)"
  shows "P (n::nat)"
proof(induct rule:nat_less_induct)
  case (1 n)
  then show ?case 
    apply(cases "n < k") 
     using assms(2) apply blast
    using assms(3)[rule_format, of "n-k"] assms(1) by auto
qed

lemma fix_ind_k_skip [case_names lower_bound admissibility base_k_steps step]:
  fixes k::nat
  assumes k_1: "k ≥ 1"
  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)"
  unfolding fix_def2 apply (rule admD [OF adm chain_iterate])
  apply(rule nat_k_skip_induct[of k]) 
  using k_1 base_k_steps apply auto
  using step by (subst add.commute, unfold iterate_iterate[symmetric]) blast

thm parallel_fix_ind

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⋅⊥)" 
       and "P (iterate i'⋅G⋅⊥) (iterate j⋅H⋅⊥)" 
       and "P (iterate i⋅G⋅⊥) (iterate j'⋅H⋅⊥)"
        using "1.hyps" add_strict_mono i j apply blast 
        using "1.hyps" i apply auto[1] 
        using "1.hyps" j by auto
      hence ?case by (simp add: i j step)
    }
    thus ?case
      apply(cases i, simp add:base_fst)
      apply(cases j, simp add:base_snd)
      by assumption
  qed
  then have "⋀i. case_prod P (iterate i⋅G⋅⊥, iterate i⋅H⋅⊥)"
    by simp
  then have "case_prod P (⨆i. (iterate i⋅G⋅⊥, iterate i⋅H⋅⊥))"
    by - (rule admD [OF adm'], simp, assumption)
  then have "P (⨆i. iterate i⋅G⋅⊥) (⨆i. iterate i⋅H⋅⊥)"
    by (simp add: lub_Pair)  
  then show "P (fix⋅G) (fix⋅H)"
    by (simp add: fix_def2)
qed

end