Theory Iteration

section ‹Iteration \label{S:iteration}›

theory Iteration
imports
  Galois_Connections
  CRA
begin

subsection ‹Possibly infinite iteration›

text ‹
  Iteration of finite or infinite steps can be defined using a least fixed point.
›


(* hide_fact (open) Random_Sequence.iter_def *)

locale finite_or_infinite_iteration = seq_distrib + upper_galois_connections
begin

definition
  iter :: "'a ⇒ 'a" (‹_⇧ω› [103] 102) (* this can be entered as \sup\circ *)
where
  "c⇧ω ≡ lfp (λ x. nil ⊓ c;x)"

lemma iter_step_mono: "mono (λ x. nil ⊓ c;x)"
  by (meson inf_mono order_refl seq_mono_right mono_def)

text ‹
  This fixed point definition leads to the two core iteration lemmas:
  folding and induction.
›

theorem iter_unfold: "c⇧ω = nil ⊓ c;c⇧ω"
  using iter_def iter_step_mono lfp_unfold by auto

lemma iter_induct_nil: "nil ⊓ c;x ⊑ x ⟹ c⇧ω ⊑ x"
  by (simp add: iter_def lfp_lowerbound)

lemma iter0: "c⇧ω ⊑ nil"
  by (metis iter_unfold sup.orderI sup_inf_absorb)

lemma iter1: "c⇧ω ⊑ c"
  by (metis inf_le2 iter0 iter_unfold order.trans seq_mono_right seq_nil_right)

lemma iter2 [simp]: "c⇧ω;c⇧ω = c⇧ω"
proof (rule antisym)
  show "c⇧ω;c⇧ω ⊑ c⇧ω" using iter0 seq_mono_right by fastforce
next
  have a: "nil ⊓ c;c⇧ω;c⇧ω ⊑ nil ⊓ c;c⇧ω ⊓ c;c⇧ω;c⇧ω"
    by (metis inf_greatest inf_le2 inf_mono iter0 order_refl seq_distrib_left.seq_mono_right seq_distrib_left_axioms seq_nil_right) 
  then have b: "… = c⇧ω ⊓ c;c⇧ω;c⇧ω" using iter_unfold by auto 
  then have c: "… = (nil ⊓ c;c⇧ω);c⇧ω" by (simp add: inf_seq_distrib)
  thus "c⇧ω ⊑ c⇧ω;c⇧ω" using a iter_induct_nil iter_unfold seq_assoc by auto 
qed

lemma iter_mono: "c ⊑ d ⟹ c⇧ω ⊑ d⇧ω"
proof -
  assume "c ⊑ d"
  then have "nil ⊓ c;d⇧ω ⊑ d;d⇧ω" by (metis inf.absorb_iff2 inf_left_commute inf_seq_distrib)
  then have "nil ⊓ c;d⇧ω ⊑ d⇧ω" by (metis inf.bounded_iff inf_sup_ord(1) iter_unfold) 
  thus ?thesis by (simp add: iter_induct_nil)
qed

lemma iter_abort: "⊥ = nil⇧ω"
  by (simp add: antisym iter_induct_nil)

lemma nil_iter: "⊤⇧ω = nil"
   by (metis (no_types) inf_top.right_neutral iter_unfold seq_top)
(*
lemma iter_conj_distrib:
  assumes nil: "c ⊑ nil"
    and repeat: "c ⊑ c ; c"
  shows "c \<iinter> d⇧ω ⊑ (c \<iinter> d)⇧ω"
proof (unfold iter_def)
  def F ≡ "(λ x. c \<iinter> x)"
  def G ≡ "(λ x. nil ⊓ d;x)"
  def H ≡ "(λ x. nil ⊓ ((c \<iinter> d);x))"

  have FG: "F ∘ G = (λ x. c \<iinter> (nil ⊓ d;x))"  by (metis comp_def F_def G_def) 
  have HF: "H ∘ F = (λ x. (nil ⊓ (c \<iinter> d);(c \<iinter> x)))" by (metis comp_def H_def F_def) 

  have "F (lfp G) ⊑ lfp H"
  proof (rule fusion_lfp_leq)
    show "mono H" by (simp add: H_def iter_step_mono)
  next
    show "dist_over_sup F" by (simp add: F_def conj_Sup_distrib)
  next
    fix x
    have "c \<iinter> (nil ⊓ d;x) = (c \<iinter> nil) ⊓ (c \<iinter> d;x)" by (metis inf_conj_distrib conj_commute)
    also have "... ⊑ nil ⊓ (c \<iinter> d;x)" by (metis conjunction_sup inf_mono_left le_iff_sup nil)
    also have "... ⊑ nil ⊓ (c;c \<iinter> d;x)" by (metis inf_conj_distrib inf.absorb_iff2 inf_mono_right repeat)
    also have "... ⊑ nil ⊓ (c \<iinter> d);(c \<iinter> x)" by (meson inf_mono_right sequential_interchange)
    finally show "(F ∘ G) x ⊑ (H ∘ F) x" by (simp add: FG HF)
  qed

  then show "c \<iinter> lfp(λx. nil ⊓ d ; x) ⊑ lfp (λx. nil ⊓ (c \<iinter> d) ; x)" using F_def G_def H_def by simp
qed

lemma iter_conj_distrib1: "c⇧ω \<iinter> d⇧ω ⊑ (c⇧ω \<iinter> d)⇧ω"
  by (simp add: iter0 iter_conj_distrib)

lemma iter_conj_distrib2: "c⇧ω \<iinter> d⇧ω ⊑ (c \<iinter> d)⇧ω"
proof -
  have a: "c⇧ω ⊑ c" by (metis iter1)
  have b: "c⇧ω \<iinter> d⇧ω ⊑ (c⇧ω \<iinter> d)⇧ω" by (metis iter_conj_distrib1)
  have "c⇧ω \<iinter> d ⊑ c \<iinter> d" by (metis a conj_mono order.refl) 
  thus ?thesis using a b by (metis refine_trans iter_mono) 
qed
*)
end



subsection ‹Finite iteration›

text ‹
  Iteration of a finite number of steps (Kleene star) is defined
  using the greatest fixed point.
›

locale finite_iteration = seq_distrib + lower_galois_connections
begin

definition
  fiter :: "'a ⇒ 'a" (‹_⇧⋆› [101] 100)
where
  "c⇧⋆ ≡ gfp (λ x. nil ⊓ c;x)"


lemma fin_iter_step_mono: "mono (λ x. nil ⊓ c;x)"
  by (meson inf_mono order_refl seq_mono_right mono_def)

text ‹
  This definition leads to the two core iteration lemmas:
  folding and induction.
›

lemma fiter_unfold: "c⇧⋆ = nil ⊓ c;c⇧⋆"
  using fiter_def gfp_unfold fin_iter_step_mono by auto

lemma fiter_induct_nil: "x ⊑ nil ⊓ c;x ⟹ x ⊑ c⇧⋆"
  by (simp add: fiter_def gfp_upperbound)

lemma fiter0: "c⇧⋆ ⊑ nil"
  by (metis fiter_unfold inf.cobounded1)

lemma fiter1: "c⇧⋆ ⊑ c"
  by (metis fiter0 fiter_unfold inf_le2 order.trans seq_mono_right seq_nil_right)

lemma fiter_induct_eq: "c⇧⋆;d = gfp (λ x. c;x ⊓ d)"
proof -
  define F where "F = (λ x. x;d)"
  define G where "G = (λ x. nil ⊓ c;x)"
  define H where "H = (λ x. c;x ⊓ d)"

  have FG: "F ∘ G = (λ x. c;x;d ⊓ d)" by (simp add: F_def G_def comp_def inf_commute inf_seq_distrib)
  have HF: "H ∘ F = (λ x. c;x;d ⊓ d)" by (metis comp_def seq_assoc H_def F_def) 

  have adjoint: "dist_over_inf F" using Inf_seq_distrib F_def by simp
  have monoH: "mono H"
    by (metis H_def inf_mono_left monoI seq_distrib_left.seq_mono_right seq_distrib_left_axioms)
  have monoG: "mono G" by (metis G_def inf_mono_right mono_def seq_mono_right) 
  have "∀ x. ((F ∘ G) x = (H ∘ F) x)" using FG HF by simp
  then have "F (gfp G) = gfp H" using adjoint monoG monoH fusion_gfp_eq by blast 
  then have "(gfp (λ x. nil ⊓ c;x));d = gfp (λ x. c;x ⊓ d)" using F_def G_def H_def inf_commute by simp
  thus ?thesis by (metis fiter_def) 
qed

theorem fiter_induct: "x ⊑ d ⊓ c;x ⟹ x ⊑ c⇧⋆;d"
proof -
  assume "x ⊑ d ⊓ c;x"
  then have "x ⊑ c;x ⊓ d" using inf_commute by simp
  then have "x ⊑ gfp (λ x. c;x ⊓ d)" by (simp add: gfp_upperbound)
  thus ?thesis by (metis (full_types) fiter_induct_eq)
qed

lemma fiter2 [simp]: "c⇧⋆;c⇧⋆ = c⇧⋆"
proof -
  have lr: "c⇧⋆;c⇧⋆ ⊑ c⇧⋆" using fiter0 seq_mono_right seq_nil_right by fastforce 
  have rl: "c⇧⋆ ⊑ c⇧⋆;c⇧⋆" by (metis fiter_induct fiter_unfold inf.right_idem order_refl) 
  thus ?thesis by (simp add: antisym lr) 
qed

lemma fiter3 [simp]: "(c⇧⋆)⇧⋆ = c⇧⋆"
  by (metis dual_order.refl fiter0 fiter1 fiter2 fiter_induct inf.commute inf_absorb1 seq_nil_right)

lemma fiter_mono: "c ⊑ d ⟹ c⇧⋆ ⊑ d⇧⋆"
proof -
  assume "c ⊑ d"
  then have "c⇧⋆ ⊑ nil ⊓ d;c⇧⋆" by (metis fiter0 fiter1 fiter2 inf.bounded_iff refine_trans seq_mono_left)
  thus ?thesis  by (metis seq_nil_right fiter_induct)
qed

end



subsection ‹Infinite iteration›

text ‹
  Iteration of infinite number of steps can be defined
  using a least fixed point.
›

locale infinite_iteration = seq_distrib + lower_galois_connections
begin

definition
  infiter :: "'a  ⇒ 'a" (‹_⇧∞› [105] 106)
where
  "c⇧∞ ≡ lfp (λ x. c;x)"

lemma infiter_step_mono: "mono (λ x. c;x)"
  by (meson inf_mono order_refl seq_mono_right mono_def)

text ‹
  This definition leads to the two core iteration lemmas:
  folding and induction.
›

theorem infiter_unfold: "c⇧∞ = c;c⇧∞"
  using infiter_def infiter_step_mono lfp_unfold by auto

lemma infiter_induct: "c;x ⊑ x ⟹ c⇧∞ ⊑ x"
  by (simp add: infiter_def lfp_lowerbound)

theorem infiter_unfold_any: "c⇧∞ = (c ⇧;^ i) ; c⇧∞"
proof (induct i)
  case 0
  thus ?case by simp
next
  case (Suc i)
  thus ?case using infiter_unfold seq_assoc seq_power_Suc by auto
qed

lemma infiter_annil: "c⇧∞;x = c⇧∞"
proof -
  have "∀a. (⊥::'a) ⊑ a"
    by auto
  thus ?thesis
    by (metis (no_types) eq_iff inf.cobounded2 infiter_induct infiter_unfold inf_sup_ord(1) seq_assoc seq_bot weak_seq_inf_distrib seq_nil_right)
qed

end



subsection ‹Combined iteration›

text ‹
  The three different iteration operators can be combined to show that 
  finite iteration refines finite-or-infinite iteration.
›

locale iteration = finite_or_infinite_iteration + finite_iteration + 
                   infinite_iteration
begin

lemma refine_iter: "c⇧ω ⊑ c⇧⋆"
  by (metis seq_nil_right order.refl iter_unfold fiter_induct)

lemma iter_absorption [simp]: "(c⇧ω)⇧⋆ = c⇧ω"
proof (rule antisym)
  show "(c⇧ω)⇧⋆ ⊑ c⇧ω" by (metis fiter1)
next
  show "c⇧ω ⊑ (c⇧ω)⇧⋆" by (metis fiter1 fiter_induct inf_left_idem iter2 iter_unfold seq_nil_right sup.cobounded2 sup.orderE sup_commute)
qed

lemma infiter_inf_top: "c⇧∞ = c⇧ω ; ⊤" 
proof -
  have lr: "c⇧∞ ⊑ c⇧ω ; ⊤"
  proof -
    have "c ; (c⇧ω ; ⊤) = nil ; ⊤ ⊓ c ; c⇧ω ; ⊤"
      using semigroup.assoc seq.semigroup_axioms by fastforce
    then show ?thesis
      by (metis (no_types) eq_refl finite_or_infinite_iteration.iter_unfold 
         finite_or_infinite_iteration_axioms infiter_induct 
         seq_distrib_right.inf_seq_distrib seq_distrib_right_axioms)
  qed 
  have rl: "c⇧ω ; ⊤ ⊑ c⇧∞"
    by (metis inf_le2 infiter_annil infiter_unfold iter_induct_nil seq_mono_left) 
  thus ?thesis using antisym_conv lr by blast 
qed

lemma infiter_fiter_top:
  shows "c⇧∞ ⊑ c⇧⋆ ; ⊤"
  by (metis eq_iff fiter_induct inf_top_left infiter_unfold)

lemma inf_ref_infiter: "c⇧ω ⊑ c⇧∞"
  using infiter_unfold iter_induct_nil by auto

end

end