Theory RF_LTL

section "Relative Frequency LTL"

theory RF_LTL
  imports Main "HOL-Library.Sublist" Auxiliary DynamicArchitectures.Dynamic_Architecture_Calculus
begin

type_synonym 's seq = "nat ⇒ 's"

abbreviation "ccard n n' p ≡ card {i. i>n ∧ i ≤ n' ∧ p i}"

lemma ccard_same:
  assumes "¬ p (Suc n')"
  shows "ccard n n' p = ccard n (Suc n') p"
proof -
  have "{i. i > n ∧ i ≤ Suc n' ∧ p i} = {i. i>n ∧ i ≤ n' ∧ p i}"
  proof
    show "{i. n < i ∧ i ≤ Suc n' ∧ p i} ⊆ {i. n < i ∧ i ≤ n' ∧ p i}"
    proof
      fix x assume "x ∈ {i. n < i ∧ i ≤ Suc n' ∧ p i}"
      hence "n<x" and "x≤Suc n'" and "p x" by auto
      with assms (1) have "x≠Suc n'" by auto
      with ‹x≤Suc n'› have "x ≤ n'" by simp
      with ‹n<x› ‹p x› show "x ∈ {i. n < i ∧ i ≤ n' ∧ p i}" by simp
    qed
  next
    show "{i. n < i ∧ i ≤ n' ∧ p i} ⊆ {i. n < i ∧ i ≤ Suc n' ∧ p i}" by auto
  qed
  thus ?thesis by simp
qed

lemma ccard_zero[simp]:
  fixes n::nat
  shows "ccard n n p = 0"
  by auto

lemma ccard_inc:
  assumes "p (Suc n')"
    and "n' ≥ n"
  shows "ccard n (Suc n') p = Suc (ccard n n' p)"
proof -
  let ?A = "{i. i > n ∧ i ≤ n' ∧ p i}"
  have "finite ?A" by simp
  moreover have "Suc n' ∉ ?A" by simp
  ultimately have "card (insert (Suc n') ?A) = Suc (card ?A)" using card_insert_disjoint[of ?A] by simp
  moreover have "insert (Suc n') ?A = {i. i>n ∧ i ≤ (Suc n') ∧ p i}"
  proof
    show "insert (Suc n') ?A ⊆ {i. n < i ∧ i ≤ Suc n' ∧ p i}"
    proof
      fix x assume "x ∈ insert (Suc n') {i. n < i ∧ i ≤ n' ∧ p i}"
      hence "x=Suc n' ∨ n < x ∧ x ≤ n' ∧ p x" by simp
      thus "x ∈ {i. n < i ∧ i ≤ Suc n' ∧ p i}"
      proof
        assume "x = Suc n'"
        with assms (1) assms (2) show ?thesis by simp
      next
        assume "n < x ∧ x ≤ n' ∧ p x"
        thus ?thesis by simp
      qed
    qed
  next
    show "{i. n < i ∧ i ≤ Suc n' ∧ p i} ⊆ insert (Suc n') ?A" by auto
  qed
  ultimately show ?thesis by simp
qed

lemma ccard_mono:
  assumes "n'≥n"
  shows "n''≥n' ⟹ ccard n (n''::nat) p ≥ ccard n n' p"
proof (induction n'' rule: dec_induct)
  case base
  then show ?case ..
next
  case (step n'')
  then show ?case
  proof cases
    assume "p (Suc n'')"
    moreover from step.hyps assms have "n≤n''" by simp
    ultimately have "ccard n (Suc n'') p = Suc (ccard n n'' p)" using ccard_inc[of p n'' n] by simp
    also have "… ≥ ccard n n' p" using step.IH by simp
    finally show ?case .
  next
    assume "¬ p (Suc n'')"
    moreover from step.hyps assms have "n≤n''" by simp
    ultimately have "ccard n (Suc n'') p = ccard n n'' p" using ccard_same[of p n'' n] by simp
    also have "… ≥ ccard n n' p" using step.IH by simp
    finally show ?case by simp
  qed
qed

lemma ccard_ub[simp]:
  "ccard n n' p ≤ Suc n' - n"
proof -
  have "{i. i>n ∧ i ≤ n' ∧ p i} ⊆ {i. i≥n ∧ i ≤ n'}" by auto
  hence "ccard n n' p ≤ card {i. i≥n ∧ i ≤ n'}" by (simp add: card_mono)
  moreover have "{i. i≥n ∧ i ≤ n'} = {n..n'}" by auto
  hence "card {i. i≥n ∧ i ≤ n'} = Suc n' - n" by simp
  ultimately show ?thesis by simp
qed

lemma ccard_sum:
  fixes n::nat
  assumes "n'≥n''"
    and "n''≥n"
  shows "ccard n n' P = ccard n n'' P + ccard n'' n' P"
proof -
  have "ccard n n' P = card {i. i>n ∧ i ≤ n' ∧ P i}" by simp
  moreover have "{i. i>n ∧ i ≤ n' ∧ P i} =
    {i. i>n ∧ i ≤ n'' ∧ P i} ∪ {i. i>n'' ∧ i ≤ n' ∧ P i}" (is "?LHS = ?RHS")
  proof
    show "?LHS ⊆ ?RHS" by auto
  next
    show "?RHS ⊆ ?LHS"
    proof
      fix x
      assume "x∈?RHS"
      hence "x>n ∧ x ≤ n'' ∧ P x ∨ x>n'' ∧ x ≤ n' ∧ P x" by auto
      thus "x∈?LHS"
      proof
        assume "n < x ∧ x ≤ n'' ∧ P x"
        with assms show ?thesis by simp
      next
        assume "n'' < x ∧ x ≤ n' ∧ P x"
        with assms show ?thesis by simp
      qed
    qed
  qed
  hence "card ?LHS = card ?RHS" by simp
  ultimately have "ccard n n' P = card ?RHS" by simp
  moreover have "card ?RHS = card {i. i>n ∧ i ≤ n'' ∧ P i} + card {i. i>n'' ∧ i ≤ n' ∧ P i}"
  proof (rule card_Un_disjoint)
    show "finite {i. n < i ∧ i ≤ n'' ∧ P i}" by simp
    show "finite {i. n'' < i ∧ i ≤ n' ∧ P i}" by simp
    show "{i. n < i ∧ i ≤ n'' ∧ P i} ∩ {i. n'' < i ∧ i ≤ n' ∧ P i} = {}" by auto
  qed
  moreover have "ccard n n'' P = card {i. i>n ∧ i ≤ n'' ∧ P i}" by simp
  moreover have "ccard n'' n' P= card {i. i>n'' ∧ i ≤ n' ∧ P i}" by simp
  ultimately show ?thesis by simp
qed

lemma ccard_ex:
  fixes n::nat
  shows "c≥1 ⟹ c < ccard n n'' P ⟹ ∃n'<n''. n'>n ∧ ccard n n' P = c"
proof (induction c rule: dec_induct)
  let ?l = "LEAST i::nat. n < i ∧ i < n'' ∧ P i"
  case base
  moreover have "ccard n n'' P ≤ Suc (card {i. n < i ∧ i < n'' ∧ P i})"
  proof -
    from ‹ccard n n'' P > 1› have "n''>n" using less_le_trans by force
    then obtain n' where "Suc n' = n''" and "Suc n' ≥ n" by (metis lessE less_imp_le_nat)
    moreover have "{i. n < i ∧ i < Suc n' ∧ P i} = {i. n < i ∧ i ≤ n' ∧ P i}" by auto
    hence "card {i. n < i ∧ i < Suc n' ∧ P i} = card {i. n < i ∧ i ≤ n' ∧ P i}" by simp
    moreover have "card {i. n < i ∧ i ≤ Suc n' ∧ P i} ≤ Suc (card {i. n < i ∧ i ≤ n' ∧ P i})"
    proof cases
      assume "P (Suc n')"
      moreover from ‹n''>n› ‹Suc n'=n''› have "n'≥n" by simp
      ultimately show ?thesis using ccard_inc[of P n' n] by simp
    next
      assume "¬ P (Suc n')"
      moreover from ‹n''>n› ‹Suc n'=n''› have "n'≥n" by simp
      ultimately show ?thesis using ccard_same[of P n' n] by simp
    qed
    ultimately show ?thesis by simp
  qed
  ultimately have "card {i. n < i ∧ i < n'' ∧ P i} ≥ 1" by simp
  hence "{i. n < i ∧ i < n'' ∧ P i} ≠ {}" by fastforce
  hence "∃i. n < i ∧ i < n'' ∧ P i" by auto
  hence "?l>n" and "?l<n''" and "P ?l" using LeastI_ex[of "λi::nat. n < i ∧ i < n'' ∧ P i"] by auto
  moreover have "{i. n < i ∧ i ≤ ?l ∧ P i} = {?l}"
  proof
    show "{i. n < i ∧ i ≤ ?l ∧ P i} ⊆ {?l}"
    proof
      fix i
      assume "i∈{i. n < i ∧ i ≤ ?l ∧ P i}"
      hence "n < i" and "i ≤ ?l" and "P i" by auto
      with ‹∃i. n < i ∧ i < n'' ∧ P i› have "i=?l"
        using Least_le[of "λi. n < i ∧ i < n'' ∧ P i"] by (meson antisym le_less_trans)
      thus "i∈{?l}" by simp
    qed
  next
    show "{?l} ⊆ {i. n < i ∧ i ≤ ?l ∧ P i}"
    proof
      fix i
      assume "i∈{?l}"
      hence "i=?l" by simp
      with ‹?l>n› ‹?l<n''› ‹P ?l› show "i∈{i. n < i ∧ i ≤ ?l ∧ P i}" by simp
    qed
  qed
  hence "ccard n ?l P = 1" by simp
  ultimately show ?case by auto
next
  case (step c)
  moreover from step.prems have "Suc c<ccard n n'' P" by simp
  ultimately obtain n' where "n'<n''" and "n < n'" and "ccard n n' P = c" by auto
  hence "ccard n n'' P = ccard n n' P + ccard n' n'' P" using ccard_sum[of n' n'' n] by simp
  with ‹Suc c<ccard n n'' P› ‹ccard n n' P = c› have "ccard n' n'' P>1" by simp
  moreover have "ccard n' n'' P ≤ Suc (card {i. n' < i ∧ i < n'' ∧ P i})"
  proof -
    from ‹ccard n' n'' P > 1› have "n''>n'" using less_le_trans by force
    then obtain n''' where "Suc n''' = n''" and "Suc n''' ≥ n'" by (metis lessE less_imp_le_nat)
    moreover have "{i. n' < i ∧ i < Suc n''' ∧ P i} = {i. n' < i ∧ i ≤ n''' ∧ P i}" by auto
    hence "card {i. n' < i ∧ i < Suc n''' ∧ P i} = card {i. n' < i ∧ i ≤ n''' ∧ P i}" by simp
    moreover have "card {i. n' < i ∧ i ≤ Suc n''' ∧ P i} ≤ Suc (card {i. n' < i ∧ i ≤ n''' ∧ P i})"
    proof cases
      assume "P (Suc n''')"
      moreover from ‹n''>n'› ‹Suc n'''=n''› have "n'''≥n'" by simp
      ultimately show ?thesis using ccard_inc[of P n''' n'] by simp
    next
      assume "¬ P (Suc n''')"
      moreover from ‹n''>n'› ‹Suc n'''=n''› have "n'''≥n'" by simp
      ultimately show ?thesis using ccard_same[of P n''' n'] by simp
    qed
    ultimately show ?thesis by simp
  qed
  ultimately have "card {i. n' < i ∧ i < n'' ∧ P i} ≥ 1" by simp
  hence "{i. n' < i ∧ i < n'' ∧ P i} ≠ {}" by fastforce
  hence "∃i. n' < i ∧ i < n'' ∧ P i" by auto
  let ?l = "LEAST i::nat. n' < i ∧ i < n'' ∧ P i"
  from ‹∃i. n' < i ∧ i < n'' ∧ P i› have "n' < ?l"
    using LeastI_ex[of "λi::nat. n' < i ∧ i < n'' ∧ P i"] by auto
  with ‹n < n'› have "ccard n ?l P = ccard n n' P + ccard n' ?l P" using ccard_sum[of n' ?l n] by simp
  moreover have "{i. n' < i ∧ i ≤ ?l ∧ P i} = {?l}"
  proof
    show "{i. n' < i ∧ i ≤ ?l ∧ P i} ⊆ {?l}"
    proof
      fix i
      assume "i∈{i. n' < i ∧ i ≤ ?l ∧ P i}"
      hence "n' < i" and "i ≤ ?l" and "P i" by auto
      with ‹∃i. n' < i ∧ i < n'' ∧ P i› have "i=?l"
        using Least_le[of "λi. n' < i ∧ i < n'' ∧ P i"] by (meson antisym le_less_trans)
      thus "i∈{?l}" by simp
    qed
  next
    show "{?l} ⊆ {i. n' < i ∧ i ≤ ?l ∧ P i}"
    proof
      fix i
      assume "i∈{?l}"
      hence "i=?l" by simp
      moreover from ‹∃i. n' < i ∧ i < n'' ∧ P i› have "?l<n''" and "P ?l"
        using LeastI_ex[of "λi. n' < i ∧ i < n'' ∧ P i"] by auto
      ultimately show "i∈{i. n' < i ∧ i ≤ ?l ∧ P i}" using ‹?l>n'› by simp
    qed
  qed
  hence "ccard n' ?l P = 1" by simp
  ultimately have "card {i. n < i ∧ i ≤ ?l ∧ P i} = Suc c" using ‹ccard n n' P = c› by simp
  moreover from ‹∃i. n' < i ∧ i < n'' ∧ P i› have "n' < ?l" and "?l < n''" and "P ?l"
    using LeastI_ex[of "λi::nat. n' < i ∧ i < n'' ∧ P i"] by auto
  with ‹n < n'› have "n<?l" and "?l<n''" by auto
  ultimately show ?case by auto
qed

lemma ccard_freq:
  assumes "(n'::nat)≥n"
    and "ccard n n' P > ccard n n' Q + cnf"
  shows "∃n' n''. ccard n' n'' P > cnf ∧ ccard n' n'' Q ≤ cnf"
proof cases
  assume "cnf = 0"
  with assms(2) have "ccard n n' P > ccard n n' Q" by simp
  hence "card {i. n < i ∧ i ≤ n' ∧ P i}>card {i. n < i ∧ i ≤ n' ∧ Q i}" (is "card ?LHS>card ?RHS")
    by simp
  then obtain i where "i∈?LHS" and "¬ i ∈ ?RHS" and "i>0" using cardEx[of ?LHS ?RHS] by auto
  hence "P i" and "¬ Q i" by auto
  with ‹i>0› obtain n'' where "P (Suc n'')" and "¬Q (Suc n'')" using gr0_implies_Suc by auto
  hence "ccard n'' (Suc n'') P = 1" using ccard_inc by auto
  with ‹cnf = 0› have "ccard n'' (Suc n'') P > cnf" by simp
  moreover from ‹¬Q (Suc n'')› have "ccard n'' (Suc n'') Q = 0" using ccard_same[of Q n'' n''] by auto
  with ‹cnf = 0› have "ccard n'' (Suc n'') Q ≤ cnf" by simp
  ultimately show ?thesis by auto
next
  assume "¬ cnf = 0"
  show ?thesis
  proof (rule ccontr)
    assume "¬ (∃n' n''. ccard n' n'' P > cnf ∧ ccard n' n'' Q ≤ cnf)"
    hence hyp: "∀n' n''. ccard n' n'' Q ≤ cnf ⟶ ccard n' n'' P ≤ cnf"
      using leI less_imp_le_nat by blast
    show False
    proof cases
      assume "ccard n n' Q ≤ cnf"
      with hyp have "ccard n n' P ≤ cnf" by simp
      with assms show False by simp
    next
      let ?gcond="λn''. n''≥n ∧ n''≤n' ∧ (∃x≥1. ccard n n'' Q = x * cnf)"
      let ?g= "GREATEST n''. ?gcond n''"
      assume "¬ ccard n n' Q ≤ cnf"
      hence "ccard n n' Q > cnf" by simp
      hence "∃n''. ?gcond n''"
      proof -
        from ‹ccard n n' Q > cnf› ‹¬cnf=0› obtain n'' where "n''>n" and "n''≤n'" and "ccard n n'' Q = cnf"
          using ccard_ex[of cnf n n' Q ] by auto
        moreover from ‹ccard n n'' Q = cnf› have "∃x≥1. ccard n n'' Q = x * cnf" by auto
        ultimately show ?thesis using less_imp_le_nat by blast
      qed
      moreover have "∀n''>n'. ¬ ?gcond n''" by simp
      ultimately have gex: "∃n''. ?gcond n'' ∧ (∀n'''. ?gcond n''' ⟶ n'''≤n'')"
        using boundedGreatest[of ?gcond _ n'] by blast
      hence "∃x≥1. ccard n ?g Q = x * cnf" and "?g ≥ n" using GreatestI_ex_nat[of ?gcond] by auto
      moreover {fix n''
      have "n''≥n ⟹ ∃x≥1. ccard n n'' Q = x * cnf ⟹ ccard n n'' P ≤ ccard n n'' Q"
      proof (induction n'' rule: ge_induct)
        case (step n')
        from step.prems obtain x where "x≥1" and cas: "ccard n n' Q = x * cnf" by auto
        then show ?case
        proof cases
          assume "x=1"
          with cas have "ccard n n' Q = cnf" by simp
          with hyp have "ccard n n' P ≤ cnf" by simp
          with ‹ccard n n' Q = cnf› show ?thesis by simp
        next
          assume "¬x=1"
          with ‹x≥1› have "x>1" by simp
          hence "x-1 ≥ 1" by simp
          moreover from ‹cnf≠0› ‹x-1 ≥ 1› have "(x-1) * cnf < x * cnf ∧ (x - 1) * cnf ≠ 0" by auto
          with ‹x-1 ≥ 1› ‹cnf≠0›‹ccard n n' Q = x * cnf› obtain n''
            where "n''>n" and "n''<n'" and "ccard n n'' Q = (x-1) * cnf"
            using ccard_ex[of "(x-1)*cnf" n n' Q ] by auto
          ultimately have "∃x≥1. ccard n n'' Q = x * cnf" and "n''≥n" by auto
          with ‹n''≥n› ‹n''<n'› have "ccard n n'' P ≤ ccard n n'' Q" using step.IH by simp
          moreover have "ccard n'' n' Q = cnf"
          proof -
            from ‹x-1 ≥ 1› have "x*cnf = ((x-1) * cnf) + cnf"
              using semiring_normalization_rules(2)[of "(x - 1)" cnf] by simp
            with ‹ccard n n'' Q = (x-1) * cnf› ‹ccard n n' Q = x * cnf›
            have "ccard n n' Q = ccard n n'' Q + cnf" by simp
            moreover from ‹n''≥n› ‹n''<n'› have "ccard n n' Q = ccard n n'' Q + ccard n'' n' Q"
              using ccard_sum[of n'' n' n] by simp
            ultimately show ?thesis by simp
          qed
          moreover from ‹ccard n'' n' Q = cnf› have "ccard n'' n' P ≤ cnf" using hyp by simp
          ultimately show ?thesis using ‹n''≥n› ‹n''<n'› ccard_sum[of n'' n' n] by simp
        qed
      qed } note geq = this
      ultimately have "ccard n ?g P ≤ ccard n ?g Q" by simp
      moreover have "ccard ?g n' P ≤ cnf"
      proof (rule ccontr)
        assume "¬ ccard ?g n' P ≤ cnf"
        hence "ccard ?g n' P > cnf" by simp
        have "ccard ?g n' Q > cnf"
        proof (rule ccontr)
          assume "¬ccard ?g n' Q > cnf"
          hence "ccard ?g n' Q ≤ cnf" by simp
          with ‹ccard ?g n' P > cnf› show False
            using ‹¬ (∃n' n''. ccard n' n'' P > cnf ∧ ccard n' n'' Q ≤ cnf)› by simp
        qed
        with ‹¬ cnf=0› obtain n'' where "n''>?g" and "n''<n'" and "ccard ?g n'' Q = cnf"
          using ccard_ex[of cnf ?g n' Q] by auto
        moreover have "∃x≥1. ccard n n'' Q = x * cnf"
        proof -
          from ‹∃x≥1. ccard n ?g Q = x * cnf› obtain x where "x≥1" and "ccard n ?g Q = x * cnf" by auto
          from ‹n''>?g› ‹?g≥n› have "ccard n n'' Q = ccard n ?g Q + ccard ?g n'' Q"
            using ccard_sum[of ?g n'' n Q] by simp
          with ‹ccard n ?g Q = x * cnf› have "ccard n n'' Q = x * cnf + ccard ?g n'' Q" by simp
          with ‹ccard ?g n'' Q = cnf› have "ccard n n'' Q = Suc x * cnf" by simp
          thus ?thesis by auto
        qed
        moreover from ‹n''>?g› ‹?g≥n› have "n''≥n" by simp
        ultimately have "∃n''>?g. ?gcond n''" by auto
        moreover from gex have "∀n'''. ?gcond n''' ⟶ n'''≤?g" using Greatest_le_nat[of ?gcond] by auto
        ultimately show False by auto
      qed
      moreover from gex have "n'≥?g" using GreatestI_ex_nat[of ?gcond] by auto
      ultimately have "ccard n n' P≤ccard n n' Q + cnf" using ccard_sum[of ?g n' n] using ‹?g ≥ n› by simp
      with assms show False by simp
    qed
  qed
qed

locale honest =
  fixes bc:: "('a list) seq"
    and n::nat
  assumes growth: "n'≠0 ⟹ n'≤n ⟹ bc n' = bc (n'-1) ∨ (∃b. bc n' = bc (n' - 1) @ b)"
begin
end

locale dishonest =
  fixes bc:: "('a list) seq"
    and mining::"bool seq"
  assumes growth: "⋀n::nat. prefix (bc (Suc n)) (bc n) ∨ (∃b::'a. bc (Suc n) = bc n @ [b]) ∧ mining (Suc n)"
begin

lemma prefix_save:
  assumes "prefix sbc (bc n')"
    and "∀n'''>n'. n'''≤n'' ⟶ length (bc n''') ≥ length sbc"
  shows "n''≥n' ⟹ prefix sbc (bc n'')"
proof (induction n'' rule: dec_induct)
  case base
  with assms(1) show ?case by simp
next
  case (step n)
  from growth[of n] show ?case
  proof
    assume "prefix (bc (Suc n)) (bc n)"
    moreover from step.hyps have "length (bc (Suc n)) ≥ length sbc" using assms(2) by simp
    ultimately show ?thesis using step.IH using prefix_length_prefix by auto
  next
    assume "(∃b. bc (Suc n) = bc n @ [b]) ∧ mining (Suc n)"
    with step.IH show ?thesis by auto
  qed
qed

theorem prefix_length:
  assumes "prefix sbc (bc n')" and "¬ prefix sbc (bc n'')" and "n'≤n''"
  shows "∃n'''>n'. n'''≤n'' ∧ length (bc n''') < length sbc"
proof (rule ccontr)
  assume "¬ (∃n'''>n'. n'''≤n'' ∧ length (bc n''') < length sbc)"
  hence "∀n'''>n'. n'''≤n'' ⟶ length (bc n''') ≥ length sbc" by auto
  with assms have "prefix sbc (bc n'')" using prefix_save[of sbc n' n''] by simp
  with assms (2) show False by simp
qed

theorem grow_mining:
  assumes "length (bc n) < length (bc (Suc n))"
  shows "mining (Suc n)"
  using assms growth leD prefix_length_le by blast

lemma length_suc_length:
  "length (bc (Suc n)) ≤ Suc (length (bc n))"
  by (metis eq_iff growth le_SucI length_append_singleton prefix_length_le)

end

locale dishonest_growth =
  fixes bc:: "nat seq"
    and mining:: "nat ⇒ bool"
  assumes as1: "⋀n::nat. bc (Suc n) ≤ Suc (bc n)"
    and as2: "⋀n::nat. bc (Suc n) > bc n ⟹ mining (Suc n)"
begin

end

sublocale dishonest ⊆ dishonest_growth "λn. length (bc n)" using grow_mining length_suc_length by unfold_locales auto

context dishonest_growth
begin
  theorem ccard_diff_lgth:
    "n'≥n ⟹ ccard n n' (λn. mining n) ≥ (bc n' - bc n)"
  proof (induction n' rule: dec_induct)
    case base
    then show ?case by simp
    next
    case (step n')
    from as1 have "bc (Suc n') < Suc (bc n') ∨ bc (Suc n') = Suc (bc n')"
      using le_neq_implies_less by blast
    then show ?case
    proof
      assume "bc (Suc n') < Suc (bc n')"
      hence "bc (Suc n') - bc n ≤ bc n' - bc n" by simp
      moreover from step.hyps have "ccard n (Suc n') (λn. mining n) ≥ ccard n n' (λn. mining n)"
        using ccard_mono[of n n' "Suc n'"] by simp
      ultimately show ?thesis using step.IH by simp
    next
      assume "bc (Suc n') = Suc (bc n')"
      hence "bc (Suc n') - bc n ≤ Suc (bc n' - bc n)" by simp
      moreover from ‹bc (Suc n') = Suc (bc n')› have "mining (Suc n')" using as2 by simp
      with step.hyps have "ccard n (Suc n') (λn. mining n) ≥ Suc (ccard n n' (λn. mining n))"
        using ccard_inc by simp
      ultimately show ?thesis using step.IH by simp
    qed
  qed
end

locale honest_growth =
  fixes bc:: "nat seq"
    and mining:: "nat ⇒ bool"
    and init:: nat
  assumes as1: "⋀n::nat. bc (Suc n) ≥ bc n"
    and as2: "⋀n::nat. mining (Suc n) ⟹ bc (Suc n) > bc n"
begin
  lemma grow_mono: "n'≥n⟹bc n'≥bc n"
  proof (induction n' rule: dec_induct)
    case base
    then show ?case by simp
  next
    case (step n')
    then show ?case using as1[of n'] by simp
  qed

  theorem ccard_diff_lgth:
    shows "n'≥n ⟹ bc n' - bc n ≥ ccard n n' (λn. mining n)"
  proof (induction n' rule: dec_induct)
    case base
    then show ?case by simp
  next
    case (step n')
    then show ?case
    proof cases
      assume "mining (Suc n')"
      with as2 have "bc (Suc n') > bc n'" by simp
      moreover from step.hyps have "bc n'≥bc n" using grow_mono by simp
      ultimately have "bc (Suc n') - bc n > bc n' - bc n" by simp
      moreover from as1 have "bc (Suc n') - bc n ≥ bc n' - bc n" by (simp add: diff_le_mono)
      moreover from ‹mining (Suc n')› step.hyps
        have "ccard n (Suc n') (λn. mining n) ≤ Suc (ccard n n' (λn. mining n))"
        using ccard_inc by simp
      ultimately show ?thesis using step.IH by simp
    next
      assume "¬ mining (Suc n')"
      hence "ccard n (Suc n') (λn. mining n) ≤ (ccard n n' (λn. mining n))" using ccard_same by simp
      moreover from as1 have "bc (Suc n') - bc n ≥ bc n' - bc n" by (simp add: diff_le_mono)
      ultimately show ?thesis using step.IH by simp
    qed
  qed
end

locale bounded_growth = hg: honest_growth hbc hmining + dg: dishonest_growth dbc dmining
    for hbc:: "nat seq"
    and dbc:: "nat seq"
    and hmining:: "nat ⇒ bool"
    and dmining:: "nat ⇒ bool"
    and sbc::nat
    and cnf::nat +
  assumes fair: "⋀n n'. ccard n n' (λn. dmining n) > cnf ⟹ ccard n n' (λn. hmining n) > cnf"
    and a2: "hbc 0 ≥ sbc+cnf"
    and a3: "dbc 0 < sbc"
begin

theorem hn_upper_bound: shows "dbc n < hbc n"
proof (rule ccontr)
  assume "¬ dbc n < hbc n"
  hence "dbc n ≥ hbc n" by simp
  moreover from a2 a3 have "hbc 0 > dbc 0 + cnf" by simp
  moreover have "hbc n≥hbc 0" using hg.grow_mono by simp
  ultimately have "dbc n - dbc 0 > hbc n - hbc 0 + cnf" by simp
  moreover have "ccard 0 n (λn. hmining n) ≤ hbc n - hbc 0" using hg.ccard_diff_lgth by simp
  moreover have "dbc n - dbc 0 ≤ ccard 0 n (λn. dmining n)" using dg.ccard_diff_lgth by simp
  ultimately have "ccard 0 n (λn. dmining n) > ccard 0 n (λn. hmining n) + cnf" by simp
  hence "∃n' n''. ccard n' n'' (λn. dmining n) > cnf ∧ ccard n' n'' (λn. hmining n) ≤ cnf"
    using ccard_freq by blast
  with fair show False using leD by blast
qed

end

end