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