Quelle  Loops.thy

theory Loops
  imports Logic HOL.Wellfounded Expressivity
begin

section ‹Rules for Loops›

definition lnot where
  "lnot b σ = (¬b σ)"

definition if_then_else where
  "if_then_else b C1 C2 = If (Assume b;; C1) (Assume (lnot b);; C2)"

definition low_exp where
  "low_exp e S = (∀φ φ'. φ ∈ S ∧ φ' ∈ S ⟶ (e (snd φ) = e (snd φ')))"

lemma low_exp_lnot:
  "low_exp b S ⟷ low_exp (lnot b) S"
  by (simp add: lnot_def low_exp_def)

definition holds_forall where
  "holds_forall b S ⟷ (∀φ∈S. b (snd φ))"

lemma holds_forallI:
  assumes "∧φ. φ ∈ S ==> b (snd φ)"
  shows "holds_forall b S"
  using assms holds_forall_def by blast

lemma low_exp_two_cases:
  assumes "low_exp b S"
  shows "holds_forall b S ∨ holds_forall (lnot b) S"
  by (metis assms holds_forall_def lnot_def low_exp_def)

lemma sem_assume_low_exp:
  assumes "holds_forall b S"
  shows "sem (Assume b) S = S"
    and "sem (Assume (lnot b)) S = {}"
  using assume_sem[of b S] assms holds_forall_def[of b S] apply fastforce
  using assume_sem[of "lnot b" S] assms holds_forall_def[of b S] lnot_def[of b]
    by fastforce

lemma sem_assume_low_exp_seq:
  assumes "holds_forall b S"
  shows "sem (Assume b;; C) S = sem C S"
    and "sem (Assume (lnot b);; C) S = {}"
  apply (simp add: assms sem_assume_low_exp(1) sem_seq)
  by (metis assms empty_iff equals0I in_sem sem_assume_low_exp(2) sem_seq)

lemma lnot_involution:
  "lnot (lnot b) = b"
proof (rule ext)
  fix x show "lnot (lnot b) x = b x"
    by (simp add: lnot_def)
qed

lemma sem_if_then_else:
  shows "holds_forall b S ==> sem (if_then_else b C1 C2) S = sem C1 S"
    and "holds_forall (lnot b) S ==> sem (if_then_else b C1 C2) S = sem C2 S"
  apply (simp add: if_then_else_def sem_assume_low_exp_seq(1) sem_assume_low_exp_seq(2) sem_if)
  by (metis (no_types, opaque_lifting) if_then_else_def lnot_involution sem_assume_low_exp_seq(1) sem_assume_low_exp_seq(2) sem_if sup_bot_left)

lemma if_synchronized_aux:
  assumes "⊨ {P} C1 {Q}"
      and "⊨ {P} C2 {Q}"
      and "entails P (low_exp b)"
    shows "⊨ {P} if_then_else b C1 C2 {Q}"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "P S"
  then have r: "low_exp b S" using assms(3) entailsE
    by metis
  show "Q (sem (if_then_else b C1 C2) S)"
  proof (cases "holds_forall b S")
    case True
    then show ?thesis
      by (metis asm0 assms(1) hyper_hoare_triple_def sem_if_then_else(1))
  next
    case False
    then show ?thesis
      by (metis asm0 assms(2) hyper_hoare_tripleE low_exp_two_cases r sem_if_then_else(2))
  qed
qed

theorem if_synchronized:
  assumes "⊨ {conj P (holds_forall b)} C1 {Q}"
      and "⊨ {conj P (holds_forall (lnot b))} C2 {Q}"
    shows "⊨ {conj P (low_exp b)} if_then_else b C1 C2 {Q}"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "conj P (low_exp b) S"
  show "Q (sem (if_then_else b C1 C2) S)"
  proof (cases "holds_forall b S")
    case True
    then show ?thesis
      by (metis asm0 assms(1) conj_def hyper_hoare_triple_def sem_if_then_else(1))
  next
    case False
    then show ?thesis
      by (metis asm0 assms(2) conj_def hyper_hoare_triple_def low_exp_two_cases sem_if_then_else(2))
  qed
qed


definition while_cond where
  "while_cond b C = While (Assume b;; C);; Assume (lnot b)"


lemma while_synchronized_rec:
  assumes "∧n. ⊨ {conj (I n) (holds_forall b)} Assume b;; C {conj (I (Suc n)) (low_exp b)}"
      and "conj (I 0) (low_exp b) S"
    shows "conj (I n) (low_exp b) (iterate_sem n (Assume b;; C) S) ∨ holds_forall (lnot b) (iterate_sem n (Assume b;; C) S)"
  using assms
proof (induct n)
  case (Suc n)
  then have r: "conj (I n) (low_exp b) (iterate_sem n (Assume b;; C) S) ∨ holds_forall (lnot b) (iterate_sem n (Assume b;; C) S)"
    by blast
  then show ?case
  proof (cases "conj (I n) (holds_forall b) (iterate_sem n (Assume b;; C) S)")
    case True
    then show ?thesis
      using Suc.prems(1) hyper_hoare_tripleE by fastforce
  next
    case False
    then have "holds_forall (lnot b) (iterate_sem n (Assume b;; C) S)"
      by (metis conj_def low_exp_two_cases r)
    then have "iterate_sem (Suc n) (Assume b;; C) S = {}"
      by (metis iterate_sem.simps(2) lnot_involution sem_assume_low_exp_seq(2))
    then show ?thesis
      by (simp add: holds_forall_def)
  qed
qed (auto)

lemma false_then_empty_later:
  assumes "holds_forall (lnot b) (iterate_sem n (Assume b;; C) S)"
      and "m > n"
    shows "iterate_sem m (Assume b;; C) S = {}"
  using assms
proof (induct "m - n" arbitrary: n m)
  case (Suc x)
  then show ?case
  proof (cases x)
    case 0
    then show ?thesis
      by (metis One_nat_def Suc.hyps(2) Suc.prems(1) Suc.prems(2) Suc_eq_plus1 iterate_sem.simps(2) le_add_diff_inverse linorder_not_le lnot_involution order.asym sem_assume_low_exp_seq(2))
  next
    case (Suc nat)
    then have "m - 1 > n"
      using Suc.hyps(2) by auto
    then have "iterate_sem (m-1) (Assume b ;; C) S = {}"
      by (metis (no_types, lifting) Suc.hyps(1) Suc.hyps(2) Suc.prems(1) diff_Suc_1 diff_commute)
    then show ?thesis
      by (metis Nat.lessE Suc.prems(1) Suc.prems(2) diff_Suc_1 iterate_sem.simps(2) sem_assume_low_exp_seq(2) sem_seq)
  qed
qed (simp)

lemma split_union_triple:
  "(∪(m::nat). f m) = (∪m∈{m |m. m < n}. f m) ∪ f n ∪ (∪m∈{m |m. m > n}. f m)" (is "?A = ?B")
proof
  show "?B ⊆ ?A"
    by blast
  show "?A ⊆ ?B"
  proof
    fix x assume "x ∈ ?A"
    then obtain m where "x ∈ f m"
      by blast
    then have "m < n ∨ m = n ∨ m > n"
      by force
    then show "x ∈ ?B"
      using ‹x ∈ f m› by auto
  qed
qed


lemma sem_union_swap:
  "sem C (∪x∈S. f x) = (∪x∈S. sem C (f x))" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof
    fix y assume "y ∈ ?A"
    then obtain x where "x ∈ S" "y ∈ sem C (f x)"
      using UN_iff in_sem[of y C] by force
    then show "y ∈ ?B"
      by blast
  qed
  show "?B ⊆ ?A"
    by (simp add: SUP_least SUP_upper sem_monotonic)
qed



lemma while_synchronized_case_1:
  assumes "∧m. m < n ==> holds_forall b (iterate_sem m (Assume b;; C) S)"
      and "holds_forall (lnot b) (iterate_sem n (Assume b;; C) S)"
      and "∧n. ⊨ {conj (I n) (holds_forall b)} Assume b;; C {conj (I (Suc n)) (low_exp b)}"
      and "conj (I 0) (low_exp b) S"
    shows "sem (while_cond b C) S = iterate_sem n (Assume b;; C) S"
proof -
  have "∧m. m > n ==> iterate_sem m (Assume b;; C) S = {}"
    using assms(2) false_then_empty_later by blast
  moreover have "sem (While (Assume b;; C)) S =
  (∪m∈{m|m. m < n}. iterate_sem m (Assume b ;; C) S) ∪ iterate_sem n (Assume b ;; C) S ∪ (∪m∈{m|m. m > n}. iterate_sem m (Assume b ;; C) S)"
    using sem_while[of "Assume b;; C" S] split_union_triple by metis
  ultimately have "sem (While (Assume b;; C)) S = (∪m∈{m|m. m < n}. iterate_sem m (Assume b ;; C) S) ∪ iterate_sem n (Assume b ;; C) S "
    by auto
  moreover have "∧m. m < n ==> sem (Assume (lnot b)) (iterate_sem m (Assume b ;; C) S) = {}"
    using assms(1) sem_assume_low_exp(2) by blast
  then have "sem (Assume (lnot b)) (∪m∈{m|m. m < n}. iterate_sem m (Assume b ;; C) S) = {}"
    by (simp add: sem_union_swap)
  then have "sem (while_cond b C) S = sem (Assume (lnot b)) (iterate_sem n (Assume b ;; C) S)"
    by (simp add: calculation sem_seq sem_union while_cond_def)
  then show ?thesis
    using assms(2) sem_assume_low_exp(1) by blast
qed

lemma while_synchronized_case_2:
  assumes "∧m. holds_forall b (iterate_sem m (Assume b;; C) S)"
      and "∧n. ⊨ {conj (I n) (holds_forall b)} Assume b;; C {conj (I (Suc n)) (low_exp b)}"
      and "conj (I 0) (low_exp b) S"
  shows "sem (while_cond b C) S = {}"
proof -
  have "sem (While (Assume b ;; C)) S = (∪n. iterate_sem n (Assume b ;; C) S)"
    by (simp add: sem_while)
  then have "holds_forall b (sem (While (Assume b;; C)) S)"
    by (metis (no_types, lifting) UN_iff assms(1) holds_forall_def)
  then show ?thesis
    by (simp add: sem_assume_low_exp(2) sem_seq while_cond_def)
qed

definition emp where
  "emp S ⟷ S = {}"

lemma holds_forall_empty:
  "holds_forall b {}"
  by (simp add: holds_forall_def)

definition exists where
  "exists I S ⟷ (∃n. I n S)"

theorem while_synchronized:
  assumes "∧n. ⊨ {conj (I n) (holds_forall b)} C {conj (I (Suc n)) (low_exp b)}"
  shows "⊨ {conj (I 0) (low_exp b)} while_cond b C {conj (disj (exists I) emp) (holds_forall (lnot b))}"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "conj (I 0) (low_exp b) S"
  have triple: "∧n. ⊨ {conj (I n) (holds_forall b)} Assume b ;; C {conj (I (Suc n)) (low_exp b)}"
  proof (rule hyper_hoare_tripleI)
    fix n S assume "conj (I n) (holds_forall b) S"
    then have "sem (Assume b) S = S"
      by (simp add: conj_def sem_assume_low_exp(1))
    then show "conj (I (Suc n)) (low_exp b) (sem (Assume b ;; C) S)"
      by (metis ‹conj (I n) (holds_forall b) S› assms hyper_hoare_tripleE sem_seq)
  qed
  show "conj (disj (exists I) emp) (holds_forall (lnot b)) (sem (while_cond b C) S)"
  proof (cases "∀m. holds_forall b (iterate_sem m (Assume b;; C) S)")
    case True
    then have "sem (while_cond b C) S = {}"
      using while_synchronized_case_2[of b C S I]
      by (metis (no_types, opaque_lifting) asm0 assms hyper_hoare_tripleI conj_def sem_assume_low_exp(1) seq_rule)
    then show ?thesis
      by (simp add: disj_def conj_def emp_def holds_forall_empty)
  next
    case False
    then have F: "¬ (∀m. holds_forall b (iterate_sem m (Assume b;; C) S))" by simp
    have "∃n. (∀m. m < n ⟶ holds_forall b (iterate_sem m (Assume b;; C) S)) ∧ holds_forall (lnot b) (iterate_sem n (Assume b;; C) S)"
    proof (cases "∃n. ¬ holds_forall b (iterate_sem n (Assume b;; C) S) ∧ iterate_sem n (Assume b;; C) S ≠ {}")
      case True
      then obtain n where "¬ holds_forall b (iterate_sem n (Assume b;; C) S) ∧ iterate_sem n (Assume b;; C) S ≠ {}"
        by blast
      then have "holds_forall (lnot b) (iterate_sem n (Assume b;; C) S)"
        by (metis asm0 conj_def low_exp_two_cases triple while_synchronized_rec)
      moreover have "∧m. m < n ==> holds_forall b (iterate_sem m (Assume b;; C) S)"
      proof -
        fix m assume asm1: "m < n"
        show "holds_forall b (iterate_sem m (Assume b;; C) S)"
        proof (rule ccontr)
          assume "¬ holds_forall b (iterate_sem m (Assume b ;; C) S)"
          then have "holds_forall (lnot b) (iterate_sem m (Assume b;; C) S)"
            by (metis asm0 conj_def low_exp_two_cases triple while_synchronized_rec)
          then have "iterate_sem n (Assume b;; C) S = {}"
            using asm1 false_then_empty_later by blast
          then show False
            using ‹¬ holds_forall b (iterate_sem n (Assume b ;; C) S) ∧ iterate_sem n (Assume b ;; C) S ≠ {}› by fastforce
        qed
      qed
      ultimately show ?thesis 
        by blast
    next
      case False
      then have "∧n. holds_forall b (iterate_sem n (Assume b;; C) S)"
        using holds_forall_empty by fastforce
      then show ?thesis using F by blast
    qed
    then obtain n where "∧m. m < n ==> holds_forall b (iterate_sem m (Assume b;; C) S)"
      and "holds_forall (lnot b) (iterate_sem n (Assume b;; C) S)"
      by blast
    then have "sem (while_cond b C) S = iterate_sem n (Assume b;; C) S"
      using triple
    proof (rule while_synchronized_case_1)
    qed (simp_all add: asm0)
    moreover have "I n (iterate_sem n (Assume b;; C) S)"
    proof (cases n)
      case 0
      then show ?thesis
        by (metis asm0 iterate_sem.simps(1) conj_def)
    next
      case (Suc k)
      then have "conj (I k) (low_exp b) (iterate_sem k (Assume b ;; C) S) ∨ holds_forall (lnot b) (iterate_sem k (Assume b ;; C) S)"
        using while_synchronized_rec[of I b C S k] asm0 triple by blast      
      then show ?thesis
      proof (cases "conj (I k) (low_exp b) (iterate_sem k (Assume b ;; C) S)")
        case True
        then show ?thesis
          using conj_def[of _ "holds_forall b"] conj_def[of _ "low_exp b"] Suc
            ‹∧m. m < n ==> holds_forall b (iterate_sem m (Assume b ;; C) S)› assms
            hyper_hoare_triple_def[of ] iterate_sem.simps(2) lessI sem_assume_low_exp(1)[of b "iterate_sem k (Assume b ;; C) S"]
            sem_seq[of "Assume b" C] by metis
      next
        case False
        then show ?thesis
          by (metis F Suc ‹∧m. m < n ==> holds_forall b (iterate_sem m (Assume b ;; C) S)› ‹conj (I k) (low_exp b) (iterate_sem k (Assume b ;; C) S) ∨ holds_forall (lnot b) (iterate_sem k (Assume b ;; C) S)› empty_iff false_then_empty_later holds_forall_def not_less_eq)
      qed
    qed
    ultimately show ?thesis
      by (metis disj_def Loops.exists_def ‹holds_forall (lnot b) (iterate_sem n (Assume b ;; C) S)› conj_def)
  qed
qed

lemma WhileSync_simpler:
  assumes "⊨ {conj I (holds_forall b)} C {conj I (low_exp b)}"
  shows "⊨ {conj I (low_exp b)} while_cond b C {conj (disj I emp) (holds_forall (lnot b))}"
  using assms while_synchronized[of "λn. I"]
  by (simp add: disj_def Loops.exists_def conj_def hyper_hoare_triple_def)

definition if_then where
  "if_then b C = If (Assume b;; C) (Assume (lnot b))"

definition filter_exp where
  "filter_exp b S = Set.filter (b ∘ snd) S"

lemma filter_exp_union:
  "filter_exp b (S1 ∪ S2) = filter_exp b S1 ∪ filter_exp b S2" (is "?A = ?B")
  by (auto simp add: filter_exp_def)

lemma filter_exp_union_general:
  "filter_exp b (∪x. f x) = (∪x. filter_exp b (f x))" (is "?A = ?B")
  by (auto simp add: filter_exp_def)

lemma filter_exp_contradict:
  "filter_exp b (filter_exp (lnot b) S) = {}"
  by (auto simp add: filter_exp_def lnot_def)

lemma filter_exp_same:
  "filter_exp b (filter_exp b S) = filter_exp b S" (is "?A = ?B")
  by (auto simp add: filter_exp_def)

lemma if_then_sem:
  "sem (if_then b C) S = sem C (filter_exp b S) ∪ filter_exp (lnot b) S"
  by (simp add: assume_sem filter_exp_def if_then_def sem_if sem_seq)

fun union_up_to_n where
  "union_up_to_n C S 0 = iterate_sem 0 C S"
| "union_up_to_n C S (Suc n) = iterate_sem (Suc n) C S ∪ union_up_to_n C S n"

lemma union_up_to_increasing:
  assumes "m ≤ n"
  shows "union_up_to_n C S m ⊆ union_up_to_n C S n"
  using assms
proof (induct "n - m" arbitrary: m n)
  case (Suc x)
  then show ?case
    by (simp add: lift_Suc_mono_le)
qed (simp)

lemma union_union_up_to_n_equiv_aux:
  "union_up_to_n C S n ⊆ (∪m. iterate_sem m C S)"
proof (induct n)
  case 0
  then show ?case
    by (metis UN_upper iso_tuple_UNIV_I union_up_to_n.simps(1))
next
  case (Suc n)
  show ?case
  proof
    fix x assume "x ∈ union_up_to_n C S (Suc n)" (* \<subseteq> (\<Union>m. iterate_sem m C S) *)
    then have "x ∈ iterate_sem (Suc n) C S ∨ x ∈ union_up_to_n C S n"
      by simp
    then show "x ∈ (∪m. iterate_sem m C S)"
      using Suc by blast
  qed
qed

lemma union_union_up_to_n_equiv:
  "(∪n. union_up_to_n C S n) = (∪n. iterate_sem n C S)" (is "?A = ?B")
proof
  show "?B ⊆ ?A"
    by (metis (no_types, lifting) SUP_subset_mono UnCI subsetI union_up_to_n.elims)
  show "?A ⊆ ?B"
    by (simp add: SUP_le_iff union_union_up_to_n_equiv_aux)
qed


lemma filter_exp_union_itself:
  "filter_exp b S ∪ S = S"
  by (auto simp add: filter_exp_def)

lemma iterate_sem_equiv:
  "iterate_sem m (if_then b C) S
  = filter_exp (lnot b) (union_up_to_n (Assume b;; C) S m) ∪ iterate_sem m (Assume b;; C) S"
proof (induct m)
  case 0
  have "union_up_to_n (Assume b ;; C) S 0 = S"
    by auto
  then show "iterate_sem 0 (if_then b C) S = filter_exp (lnot b) (union_up_to_n (Assume b ;; C) S 0) ∪ iterate_sem 0 (Assume b ;; C) S"
    by (auto simp add: filter_exp_def)
next
  case (Suc m)

  let ?S = "iterate_sem m (if_then b C) S"
  let ?SU = "union_up_to_n (Assume b ;; C) S m"
  let ?SN = "iterate_sem m (Assume b ;; C) S"
  have "iterate_sem (Suc m) (if_then b C) S = sem C (filter_exp b ?S) ∪ filter_exp (lnot b) ?S"
    by (simp add: if_then_sem)
  also have "... = sem C (filter_exp b (filter_exp (lnot b) ?SU)) ∪ sem C (filter_exp b ?SN)
  ∪ filter_exp (lnot b) (filter_exp (lnot b) ?SU) ∪ filter_exp (lnot b) ?SN"
    by (simp add: Suc filter_exp_union sem_union sup_assoc)
  also have "... = sem C (filter_exp b ?SN) ∪ filter_exp (lnot b) ?SU ∪ filter_exp (lnot b) ?SN"
    by (metis Un_empty_left filter_exp_contradict filter_exp_same sem_union)
  moreover have "iterate_sem (Suc m) (Assume b ;; C) S = sem C (filter_exp b ?SN)"
    by (simp add: assume_sem filter_exp_def sem_seq)
  moreover have "union_up_to_n (Assume b ;; C) S (Suc m) = sem C (filter_exp b ?SN) ∪ ?SU"
    using calculation(3) by force
  moreover have "filter_exp (lnot b) (union_up_to_n (Assume b ;; C) S (Suc m)) ∪ iterate_sem (Suc m) (Assume b ;; C) S
  = filter_exp (lnot b) (sem C (filter_exp b ?SN) ∪ ?SU) ∪ sem C (filter_exp b ?SN)"
    using calculation(3) by force
  then have "... = filter_exp (lnot b) ?SU ∪ sem C (filter_exp b ?SN)"
    using filter_exp_union_itself[of "lnot b"] filter_exp_union[of "lnot b"] Un_commute sup_assoc by blast
  moreover have "?SN ⊆ ?SU"
    by (metis UnCI subsetI union_up_to_n.elims)
  ultimately have "filter_exp (lnot b) ?SU ∪ sem C (filter_exp b ?SN)
  = sem C (filter_exp b ?SN) ∪ filter_exp (lnot b) ?SU ∪ filter_exp (lnot b) ?SN"
    using filter_exp_union[of "lnot b" ?SU ?SN]
    using Un_commute[of "filter_exp (lnot b) ?SU" "sem C (filter_exp b ?SN)"]
      sup.orderE sup_assoc[of "sem C (filter_exp b ?SN)"] by metis
  then show ?case
    using ‹filter_exp (lnot b) (sem C (filter_exp b (iterate_sem m (Assume b ;; C) S)) ∪ union_up_to_n (Assume b ;; C) S m) ∪ sem C (filter_exp b (iterate_sem m (Assume b ;; C) S)) = filter_exp (lnot b) (union_up_to_n (Assume b ;; C) S m) ∪ sem C (filter_exp b (iterate_sem m (Assume b ;; C) S))› ‹iterate_sem (Suc m) (Assume b ;; C) S = sem C (filter_exp b (iterate_sem m (Assume b ;; C) S))› ‹iterate_sem (Suc m) (if_then b C) S = sem C (filter_exp b (iterate_sem m (if_then b C) S)) ∪ filter_exp (lnot b) (iterate_sem m (if_then b C) S)› ‹sem C (filter_exp b (filter_exp (lnot b) (union_up_to_n (Assume b ;; C) S m))) ∪ sem C (filter_exp b (iterate_sem m (Assume b ;; C) S)) ∪ filter_exp (lnot b) (filter_exp (lnot b) (union_up_to_n (Assume b ;; C) S m)) ∪ filter_exp (lnot b) (iterate_sem m (Assume b ;; C) S) = sem C (filter_exp b (iterate_sem m (Assume b ;; C) S)) ∪ filter_exp (lnot b) (union_up_to_n (Assume b ;; C) S m) ∪ filter_exp (lnot b) (iterate_sem m (Assume b ;; C) S)› ‹sem C (filter_exp b (iterate_sem m (if_then b C) S)) ∪ filter_exp (lnot b) (iterate_sem m (if_then b C) S) = sem C (filter_exp b (filter_exp (lnot b) (union_up_to_n (Assume b ;; C) S m))) ∪ sem C (filter_exp b (iterate_sem m (Assume b ;; C) S)) ∪ filter_exp (lnot b) (filter_exp (lnot b) (union_up_to_n (Assume b ;; C) S m)) ∪ filter_exp (lnot b) (iterate_sem m (Assume b ;; C) S)› by auto
qed


lemma sem_while_with_if:
  "sem (while_cond b C) S = filter_exp (lnot b) (∪n. iterate_sem n (if_then b C) S)"
proof -
  have "(∪n. iterate_sem n (if_then b C) S)
  = (∪n. filter_exp (lnot b) (union_up_to_n (Assume b;; C) S n) ∪ iterate_sem n (Assume b;; C) S)"
    by (simp add: iterate_sem_equiv)
  also have "... = filter_exp (lnot b) (∪n. union_up_to_n (Assume b;; C) S n) ∪ (∪n. iterate_sem n (Assume b;; C) S)"
    by (simp add: complete_lattice_class.SUP_sup_distrib filter_exp_union_general)
  also have "... = filter_exp (lnot b) (∪n. iterate_sem n (Assume b;; C) S) ∪ (∪n. iterate_sem n (Assume b;; C) S)"
    by (simp add: union_union_up_to_n_equiv)
  also have "... = (∪n. iterate_sem n (Assume b;; C) S)"
    by (meson filter_exp_union_itself)
  moreover have "sem (while_cond b C) S = filter_exp (lnot b) (∪n. iterate_sem n (Assume b ;; C) S)"
    by (simp add: assume_sem filter_exp_def sem_seq sem_while while_cond_def)
  ultimately show ?thesis
    by presburger
qed

lemma iterate_sem_assume_increasing:
  "filter_exp (lnot b) (iterate_sem n (if_then b C) S) ⊆ filter_exp (lnot b) (iterate_sem (Suc n) (if_then b C) S)"
  by (auto simp add: filter_exp_def lnot_def if_then_sem)

lemma iterate_sem_assume_increasing_union_up_to:
  "filter_exp (lnot b) (iterate_sem n (if_then b C) S) = filter_exp (lnot b) (union_up_to_n (if_then b C) S n)"
proof (induct n)
  case (Suc n)
  then show ?case
    by (metis filter_exp_union iterate_sem_assume_increasing sup.orderE union_up_to_n.simps(2))
qed (simp)

(* Set becomes larger *)
definition ascending :: "(nat ==> 'b set) ==> bool" where
  "ascending S ⟷ (∀n m. n ≤ m ⟶ S n ⊆ S m)"

lemma ascendingI_direct:
  assumes "∧n m. n ≤ m ==> S n ⊆ S m"
  shows "ascending S"
  by (simp add: ascending_def assms)

lemma ascendingI:
  assumes "∧n. S n ⊆ S (Suc n)"
  shows "ascending S"
proof (rule ascendingI_direct)
  fix n m :: nat assume asm0: "n ≤ m"
  moreover have "n ≤ m ==> S n ⊆ S m"
  proof (induct "m - n" arbitrary: m n)
    case (Suc x)
    then show ?case
      using assms lift_Suc_mono_le by blast
  qed (simp)
  ultimately show "S n ⊆ S m" 
    by blast
qed



definition upwards_closed where
  "upwards_closed P P_inf ⟷ (∀S. ascending S ∧ (∀n. P n (S n)) ⟶ P_inf (∪n. S n))"

lemma upwards_closedI:
  assumes "∧S. ascending S ==> (∀n. P n (S n)) ==> P_inf (∪n. S n)"
  shows "upwards_closed P P_inf"
  using assms upwards_closed_def by blast

lemma upwards_closedE:
  assumes "upwards_closed P P_inf"
      and "ascending S"
      and "∧n. P n (S n)"
    shows "P_inf (∪n. S n)"
  using assms(1) assms(2) assms(3) upwards_closed_def by blast

lemma ascending_iterate_filter:
  "ascending (λn. filter_exp (lnot b) (union_up_to_n (if_then b C) S n))"
  by (metis ascendingI iterate_sem_assume_increasing iterate_sem_assume_increasing_union_up_to)


theorem while_general:
  assumes "∧n. ⊨ {P n} if_then b C {P (Suc n)}"
      and "∧n. ⊨ {P n} Assume (lnot b) {Q n}"
      and "upwards_closed Q Q_inf"
    shows "⊨ {P 0} while_cond b C {conj Q_inf (holds_forall (lnot b))}"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "P 0 S"
  then have "∧n. P n (iterate_sem n (if_then b C) S)"
    by (meson assms(1) indexed_invariant_then_power)
  then have "∧n. Q n (filter_exp (lnot b) (union_up_to_n (if_then b C) S n))"
    by (metis assms(2) assume_sem filter_exp_def hyper_hoare_triple_def iterate_sem_assume_increasing_union_up_to)
  moreover have "ascending (λn. filter_exp (lnot b) (union_up_to_n (if_then b C) S n))"
    by (simp add: ascending_iterate_filter)
  ultimately have "Q_inf (sem (while_cond b C) S)"
    by (metis (no_types, lifting) SUP_cong assms(3) filter_exp_union_general iterate_sem_assume_increasing_union_up_to sem_while_with_if upwards_closed_def)
  then show "Logic.conj Q_inf (holds_forall (lnot b)) (sem (while_cond b C) S)"
    by (simp add: conj_def filter_exp_def holds_forall_def sem_while_with_if)
qed

definition while_loop_assertion_n where
  "while_loop_assertion_n C S0 n S ⟷ (S = union_up_to_n C S0 n)"

definition while_loop_assertion_inf where
  "while_loop_assertion_inf C S0 S ⟷ (S = (∪n. union_up_to_n C S0 n))"

(* Probably could have completeness with this? *)
lemma while_loop_assertion_upwards_closed:
  "upwards_closed (while_loop_assertion_n C S0) (while_loop_assertion_inf C S0)"
proof (rule upwards_closedI)
  fix S assume asm0: "ascending S" "∀n. while_loop_assertion_n C S0 n (S n)"
  then have "∧n. S n = union_up_to_n C S0 n"
    by (simp add: while_loop_assertion_n_def)
  then have "∪ (range S) = (∪n. union_up_to_n C S0 n)"
    by auto
  then show "while_loop_assertion_inf C S0 (∪ (range S))"
    by (simp add: while_loop_assertion_inf_def)
qed

(* Each element is either always in the sets, or never in the sets, from some point *)
definition converges_sets where
  "converges_sets S ⟷ (∀x. ∃n. (∀m. m ≥ n ⟶ (x ∈ S m)) ∨ (∀m. m ≥ n ⟶ (x ∉ S m)))"

lemma converges_setsI:
  assumes "∧x. ∃n. (∀m. m ≥ n ⟶ (x ∈ S m)) ∨ (∀m. m ≥ n ⟶ (x ∉ S m))"
  shows "converges_sets S"
  by (simp add: assms converges_sets_def)

lemma ascending_converges:
  assumes "ascending S"
  shows "converges_sets S"
proof (rule converges_setsI)
  fix x
  show "∃n. (∀m≥n. x ∈ S m) ∨ (∀m≥n. x ∉ S m)"
  proof (cases "x ∈ (∪n. S n)")
    case True
    then show ?thesis
      by (meson ascending_def assms in_mono)
  qed (blast)
qed

(* Set becomes smaller *)
definition descending :: "(nat ==> 'b set) ==> bool" where
  "descending S ⟷ (∀n m. n ≥ m ⟶ S n ⊆ S m)"

lemma descending_converges:
  assumes "descending S"
  shows "converges_sets S"
proof (rule converges_setsI)
  fix x
  show "∃n. (∀m≥n. x ∈ S m) ∨ (∀m≥n. x ∉ S m)"
  proof (cases "x ∈ (∩n. S n)")
    case False
    then show ?thesis
      by (meson assms descending_def in_mono)
  qed (blast)
qed


definition limit_sets where
  "limit_sets S = {x |x. ∃n. ∀m. m ≥ n ⟶ (x ∈ S m)}"

lemma in_limit_sets:
  "x ∈ limit_sets S ⟷ (∃n. ∀m. m ≥ n ⟶ (x ∈ S m))"
  by (simp add: limit_sets_def)

lemma ascending_limits_union:
  assumes "ascending S"
  shows "limit_sets S = (∪n. S n)" (is "?A = ?B")
proof
  show "?A ⊆ ?B" using limit_sets_def[of S] by auto
  show "?B ⊆ ?A"
  proof
    fix x assume "x ∈ ?B"
    then obtain n where "x ∈ S n"
      by blast
    then have "∀m. m ≥ n ⟶ (x ∈ S m)"
      by (meson ascending_def assms subsetD)
    then show "x ∈ ?A"
      using limit_sets_def[of S] by auto
  qed
qed

lemma descending_limits_union:
  assumes "descending S"
  shows "limit_sets S = (∩n. S n)" (is "?A = ?B")
proof
  show "?B ⊆ ?A" using limit_sets_def[of S] by fastforce
  show "?A ⊆ ?B"
  proof
    fix x assume "x ∈ ?A"
    then obtain n where "∀m. m ≥ n ⟶ (x ∈ S m)"
      using limit_sets_def[of S] by blast
    then have "∀m. m < n ⟶ (x ∈ S m)"
      by (meson assms descending_def lessI less_imp_le_nat subsetD)
    then show "x ∈ ?B"
      by (meson INT_I ‹∀m≥n. x ∈ S m› linorder_not_le)
  qed
qed



definition t_closed where
  "t_closed P P_inf ⟷ (∀S. converges_sets S ∧ (∀n. P n (S n)) ⟶ P_inf (limit_sets S))"

lemma t_closed_implies_u_closed:
  assumes "t_closed P P_inf"
  shows "upwards_closed P P_inf"
proof (rule upwards_closedI)
  fix S assume "ascending S" "∀n. P n (S n)"
  then have "converges_sets S"
    using ascending_converges by blast
  then show "P_inf (∪ (range S))"
    by (metis ‹∀n. P n (S n)› ‹ascending S› ascending_limits_union assms t_closed_def)
qed

(* forall assertions *)
definition downwards_closed where
  "downwards_closed P_inf ⟷ (∀S S'. S ⊆ S' ∧ P_inf S' ⟶ P_inf S)"

(* Slight change compared to Ellora paper *)
definition d_closed where
  "d_closed P P_inf ⟷ t_closed P P_inf ∧ downwards_closed P_inf"

lemma converges_to_merged:
  assumes "∧x. x ∈ S_inf ==> ∃n. ∀m. m ≥ n ⟶ (x ∈ S (m::nat))"
      and "∧x. x ∉ S_inf ==> ∃n. ∀m. m ≥ n ⟶ (x ∉ S m)"
    shows "converges_sets S ∧ limit_sets S = S_inf"
proof (rule conjI)
  show "converges_sets S" using converges_setsI assms by metis
  show "limit_sets S = S_inf" (is "?A = ?B")
  proof
    show "?B ⊆ ?A"
      by (simp add: assms(1) limit_sets_def subsetI)
    show "?A ⊆ ?B"
    proof
      fix x assume "x ∈ ?A"
      then obtain n where n_def: "∀m. m ≥ n ⟶ (x ∈ S m)"
        using in_limit_sets by metis
      show "x ∈ ?B"
      proof (rule ccontr)
        assume "x ∉ S_inf"
        then obtain n' where "∀m. m ≥ n' ⟶ (x ∉ S m)"
          using assms(2) by presburger
        then have "x ∈ S (max n n') ∧ x ∉ S (max n n')"
          using n_def by fastforce
        then show False by blast
      qed
    qed
  qed
qed

lemma ascending_union_up:
  "ascending (λn. union_up_to_n C S n)"
  by (simp add: ascending_def union_up_to_increasing)

(* actually ascending... *)
lemma converges_union:
  "converges_sets (λn. union_up_to_n C S n) ∧ limit_sets (λn. union_up_to_n C S n) = (∪n. union_up_to_n C S n)"
proof (rule converges_to_merged)
  fix x
  show "x ∈ ∪ (range (union_up_to_n C S)) ==> ∃n. ∀m≥n. x ∈ union_up_to_n C S m"
    by (meson UN_iff subset_eq union_up_to_increasing)
  show "x ∉ ∪ (range (union_up_to_n C S)) ==> ∃n. ∀m≥n. x ∉ union_up_to_n C S m"
    by blast
qed


theorem while_d:
  assumes "∧n. ⊨ {P n} if_then b C {P (Suc n)}"
      and "upwards_closed P P_inf"
      and "∧n. downwards_closed (P n)" ―‹Satisfied by hyper-assertions that do not existentially quantify over states›
    shows "⊨ {P 0} while_cond b C {conj P_inf (holds_forall (lnot b))}"
  using assms(1)
proof (rule while_general)
  show "upwards_closed P P_inf"
    using assms(2) by blast
  fix n show "⊨ {P n} Assume (lnot b) {P n}"
  proof (rule hyper_hoare_tripleI)
    fix S assume "P n S"
    moreover have "sem (Assume (lnot b)) S ⊆ S"
      by (simp add: assume_sem)
    ultimately show "P n (sem (Assume (lnot b)) S)"
      by (meson assms(3) downwards_closed_def)
  qed
qed



lemma in_union_up_to:
  "x ∈ union_up_to_n C S n ⟷ (∃m. m ≤ n ∧ x ∈ iterate_sem m C S)"
proof (induct n)
  case (Suc n)
  then show ?case
    by (metis UnCI UnE le_SucE le_SucI order_refl union_up_to_n.simps(2))
qed (simp)


theorem rule_while_terminates_strong:
  assumes "∧n. n < m ==> ⊨ {P n} if_then b C {P (Suc n)}"
      and "∧S. P m S ⟶ holds_forall (lnot b) S"
  shows "⊨ {P 0} while_cond b C {P m}"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "P 0 S"
  let ?S = "iterate_sem m (if_then b C) S"
  let ?S' = "iterate_sem (Suc m) (if_then b C) S"
  have "P m ?S"
    using asm0 assms(1) indexed_invariant_then_power_bounded by blast
  then have "holds_forall (lnot b) ?S"    
    using assms(2) by auto
  moreover have "sem (while_cond b C) S = filter_exp (lnot b) (∪n. iterate_sem n (Assume b ;; C) S)"
    by (simp add: assume_sem filter_exp_def sem_seq sem_while while_cond_def)


(* this is constant *)
  then have "P m (filter_exp (lnot b) (union_up_to_n (Assume b;; C) S m) ∪ iterate_sem m (Assume b;; C) S)"
    by (metis ‹P m (iterate_sem m (if_then b C) S)› iterate_sem_equiv)

  moreover have "iterate_sem m (Assume b;; C) S ⊆ filter_exp (lnot b) (union_up_to_n (Assume b;; C) S m)"
  proof
    fix x assume "x ∈ iterate_sem m (Assume b;; C) S"
    then have "x ∈ union_up_to_n (Assume b;; C) S m"
      by (metis UnCI union_up_to_n.elims)
    then have "x ∈ ?S"
      by (simp add: ‹x ∈ iterate_sem m (Assume b ;; C) S› iterate_sem_equiv)
    then have "lnot b (snd x)"
      by (metis calculation(1) holds_forall_def)
    then show "x ∈ filter_exp (lnot b) (union_up_to_n (Assume b;; C) S m)"
      using ‹x ∈ union_up_to_n (Assume b;; C) S m›
      by (simp add: filter_exp_def)
  qed
  moreover have "filter_exp (lnot b) (∪n. iterate_sem n (Assume b ;; C) S)
  = filter_exp (lnot b) (union_up_to_n (Assume b;; C) S m)"
  proof -
    have "∧n. n > m ==> iterate_sem n (Assume b ;; C) S = {}"
    proof -
      fix n show "n > m ==> iterate_sem n (Assume b ;; C) S = {}"
      proof (induct "n - m - 1")
        case 0
        then show ?case
          by (metis (no_types, lifting) UnCI calculation(1) false_then_empty_later holds_forall_def iterate_sem_equiv)
      next
        case (Suc x)
        then show ?case
          by (metis (no_types, lifting) UnCI calculation(1) false_then_empty_later holds_forall_def iterate_sem_equiv)
      qed
    qed
    moreover have "union_up_to_n (Assume b;; C) S m = (∪n. union_up_to_n (Assume b;; C) S n)" (is "?A = ?B")
    proof
      show "?B ⊆ ?A"
      proof
        fix x assume "x ∈ ?B"
        then obtain n where "x ∈ union_up_to_n (Assume b;; C) S n"
          by blast
        then show "x ∈ ?A"
          by (metis calculation empty_iff in_union_up_to linorder_not_le)
      qed
    qed (blast)
    then have "(∪n. iterate_sem n (Assume b ;; C) S) = union_up_to_n (Assume b;; C) S m"
      by (simp add: union_union_up_to_n_equiv)
    then show ?thesis
      by auto
  qed
  ultimately show "P m (sem (while_cond b C) S)"
    by (simp add: ‹sem (while_cond b C) S = filter_exp (lnot b) (∪n. iterate_sem n (Assume b ;; C) S)› sup.absorb1)
qed


lemma false_state_in_if_then:
  assumes "φ ∈ S"
      and "¬ b (snd φ)"
    shows "φ ∈ sem (if_then b C) S"
proof -
  have "φ ∈ sem (Assume (lnot b)) S"
    by (metis SemAssume assms(1) assms(2) in_sem lnot_def prod.collapse)
  then show ?thesis
    by (simp add: assume_sem filter_exp_def if_then_sem)
qed

lemma false_state_in_while_cond_aux:
  assumes "φ ∈ S"
      and "¬ b (snd φ)"
    shows "φ ∈ iterate_sem n (if_then b C) S"
proof (induct n)
  case 0
  then show ?case
    by (simp add: assms(1))
next
  case (Suc n)
  then show ?case
    by (simp add: assms(2) false_state_in_if_then)
qed

lemma false_state_in_while_cond:
  assumes "φ ∈ S"
      and "¬ b (snd φ)"
    shows "φ ∈ sem (while_cond b C) S"
proof -
  have "φ ∈ (∪n. iterate_sem n (if_then b C) S)"
    by (simp add: assms(1) assms(2) false_state_in_while_cond_aux)
  then show ?thesis using sem_while_with_if[of b C S] assms(2)
    by (simp add: filter_exp_def lnot_def)
qed

theorem while_exists:
  assumes "∧φ. ⊨ { P φ } while_cond b C { Q φ }"
  shows "⊨ { (λS. ∃φ ∈ S. ¬ b (snd φ) ∧ P φ S) } while_cond b C { (λS. ∃φ ∈ S. Q φ S) }"
proof (rule hyper_hoare_tripleI)
  fix S assume "∃φ∈S. ¬ b (snd φ) ∧ P φ S"
  then obtain φ where asm0: "φ∈S" "¬ b (snd φ) ∧ P φ S" by blast
  then have "Q φ (sem (while_cond b C) S)"
    using assms hyper_hoare_tripleE by blast
  then show "∃φ∈sem (while_cond b C) S. Q φ (sem (while_cond b C) S)"
    using asm0(1) asm0(2) false_state_in_while_cond by blast
qed

lemma sem_while_cond_union_up_to:
  "sem (while_cond b C) S = filter_exp (lnot b) (∪n. union_up_to_n (if_then b C) S n)"
  by (simp add: sem_while_with_if union_union_up_to_n_equiv)

lemma iterate_sem_sum:
  "iterate_sem n C (iterate_sem m C S) = iterate_sem (n + m) C S"
  by (induct n) simp_all


lemma unroll_while_sem:
  "sem (while_cond b C) (iterate_sem n (if_then b C) S) = sem (while_cond b C) S"
proof -
  let ?S = "iterate_sem n (if_then b C) S"
  have "filter_exp (lnot b) (∪m. iterate_sem m (if_then b C) S) = filter_exp (lnot b) (∪m. iterate_sem (n + m) (if_then b C) S)" (is "?A = ?B")
  proof
    show "?A ⊆ ?B"
    proof
      fix x assume "x ∈ ?A"
      then obtain m where "x ∈ iterate_sem m (if_then b C) S" "¬ b (snd x)"
        by (auto simp add: filter_exp_def lnot_def)
      then have "x ∈ iterate_sem (n + m) (if_then b C) S"
        using false_state_in_while_cond_aux[of x "iterate_sem m (if_then b C) S" b n C] iterate_sem_sum[of n "if_then b C" m S]
        by blast
      then have "x ∈ (∪m. iterate_sem (n + m) (if_then b C) S)"
        by blast
      then show "x ∈ ?B"
        using ‹x ∈ filter_exp (lnot b) (∪m. iterate_sem m (if_then b C) S)›
        by (simp add: filter_exp_def)
    qed
    show "?B ⊆ ?A"
    proof
      fix x assume "x ∈ ?B"
      then obtain m where "x ∈ iterate_sem (n + m) (if_then b C) S" "¬ b (snd x)"
        by (auto simp add: filter_exp_def lnot_def)
      then show "x ∈ ?A"
        using ‹x ∈ filter_exp (lnot b) (∪m. iterate_sem (n + m) (if_then b C) S)›
        by (auto simp add: filter_exp_def)
    qed
  qed
  then show ?thesis
    using iterate_sem_sum[of _ "if_then b C" n S] sem_while_with_if[of b C S] sem_while_with_if[of b C ?S]
    by (simp add: add.commute)
qed


theorem while_unroll:
  assumes "∧n. n < m ==> ⊨ {P n} if_then b C {P (Suc n)}"
      and "⊨ {P m} while_cond b C {Q}"
    shows "⊨ {P 0} while_cond b C {Q}"
proof (rule hyper_hoare_tripleI)
  fix S assume "P 0 S"
  let ?S = "iterate_sem m (if_then b C) S"
  have "(∀n. n < m ⟶ (⊨ {P n} if_then b C {P (Suc n)})) ⟶ P m ?S"
  proof (induct m)
    case 0
    then show ?case
      by (simp add: ‹P 0 S›)
  next
    case (Suc m)
    then show ?case
      by (simp add: hyper_hoare_triple_def)
  qed
  then have "P m ?S" using assms(1)
    by blast
  then have "Q (sem (while_cond b C) ?S)"
    using assms(2) hyper_hoare_tripleE by blast
  then show "Q (sem (while_cond b C) S)"
    by (metis unroll_while_sem)
qed








text ‹Deriving LoopExit from NormalWhile, and ForLoop from LoopExit and Unroll›

lemma while_desugared_easy:
  assumes "∧n. ⊨ {I n} Assume b;; C {I (Suc n)}"
      and "⊨ { natural_partition I } Assume (lnot b) { Q }"
    shows "⊨ {I 0} while_cond b C { Q }"
  by (metis assms(1) assms(2) seq_rule while_cond_def while_rule)


corollary loop_exit:
  assumes "entails P (holds_forall (lnot b))"
  shows "⊨ {P} while_cond b C {P}"
proof -
  have "⊨ {(if (0::nat) = 0 then P else emp)} while_cond b C {P}"
  proof (rule while_desugared_easy[of "λ(n::nat). if n = 0 then P else emp" b C P])
    show "⊨ {natural_partition (λ(n::nat). if n = 0 then P else emp)} Assume (lnot b) {P}"
    proof (rule hyper_hoare_tripleI)
      fix S assume asm0: "natural_partition (λ(n::nat). if n = 0 then P else emp) S"
      then obtain F where "S = (∪(n::nat). F n)" "∧(n::nat). (λ(n::nat). if n = 0 then P else emp) n (F n)"
        using natural_partitionE by blast
      then have "∧n. F (Suc n) = {}"
        by (metis (mono_tags, lifting) emp_def old.nat.distinct(2))
      moreover have "S = F 0"
      proof
        show "S ⊆ F 0"
        proof
          fix x assume "x ∈ S"
          then obtain n where "x ∈ F n"
            using ‹S = ∪ (range F)› by blast
          then show "x ∈ F 0"
            by (metis calculation empty_iff gr0_implies_Suc zero_less_iff_neq_zero)
        qed
        show "F 0 ⊆ S"
          using ‹S = ∪ (range F)› by blast
      qed
      ultimately have "P S"
        using ‹∧n. (if n = 0 then P else emp) (F n)› by presburger
      then show "P (sem (Assume (lnot b)) S)"
        by (metis assms entailsE sem_assume_low_exp(1))
    qed
    fix n :: nat
    show "⊨ {(if n = 0 then P else emp)} Assume b ;; C {if Suc n = 0 then P else emp}"
    proof (rule hyper_hoare_tripleI)
      fix S assume asm0: "(if n = 0 then P else emp) S"
      then show "(if Suc n = 0 then P else emp) (sem (Assume b ;; C) S)"
        by (metis (mono_tags, lifting) assms emp_def entailsE holds_forall_empty lnot_involution nat.distinct(1) sem_assume_low_exp_seq(2))
    qed
  qed
  then show ?thesis
    by fastforce
qed

corollary for_loop:
  assumes "∧n. n < m ==> ⊨ {P n} if_then b C {P (Suc n)}"
      and "entails (P m) (holds_forall (lnot b))"
    shows "⊨ {P 0} while_cond b C {P m}"
  using assms(1)
proof (rule while_unroll)
  show "⊨ {P m} while_cond b C {P m}"
    using assms(2) loop_exit by blast
qed


end