Theory Conjunctive_Iteration

section ‹Iteration for conjunctive models \label{S:conjunctive-iteration}›

theory Conjunctive_Iteration
imports
  Conjunctive_Sequential
  Iteration
  Infimum_Nat
begin

text ‹
  Sequential left-distributivity is only supported by conjunctive models
  but does not apply in general. The relational model is one such example.
›

locale iteration_finite_conjunctive = seq_finite_conjunctive + iteration

begin

lemma isolation: "cω = c⋆ ⊓ c∞"
proof -
  define F where "F = (λ x. c⋆ ⊓ x)"
  define G where "G = (λ x. c;x)"
  define H where "H = (λ x. nil ⊓ c;x)"

  have FG: "F ∘ G = (λ x. c⋆ ⊓ c;x)" using F_def G_def by auto
  have HF: "H ∘ F = (λ x. nil ⊓ c;(c⋆ ⊓ x))" using F_def H_def by auto

  have adjoint: "dist_over_sup F" by (simp add: F_def inf_Sup)
  have monoH: "mono H" by (metis H_def inf_mono monoI order_refl seq_mono_right)
  have monoG: "mono G" by (metis G_def inf.absorb_iff2 monoI seq_inf_distrib)

  have "∀ x. ((F ∘ G) x = (H ∘ F) x)" using FG HF 
    by (metis fiter_unfold inf_sup_aci(2) seq_inf_distrib)
  then have "F (lfp G) = lfp H" using adjoint monoH monoG fusion_lfp_eq by blast
  then have "c⋆ ⊓ lfp (λ x. c;x) = lfp (λ x. nil ⊓ c;x)"
     using F_def G_def H_def by blast
  thus ?thesis by (simp add: infiter_def iter_def)
qed

lemma iter_induct_isolate: "c⋆;d ⊓ c∞ = lfp (λ x. d ⊓ c;x)"
proof - 
  define F where "F = (λ x. c⋆;d ⊓ x)"
  define G where "G = (λ x. c;x)"
  define H where "H = (λ x. d ⊓ c;x)"

  have FG: "F ∘ G = (λ x. c⋆;d ⊓ c;x)" using F_def G_def by auto
  have HF: "H ∘ F = (λ x. d ⊓ c;c⋆;d ⊓ c;x)" using F_def H_def weak_seq_inf_distrib
    by (metis comp_apply inf.commute inf.left_commute seq_assoc seq_inf_distrib)
  have unroll: "c⋆;d = (nil ⊓ c;c⋆);d" using fiter_unfold by auto
  have distribute: "c⋆;d = d ⊓ c;c⋆;d" by (simp add: unroll inf_seq_distrib)
  have FGx: "(F ∘ G) x = d ⊓ c;c⋆;d ⊓ c;x" using FG distribute by simp

  have adjoint: "dist_over_sup F" by (simp add: F_def inf_Sup)
  have monoH: "mono H" by (metis H_def inf_mono monoI order_refl seq_mono_right)
  have monoG: "mono G" by (metis G_def inf.absorb_iff2 monoI seq_inf_distrib)

  have "∀ x. ((F ∘ G) x = (H ∘ F) x)" using FGx HF by (simp add: FG distribute)
  then have "F (lfp G) = lfp H" using adjoint monoH monoG fusion_lfp_eq by blast
  then have "c⋆;d ⊓ lfp (λ x. c;x) = lfp (λ x. d ⊓ c;x)"
     using F_def G_def H_def by blast
  thus ?thesis by (simp add: infiter_def)
qed 

lemma iter_induct_eq: "cω;d = lfp (λ x. d ⊓ c;x)"
proof -
  have "cω;d = c⋆;d ⊓ c∞;d" by (simp add: isolation inf_seq_distrib)
  then have "c⋆;d ⊓ c∞;d = c⋆;d ⊓ c∞" by (simp add: infiter_annil)
  then have "c⋆;d ⊓ c∞ = lfp (λ x. d ⊓ c;x)" by (simp add: iter_induct_isolate)
  thus ?thesis 
    by (simp add: ‹cω ; d = c⋆ ; d ⊓ c∞ ; d› ‹c⋆ ; d ⊓ c∞ ; d = c⋆ ; d ⊓ c∞›)
qed

lemma iter_induct: "d ⊓ c;x ⊑ x ⟹ cω;d ⊑ x"
  by (simp add: iter_induct_eq lfp_lowerbound)

lemma iter_isolate: "c⋆;d ⊓ c∞ = cω;d"
  by (simp add: iter_induct_eq iter_induct_isolate)

lemma iter_isolate2: "c;c⋆;d ⊓ c∞ = c;cω;d"
  by (metis infiter_unfold iter_isolate seq_assoc seq_inf_distrib)

lemma iter_decomp: "(c ⊓ d)ω = cω;(d;cω)ω"
proof (rule antisym)
  have      "c;cω;(d;cω)ω ⊓ (d;cω)ω ⊑ cω;(d;cω)ω" by (metis inf_commute order.refl inf_seq_distrib seq_nil_left iter_unfold)
  thus "(c ⊓ d)ω ⊑ cω;(d;cω)ω" by (metis inf.left_commute iter_induct_nil iter_unfold seq_assoc inf_seq_distrib)
next
  have "(c;(c ⊓ d)ω ⊓ d;(c ⊓ d)ω) ⊓ nil ⊑ (c ⊓ d)ω" by (metis inf_commute order.refl inf_seq_distrib iter_unfold) 
  then have a: "cω;(d;(c ⊓ d)ω ⊓ nil) ⊑ (c ⊓ d)ω" 
  proof -
    have "nil ⊓ d;(c ⊓ d)ω ⊓ c;(c ⊓ d)ω ⊑ (c ⊓ d)ω"
      by (metis eq_iff inf.semigroup_axioms inf_commute inf_seq_distrib iter_unfold semigroup.assoc)
    thus ?thesis using iter_induct_eq by (metis inf_sup_aci(1) iter_induct) 
  qed
  then have "d;cω;(d;(c ⊓ d)ω ⊓ nil) ⊓ nil ⊑ d;(c ⊓ d)ω ⊓ nil" by (metis inf_mono order.refl seq_assoc seq_mono) 
  then have "(d;cω)ω ⊑ d;(c ⊓ d)ω ⊓ nil" by (metis inf_commute iter_induct_nil) 
  then have "cω;(d;cω)ω ⊑ cω;(d;(c ⊓ d)ω ⊓ nil)" by (metis order.refl seq_mono) 
  thus "cω;(d;cω)ω ⊑ (c ⊓ d)ω" using a refine_trans by blast
qed

lemma iter_leapfrog_var: "(c;d)ω;c ⊑ c;(d;c)ω"
proof -
  have "c ⊓ c;d;c;(d;c)ω ⊑ c;(d;c)ω"
    by (metis iter_unfold order_refl seq_assoc seq_inf_distrib seq_nil_right)
  thus ?thesis using iter_induct_eq by (metis iter_induct seq_assoc) 
qed

lemma iter_leapfrog: "c;(d;c)ω = (c;d)ω;c"
proof (rule antisym)
  show "(c;d)ω;c ⊑ c;(d;c)ω" by (metis iter_leapfrog_var)
next
  have "(d;c)ω ⊑ ((d;c)ω;d);c ⊓ nil" by (metis inf.bounded_iff order.refl seq_assoc seq_mono iter_unfold iter1 iter2) 
  then have "(d;c)ω ⊑ (d;(c;d)ω);c ⊓ nil" by (metis inf.absorb_iff2 inf.boundedE inf_assoc iter_leapfrog_var inf_seq_distrib)
  then have "c;(d;c)ω ⊑ c;d;(c;d)ω;c ⊓ nil;c" using inf.bounded_iff seq_assoc seq_mono_right seq_nil_left seq_nil_right by fastforce
  thus "c;(d;c)ω ⊑ (c;d)ω;c" by (metis inf_commute inf_seq_distrib iter_unfold) 
qed

lemma fiter_leapfrog: "c;(d;c)⋆ = (c;d)⋆;c"
proof -
  have lr: "c;(d;c)⋆ ⊑ (c;d)⋆;c"
  proof -
    have "(d ; c)⋆ = nil ⊓ d ; c ; (d ; c)⋆"
      by (meson finite_iteration.fiter_unfold finite_iteration_axioms)
    then show ?thesis
      by (metis fiter_induct seq_assoc seq_distrib_left.weak_seq_inf_distrib 
          seq_distrib_left_axioms seq_nil_right)
  qed
  have rl: "(c;d)⋆;c ⊑ c;(d;c)⋆" 
  proof -
    have a1: "(c;d)⋆;c = c ⊓ c;d;(c;d)⋆;c"
       by (metis finite_iteration.fiter_unfold finite_iteration_axioms 
           inf_seq_distrib seq_nil_left)  
    have a2: "(c;d)⋆;c ⊑ c;(d;c)⋆ ⟷ c ⊓ c;d;(c;d)⋆;c ⊑ c;(d;c)⋆" by (simp add: a1)  
    then have a3: "... ⟷ c;( nil ⊓ d;(c;d)⋆;c) ⊑ c;(d;c)⋆"
       by (metis a1 eq_iff fiter_unfold lr seq_assoc seq_inf_distrib seq_nil_right)  
    have a4: "(nil ⊓ d;(c;d)⋆;c) ⊑ (d;c)⋆ ⟹ c;( nil ⊓ d;(c;d)⋆;c) ⊑ c;(d;c)⋆"
       using seq_mono_right by blast
    have a5: "(nil ⊓ d;(c;d)⋆;c) ⊑ (d;c)⋆"
      proof -
        have f1: "d ; (c ; d)⋆ ; c ⊓ nil = d ; ((c ; d)⋆ ; c) ⊓ nil ⊓ nil"
           by (simp add: seq_assoc)
        have "d ; c ; (d ; (c ; d)⋆ ; c ⊓ nil) = d ; ((c ; d)⋆ ; c)"
           by (metis (no_types) a1 inf_sup_aci(1) seq_assoc 
                seq_finite_conjunctive.seq_inf_distrib seq_finite_conjunctive_axioms 
                seq_nil_right)
        then show ?thesis
           using f1 by (metis (no_types) finite_iteration.fiter_induct finite_iteration_axioms 
                           inf.cobounded1 inf_sup_aci(1) seq_nil_right)
     qed
   thus ?thesis using a2 a3 a4 by blast 
  qed
  thus ?thesis by (simp add: eq_iff lr)
qed

end


locale iteration_infinite_conjunctive = seq_infinite_conjunctive + iteration + infimum_nat

begin

lemma fiter_seq_choice: "c⋆ = (⨅i::nat. c ;^ i)"
proof (rule antisym)
  show "c⋆ ⊑ (⨅i. c ;^ i)"
  proof (rule INF_greatest) 
    fix i
    show "c⋆ ⊑ c ;^ i"
      proof (induct i type: nat)
        case 0
        show "c⋆ ⊑ c ;^ 0" by (simp add: fiter0)
      next
        case (Suc n)
        have "c⋆ ⊑ c ; c⋆" by (metis fiter_unfold inf_le2)
        also have "... ⊑ c ; (c ;^ n)" using Suc.hyps by (simp only: seq_mono_right)
        also have "... = c ;^ Suc n" by simp
        finally show "c⋆ ⊑ c ;^ Suc n" .
      qed
  qed
next
  have "(⨅i. c ;^ i) ⊑ (c ;^ 0) ⊓ (⨅i. c ;^ Suc i)"
    by (meson INF_greatest INF_lower UNIV_I le_inf_iff)
  also have "... = nil ⊓ (⨅i. c ; (c ;^ i))" by simp
  also have "... = nil ⊓ c ; (⨅i. c ;^ i)" by (simp add: seq_INF_distrib)
  finally show "(⨅i. c ;^ i) ⊑ c⋆" using fiter_induct by fastforce
qed

lemma fiter_seq_choice_nonempty: "c ; c⋆ = (⨅i∈{i. 0 < i}. c ;^ i)"
proof -
  have "(⨅i∈{i. 0 < i}. c ;^ i) = (⨅i. c ;^ (Suc i))" by (simp add: INF_nat_shift)
  also have "... = (⨅i. c ; (c ;^ i))" by simp
  also have "... = c ; (⨅i. c ;^ i)" by (simp add: seq_INF_distrib_UNIV)
  also have "... = c ; c⋆" by (simp add: fiter_seq_choice)
  finally show ?thesis by simp
qed

end

locale conj_iteration = cra + iteration_infinite_conjunctive

begin

lemma conj_distrib4: "c⋆ \<iinter> d⋆ ⊑ (c \<iinter> d)⋆"
proof -
  have "c⋆ \<iinter> d⋆ = (nil ⊓ (c;c⋆)) \<iinter> d⋆" by (metis fiter_unfold) 
  then have "c⋆ \<iinter> d⋆ = (nil \<iinter> d⋆) ⊓ ((c;c⋆) \<iinter> d⋆)" by (simp add: inf_conj_distrib) 
  then have "c⋆ \<iinter> d⋆ ⊑ nil ⊓ ((c;c⋆) \<iinter> (d;d⋆))" by (metis conj_idem fiter0 fiter_unfold inf.bounded_iff inf_le2 local.conj_mono)
  then have "c⋆ \<iinter> d⋆ ⊑ nil ⊓ ((c \<iinter> d);(c⋆ \<iinter> d⋆))" by (meson inf_mono_right order.trans sequential_interchange) 
  thus ?thesis by (metis seq_nil_right fiter_induct) 
qed

end

end