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 "n0. (i<k. P (n0+i))  P (n0+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 if)"
  and step: "x. (i<k.  P (iterate ifx))  P (iterate kfx)"
  shows "P (fixf)"
  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 "n0. P (n0)  P (n0+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 if)"
  and step: "x. P x  P (iterate kfx)"
  shows "P (fixf)"
  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 (Gx) y  P x (Hy)  P (Gx) (Hy)"
  shows "P (fixG) (fixH)"
proof -
  from adm have adm': "adm (case_prod P)"
    unfolding split_def .
  have "P (iterate iG) (iterate jH)" 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 jH)" 
       and "P (iterate iG) (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 iG, iterate iH)"
    by simp
  then have "case_prod P (i. (iterate iG, iterate iH))"
    by - (rule admD [OF adm'], simp, assumption)
  then have "P (i. iterate iG) (i. iterate iH)"
    by (simp add: lub_Pair)  
  then show "P (fixG) (fixH)"
    by (simp add: fix_def2)
qed

end