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