Theory TotalLogic

theory TotalLogic
  imports Loops Compositionality SyntacticAssertions
begin

section ‹Terminating Hyper-Triples›

definition total_hyper_triple (‹⊨TERM {_} _ {_}› [51,0,0] 81) where
  "⊨TERM {P} C {Q} ⟷ ( ⊨ {P} C {Q} ∧ (∀S. P S ⟶ (∀φ ∈ S. ∃σ'. single_sem C (snd φ) σ' )))"

lemma total_hyper_triple_equiv:
  "⊨TERM {P} C {Q} ⟷ ( ⊨ {P} C {Q} ∧ (∀S. P S ⟶ (∀φ ∈ S. ∃σ'. (fst φ, σ') ∈ sem C S ∧ single_sem C (snd φ) σ' )))"
  by (metis prod.collapse single_step_then_in_sem total_hyper_triple_def)

lemma total_hyper_tripleI:
  assumes "⊨ {P} C {Q}"
      and "⋀φ S. P S ∧ φ ∈ S ⟹ (∃σ'. single_sem C (snd φ) σ' )"
    shows "⊨TERM {P} C {Q}"
  by (simp add: assms(1) assms(2) total_hyper_triple_def)

definition terminates_in where
  "terminates_in C S ⟷ (∀φ ∈ S. ∃σ'. single_sem C (snd φ) σ')"

lemma terminates_inI:
  assumes "⋀φ. φ ∈ S ⟹ ∃σ'. single_sem C (snd φ) σ'"
  shows "terminates_in C S"
  using assms terminates_in_def by blast

lemma iterate_sem_mono:
  assumes "S ⊆ S'"
  shows "iterate_sem n C S ⊆ iterate_sem n C S'"
  using assms
  by (induct n arbitrary: S S') (simp_all add: sem_monotonic)

lemma terminates_in_while_loop:
  assumes "wfP lt"
      and "⋀φ n. φ ∈ iterate_sem n (Assume b;; C) S ∧ b (snd φ) ⟹ (∃σ'. single_sem C (snd φ) σ' ∧ (¬ b σ' ∨ lt (e σ') (e (snd φ))))"
  shows "terminates_in (while_cond b C) S"
proof (rule terminates_inI)
  fix φ assume asm0: "φ ∈ S"
  let ?S = "{φ}"
  let ?R = "{(x, y). lt x y}"
  let ?Q = "{ e (snd φ) |φ n. b (snd φ) ∧ φ ∈ iterate_sem n (Assume b;; C) ?S}"

  show "∃σ'. ⟨while_cond b C, snd φ⟩ → σ'"
  proof (cases "b (snd φ)")
    case False
    then show ?thesis
      by (metis SemAssume SemSeq SemWhileExit lnot_def while_cond_def)
  next
    case True
    show ?thesis
    proof (rule wfE_min)
      show "wf ?R"
        using assms(1) wfp_def by blast
      show "e (snd φ) ∈ ?Q"
        using True asm0 iterate_sem.simps(1) by fastforce
      fix z assume asm1: "z ∈ ?Q" "(⋀y. (y, z) ∈ {(x, y). lt x y} ⟹ y ∉ ?Q)"
      then obtain φ' n where "z = e (snd φ')" "b (snd φ')" "φ' ∈ iterate_sem n (Assume b;; C) ?S"
        by blast
      then obtain σ' where "single_sem C (snd φ') σ' ∧ (¬ b σ' ∨ lt (e σ') (e (snd φ')))"
        using assms(2) iterate_sem_mono[of ?S S n "Assume b;; C"]
        by (meson asm0 empty_subsetI in_mono insert_subsetI)
      then have "¬ b σ' ∨ e σ' ∉ ?Q"
        using ‹z = e (snd φ')› asm1(2) by blast
      moreover have "(fst φ', σ') ∈ sem (Assume b;; C) (iterate_sem n (Assume b;; C) ?S)"
        by (metis (no_types, opaque_lifting) SemAssume SemSeq ‹(⟨C, snd φ'⟩ → σ') ∧ (¬ b σ' ∨ lt (e σ') (e (snd φ')))› ‹φ' ∈ iterate_sem n (Assume b ;; C) ?S› ‹b (snd φ')› single_step_then_in_sem surjective_pairing)
      ultimately have "¬ b σ'"
        using iterate_sem.simps(2)[of n "Assume b;; C" "{φ}"] mem_Collect_eq snd_conv
        by (metis (mono_tags, lifting))
      then have "(fst φ', σ') ∈ iterate_sem (Suc n) (Assume b;; C) ?S"
        by (simp add: ‹(fst φ', σ') ∈ sem (Assume b ;; C) (iterate_sem n (Assume b ;; C) ?S)›)
      then have "(fst φ', σ') ∈ (⋃n. iterate_sem n (Assume b;; C) ?S)" by blast
      then have "(fst φ', σ') ∈ filter_exp (lnot b) (⋃n. iterate_sem n (Assume b;; C) ?S)"
        using filter_exp_def[of "lnot b"] lnot_def[of b σ'] ‹¬ b σ'› by force
      then have "(fst φ', σ') ∈ sem (while_cond b C) ?S"
        by (simp add: assume_sem filter_exp_def sem_seq sem_while while_cond_def)
      then show "∃σ'. ⟨while_cond b C, snd φ⟩ → σ'"
        by (metis in_sem singletonD snd_conv)
    qed
  qed
qed

lemma total_hyper_triple_altI:
  assumes "⋀S. P S ⟹ Q (sem C S)"
      and "⋀S. P S ⟹ terminates_in C S"
    shows "⊨TERM {P} C {Q}"
  by (metis assms(1) assms(2) hyper_hoare_tripleI terminates_in_def total_hyper_triple_def)



lemma syntactic_frame_preserved:
  assumes "terminates_in C S"
      and "wr C ∩ fv F = {}"
      and "sat_assertion vals states F S"
      and "wf_assertion_aux nv (length states) F"
    shows "sat_assertion vals states F (sem C S)"
  using assms
proof (induct F arbitrary: vals states nv)
  case (AForallState F)
  then have "⋀φ. φ ∈ sem C S ⟹ sat_assertion vals (φ # states) F (sem C S)"
  proof -
    fix φ assume asm0: "φ ∈ sem C S"
    then obtain σ where "single_sem C σ (snd φ)" "(fst φ, σ) ∈ S"
      using in_sem by blast
    then have "sat_assertion vals ((fst φ, σ) # states) F (sem C S)"
      using AForallState.hyps AForallState.prems assms(1) by auto
    moreover have "agree_on (fv F) σ (snd φ)"
      using AForallState.prems(2) ‹⟨(C::(nat, nat) stmt), σ::nat ⇒ nat⟩ → snd (φ::(nat ⇒ nat) × (nat ⇒ nat))› wr_charact by auto
    moreover have "wf_assertion_aux nv (Suc (length states)) F"
      using AForallState.prems(4) by auto
    ultimately have "sat_assertion vals ((fst φ, snd φ) # states) F (sem C S)"
      using fv_wr_charact[of F σ "snd φ" vals "fst φ" states "sem C S"]
      by fast
    then show "sat_assertion vals (φ # states) F (sem C S)"
      by simp
  qed
  then show ?case
    using AForallState.hyps AForallState.prems(2) assms(1) by auto
next
  case (AExistsState F)
  then obtain φ where asm0: "φ ∈ S" "sat_assertion vals (φ # states) F S"
    by auto
  then obtain σ' where "single_sem C (snd φ) σ'"
    using assms(1) terminates_in_def by blast
  then have "sat_assertion vals ((fst φ, σ') # states) F S"
    by (metis AExistsState.prems(2) AExistsState.prems(4) asm0(2) fv.simps(6) fv_wr_charact prod.collapse wf_assertion_aux.simps(8) wr_charact)
  then show ?case
    by (metis AExistsState.hyps AExistsState.prems(2) AExistsState.prems(4) ‹⟨C, snd φ⟩ → σ'› asm0(1) assms(1) fv.simps(6) length_Cons prod.collapse sat_assertion.simps(4) single_step_then_in_sem wf_assertion_aux.simps(8))
qed (fastforce+)


theorem frame_rule_syntactic:
  assumes "⊨TERM {P} C {Q}"
      and "wr C ∩ fv F = {}" (* free *program* variables *)
      and "wf_assertion F" (* No unbound free variable *)
    shows "⊨TERM {conj P (interp_assert F)} C {conj Q (interp_assert F)}"
proof (rule total_hyper_tripleI)
  let ?F = "interp_assert F"
  show "⋀φ S. Logic.conj P ?F S ∧ φ ∈ S ⟹ ∃σ'. ⟨C, snd φ⟩ → σ'"
    by (metis assms(1) conj_def total_hyper_triple_def)
  show "⊨ {Logic.conj P ?F} C {Logic.conj Q ?F}"
  proof (rule hyper_hoare_tripleI)
    fix S assume asm0: "Logic.conj P ?F S"
    then have "terminates_in C S"
      by (simp add: ‹⋀φ S. Logic.conj P ?F S ∧ φ ∈ S ⟹ ∃σ'. ⟨C, snd φ⟩ → σ'› terminates_in_def)
    moreover have "?F (sem C S)"
      by (metis asm0 assms(2) assms(3) calculation conj_def list.size(3) syntactic_frame_preserved)
    ultimately show "Logic.conj Q ?F (sem C S)"
      by (metis asm0 assms(1) conj_def hyper_hoare_tripleE total_hyper_triple_def)
  qed
qed




subsection ‹Specialize rule›


definition same_syn_sem_all :: "'a assertion ⇒ ((nat, 'a, nat, 'a) state ⇒ bool) ⇒ bool"
  where
  "same_syn_sem_all bsyn bsem ⟷
  (∀states vals S. length states > 0 ⟶ bsem (hd states) = sat_assertion vals states bsyn S)"

lemma same_syn_sem_allI:
  assumes "⋀states vals S. length states > 0 ⟹ bsem (hd states) ⟷ sat_assertion vals states bsyn S"
  shows "same_syn_sem_all bsyn bsem"
  by (simp add: assms same_syn_sem_all_def)

lemma transform_assume_valid:
  assumes "same_syn_sem_all bsyn bsem"
  shows "sat_assertion vals states A (Set.filter bsem S)
  ⟷ sat_assertion vals states (transform_assume bsyn A) S"
proof (induct A arbitrary: vals states)
  case (AForallState A)
  let ?S = "Set.filter (bsem) S"
  let ?A = "transform_assume bsyn A"
  have "sat_assertion vals states (AForallState A) ?S ⟷ (∀φ∈?S. sat_assertion vals (φ # states) A ?S)"
    by force
  also have "... ⟷ (∀φ∈?S. sat_assertion vals (φ # states) ?A S)"
    using AForallState by presburger
  also have "... ⟷ (∀φ∈S. bsem φ ⟶ sat_assertion vals (φ # states) ?A S)"
    by fastforce
  also have "... ⟷ (∀φ∈S. sat_assertion vals (φ # states) bsyn S ⟶ sat_assertion vals (φ # states) ?A S)"
    using assms same_syn_sem_all_def[of bsyn bsem] by auto
  also have "... ⟷ (∀φ∈S. sat_assertion vals (φ # states) (AImp bsyn ?A) S)"
    using sat_assertion_Imp by fast
  also have "... ⟷ sat_assertion vals states (AForallState (AImp bsyn ?A)) S"
    using sat_assertion.simps(2) by force
  then show ?case
    using calculation transform_assume.simps(1) by fastforce
next
  case (AExistsState A)
  let ?S = "Set.filter (bsem) S"
  let ?A = "transform_assume bsyn A"
  have "sat_assertion vals states (AExistsState A) ?S ⟷ (∃φ∈?S. sat_assertion vals (φ # states) A ?S)"
    by force
  also have "... ⟷ (∃φ∈?S. sat_assertion vals (φ # states) ?A S)"
    using AExistsState by presburger
  also have "... ⟷ (∃φ∈S. bsem φ ∧ sat_assertion vals (φ # states) ?A S)"
    by force
  also have "... ⟷ (∃φ∈S. sat_assertion vals (φ # states) bsyn S ∧ sat_assertion vals (φ # states) ?A S)"
    using assms same_syn_sem_all_def[of bsyn bsem] by auto
  also have "... ⟷ (∃φ∈S. sat_assertion vals (φ # states) (AAnd bsyn ?A) S)"
    by simp
  also have "... ⟷ sat_assertion vals states (AExistsState (AAnd bsyn ?A)) S"
    using sat_assertion.simps(3) by force
  then show ?case
    using calculation transform_assume.simps(2) by fastforce
next
  case (AForall A)
  let ?S = "Set.filter (bsem) S"
  let ?A = "transform_assume bsyn A"
  have "sat_assertion vals states (AForall A) ?S ⟷ (∀v. sat_assertion (v # vals) states A ?S)"
    by force
  also have "... ⟷ (∀v. sat_assertion (v # vals) states ?A S)"
    using AForall by presburger
  also have "... ⟷ sat_assertion vals states (AForall ?A) S"
    by simp
  then show ?case
    using calculation transform_assume.simps(3) by fastforce
next
  case (AExists A)
  let ?S = "Set.filter (bsem) S"
  let ?A = "transform_assume bsyn A"
  have "sat_assertion vals states (AExists A) ?S ⟷ (∃v. sat_assertion (v # vals) states A ?S)"
    by force
  also have "... ⟷ (∃v. sat_assertion (v # vals) states ?A S)"
    using AExists by presburger
  also have "... ⟷ sat_assertion vals states (AExists ?A) S"
    by simp
  then show ?case
    using calculation transform_assume.simps(4) by fastforce
qed (simp_all)


fun indep_of_set where
  "indep_of_set (AForall A) ⟷ indep_of_set A"
| "indep_of_set (AExists A) ⟷ indep_of_set A"
| "indep_of_set (AOr A B) ⟷ indep_of_set A ∧ indep_of_set B"
| "indep_of_set (AAnd A B) ⟷ indep_of_set A ∧ indep_of_set B"
| "indep_of_set (AComp _ _ _) ⟷ True"
| "indep_of_set (AConst _) ⟷ True"
| "indep_of_set (AForallState _) ⟷ False"
| "indep_of_set (AExistsState _) ⟷ False"

lemma indep_of_set_charact:
  assumes "indep_of_set A"
      and "sat_assertion vals states A S"
    shows "sat_assertion vals states A S'"
  using assms
by (induct A arbitrary: vals states) (auto)

lemma wf_exp_take:
  assumes "wf_exp nv ns e"
  shows "interp_exp vals states e = interp_exp (take nv vals) (take ns states) e"
  using assms
proof (induct e arbitrary: nv ns vals states)
  case (EQVar x)
  then show ?case
    by force
next
  case (EBinop e1 x2 e2)
  then show ?case
    by (metis interp_exp.simps(5) wf_exp.simps(4))
next
  case (EFun f e)
  then show ?case
    by (metis interp_exp.simps(6) wf_exp.simps(5))
qed (simp_all)

lemma wf_assertion_aux_take:
  assumes "wf_assertion_aux nv ns A"
  shows "sat_assertion vals states A S ⟷ sat_assertion (take nv vals) (take ns states) A S"
  using assms
proof (induct A arbitrary: nv ns vals states)
  case (AConst x)
  then show ?case
    by simp
next
  case (AComp x1a x2 x3a)
  then show ?case
    by (metis sat_assertion.simps(2) wf_assertion_aux.simps(2) wf_exp_take)
next
  case (AForallState A)
  then show ?case using AForallState.hyps[of nv "Suc ns" vals]
    by (metis sat_assertion.simps(3) take_Suc_Cons wf_assertion_aux.simps(7))
next
  case (AExistsState A)
  then show ?case using AExistsState.hyps[of nv "Suc ns" vals]
    by (metis sat_assertion.simps(4) take_Suc_Cons wf_assertion_aux.simps(8))
next
  case (AForall A)
  then show ?case using AForall.hyps[of "Suc nv" ns _ states]
    by (metis sat_assertion.simps(5) take_Suc_Cons wf_assertion_aux.simps(5))
next
  case (AExists A)
  then show ?case using AExists.hyps[of "Suc nv" ns _ states]
    by (metis sat_assertion.simps(6) take_Suc_Cons wf_assertion_aux.simps(6))
next
  case (AOr A1 A2)
  then show ?case
    by (metis sat_assertion.simps(8) wf_assertion_aux.simps(4))
next
  case (AAnd A1 A2)
  then show ?case
    by (metis sat_assertion.simps(7) wf_assertion_aux.simps(3))
qed

lemma syntactic_charact_for_equivalence:
  assumes "indep_of_set A"
      and "wf_assertion_aux (0::nat) (1::nat) A"
    shows "sat_assertion vals (φ # states) A S ⟷ sat_assertion [] [φ] A {}" (is "?A ⟷ ?B")
proof -
  have "?A ⟷ sat_assertion vals (φ # states) A {}"
    using assms(1) indep_of_set_charact by blast
  also have "... ⟷ sat_assertion (take (0::nat) vals) (take (1::nat) (φ # states)) A {}"
    using wf_assertion_aux_take[of 0 1 A vals "φ # states" "{}"] assms(2)
    by blast
  ultimately show ?thesis by simp
qed


definition get_bsem where
  "get_bsem bsyn φ ⟷ sat_assertion [] [φ] bsyn {}"

lemma syntactic_charact_for_bsem:
  assumes "indep_of_set A"
      and "wf_assertion_aux (0::nat) (1::nat) A"
    shows "same_syn_sem_all A (get_bsem A)"
proof (rule same_syn_sem_allI)
  fix states :: "((nat ⇒ 'a) × (nat ⇒ 'a)) list"
  fix vals S
  assume asm0: "0 < length states"
  then show "get_bsem A (hd states) = sat_assertion vals states A S"
    by (metis assms(1) assms(2) get_bsem_def length_greater_0_conv list.collapse syntactic_charact_for_equivalence)
qed



lemma get_bsem_is_bsem:
  assumes "same_syn_sem_all bsyn bsem"
  shows "bsem = get_bsem bsyn"
proof (rule ext)
  fix x
  have "bsem (hd [x]) = sat_assertion [] [x] bsyn {}"
    using assms same_syn_sem_all_def by fastforce
  then show "bsem x = get_bsem bsyn x"
    by (simp add: get_bsem_def)
qed


lemma free_vars_syn_sem:
  assumes "same_syn_sem_all bsyn bsem"
      and "fst φ = fst φ'"
      and "agree_on (fv bsyn) (snd φ) (snd φ')"
      and "bsem φ"
      and "wf_assertion_aux 0 (Suc 0) bsyn"
    shows "bsem φ'"
proof -
  have "sat_assertion [] (insert_at 0 (fst φ, snd φ') []) bsyn {}"
    using assms(3)
  proof (rule fv_wr_charact_aux)
    show "sat_assertion [] (insert_at 0 (fst φ, snd φ) []) bsyn {}"
      by (metis assms(1) assms(4) get_bsem_def get_bsem_is_bsem insert_at.simps(1) prod.collapse)
    show "wf_assertion_aux 0 (Suc (length [])) bsyn"
      by (simp add: assms(5))
  qed (simp)
  then show ?thesis
    by (metis assms(1) assms(2) get_bsem_def get_bsem_is_bsem insert_at.simps(1) prod.collapse)
qed


lemma free_vars_charact:
  assumes "wr C ∩ fv bsyn = {}"
      and "same_syn_sem_all bsyn bsem"
      and "wf_assertion_aux 0 (Suc 0) bsyn"
    shows "sem C (Set.filter bsem S) = Set.filter bsem (sem C S)" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof
    fix x assume asm0: "x ∈ sem C (Set.filter bsem S)"
    then obtain σ where "(fst x, σ) ∈ Set.filter bsem S" "single_sem C σ (snd x)"
      by (meson in_sem)
    then have "agree_on (fv bsyn) σ (snd x)"
      using assms(1) wr_charact by blast
    then show "x ∈ Set.filter bsem (sem C S)"
      using ‹(fst x, σ) ∈ Set.filter bsem S› ‹⟨C, σ⟩ → snd x› assms(2) assms(3)
      free_vars_syn_sem [of bsyn bsem]
      by (cases x) (auto intro: single_step_then_in_sem)
  qed
  show "?B ⊆ ?A"
  proof
    fix x assume asm0: "x ∈ ?B"
    then obtain σ where "bsem x" "(fst x, σ) ∈ S" "single_sem C σ (snd x)"
      by (auto simp add: in_sem)
    then have "agree_on (fv bsyn) σ (snd x)"
      using assms(1) wr_charact by blast
    then have "bsem (fst x, σ)"
      using ‹bsem x› agree_on_sym assms(2) assms(3) free_vars_syn_sem by fastforce
    then show "x ∈ ?A"
      using ‹(fst x, σ) ∈ S› ‹⟨C, σ⟩ → snd x› by (auto simp add: in_sem)
  qed
qed


lemma filter_rule_semantic:
  assumes "⊨ {interp_assert P} C {interp_assert Q}"
      and "same_syn_sem_all bsyn bsem"
      and "wr C ∩ fv bsyn = {}"
      and "wf_assertion_aux 0 (Suc 0) bsyn"
    shows "⊨ { interp_assert (transform_assume bsyn P) } C { interp_assert (transform_assume bsyn Q) }"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "interp_assert (transform_assume bsyn P) S"
  then have "sat_assertion [] [] P (Set.filter bsem S)"
    using TotalLogic.transform_assume_valid assms(2) by blast
  then have "sat_assertion [] [] Q (sem C (Set.filter bsem S))"
    using assms(1) hyper_hoare_tripleE by blast
  moreover have "sem C (Set.filter bsem S) = Set.filter bsem (sem C S)"
    using assms(2) assms(3) assms(4) free_vars_charact by presburger
  ultimately show "interp_assert (transform_assume bsyn Q) (sem C S)"
    using TotalLogic.transform_assume_valid assms(2) by fastforce
qed

lemma filter_rule_syntactic:
  assumes "⊨ {interp_assert P} C {interp_assert Q}"
      and "indep_of_set b"
      and "wf_assertion_aux 0 1 b"
      and "wr C ∩ fv b = {}"
    shows "⊨ { interp_assert (transform_assume b P) } C { interp_assert (transform_assume b Q) }"
  using assms(1) filter_rule_semantic
  by (metis One_nat_def assms(2) assms(3) assms(4) syntactic_charact_for_bsem)


definition terminates where
  "terminates C ⟷ (∀σ. ∃σ'. single_sem C σ σ')"

lemma terminatesI:
  assumes "⋀σ. ∃σ'. single_sem C σ σ'"
  shows "terminates C"
  using terminates_def assms by auto

lemma terminates_implies_total:
  assumes "⊨ {P} C {Q}"
      and "terminates C"
    shows "⊨TERM {P} C {Q}"
  using assms(1)
proof (rule total_hyper_tripleI)
  fix φ S assume asm0: "P S ∧ φ ∈ S"
  then show "∃σ'. ⟨C, snd φ⟩ → σ'"
    by (metis assms(2) terminates_def)
qed

lemma terminates_seq:
  assumes "terminates C1"
      and "terminates C2"
    shows "terminates (C1;; C2)"
  by (meson SemSeq assms(1) assms(2) terminates_def)

lemma terminates_assign:
  "terminates (Assign x e)"
  by (meson SemAssign terminates_def)

lemma terminates_havoc:
  "terminates (Havoc c)"
  by (meson SemHavoc terminates_def)

lemma terminates_if:
  assumes "terminates C1"
      and "terminates C2"
    shows "terminates (If C1 C2)"
  by (meson SemIf2 assms(2) terminates_def)


lemma rule_lframe_exist:
   fixes b :: "('a ⇒ ('lvar ⇒ 'lval)) ⇒ bool"
    ―‹b takes a mapping from keys to logical states (representing the tuple), and returns a boolean›

   assumes "⊨TERM {P} C {Q}"
     shows "⊨TERM { conj P (λS. ∃φ. (∀k. φ k ∈ S) ∧ b (fst ∘ φ)) } C { conj Q (λS. ∃φ. (∀k. φ k ∈ S) ∧ b (fst ∘ φ)) }"

proof (rule total_hyper_tripleI)
  fix φ S
  show "Logic.conj P (λS. ∃φ. (∀k. φ k ∈ S) ∧ b (fst ∘ φ)) S ∧ φ ∈ S ⟹ ∃σ'. ⟨C, snd φ⟩ → σ'"
    by (metis (mono_tags, lifting) assms conj_def total_hyper_triple_equiv)
next
  show "⊨ {Logic.conj P (λS. ∃φ. (∀k. φ k ∈ S) ∧ b (fst ∘ φ))} C {Logic.conj Q (λS. ∃φ. (∀k. φ k ∈ S) ∧ b (fst ∘ φ))}"
  proof (rule hyper_hoare_tripleI)
    fix S :: "('lvar, 'lval, 'b, 'c) state set"
    assume asm0: "Logic.conj P (λS. ∃φ. (∀k. φ k ∈ S) ∧ b (fst ∘ φ)) S"
    then obtain φ where "(∀k. φ k ∈ S) ∧ b (fst ∘ φ)"
      using conj_def[of P "λS. ∃φ. (∀k. φ k ∈ S) ∧ b (fst ∘ φ)" S] by blast
    let ?σ = "λk. SOME σ'. (fst (φ k), σ') ∈ sem C S ∧ single_sem C (snd (φ k)) σ'"
    let ?φ = "λk. (fst (φ k), ?σ k)"
    have r: "⋀k. (fst (φ k), ?σ k) ∈ sem C S ∧ single_sem C (snd (φ k)) (?σ k)"
    proof -
      fix k show "(fst (φ k), ?σ k) ∈ sem C S ∧ single_sem C (snd (φ k)) (?σ k)"
      proof (rule someI_ex[of "λσ'. (fst (φ k), σ') ∈ sem C S ∧ single_sem C (snd (φ k)) σ'"])
        show "∃σ'. (fst (φ k), σ') ∈ sem C S ∧ ⟨C, snd (φ k)⟩ → σ'"
          by (metis (mono_tags, lifting) ‹(∀k. φ k ∈ S) ∧ b (fst ∘ φ)› asm0 assms conj_def total_hyper_triple_equiv)
      qed
    qed
    moreover have "fst ∘ φ = fst ∘ ?φ" by (rule ext) simp
    ultimately have "∃φ. (∀k. φ k ∈ sem C S) ∧ b (fst ∘ φ)"
      using ‹(∀k. φ k ∈ S) ∧ b (fst ∘ φ)› by force
    moreover have "Q (sem C S)"
      by (metis (mono_tags, lifting) asm0 assms conj_def hyper_hoare_tripleE total_hyper_triple_def)
    ultimately show "Logic.conj Q (λS. ∃φ. (∀k. φ k ∈ S) ∧ b (fst ∘ φ)) (sem C S)"
      using conj_def[of Q "λS. ∃φ. (∀k. φ k ∈ S) ∧ b (fst ∘ φ)"] by simp
  qed
qed

lemma terminates_if_then:
  assumes "terminates C1"
      and "terminates C2"
    shows "terminates (if_then_else b C1 C2)"
proof (rule terminatesI)
  fix σ
  show "∃σ'. ⟨if_then_else b C1 C2, σ⟩ → σ'"
  proof (cases "b σ")
    case True
    then show ?thesis
      by (metis SemAssume SemIf1 SemSeq assms(1) if_then_else_def terminates_def)
  next
    case False
    then show ?thesis
      by (metis (no_types, opaque_lifting) SemAssume SemIf2 SemSeq assms(2) if_then_else_def lnot_def terminates_def)
  qed
qed


definition min_prop :: "(nat ⇒ bool) ⇒ nat" where
  "min_prop P = (SOME n. P n ∧ (∀m. m < n ⟶ ¬ P m))"

lemma min_prop_charact:
  assumes "P n"
  shows "P (min_prop P) ∧ (∀m. m < (min_prop P) ⟶ ¬ P m)"
  unfolding min_prop_def
  using min_prop_def[of P] assms exists_least_iff[of P] someI[of "λn. P n ∧ (∀m. m < n ⟶ ¬ P m)"]
  by blast


lemma hyper_tot_set_not_empty:
  assumes "⊨TERM {P} C {Q}"
      and "P S"
      and "S ≠ {}"
    shows "sem C S ≠ {}"
  by (metis assms(1) assms(2) assms(3) ex_in_conv total_hyper_triple_equiv)

lemma iterate_sem_mod_updates_same:
  assumes "same_mod_updates vars S S'"
  shows "same_mod_updates vars (iterate_sem n C S) (iterate_sem n C S')"
  using assms
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case
    by (simp add: sem_update_commute)
qed


theorem while_synchronized_tot:
  assumes "wfP lt"
      and "⋀n. not_fv_hyper t (I n)"
      and "⋀n. ⊨TERM {conj (conj (I n) (holds_forall b)) (e_recorded_in_t e t)} C {conj (conj (I (Suc n)) (low_exp b)) (e_smaller_than_t e t lt)}"
    shows "⊨TERM {conj (I 0) (low_exp b)} while_cond b C {conj (exists I) (holds_forall (lnot b))}"
proof (rule total_hyper_triple_altI)
  fix S assume asm0: "conj (I 0) (low_exp b) S"
  let ?S = "λn. assign_exp_to_lvar_set e t (iterate_sem n (Assume b;; C) S)"

  have S_same: "⋀n. same_mod_updates {t} (?S n) (iterate_sem n (Assume b;; C) S)"
    by (simp add: assign_exp_to_lvar_set_same_mod_updates same_mod_updates_sym)


  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"
    let ?S = "assign_exp_to_lvar_set e t S"
    have "conj (I n) (holds_forall b) ?S"
      by (metis ‹Logic.conj (I n) (holds_forall b) S› assms(2) conj_def holds_forall_same_assign_lvar not_fv_hyper_assign_exp)
    then have "conj (conj (I n) (holds_forall b)) (e_recorded_in_t e t) ?S"
      by (simp add: conj_def e_recorded_in_t_if_assigned)
    then have "Logic.conj (I (Suc n)) (low_exp b) (sem (Assume b ;; C) ?S)"
      by (metis (mono_tags, lifting) assms(3) conj_def hyper_hoare_tripleE sem_assume_low_exp_seq(1) total_hyper_triple_def)
    moreover have "same_mod_updates {t} (sem (Assume b ;; C) ?S) (sem (Assume b ;; C) S)"
      by (simp add: assign_exp_to_lvar_set_same_mod_updates same_mod_updates_sym sem_update_commute)
    ultimately show "conj (I (Suc n)) (low_exp b) (sem (Assume b ;; C) S)"
      by (metis assms(2) conj_def low_exp_forall_same_mod_updates not_fv_hyperE)
  qed

  have "⋀n. iterate_sem n (Assume b ;; C) S ≠ {} ⟹ conj (I n) (low_exp b) (iterate_sem n (Assume b ;; C) S)"
  proof -
    fix n
    show "iterate_sem n (Assume b ;; C) S ≠ {} ⟹ conj (I n) (low_exp b) (iterate_sem n (Assume b ;; C) S)"
    proof (induct n)
      case 0
      then show ?case
        by (simp add: asm0)
    next
      case (Suc n)
      then show ?case
        by (metis (full_types) conj_def false_then_empty_later holds_forall_empty hyper_hoare_tripleE iterate_sem.simps(2) lessI low_exp_two_cases triple)
    qed
  qed

  have terminates: "∃n. iterate_sem n (Assume b;; C) S = {}"
  proof (rule ccontr)
    assume asm0: "¬ (∃n. iterate_sem n (Assume b ;; C) S = {})"
    
    let ?R = "{(x, y). lt x y}"
    let ?Q = "{ e (snd φ) |φ n. φ ∈ ?S n}"

    obtain φ0 where "φ0 ∈ ?S 0"
      by (metis all_not_in_conv asm0 false_then_empty_later holds_forall_empty holds_forall_same_assign_lvar lessI)

    show False
    proof (rule wfE_min)
      show "wf ?R"
        using assms(1) wfp_def by blast
      show "e (snd φ0) ∈ ?Q"
        using ‹φ0 ∈ assign_exp_to_lvar_set e t (iterate_sem 0 (Assume b ;; C) S)› by blast
      fix z assume asm1: "z ∈ ?Q" "(⋀y. (y, z) ∈ {(x, y). lt x y} ⟹ y ∉ ?Q)"
      then obtain φ n where "z = e (snd φ)" "φ ∈ ?S n" by blast
      moreover have "conj (I n) (holds_forall b) (iterate_sem n (Assume b ;; C) S)"
      proof -
        have "conj (I n) (low_exp b) (iterate_sem n (Assume b ;; C) S)"
          using ‹⋀n. iterate_sem n (Assume b ;; C) S ≠ {} ⟹ Logic.conj (I n) (low_exp b) (iterate_sem n (Assume b ;; C) S)› asm0 by presburger
        moreover have "sem (Assume b;; C) (iterate_sem n (Assume b ;; C) S) ≠ {}"
          using asm0 iterate_sem.simps(2) by blast
        ultimately show ?thesis
          by (metis asm0 conj_def false_then_empty_later lessI low_exp_two_cases)
      qed
      then have "conj (conj (I n) (holds_forall b)) (e_recorded_in_t e t) (?S n)"
        by (metis (mono_tags, lifting) assms(2) conj_def e_recorded_in_t_if_assigned holds_forall_same_assign_lvar not_fv_hyper_assign_exp)
      then have "conj (conj (I (Suc n)) (low_exp b)) (e_smaller_than_t e t lt) (sem C (?S n))"
        using assms(3) hyper_hoare_tripleE total_hyper_triple_def by blast
      moreover obtain σ' where "⟨C, snd φ⟩ → σ'"
        by (meson ‹Logic.conj (Logic.conj (I n) (holds_forall b)) (e_recorded_in_t e t) (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))› assms(3) calculation(2) total_hyper_triple_def)

      then have "(fst φ, σ') ∈ sem (Assume b;; C) (?S n)"
        by (metis ‹Logic.conj (Logic.conj (I n) (holds_forall b)) (e_recorded_in_t e t) (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))› calculation(2) conj_def prod.collapse sem_assume_low_exp_seq(1) single_step_then_in_sem)
      then have "lt (e σ') z"
        by (metis (no_types, lifting) ‹Logic.conj (Logic.conj (I n) (holds_forall b)) (e_recorded_in_t e t) (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))› calculation(1) calculation(2) calculation(3) conj_def e_recorded_in_t_def e_smaller_than_t_def fst_conv sem_assume_low_exp_seq(1) snd_conv)

      moreover obtain σ where "(fst φ, σ) ∈ ?S n" "single_sem (Assume b;; C) σ σ'"
        by (metis ‹(fst φ, σ') ∈ sem (Assume b ;; C) (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))› fst_conv in_sem snd_conv)
      then obtain l where "(l, σ) ∈ iterate_sem n (Assume b;; C) S"
        using assign_exp_to_lvar_def[of e t] assign_exp_to_lvar_set_def[of e t] image_iff prod.collapse snd_conv
        by fastforce
      then have "(l, σ') ∈ iterate_sem (Suc n) (Assume b;; C) S"
        by (metis ‹⟨Assume b ;; C, σ⟩ → σ'› iterate_sem.simps(2) single_step_then_in_sem)
      then have "assign_exp_to_lvar e t (l, σ') ∈ ?S (Suc n)"
        by (simp add: assign_exp_to_lvar_set_def)
      then have "e σ' ∈ ?Q"
        by (metis (mono_tags, lifting) CollectI same_outside_set_lvar_assign_exp snd_conv)
      ultimately show False
        using asm1(2) by blast
    qed
  qed
    
  show "conj (exists I) (holds_forall (lnot b)) (sem (while_cond b C) S)"
  proof -
    let ?n_emp = "min_prop (λn. iterate_sem n (Assume b;; C) S = {})"
    have rr: "iterate_sem ?n_emp (Assume b;; C) S = {} ∧ (∀m<?n_emp. iterate_sem m (Assume b;; C) S ≠ {})"
      using min_prop_charact terminates by fast
    show ?thesis
    proof (cases "?n_emp")
      case 0
      then have "S = {}"
        using rr by auto
      then show ?thesis
        by (metis Loops.exists_def asm0 conj_def holds_forall_empty sem_assume_low_exp_seq(2) sem_seq)
    next
      case (Suc k)
      then have "iterate_sem k (Assume b;; C) S ≠ {}"
        using lessI rr by presburger
      then have "conj (I k) (low_exp b) (iterate_sem k (Assume b ;; C) S)"
        by (simp add: ‹⋀n. iterate_sem n (Assume b ;; C) S ≠ {} ⟹ Logic.conj (I n) (low_exp b) (iterate_sem n (Assume b ;; C) S)›)
      moreover have "holds_forall (lnot b) (iterate_sem k (Assume b;; C) S)"
      proof (rule ccontr)
        assume asm2: "¬ holds_forall (lnot b) (iterate_sem k (Assume b ;; C) S)"
        then have "holds_forall b (iterate_sem k (Assume b ;; C) S)"
          by (metis calculation conj_def low_exp_two_cases)
        let ?S = "assign_exp_to_lvar_set e t (iterate_sem k (Assume b ;; C) S)"
        have "conj (conj (I k) (holds_forall b)) (e_recorded_in_t e t) ?S"
          by (metis (no_types, lifting) ‹holds_forall b (iterate_sem k (Assume b ;; C) S)› assign_exp_to_lvar_set_same_mod_updates assms(2) calculation conj_def e_recorded_in_t_if_assigned holds_forall_same_mod_updates not_fv_hyperE)
        moreover have "sem (Assume b) ?S = ?S"
          by (metis calculation conj_def sem_assume_low_exp(1))
        ultimately have "sem (Assume b;; C) ?S ≠ {}"
          by (metis asm2 assms(3) holds_forall_empty holds_forall_same_assign_lvar hyper_tot_set_not_empty sem_seq)

        moreover have "same_mod_updates {t} (sem (Assume b;; C) ?S) (assign_exp_to_lvar_set e t (iterate_sem ?n_emp (Assume b;; C) S))"
          by (metis Suc assign_exp_to_lvar_set_def assign_exp_to_lvar_set_same_mod_updates image_empty iterate_sem.simps(2) rr same_mod_updates_sym sem_update_commute)
        ultimately show False
          by (metis assign_exp_to_lvar_set_def image_empty rr same_mod_updates_empty same_mod_updates_sym)
      qed
      then have "∃n. holds_forall (lnot b) (iterate_sem n (Assume b;; C) S) ∧ iterate_sem n (Assume b ;; C) S ≠ {}
     ∧ (∀m. m < n ⟶ ¬ (holds_forall (lnot b) (iterate_sem m (Assume b;; C) S) ∧ iterate_sem m (Assume b ;; C) S ≠ {}))"
        using exists_least_iff[of "λn. holds_forall (lnot b) (iterate_sem n (Assume b;; C) S) ∧ iterate_sem n (Assume b ;; C) S ≠ {}"]
        using ‹iterate_sem k (Assume b ;; C) S ≠ {}› by blast
      then obtain n where def_n: "holds_forall (lnot b) (iterate_sem n (Assume b;; C) S)" "iterate_sem n (Assume b ;; C) S ≠ {}"
        "⋀m. m < n ⟹ ¬ (holds_forall (lnot b) (iterate_sem m (Assume b;; C) S) ∧ iterate_sem m (Assume b ;; C) S ≠ {})" by blast
      moreover have "(∀m. m < n ⟶ holds_forall b (iterate_sem m (Assume b;; C) S)) ∧ holds_forall (lnot b) (iterate_sem n (Assume b;; C) S)"
  
        by (metis ‹⋀n. iterate_sem n (Assume b ;; C) S ≠ {} ⟹ Logic.conj (I n) (low_exp b) (iterate_sem n (Assume b ;; C) S)› conj_def def_n(1) def_n(2) false_then_empty_later holds_forall_empty low_exp_two_cases)
      then have "sem (while_cond b C) S = iterate_sem n (Assume b;; C) S"
        using triple while_synchronized_case_1 asm0 by blast
      ultimately show ?thesis
        by (metis Loops.exists_def ‹⋀n. iterate_sem n (Assume b ;; C) S ≠ {} ⟹ Logic.conj (I n) (low_exp b) (iterate_sem n (Assume b ;; C) S)› conj_def)
    qed
  qed



  show "terminates_in (while_cond b C) S"
  proof (rule terminates_in_while_loop)
    show "wfP lt"
      by (simp add: assms(1))
    fix φ n
    assume asm1: "φ ∈ iterate_sem n (Assume b ;; C) S ∧ b (snd φ)"
    let ?S = "iterate_sem n (Assume b ;; C) S"
    have "conj (I n) (low_exp b) ?S"
      using ‹⋀n. iterate_sem n (Assume b ;; C) S ≠ {} ⟹ Logic.conj (I n) (low_exp b) (iterate_sem n (Assume b ;; C) S)› asm1 by blast
    then have "conj (I n) (holds_forall b) ?S"
      by (metis asm1 conj_def holds_forall_def lnot_def low_exp_two_cases)
    let ?SS = "assign_exp_to_lvar_set e t ?S"
    have "conj (conj (I n) (holds_forall b)) (e_recorded_in_t e t) ?SS"
      by (metis (no_types, lifting) ‹Logic.conj (I n) (holds_forall b) (iterate_sem n (Assume b ;; C) S)› assign_exp_to_lvar_set_same_mod_updates assms(2) conj_def e_recorded_in_t_if_assigned holds_forall_same_mod_updates not_fv_hyperE)
    then have "conj (conj (I (Suc n)) (low_exp b)) (e_smaller_than_t e t lt) (sem C ?SS)"
      using assms(3) hyper_hoare_tripleE total_hyper_triple_def by blast
    moreover have "assign_exp_to_lvar e t φ ∈ ?SS"
      by (simp add: asm1 assign_exp_to_lvar_set_def)
    then obtain σ' where "⟨C, snd (assign_exp_to_lvar e t φ)⟩ → σ'"
      by (meson ‹Logic.conj (Logic.conj (I n) (holds_forall b)) (e_recorded_in_t e t) (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))› assms(3) total_hyper_triple_def)    
    then have "(⟨C, snd φ⟩ → σ') ∧ (fst (assign_exp_to_lvar e t φ), σ') ∈ sem C ?SS"
      by (metis ‹assign_exp_to_lvar e t φ ∈ assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S)› assign_exp_to_lvar_def prod.collapse single_step_then_in_sem snd_conv)
    then have "lt (e σ') (fst (fst (assign_exp_to_lvar e t φ), σ') t)"
      by (metis calculation conj_def e_smaller_than_t_def snd_conv)
    then show "∃σ'. (⟨C, snd φ⟩ → σ') ∧ (¬ b σ' ∨ lt (e σ') (e (snd φ)))"
      by (metis ‹(⟨C, snd φ⟩ → σ') ∧ (fst (assign_exp_to_lvar e t φ), σ') ∈ sem C (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))› assign_exp_to_lvar_def fst_conv fun_upd_same)
  qed
qed

lemma total_consequence_rule:
  assumes "entails P P'"
    and "entails Q' Q"
      and "⊨TERM {P'} C {Q'}"
    shows "⊨TERM {P} C {Q}"
proof (rule total_hyper_tripleI)
  show "⊨ {P} C {Q}"
    using assms(1) assms(2) assms(3) consequence_rule total_hyper_triple_def by blast
  fix φ S show "P S ∧ φ ∈ S ⟹ ∃σ'. ⟨C, snd φ⟩ → σ'"
    by (meson assms(1) assms(3) entailsE total_hyper_triple_def)
qed

theorem WhileSyncTot:
  assumes "wfP lt"
      and "not_fv_hyper t I"
      and "⊨TERM {conj I (λS. ∀φ∈S. b (snd φ) ∧ fst φ t = e (snd φ))} C {conj (conj I (low_exp b)) (e_smaller_than_t e t lt)}"
    shows "⊨TERM {conj I (low_exp b)} while_cond b C {conj I (holds_forall (lnot b))}"
proof -
  define I' where "I' = (λ(n::nat). I)"
  have "⊨TERM {conj (conj I (holds_forall b)) (e_recorded_in_t e t)} C {conj (conj I (low_exp b)) (e_smaller_than_t e t lt)}"
  proof (rule total_consequence_rule)
    show "⊨TERM {conj I (λS. ∀φ∈S. b (snd φ) ∧ fst φ t = e (snd φ))} C {conj (conj I (low_exp b)) (e_smaller_than_t e t lt)}"
      using assms(3) by blast
    show "entails (Logic.conj (Logic.conj I (holds_forall b)) (e_recorded_in_t e t)) (Logic.conj I (λS. ∀φ∈S. b (snd φ) ∧ fst φ t = e (snd φ)))"
      by (simp add: conj_def e_recorded_in_t_def entails_def holds_forall_def)
  qed (simp add: entails_refl)
  then have "⊨TERM {Logic.conj (I' 0) (low_exp b)} while_cond b C {Logic.conj (Loops.exists I') (holds_forall (lnot b))}"
    using while_synchronized_tot[of lt t I' b e C] I'_def assms by blast
  then show ?thesis using I'_def
    by (simp add: Loops.exists_def conj_def hyper_hoare_triple_def total_hyper_triple_def)
qed




lemma total_hyper_tripleE:
  assumes "⊨TERM {P} C {Q}"
      and "P S"
      and "φ ∈ S"
    shows "∃σ'. (fst φ, σ') ∈ sem C S ∧ single_sem C (snd φ) σ'"
  by (meson assms(1) assms(2) assms(3) total_hyper_triple_equiv)

theorem normal_while_tot:
  assumes "⋀n. ⊨ {P n} Assume b {Q n}"
      and "⋀n. ⊨TERM {conj (Q n) (e_recorded_in_t e t)} C {conj (P (Suc n)) (e_smaller_than_t e t lt)}"
      and "⊨ {natural_partition P} Assume (lnot b) {R}"

      and "wfP lt"
      and "⋀n. not_fv_hyper t (P n)"
      and "⋀n. not_fv_hyper t (Q n)"

    shows "⊨TERM {P 0} while_cond b C {R}"
proof (rule total_hyper_triple_altI)
  fix S assume asm0: "P 0 S"
  have "⋀n. P n (iterate_sem n (Assume b;; C) S)"
  proof (rule indexed_invariant_then_power)
    fix n
    have "⊨ {Q n} C {P (Suc n)}"
    proof (rule hyper_hoare_tripleI)
      fix S assume asm1: "Q n S"
      let ?S = "assign_exp_to_lvar_set e t S"
      have "conj (Q n) (e_recorded_in_t e t) ?S"
        by (metis asm1 assms(6) conj_def e_recorded_in_t_if_assigned not_fv_hyper_assign_exp)
      then have "conj (P (Suc n)) (e_smaller_than_t e t lt) (sem C ?S)"
        using assms(2) hyper_hoare_tripleE total_hyper_triple_def by blast
      then show "P (Suc n) (sem C S)"
        using assign_exp_to_lvar_set_same_mod_updates[of t S e] assms(5) conj_def not_fv_hyperE same_mod_updates_sym[of "{t}"] sem_update_commute[of "{t}"]
        by metis
    qed
    then show " ⊨ {P n} Assume b ;; C {P (Suc n)}"
      using assms(1) seq_rule total_hyper_triple_def by blast
  qed (simp add: asm0)
  then have "natural_partition P (⋃n. iterate_sem n (Assume b;; C) S)"
    by (simp add: natural_partitionI)
  then show "R (sem (while_cond b C) S)"
    by (metis (no_types, lifting) SUP_cong assms(3) hyper_hoare_triple_def sem_seq sem_while while_cond_def)

  show "terminates_in (while_cond b C) S"
  proof (rule terminates_in_while_loop)
    show "wfP lt"
      by (simp add: assms(4))
    fix φ n
    assume asm1: "φ ∈ iterate_sem n (Assume b ;; C) S ∧ b (snd φ)"

    let ?S = "assign_exp_to_lvar_set e t (iterate_sem n (Assume b;; C) S)"
    let ?φ = "assign_exp_to_lvar e t φ"
    have "conj (P n) (e_recorded_in_t e t) ?S"
      by (metis ‹⋀n. P n (iterate_sem n (Assume b ;; C) S)› assms(5) conj_def e_recorded_in_t_if_assigned not_fv_hyper_assign_exp)
    then have "conj (Q n) (e_recorded_in_t e t) (sem (Assume b) ?S)"
      using assms(1)
      by (metis (mono_tags, lifting) IntE conj_def e_recorded_in_t_def hyper_hoare_tripleE
          sem_assume_setify) 
    then have "conj (P (Suc n)) (e_smaller_than_t e t lt) (sem C (sem (Assume b) ?S))"
      using assms(2) hyper_hoare_tripleE total_hyper_triple_def by blast
    moreover have "?φ ∈ (sem (Assume b) ?S)"
      using asm1
      by (simp add: assign_exp_to_lvar_set_def assume_sem same_outside_set_lvar_assign_exp [of φ e t])
    then obtain σ' where "(fst ?φ, σ') ∈ sem C (sem (Assume b) ?S) ∧ ⟨C, snd ?φ⟩ → σ'"
      using total_hyper_tripleE assms(2)[of n]
      using ‹Logic.conj (Q n) (e_recorded_in_t e t) (sem (Assume b) (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S)))› by blast
    then have "lt (e (snd (fst ?φ, σ'))) (fst (fst ?φ, σ') t)"
      using calculation
      by (auto simp add: conj_def e_smaller_than_t_def)
    ultimately show "∃σ'. ⟨C, snd φ⟩ → σ' ∧ (¬ b σ' ∨ lt (e σ') (e (snd φ)))"
      by (metis ‹(fst (assign_exp_to_lvar e t φ), σ') ∈ sem C (sem (Assume b) (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))) ∧ ⟨C, snd (assign_exp_to_lvar e t φ)⟩ → σ'› assign_exp_to_lvar_def fst_conv fun_upd_same snd_conv)
  qed
qed


definition e_smaller_than_t_weaker where
  "e_smaller_than_t_weaker e t u lt S ⟷ (∀φ∈S. ∃φ'∈S. fst φ u = fst φ' u ∧ lt (e (snd φ)) (fst φ' t))"


lemma exists_terminates_loop:
  assumes "wfP lt"
      and "⋀v. ⊨ { (λS. ∃φ∈S. e (snd φ) = v ∧ b (snd φ) ∧ P φ S) } if_then b C { (λS. ∃φ∈S. lt (e (snd φ)) v ∧ P φ S) }"
      and "⋀φ. ⊨ { P φ } while_cond b C { Q φ }"
    shows "⊨ { (λS. ∃φ∈S. P φ S) } while_cond b C { (λS. ∃φ∈S. Q φ S)}"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "∃φ∈S. P φ S"
  then obtain φ where "φ ∈ S" "P φ S" by blast
  show "∃φ∈sem (while_cond b C) S. Q φ (sem (while_cond b C) S)"
  proof (cases "b (snd φ)")
    case True

    let ?R = "{(x, y). lt x y}"
    let ?Q = "{ e (snd φ') |φ' n. φ' ∈ iterate_sem n (if_then b C) S ∧ b (snd φ') ∧ P φ' (iterate_sem n (if_then b C) S) }"
  
    have main_res: "∃n φ'. φ' ∈ iterate_sem n (if_then b C) S ∧ ¬ b (snd φ') ∧ P φ' (iterate_sem n (if_then b C) S)"
    proof (rule wfE_min)
      show "wf ?R"
        using assms(1) wfp_def by blast
      show "e (snd φ) ∈ ?Q"
        using True ‹P φ S› ‹φ ∈ S› iterate_sem.simps(1) by fastforce
      fix z
      assume asm1: "z ∈ ?Q" "⋀y. (y, z) ∈ ?R ⟹ y ∉ ?Q"
      then obtain n φ' where "φ' ∈ iterate_sem n (if_then b C) S" "b (snd φ')" "P φ' (iterate_sem n (if_then b C) S)" "z = e (snd φ')"
        by blast
      then have "(λS. ∃φ∈S. (b (snd φ) ⟶ lt (e (snd φ)) z) ∧ P φ S) (sem (if_then b C) ((iterate_sem n (if_then b C) S)))"
        using assms(2) hyper_hoare_tripleE by blast
      then obtain φ'' where "(b (snd φ'') ⟶ lt (e (snd φ'')) z) ∧ P φ'' (sem (if_then b C) ((iterate_sem n (if_then b C) S)))"
        "φ'' ∈ (sem (if_then b C) ((iterate_sem n (if_then b C) S)))"
        by blast
      then have "¬ b (snd φ'')"
        by (metis (mono_tags, lifting) asm1(2) case_prodI iterate_sem.simps(2) mem_Collect_eq)
      then show "∃n φ'. φ' ∈ iterate_sem n (if_then b C) S ∧ ¬ b (snd φ') ∧ P φ' (iterate_sem n (if_then b C) S)"
        by (metis ‹(b (snd φ'') ⟶ lt (e (snd φ'')) z) ∧ P φ'' (sem (if_then b C) (iterate_sem n (if_then b C) S))› ‹φ'' ∈ sem (if_then b C) (iterate_sem n (if_then b C) S)› iterate_sem.simps(2))
    qed
    then obtain n φ' where "φ' ∈ iterate_sem n (if_then b C) S" "¬ b (snd φ')" "P φ' (iterate_sem n (if_then b C) S)"
      by blast
    then have "∃φ∈sem (while_cond b C) (iterate_sem n (if_then b C) S). Q φ (sem (while_cond b C) (iterate_sem n (if_then b C) S))"
      using while_exists[of P b C Q] assms(3) hyper_hoare_tripleE by blast
    then show "∃φ∈sem (while_cond b C) S. Q φ (sem (while_cond b C) S)"
      by (simp add: unroll_while_sem)
  next
    case False
    then show ?thesis
    using while_exists[of P b C Q] assms(3) hyper_hoare_tripleE ‹P φ S› ‹φ ∈ S› by blast
  qed
qed

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

lemma t_closedE:
  assumes "t_closed P P_inf"
      and "converges_sets S"
      and "⋀n. P n (S n)"
    shows "P_inf (⋃n. S n)"
  using TotalLogic.t_closed_def assms(1) assms(2) assms(3) by blast


subsection ‹Total version of core rules›

lemma total_skip_rule:
  "⊨TERM {P} Skip {P}"
  by (meson SemSkip skip_rule total_hyper_triple_def)

lemma total_seq_rule:
  assumes "⊨TERM {P} C1 {R}"
    and "⊨TERM {R} C2 {Q}"
  shows "⊨TERM {P} Seq C1 C2 {Q}"
proof (rule total_hyper_tripleI)
  show "⊨ {P} C1 ;; C2 {Q}"
    using assms(1) assms(2) seq_rule total_hyper_triple_def by blast
  fix φ S assume "P S ∧ φ ∈ S"
  then obtain σ' where "⟨C1, snd φ⟩ → σ'" "(fst φ, σ') ∈ sem C1 S"
    using assms(1) total_hyper_tripleE by blast
  then obtain σ'' where "⟨C2, σ'⟩ → σ''"
    using assms
    by (metis (full_types) ‹P S ∧ φ ∈ S› hyper_hoare_tripleE snd_conv total_hyper_triple_def)
  then show "∃σ''. ⟨C1 ;; C2, snd φ⟩ → σ''"
    using SemSeq ‹⟨C1, snd φ⟩ → σ'› by blast
qed

lemma total_if_rule:
  assumes "⊨TERM {P} C1 {Q1}"
      and "⊨TERM {P} C2 {Q2}"
    shows "⊨TERM {P} If C1 C2 {join Q1 Q2}"
proof (rule total_hyper_tripleI)
  show "⊨ {P} stmt.If C1 C2 {join Q1 Q2}"
    using assms(1) assms(2) if_rule total_hyper_triple_equiv by blast
  fix φ S assume "P S ∧ φ ∈ S"
  then show "∃σ'. ⟨stmt.If C1 C2, snd φ⟩ → σ'"
    using SemIf1 assms(1) total_hyper_tripleE by blast
qed


lemma total_rule_exists:
  assumes "⋀x. ⊨TERM {P x} C {Q x}"
  shows "⊨TERM {exists P} C {exists Q}"
  using total_hyper_tripleI[of "exists P" C "exists Q"]
  by (metis (mono_tags, lifting) Loops.exists_def assms hyper_hoare_triple_def total_hyper_triple_def)


lemma total_assign_rule:
  "⊨TERM { (λS. P { (l, σ(x := e σ)) |l σ. (l, σ) ∈ S }) } (Assign x e) {P}"
  using total_hyper_tripleI[of _ "Assign x e" P]
  using SemAssign assign_rule by fastforce

lemma total_havoc_rule:
  "⊨TERM { (λS. P { (l, σ(x := v)) |l σ v. (l, σ) ∈ S }) } (Havoc x) {P}"
  using total_hyper_tripleI[of _ "Havoc x" P]
  using SemHavoc havoc_rule by fastforce

lemma in_semI:
  assumes "φ ∈ S"
      and "fst φ = fst φ'"
      and "single_sem C (snd φ) (snd φ')"
    shows "φ' ∈ sem C S"
  using assms
  by (metis (no_types, lifting) prod.collapse single_step_then_in_sem)


theorem normal_while_tot_stronger:
  fixes P :: "nat ⇒ ('lvar, 'lval, 'pvar, 'pval) state set ⇒ bool"

  assumes "⋀n. ⊨ {P n} Assume b {Q n}"
      and "⋀n. ⊨TERM {conj (Q n) (e_recorded_in_t e t)} C {conj (P (Suc n)) (e_smaller_than_t_weaker e t u lt)}"
      and "⊨ {natural_partition P} Assume (lnot b) {R}"

      and "wfP lt"
      and "⋀n. not_fv_hyper t (P n)"
      and "⋀n. not_fv_hyper t (Q n)"

      and "⋀n. not_fv_hyper u (P n)"
      and "⋀n. not_fv_hyper u (Q n)"

      and "(tr :: 'lval) ≠ fa"
      and "u ≠ t"

    shows "⊨TERM {P 0} while_cond b C {R}"
proof (rule total_hyper_triple_altI)
  fix S :: "('lvar, 'lval, 'pvar, 'pval) state set"
  assume asm0: "P 0 S"
  have "⋀n. P n (iterate_sem n (Assume b;; C) S)"
  proof (rule indexed_invariant_then_power)
    fix n
    have "⊨ {Q n} C {P (Suc n)}"
    proof (rule hyper_hoare_tripleI)
      fix S assume asm1: "Q n S"
      let ?S = "assign_exp_to_lvar_set e t S"
      have "conj (Q n) (e_recorded_in_t e t) ?S"
        by (metis asm1 assms(6) conj_def e_recorded_in_t_if_assigned not_fv_hyper_assign_exp)
      then have "conj (P (Suc n)) (e_smaller_than_t_weaker e t u lt) (sem C ?S)"
        using assms(2) hyper_hoare_tripleE total_hyper_triple_def by blast
      then show "P (Suc n) (sem C S)"
        using assign_exp_to_lvar_set_same_mod_updates[of t] assms(5) conj_def not_fv_hyperE[of t "P (Suc n)"] same_mod_updates_sym[of "{t}"] sem_update_commute[of "{t}"]
        by metis
    qed
    then show " ⊨ {P n} Assume b ;; C {P (Suc n)}"
      using assms(1) seq_rule total_hyper_triple_def by blast
  qed (simp add: asm0)
  then have "natural_partition P (⋃n. iterate_sem n (Assume b;; C) S)"
    by (simp add: natural_partitionI)
  then show "R (sem (while_cond b C) S)"
    using SUP_cong assms(3) hyper_hoare_triple_def[of "natural_partition P" "Assume (lnot b)" R] sem_seq sem_while while_cond_def
    by metis


  show "terminates_in (while_cond b C) S"
  proof (rule terminates_in_while_loop)
    show "wfP lt"
      by (simp add: assms(4))
    fix φ n
    assume asm1: "φ ∈ iterate_sem n (Assume b ;; C) S ∧ b (snd φ)"

    let ?S = "assign_exp_to_lvar_set e t (iterate_sem n (Assume b;; C) S)"
    let ?φ = "assign_exp_to_lvar e t φ"

    let ?SS = "update_lvar_set u (λφ'. if φ' = ?φ then tr else fa) ?S" 

    have SS_def: "?SS = { ((fst φ')(u := if φ' = ?φ then tr else fa), snd φ') |φ'. φ' ∈ ?S}"
      by (simp add: update_lvar_set_def)

    have same: "same_mod_updates {u} ?S ?SS"
      by (meson same_update_lvar_set)


    let ?φ' = "((fst ?φ)(u := tr), snd ?φ)"

    have "conj (P n) (e_recorded_in_t e t) ?S"
      by (metis ‹⋀n. P n (iterate_sem n (Assume b ;; C) S)› assms(5) conj_def e_recorded_in_t_if_assigned not_fv_hyper_assign_exp)
    moreover have "e_recorded_in_t e t ?SS"
    proof (rule e_recorded_in_tI)
      fix φ' assume "φ' ∈ ?SS"
      then show "fst φ' t = e (snd φ')" unfolding SS_def
        using assms(10) e_recorded_in_t_def e_recorded_in_t_if_assigned by fastforce
    qed

    then have "conj (P n) (e_recorded_in_t e t) ?SS"
      using assms(7) calculation conj_def not_fv_hyperE[of u "P n"] same
      by metis
    then have "conj (Q n) (e_recorded_in_t e t) (sem (Assume b) ?SS)"
      using assms(1) assume_sem[of b] e_recorded_in_t_def[of e t] hyper_hoare_tripleE[of "P n" "Assume b" "Q n"
        "update_lvar_set u (λφ'. if φ' = assign_exp_to_lvar e t φ then tr else fa) (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))"]
      by (simp add: conj_def sem_assume_setify)
    then have "conj (P (Suc n)) (e_smaller_than_t_weaker e t u lt) (sem C (sem (Assume b) ?SS))"
      using assms(2) hyper_hoare_tripleE total_hyper_triple_def by blast
    moreover have "?φ ∈ (sem (Assume b) ?S)"
      using asm1 same_outside_set_lvar_assign_exp [of φ e t]
      by (auto simp add: assign_exp_to_lvar_set_def assume_sem)
    moreover have "?φ' ∈ (sem (Assume b) ?SS)"
      unfolding SS_def
    proof (rule in_semI)
      show "((fst ?φ)(u := if ?φ = assign_exp_to_lvar e t φ then tr else fa), snd ?φ) ∈ {((fst φ')(u := if φ' = assign_exp_to_lvar e t φ then tr else fa), snd φ') |φ'. φ' ∈ assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S)}"        
        using asm1 assign_exp_to_lvar_set_def by fastforce
      show "fst ((fst (assign_exp_to_lvar e t φ))(u := if assign_exp_to_lvar e t φ = assign_exp_to_lvar e t φ then tr else fa), snd (assign_exp_to_lvar e t φ)) =
    fst ((fst (assign_exp_to_lvar e t φ))(u := tr), snd (assign_exp_to_lvar e t φ))"
        by presburger
      show "⟨Assume
      b, snd ((fst (assign_exp_to_lvar e t φ))(u := if assign_exp_to_lvar e t φ = assign_exp_to_lvar e t φ then tr else fa),
              snd (assign_exp_to_lvar e t φ))⟩ → snd ((fst (assign_exp_to_lvar e t φ))(u := tr), snd (assign_exp_to_lvar e t φ))"
        by (metis SemAssume asm1 same_outside_set_lvar_assign_exp snd_conv)
    qed
    then obtain σ' where "(fst ?φ', σ') ∈ sem C (sem (Assume b) ?SS) ∧ ⟨C, snd ?φ'⟩ → σ'"
      using total_hyper_tripleE assms(2)[of n]
      using ‹Logic.conj (Q n) (e_recorded_in_t e t) (sem (Assume b) (update_lvar_set u (λφ'. if φ' = assign_exp_to_lvar e t φ then tr else fa) (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))))› by blast
    moreover obtain φ' where "φ' ∈ sem C (sem (Assume b) ?SS)" "fst (fst ?φ', σ') u = fst φ' u ∧ lt (e (snd (fst ?φ', σ'))) (fst φ' t)"
      using calculation conj_def[of "P (Suc n)" "e_smaller_than_t_weaker e t u lt"] e_smaller_than_t_weaker_def[of e t u lt]
      by meson
    then have "fst φ' u = tr"
      by simp
    moreover have "fst ?φ t = fst φ' t ∧ single_sem C (snd φ) (snd φ')"
    proof -
      obtain φ0 where "φ0 ∈ sem (Assume b) ?SS" "fst φ0 = fst φ'" "single_sem C (snd φ0) (snd φ')"
        by (metis (no_types, lifting) ‹φ' ∈ sem C (sem (Assume b) (update_lvar_set u (λφ'. if φ' = assign_exp_to_lvar e t φ then tr else fa) (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))))› fst_conv in_sem snd_conv)
      then have "φ0 ∈ ?SS"
        using assume_sem by auto
      then obtain φ0' where 
        "φ0' ∈ (assign_exp_to_lvar_set e t (iterate_sem n (Assume b ;; C) S))"
        "φ0 = ((fst φ0')(u := if φ0' = assign_exp_to_lvar e t φ then tr else fa), snd φ0')"
        using SS_def by auto
      then have "φ0 = ((fst ?φ)(u := tr), snd ?φ)"
        by (metis (full_types) ‹fst φ0 = fst φ'› assms(9) calculation(5) fst_conv fun_upd_same)
      then show ?thesis
        by (metis ‹⟨C, snd φ0⟩ → snd φ'› ‹fst φ0 = fst φ'› assms(10) fst_conv fun_upd_other same_outside_set_lvar_assign_exp snd_conv)
    qed
    ultimately show "∃σ'. (⟨C, snd φ⟩ → σ') ∧ (¬ b σ' ∨ lt (e σ') (e (snd φ)))"
      by (metis (no_types, lifting) ‹fst (fst ((fst (assign_exp_to_lvar e t φ))(u := tr), snd (assign_exp_to_lvar e t φ)), σ') u = fst φ' u ∧ lt (e (snd (fst ((fst (assign_exp_to_lvar e t φ))(u := tr), snd (assign_exp_to_lvar e t φ)), σ'))) (fst φ' t)› assign_exp_to_lvar_def fst_conv fun_upd_same snd_conv)
  qed
qed




end