Theory While_Combinator_Exts

(*  Title:      While_Combinator_Exts.thy
    Author:     Denis Lohner
*)

section ‹Code Generation›
subsection ‹While Combinator Extensions›

theory While_Combinator_Exts imports
  "HOL-Library.While_Combinator"
begin
lemma while_option_None_invD:
  assumes "while_option b c s = None" and "wf r"
  and "I s" and "⋀s. ⟦ I s; b s ⟧ ⟹ I (c s)"
  and "⋀s. ⟦ I s; b s ⟧ ⟹ (c s, s ) ∈ r"
  shows "False"
  using assms
  by -(drule wf_rel_while_option_Some [of r I b c], auto)

lemma while_option_NoneD:
  assumes "while_option b c s = None"
  and "wf r" and "⋀s. b s ⟹ (c s, s) ∈ r"
  shows "False"
  using assms
  by (blast intro: while_option_None_invD)

lemma while_option_sim:
  assumes start: "R (Some s1) (Some s2)"
  and cond: "⋀s1 s2. ⟦ R (Some s1) (Some s2); I s1 ⟧ ⟹ b1 s1 = b2 s2"
  and step : "⋀s1 s2. ⟦ R (Some s1) (Some s2); I s1; b1 s1 ⟧ ⟹ R (Some (c1 s1)) (Some (c2 s2))"
  and diverge: "R None None"
  and inv_start: "I s1"
  and inv_step: "⋀s1. ⟦ I s1; b1 s1 ⟧ ⟹ I (c1 s1)"
  shows "R (while_option b1 c1 s1) (while_option b2 c2 s2)"
proof -
  { fix k
    assume "∀k' < k. b1 ((c1 ^^ k') s1)"
    with start cond step inv_start inv_step
    have "b1 ((c1 ^^ k) s1) = b2 ((c2 ^^ k) s2)" and "I ((c1 ^^ k) s1)"
      and "R (Some ((c1 ^^ k) s1)) (Some ((c2 ^^ k) s2))"
      by (induction k) auto
  }
  moreover
  { fix k
    assume "¬ b1 ((c1 ^^ k) s1)"
    hence "∀k' < LEAST k. ¬ b1 ((c1 ^^ k) s1). b1 ((c1 ^^ k') s1)"
      by (metis (lifting) not_less_Least)
  }
  moreover
  { fix k
    assume "¬ b2 ((c2 ^^ k) s2)"
    hence "∀k' < LEAST k. ¬ b2 ((c2 ^^ k) s2). b2 ((c2 ^^ k') s2)"
      by (metis (lifting) not_less_Least)
  }
  moreover
  {
    assume "∃k. ¬ b1 ((c1 ^^ k) s1)"
      and "∃k. ¬ b2 ((c2 ^^ k) s2)"
    hence not_cond_Least: "¬ b1 ((c1 ^^ (LEAST k. ¬ b1 ((c1 ^^ k) s1))) s1)"
      "¬ b2 ((c2 ^^ (LEAST k. ¬ b2 ((c2 ^^ k) s2))) s2)"
      by -(drule LeastI_ex, assumption)+
    { fix k
      assume "∀k' < k. b1 ((c1 ^^ k') s1)"
      with calculation(1) dual_order.strict_trans
      have "∀k' < k. b2 ((c2 ^^ k') s2)"
        by blast
    }
    hence "(LEAST k'. ¬ b1 ((c1 ^^ k') s1)) = (LEAST k'. ¬ b2 ((c2 ^^ k') s2))"
      by (metis (no_types, lifting) not_cond_Least calculation(1,4,5) less_linear)
    with calculation(3,4)
    have "R (Some ((c1 ^^ (LEAST k. ¬ b1 ((c1 ^^ k) s1))) s1))
      (Some ((c2 ^^ (LEAST k. ¬ b2 ((c2 ^^ k) s2))) s2))"
      by auto
  }
  ultimately show ?thesis using diverge
    unfolding while_option_def
    apply (split if_split)
    apply (rule conjI)
     apply (split if_split)
     apply metis
    apply (split if_split)
    by (metis (lifting) LeastI_ex)
qed

end