Theory While

theory While imports Acc_tools Orbit Cycle
begin

section{*Definition of \emph{while} loops as tail recursive functions.*}

function (tailrec) While :: "('a => bool) => ('a => 'a) => 'a => 'a"
where
  "While continue f s = (if continue s then While continue f (f s) else s)"
by auto

text{*We delete the definition from the simplifier to avoid infinite loops.*}

declare While.simps[simp del]
lemmas While_simp = While.simps

text{*An alternative definition for termination sets.*}

fun terminates_slice :: "('a => bool) => ('a => 'a) => ('a => bool) × ('a => 'a) × 'a => bool"
where 
  "terminates_slice continue0 f0 (continue, f, x) = (continue = continue0 ∧ f = f0 ∧ terminates (continue, f, x))"

lemma lfp_const: "lfp (λ p. P) = P"
proof -
  have mono: "mono (λ p. P)" by (simp add: mono_def)
  then show ?thesis
    by (simp add: lfp_unfold[OF mono])
qed

text{*Definition of the relation condition of \emph{While} loops.*}

lemmas While_rel_def' = While_rel_def[simplified lfp_const]

lemma While_rel_continue: "While_rel q (continue, f, s) ==> continue s"
  apply (erule While_rel.cases)
  apply simp
  done

lemma assumes n_g_0: "0 < (n::nat)" shows "∃m. n = Suc m"
  using n_g_0 by arith

lemma helper: shows "!!n::nat. 0 < n ==> ∃m. n = Suc m" by arith

lemma terminates_downward: "terminates x ==> While_rel y x ==> terminates y"
  apply (auto simp add: While_rel_def' terminates_simp)    
  apply (auto simp add: Orbit_def)
  apply (rule_tac x="(f^n) s" in exI)
  apply (case_tac "n=0")
  apply simp
  apply simp
  apply (subgoal_tac "? m. n = Suc m")
  apply auto
  apply (rule_tac x=m in exI)
  apply (simp add: funpow_zip)
  apply (simp add: helper)
  done

lemma terminates_slice_downward: "terminates_slice continue f x ==> While_rel y x ==> terminates_slice continue f y"
  apply (cases x, cases y) apply auto
  unfolding While_rel_def' apply auto using terminates_rec [of continue f _] by auto


lemma terminates_subset_dom[rule_format]: "terminates (continue, f, s) --> While_dom (continue, f, s)"
proof -
  let ?Q = "terminates"
  let ?r = "While_rel"
  note Q = terminates_downward
  {
    fix F 
    assume F_Q: "!! i::nat. ?Q (F i)"
    assume F_r: "!! i::nat. ?r (F (Suc i)) (F i)"
    { fix i
      have "? continue f s. F i = (continue, f, s)"
        apply (cases "F i")
        apply simp
        done
    }      
    note F_split = this
    {
      fix continue0 f0 s0
      assume F0:"F 0 = (continue0, f0, s0)"
      {
        fix i
        fix continue f s
        have "F i = (continue, f, s) ==> continue s"
          apply (subgoal_tac "?r (F (Suc i)) (F i)")
          apply simp
          apply (rule While_rel_continue[where q="(F (Suc i))" and f="f"])
          apply simp
          apply (rule F_r)
          done
      }
      note continue = this
      {
        fix i
        have "∀ continue f s. F i = (continue, f, s) --> s = (f0^i) s0 ∧ f = f0 ∧ continue = continue0"
          apply (induct i)
          apply (simp add: continue)      
          apply (simp add: F0)
          apply clarsimp
          apply (subgoal_tac "? continue f s. F i = (continue, f, s)")
          prefer 2
          apply (simp add: F_split)
          apply clarsimp          
          apply (subgoal_tac "?r (F (Suc i)) (F i)")
          prefer 2
          apply (rule F_r)
          apply (simp add: While_rel_def')
          done
      }
      note calc_F = this
      {      
        fix n
        have "continue0 ((f0^n) s0)"
          apply (insert calc_F[of n])
          apply (cases "F n")
          apply simp
          apply (simp add: continue)
          done
      }  
      note no_Orbit = this      
      have Orbit: "∃ y0 ∈ Orbit f0 s0. ¬ (continue0 y0)"
        apply (insert F0)
        apply (insert F_Q[of 0])
        apply (simp add: terminates_simp Bex_def)
        done
      then have "∃ n. ¬ (continue0 ((f0^n) s0))"
        by (auto simp add: Orbit_def)
      with no_Orbit have "False" by auto
    }    
    then have "False"
      apply (cases "F 0")
      apply simp
      apply blast
      done
  }
  note r = this
  show ?thesis
    apply (rule_tac impI)
    apply (rule downchain_contra_imp_subset_accP[where Q="?Q"])
    prefer 3
    apply simp
    apply (drule r)
    apply simp
    apply simp
    apply (rule Q)
    apply simp_all
    done
qed

lemma terminates_slice_subset_dom: "terminates_slice continue f x ==> While_dom x"
  apply (cases x)
  apply simp
  apply (rule terminates_subset_dom)
  apply (auto)
  done

text{*Some additional induction rules for the previous \emph{While} definition.*}

lemma While_pinduct:
  assumes terminates: "terminates (continue, f, s)"
  and I: "!! s. [| terminates (continue, f, s); continue s ==> P (f s)|] ==> P s"
  shows "P s"
proof -
  show ?thesis
    apply (subgoal_tac "P s = (λ (continue, f, s). P s) (continue, f, s)") 
    prefer 2
    apply clarify
    apply (simp only:)
    apply (rule accP_subset_induct[where r="While_rel" and Q="terminates_slice continue f"])    
    apply (simp add: terminates_slice_subset_dom)
    apply (simp add: terminates_slice_downward)
    apply (simp add: terminates)
    apply clarsimp
    apply (simp add: While_rel_def' I)
    done
qed

lemma While_pinduct_weak:
  assumes terminates: "terminates (continue, f, s)"
  and I: "!! s. [| continue s ==> P (f s)|] ==> P s"
  shows "P s"
  apply (rule While_pinduct[where P=P])
  apply (rule terminates)
  apply (rule I)
  apply simp
  done

lemma While_hoare_total:
  assumes wf_R: "wf R"
  and R_down: "!! x. P x ==> continue x ==> (f x, x) ∈ R"
  and P_cont: "!! x. P x ==> continue x ==> P (f x)"
  and P_not_cont: "!! x. P x ==> ¬ (continue x) ==> Q x"
  and P_start: "P s"
  shows "Q (While continue f s)"
proof -
  {
    fix x 
    assume Px: "P x"
    assume "¬ (terminates (continue, f, x))"
    then have continue: "!! n. continue ((f^n) x)" by (auto simp add: terminates_simp Orbit_def)
    {
      fix n
      have P: "P ((f^n) x)"
        apply (induct n)
        apply (simp add: Px)
        apply (simp)
        apply (rule P_cont)
        apply (simp_all add: continue)
        done
      note R =  R_down[OF P, OF continue]
    }
    then have "¬ (wf R)"
      apply (simp add: wf_iff_no_infinite_down_chain)
      apply (rule_tac x="λ n. (f^n) x" in exI)
      apply (auto)
      done
    with wf_R have "False" by auto
  }
  then have "!! x. P x ==> terminates (continue, f, x)" by auto
  with P_start have terminates: "terminates (continue, f, s)" by auto
  have "P s --> Q (While continue f s)"
  proof (induct rule: While_pinduct_weak[OF terminates])
    case (1 x)
    show ?case
      apply (subst While_simp)
      apply (case_tac "continue x")
      apply (auto simp add: P_not_cont)
      apply (rule 1[rule_format])
      apply (simp_all add: P_cont)
      done
  qed
  then show ?thesis by (simp add: P_start)
qed

(* do the fold while the condition holds and return the accumulator *)

section{*Definition of \emph{For} loops.*}

constdefs
  For' :: "('a => bool) => ('a => 'a) => ('a => 'b => 'b) => 'a => 'b => ('b × 'a)"
  "For' continue f Ac x ac ≡ While (λ (ac, x). continue x) (λ (ac, x). (Ac x ac, f x)) (ac, x)"
  "For continue f Ac x ac ≡ fst (For' continue f Ac x ac)"

term For

lemma For'_simp: "For' continue f Ac x ac = (if continue x then For' continue f Ac (f x) (Ac x ac) else (ac, x))"
proof -
  have trivial1: "split (λac. continue) (ac, x) = continue x"
    by simp
  have trivial2: "((λ(ac, x). (Ac x ac, f x)) (ac, x)) = (Ac x ac, f x)"
    by simp
  show ?thesis      
    apply (subst For'_def)
    thm While_simp
    apply (subst For'_def)
    apply (subst While_simp[of "(λ (ac, x). continue x)" "(λ (ac, x). (Ac x ac, f x))" "(ac, x)"])
    apply (simp only: trivial1 trivial2)
    done
qed

lemma For_simp: "For continue f Ac x ac = (if continue x then For continue f Ac (f x) (Ac x ac) else ac)"
proof -
  note unfold_For' = For'_simp[of continue f Ac x ac]
  show ?thesis by (auto simp add: For_def unfold_For')
qed

lemma split_power_of_for_state: "? ac'. (((λ(ac, x). ((Ac :: 'a => 'b => 'b) x ac, (f :: 'a => 'a) x)) ^ n) (a, b) = (ac', (f^n) b))"
  apply (induct n)
  apply auto
  done

lemma swap_Ex: "(∃ a b. P a b) = (∃ b a. P a b)" by blast

lemma terminates_For: "terminates (λ(ac, x). continue x, λ(ac, x). (Ac x ac, f x), s) = terminates (continue, f, snd s)"
  apply (cases s)
  apply simp
  apply (auto simp add: terminates_simp Bex_def Orbit_def)
  apply (rule_tac x=ba in exI)
  apply clarsimp
  apply (rule_tac x=n in exI)
  apply (subgoal_tac "? ac'. (((λ(ac, x). (Ac x ac, f x)) ^ n) (a, b) = (ac', (f^n) b))")
  apply clarsimp
  apply (rule split_power_of_for_state)
  apply (subst swap_Ex)
  apply (rule_tac x="(f^n) b" in exI)
  apply clarsimp
  apply (subst swap_Ex)
  apply (rule_tac x="n" in exI)
  apply (subgoal_tac "∃aa. ((λ(ac, x). (Ac x ac, f x)) ^ n) (a, b) = (aa, (f ^ n) b)")
  prefer 2
  apply (rule split_power_of_for_state)
  apply clarsimp
  done

text{*Additional induction rules for \emph{For} loops.*}

lemma For_pinduct:
  assumes terminates: "terminates (continue, f, i)"
  and I: "!!i s. [|terminates (continue, f, i); continue i ==> P (f i) (Ac (i::'a) (s::'b::type))|] ==> P i s"
  shows "P i s"
  apply (rule While_pinduct[of "(λ (ac, x). continue x)" "(λ (ac, x). (Ac x ac, f x))", simplified terminates_For, where s="(s,i)" and P = "λ (s,i). P i s", simplified])
  apply (simp add: terminates)
  apply (subgoal_tac "? s' i'. s = (s', i')")
  prefer 2
  apply simp
  apply (auto simp add: I)
  done

lemma For_pinduct_weak:
  assumes terminates: "terminates (continue, f, i)"
  and I: "!!i s. [|continue i ==> P (f i) (Ac (i::'a) (s::'b::type))|] ==> P i s"
  shows "P i s"
  apply (rule For_pinduct[where P=P])
  apply (rule terminates)
  apply (rule I)
  apply simp
  done

constdefs
  "find f x ≡ While (λ x. f x ≠ x) f x"
  "step1 f ≡ {(y,x). y = f x ∧ y ≠ x}"

thm find_def[symmetric]
thm While_simp

lemma find_simp: "find f x = (if f x ≠ x then find f (f x) else x)"  
  apply (simp only: find_def)
  apply (rule While_simp)
  done

(*lemmas find_simp = While_simp[where continue="(λx. ?f x ≠ x)", simplified find_def[symmetric]]*)

lemma find_wf_step1_terminates: "wf (step1 f) ==> terminates (λ x. f x ≠ x, f, i)"
  apply (erule wf_induct)
  apply (auto simp add: step1_def terminates_simp)
  done

lemmas find_pinduct = While_pinduct_weak[of "(λ x. f x ≠ x)" "f" x]

lemma find:
  assumes terminates: "terminates (λ x. f x ≠ x, f, x)"
  shows "f(find f x) = find f x"
proof (induct rule: find_pinduct)
  case 1
  show ?case by (simp add: terminates)
  case (2 x)
  show ?case 
    by (auto simp add: find_simp[of f x] 2)
qed

constdefs
  "section continue f x0 ≡ For continue f insert x0"
  "card_section continue f x0 ≡ For continue f (λ x y. y + (1::nat)) x0"

lemmas section_pinduct=For_pinduct[where Ac=insert]
lemmas section_pinduct_weak=For_pinduct_weak[where Ac=insert]
lemmas card_section_pinduct_weak=For_pinduct_weak[where Ac="λ x y. y + (1::nat)"]

lemma section_simp: "section continue f x A = (if continue x then section continue f (f x) (insert x A) else A)"
  apply (simp only: section_def)
  apply (rule For_simp)
  done

lemma card_section_simp:"card_section continue f x A = (if continue x then card_section continue f (f x) (A + 1) else A)"
  apply (simp only: card_section_def)
  apply (rule For_simp)
  done

lemma section_is_Section:
  assumes terminates: "terminates (continue, f, x0)"
  shows "section continue f x0 A = A ∪ (Section continue f x0)"
proof (induct rule: section_pinduct_weak[where f=f and continue=continue and i="x0" and P="λ x0 A. section continue f x0 A = A ∪ (Section continue f x0)"])
  case 1 
  show ?case by (simp add: terminates)
  case (2 i A)
  {
    assume i_eq_x1: "¬ continue i"
    have e: "Section continue f i  = {}" by (simp add: i_eq_x1 Section_x_x)
    have ?case
      apply (simp add: e)
      apply (subst section_simp)
      apply (simp add: i_eq_x1)
      done
  }
  note eq = this
  {
    assume i_neq_x1: "continue i"
    have ?case
      apply (subst section_simp)
      apply (simp add: i_neq_x1 2[OF i_neq_x1])
      apply (simp only: Un_insert_right[symmetric])
      apply (simp add: Section_unfold[where continue=continue, OF i_neq_x1])
      done
  }
  note neq = this
  from eq neq show ?case by auto
qed  

constdefs 
  "orbit f x ≡ section (λ y. y ≠ x) f (f x) {x}"
  "card_orbit f x ≡ card_section (λ y. y ≠ x) f (f x) 1"
    
lemma terminates_implies: "terminates (cond, f, x) ==> ∃ n. ¬ (cond ((f^n) x))"
  by (auto simp add: terminates_simp Orbit_def)

lemma orbit_is_Orbit: 
  assumes terminates: "terminates (λ y. y ≠ x, f, f x)"
  shows "orbit f x = Orbit f x"
  by (simp add: orbit_def section_is_Section[OF terminates] Section_is_Orbit')

lemma card_section_add: 
  assumes terminates: "terminates (continue, f, x0)"
  shows "card_section continue f x0 (a + b) = a + (card_section continue f x0 (b::nat))"
proof (induct x0 b arbitrary: a rule: card_section_pinduct_weak[where continue=continue and f=f])
  case 1
  show ?case by (rule terminates)
  case (2 i y x)
  show ?case 
    by (auto simp add: card_section_simp[where x0=i] 2[of x, simplified])
qed

lemma card_section_suc:
  assumes terminates: "terminates (continue, f, x0)"
  shows "card_section continue f x0 (Suc a) = Suc (card_section continue f x0 a)"
  by (rule card_section_add[OF terminates, where a=1 and b=a, simplified])


lemma terminates_imp: "terminates (continue, f, i) ==> continue i ==> terminates (continue, f, f i)"
  by (simp add: terminates_rec[where x="i"])

lemma Suc_first: "Suc (a + b) = Suc a + b" by simp

lemma card_section_eq[rule_format]: 
  "terminates (continue, f, x0) ==> finite A --> card_section continue f x0 (card A) = card (section continue f x0 A) + card (Section continue f x0 ∩ A)"
  apply (rule section_pinduct[where P="λ x0 A. finite A --> card_section continue f x0 (card A) = card (section continue f x0 A) + card (Section continue f x0 ∩ A)"])
  apply (assumption)
  apply (subst section_simp)
  apply (subst card_section_simp)
  apply (case_tac "¬ (continue i)")
  apply clarsimp
  apply (simp add: Section_x_x)
  apply clarsimp
  apply (case_tac "i ∈ s")
  apply (simp add: insert_absorb)
  apply (subst card_section_suc)
  apply (subgoal_tac "terminates (continue, f, i) = (if continue i then terminates (continue, f, f i) else True)")
  apply simp
  apply (rule terminates_rec)
  apply simp
  apply (subst Suc_card_Section_eq)
  apply simp_all
  apply (subgoal_tac "terminates (continue, f, i) = (if continue i then terminates (continue, f, f i) else True)")
  apply simp
  apply (rule terminates_rec)
  apply (case_tac "i ∈ Section continue f (f i)")
  apply (simp add: terminates_imp_notin_Section)
  apply (drule Section_unfold[where f=f and continue=continue])
  apply (subgoal_tac "insert i (Section continue f (f i)) ∩ s = Section continue f (f i) ∩ insert i s")
  apply simp
  apply auto
  done

lemma 
  assumes terminates: "terminates (continue, f, x)"
  shows "card_section continue f x 0 = card (Section continue f x)"
  by (simp add: card_section_eq[OF terminates, of "{}", simplified] section_is_Section[OF terminates])

constdefs
  "orbit_terminates f x x' ≡ terminates (λ y. y ≠ x, f, f x')"

lemma card_orbit_is_card_Orbit: 
  assumes terminates: "orbit_terminates f x x"
  shows "card_orbit f x = card (Orbit f x)"  
  apply (simp add: card_orbit_def)
  apply (simp add: orbit_is_Orbit[OF terminates[simplified orbit_terminates_def], symmetric])  
  apply (auto simp add: card_section_eq[OF terminates[simplified orbit_terminates_def], where A="{x}", simplified] orbit_def)
  done

(*lemmas orbit_terminates_rec = terminates_rec[where continue="λ y. y ≠ ?x" and f="?f" and x="?f ?x'", simplified orbit_terminates_def[symmetric]]*)

lemma orbit_terminates_rec: "orbit_terminates f x x' = (if f x' ≠ x then orbit_terminates f x (f x') else True)"
  apply (simp only: orbit_terminates_def)
  apply (rule terminates_rec)
  done


(*
----------------- This works! -------------------
consts fold_section :: "('a => bool) => ('a => 'a) => ('b => 'c => 'c) => ('a => 'b) => 'a => 'c => 'c" 

defs
  fold_section_def: "fold_section continue h f g z a == For continue h (λ z a. f (g z) a) z a"
*)

(*
---------------- This does not work! ---------------
*)

constdefs
  fold_section_def: "fold_section continue h f g z a == For continue h (λ z a. f (g z) a) z a"

lemma finite_Orbit: 
  assumes terminates: "orbit_terminates f a a"
  shows "finite (Orbit f a)"
proof -
  from terminates show ?thesis
    apply (simp add: Section_is_Orbit'[symmetric])
    apply (rule finite_Section)
    apply (simp add: orbit_terminates_def)
    done
qed
(*
lemmas fold_section_simp = For_simp[of "?continue" "?h" "(λ z a. ?f (?g z) a)", simplified fold_section_def[symmetric]]
*)
lemma
  fold_section_simp:
    "fold_section continue h f g x ac =
    (if continue x
     then fold_section continue h f g (h x) (f (g x) ac) else ac)"
  apply (subst fold_section_def)+
  apply (rule For_simp)
  done

text{*The following locale is simply a rewriting, or an interpretation, of @{text "ab_semigroup_mult"}, and is only used to 
  use @{text f} as a a binary operation instead of @{term [locale=ab_semigroup_mult] "op *"}*}

locale ACf =
  fixes f :: "'a => 'a => 'a"    (infixl "·" 70)
  assumes commute: "x · y = y · x"
    and assoc: "(x · y) · z = x · (y · z)"
begin

lemma left_commute: "x · (y · z) = y · (x · z)"
proof -
  have "x · (y · z) = (y · z) · x" by (simp only: commute)
  also have "... = y · (z · x)" by (simp only: assoc)
  also have "z · x = x · z" by (simp only: commute)
  finally show ?thesis .
qed

lemmas AC = assoc commute left_commute

end

interpretation ACf ⊆ ab_semigroup_mult f (infixl "·" 70)
by unfold_locales (simp_all add: AC)

lemma (in ACf) fold_Section_eq:
  assumes terminates: "terminates (continue, h, z)"  
  shows "fold f g a (Section continue h z) = fold_section continue h f g z a"
proof -
  let ?Ac = "λ z a. f (g z) a"
  show ?thesis
  proof (rule For_pinduct [where P="λ z a. fold f g a (Section continue h z) = fold_section continue h f g z a" and Ac="?Ac"])
    show "terminates (continue, h, z)" using terminates by simp
    fix i s
    assume termin: "terminates (continue, h, i)"
      and continue: "continue i ==> fold op · g (g i · s) (Section continue h (h i)) = fold_section continue h op · g (h i) (g i · s)"
    show "fold op · g s (Section continue h i) = fold_section continue h op · g i s"
    proof (cases "continue i")
      case False with Section_x_x [of continue i h] show ?thesis using fold_section_simp [of continue h f g i s] by auto
    next
      case True show ?thesis
        unfolding fold_section_simp [of continue h f g i s]
        using True apply simp
        unfolding Section_unfold [of continue i h]
        unfolding sym [OF continue]
        using finite_Section [OF terminates_imp [OF termin]] using True apply simp
        using fold_commute [of "(Section continue h (h i))" "g i" g s] using terminates_imp_notin_Section [OF termin]
        using fold_insert [of "(Section continue h (h i))" i  g s] by simp
    qed
  qed
qed

lemma (in ACf) fold_Orbit_eq:
  assumes terminates: "orbit_terminates h z z"
  shows "fold f g a (Orbit h z) = fold_section (λ y. y ≠ z) h f g (h z) (f (g z) a)"
proof -
  note t = terminates[simplified orbit_terminates_def]
  show ?thesis
    apply (subst fold_Section_eq[symmetric])
    prefer 2
    apply (subst Section_is_Orbit'[symmetric])
    apply (subst fold_commute[symmetric])
    prefer 2
    apply (subst fold_insert)
    prefer 3
    apply (simp_all add: t finite_Section)
    apply (rule terminates_imp_notin_Section)
    apply (subst terminates_rec)
    apply simp
    done
qed

lemma While_postcondition:
  assumes terminates: "terminates (continue, f, x)"
  shows " ¬ (continue (While continue f x))"
  apply (rule While_pinduct_weak[OF terminates])
  apply (subst While_simp)
  apply (case_tac "continue s")
  apply simp_all
  done

end