(* Title: Blockchain.thy Author: Diego Marmsoler *) section "Blockchain Architectures" theory Blockchain imports Auxiliary DynamicArchitectures.Dynamic_Architecture_Calculus RF_LTL begin subsection "Blockchains" text ‹ A blockchain itself is modeled as a simple list. › type_synonym 'a BC = "'a list" abbreviation max_cond:: "('a BC) set ⇒ 'a BC ⇒ bool" where "max_cond B b ≡ b ∈ B ∧ (∀b'∈B. length b' ≤ length b)" no_syntax "_MAX1" :: "pttrns ⇒ 'b ⇒ 'b" (‹(‹indent=3 notation=‹binder MAX››MAX _./ _)› [0, 10] 10) "_MAX" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b" (‹(‹indent=3 notation=‹binder MAX››MAX _∈_./ _)› [0, 0, 10] 10) definition MAX:: "('a BC) set ⇒ 'a BC" where "MAX B = (SOME b. max_cond B b)" lemma max_ex: fixes XS::"('a BC) set" assumes "XS ≠ {}" and "finite XS" shows "∃xs∈XS. (∀ys∈XS. length ys ≤ length xs)" proof (rule Finite_Set.finite_ne_induct) show "finite XS" using assms by simp next from assms show "XS ≠ {}" by simp next fix x::"'a BC" show "∃xs∈{x}. ∀ys∈{x}. length ys ≤ length xs" by simp next fix zs::"'a BC" and F::"('a BC) set" assume "finite F" and "F ≠ {}" and "zs ∉ F" and "∃xs∈F. ∀ys∈F. length ys ≤ length xs" then obtain xs where "xs∈F" and "∀ys∈F. length ys ≤ length xs" by auto show "∃xs∈insert zs F. ∀ys∈insert zs F. length ys ≤ length xs" proof (cases) assume "length zs ≥ length xs" with ‹∀ys∈F. length ys ≤ length xs› show ?thesis by auto next assume "¬ length zs ≥ length xs" hence "length zs ≤ length xs" by simp with ‹xs ∈ F› show ?thesis using ‹∀ys∈F. length ys ≤ length xs› by auto qed qed lemma max_prop: fixes XS::"('a BC) set" assumes "XS ≠ {}" and "finite XS" shows "MAX XS ∈ XS" and "∀b'∈XS. length b' ≤ length (MAX XS)" proof - from assms have "∃xs∈XS. ∀ys∈XS. length ys ≤ length xs" using max_ex[of XS] by auto with MAX_def[of XS] show "MAX XS ∈ XS" and "∀b'∈XS. length b' ≤ length (MAX XS)" using someI_ex[of "λb. b ∈ XS ∧ (∀b'∈XS. length b' ≤ length b)"] by auto qed lemma max_less: fixes b::"'a BC" and b'::"'a BC" and B::"('a BC) set" assumes "b∈B" and "finite B" and "length b > length b'" shows "length (MAX B) > length b'" proof - from assms have "∃xs∈B. ∀ys∈B. length ys ≤ length xs" using max_ex[of B] by auto with MAX_def[of B] have "∀b'∈B. length b' ≤ length (MAX B)" using someI_ex[of "λb. b ∈ B ∧ (∀b'∈B. length b' ≤ length b)"] by auto with ‹b∈B› have "length b ≤ length (MAX B)" by simp with ‹length b > length b'› show ?thesis by simp qed subsection "Blockchain Architectures" text ‹ In the following we describe the locale for blockchain architectures. › locale Blockchain = dynamic_component cmp active for active :: "'nid ⇒ cnf ⇒ bool" (‹∥_∥⇘_⇙› [0,110]60) and cmp :: "'nid ⇒ cnf ⇒ 'ND" (‹σ⇘_⇙(_)› [0,110]60) + fixes pin :: "'ND ⇒ ('nid BC) set" and pout :: "'ND ⇒ 'nid BC" and bc :: "'ND ⇒ 'nid BC" and mining :: "'ND ⇒ bool" and honest :: "'nid ⇒ bool" and actHn :: "cnf ⇒ 'nid set" and actDn :: "cnf ⇒ 'nid set" and PoW:: "trace ⇒ nat ⇒ nat" and hmining:: "trace ⇒ nat ⇒ bool" and dmining:: "trace ⇒ nat ⇒ bool" and cb:: nat defines "actHn k ≡ {nid. ∥nid∥⇘k⇙ ∧ honest nid}" and "actDn k ≡ {nid. ∥nid∥⇘k⇙ ∧ ¬ honest nid}" and "PoW t n ≡ (LEAST x. ∀nid∈actHn (t n). length (bc (σ⇘nid⇙(t n))) ≤ x)" and "hmining t ≡ (λn. ∃nid∈actHn (t n). mining (σ⇘nid⇙(t n)))" and "dmining t ≡ (λn. ∃nid∈actDn (t n). mining (σ⇘nid⇙(t n)))" assumes consensus: "⋀nid t t' bc'::('nid BC). ⟦honest nid⟧ ⟹ eval nid t t' 0 (□⇩_{b}([λnd. bc' = (if (∃b∈pin nd. length b > length (bc nd)) then (MAX (pin nd)) else (bc nd))]⇩_{b}⟶⇧^{b}○⇩_{b}[λnd.(¬ mining nd ∧ bc nd = bc' ∨ mining nd ∧ (∃b. bc nd = bc' @ [b]))]⇩_{b}))" and attacker: "⋀nid t t' bc'. ⟦¬ honest nid⟧ ⟹ eval nid t t' 0 (□⇩_{b}([λnd. bc' = (SOME b. b ∈ (pin nd ∪ {bc nd}))]⇩_{b}⟶⇧^{b}○⇩_{b}[λnd.(¬ mining nd ∧ prefix (bc nd) bc' ∨ mining nd ∧ (∃b. bc nd = bc' @ [b]))]⇩_{b}))" and forward: "⋀nid t t'. eval nid t t' 0 (□⇩_{b}[λnd. pout nd = bc nd]⇩_{b})" ― ‹At each time point a node will forward its blockchain to the network› and init: "⋀nid t t'. eval nid t t' 0 [λnd. bc nd=[]]⇩_{b}" and conn: "⋀k nid. ⟦∥nid∥⇘k⇙; honest nid⟧ ⟹ pin (cmp nid k) = (⋃nid'∈actHn k. {pout (cmp nid' k)})" and act: "⋀t n::nat. finite {nid::'nid. ∥nid∥⇘t n⇙}" and actHn: "⋀t n::nat. ∃nid. honest nid ∧ ∥nid∥⇘t n⇙ ∧ ∥nid∥⇘t (Suc n)⇙" and fair: "⋀n n'. ccard n n' (dmining t) > cb ⟹ ccard n n' (hmining t) > cb" and closed: "⋀t nid b n::nat. ⟦∥nid∥⇘t n⇙; b ∈ pin (σ⇘nid⇙(t n))⟧ ⟹ ∃nid'. ∥nid'∥⇘t n⇙ ∧ bc (σ⇘nid'⇙(t n)) = b" and mine: "⋀t nid n::nat. ⟦honest nid; ∥nid∥⇘t (Suc n)⇙; mining (σ⇘nid⇙(t (Suc n)))⟧ ⟹ ∥nid∥⇘t n⇙" begin lemma init_model: assumes "¬ (∃n'. latestAct_cond nid t n n')" and "∥nid∥⇘t n⇙" shows "bc (σ⇘nid⇙t n) = []" proof - from assms(2) have "∃i≥0. ∥nid∥⇘t i⇙" by auto with init have "bc (σ⇘nid⇙t ⟨nid → t⟩⇘0⇙) = []" using baEA[of 0 nid t] by blast moreover from assms have "n=⟨nid → t⟩⇘0⇙" using nxtAct_eq by simp ultimately show ?thesis by simp qed lemma fwd_bc: fixes nid and t::"nat ⇒ cnf" and t'::"nat ⇒ 'ND" assumes "∥nid∥⇘t n⇙" shows "pout (σ⇘nid⇙t n) = bc (σ⇘nid⇙t n)" using assms forward globEANow[THEN baEANow[of nid t t' n]] by blast lemma finite_input: fixes t n nid assumes "∥nid∥⇘t n⇙" defines "dep nid' ≡ pout (σ⇘nid'⇙(t n))" shows "finite (pin (cmp nid (t n)))" proof - have "finite {nid'. ∥nid'∥⇘t n⇙}" using act by auto moreover have "pin (cmp nid (t n)) ⊆ dep ` {nid'. ∥nid'∥⇘t n⇙}" proof fix x assume "x ∈ pin (cmp nid (t n))" show "x ∈ dep ` {nid'. ∥nid'∥⇘t n⇙}" proof - from assms obtain nid' where "∥nid'∥⇘t n⇙" and "bc (σ⇘nid'⇙(t n)) = x" using closed ‹x ∈ pin (cmp nid (t n))› by blast hence "pout (σ⇘nid'⇙(t n)) = x" using fwd_bc by auto hence "x=dep nid'" using dep_def by simp moreover from ‹∥nid'∥⇘t n⇙› have "nid' ∈ {nid'. ∥nid'∥⇘t n⇙}" by simp ultimately show ?thesis using image_eqI by simp qed qed ultimately show ?thesis using finite_surj by metis qed lemma nempty_input: fixes t n nid assumes "∥nid∥⇘t n⇙" and "honest nid" shows "pin (cmp nid (t n))≠{}" using conn[of nid "t n"] act assms actHn_def by auto lemma onlyone: assumes "∃n'≥n. ∥tid∥⇘t n'⇙" and "∃n'<n. ∥tid∥⇘t n'⇙" shows "∃!i. ⟨tid ← t⟩⇘n⇙ ≤ i ∧ i < ⟨tid → t⟩⇘n⇙ ∧ ∥tid∥⇘t i⇙" proof show "⟨tid ← t⟩⇘n⇙ ≤ ⟨tid ← t⟩⇘n⇙ ∧ ⟨tid ← t⟩⇘n⇙ < ⟨tid → t⟩⇘n⇙ ∧ ∥tid∥⇘t ⟨tid ← t⟩⇘n⇙⇙" by (metis assms dynamic_component.nxtActI latestAct_prop(1) latestAct_prop(2) less_le_trans order_refl) next fix i show "⟨tid ← t⟩⇘n⇙ ≤ i ∧ i < ⟨tid → t⟩⇘n⇙ ∧ ∥tid∥⇘t i⇙ ⟹ i = ⟨tid ← t⟩⇘n⇙" by (metis latestActless(1) leI le_less_Suc_eq le_less_trans nxtActI order_refl) qed subsubsection "Component Behavior" lemma bhv_hn_ex: fixes t and t'::"nat ⇒ 'ND" and tid assumes "honest tid" and "∃n'≥n. ∥tid∥⇘t n'⇙" and "∃n'<n. ∥tid∥⇘t n'⇙" and "∃b∈pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙). length b > length (bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))" shows "¬ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∨ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) @ [b])" proof - let ?cond = "λnd. MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) = (if (∃b∈pin nd. length b > length (bc nd)) then (MAX (pin nd)) else (bc nd))" let ?check = "λnd. ¬ mining nd ∧ bc nd = MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∨ mining nd ∧ (∃b. bc nd = MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) @ [b])" from ‹honest tid› have "eval tid t t' 0 (□⇩_{b}([?cond]⇩_{b}⟶⇧^{b}○⇩_{b}[?check]⇩_{b}))" using consensus[of tid _ _ "MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))"] by simp moreover from assms have "∃i≥0. ∥tid∥⇘t i⇙" by auto moreover have "⟨tid ⇐ t⟩⇘0⇙ ≤ ⟨tid ← t⟩⇘n⇙" by simp ultimately have "eval tid t t' ⟨tid ← t⟩⇘n⇙ ([?cond]⇩_{b}⟶⇧^{b}○⇩_{b}[?check]⇩_{b})" using globEA[of 0 tid t t' "([?cond]⇩_{b}⟶⇧^{b}○⇩_{b}[?check]⇩_{b})" "⟨tid ← t⟩⇘n⇙"] by fastforce moreover have "eval tid t t' ⟨tid ← t⟩⇘n⇙ [?cond]⇩_{b}" proof (rule baIA) from ‹∃n'<n. ∥tid∥⇘t n'⇙› show "∃i≥⟨tid ← t⟩⇘n⇙. ∥tid∥⇘t i⇙" using latestAct_prop(1) by blast from assms(3) assms(4) show "?cond (σ⇘tid⇙t ⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙)" using latestActNxt by simp qed ultimately have "eval tid t t' ⟨tid ← t⟩⇘n⇙ (○⇩_{b}[?check]⇩_{b})" using impE[of tid t t' _ "[?cond]⇩_{b}" "○⇩_{b}[?check]⇩_{b}"] by simp moreover have "∃i>⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙. ∥tid∥⇘t i⇙" proof - from assms have "⟨tid → t⟩⇘n⇙>⟨tid ← t⟩⇘n⇙" using latestActNxtAct by simp with assms(3) have "⟨tid → t⟩⇘n⇙>⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙" using latestActNxt by simp moreover from ‹∃n'≥n. ∥tid∥⇘t n'⇙› have "∥tid∥⇘t ⟨tid → t⟩⇘n⇙⇙" using nxtActI by simp ultimately show ?thesis by auto qed moreover from assms have "⟨tid ← t⟩⇘n⇙ ≤ ⟨tid → t⟩⇘n⇙" using latestActNxtAct by (simp add: order.strict_implies_order) moreover from assms have "∃!i. ⟨tid ← t⟩⇘n⇙ ≤ i ∧ i < ⟨tid → t⟩⇘n⇙ ∧ ∥tid∥⇘t i⇙" using onlyone by simp ultimately have "eval tid t t' ⟨tid → t⟩⇘n⇙ [?check]⇩_{b}" using nxtEA1[of tid t "⟨tid ← t⟩⇘n⇙" t' "[?check]⇩_{b}" "⟨tid → t⟩⇘n⇙"] by simp moreover from ‹∃n'≥n. ∥tid∥⇘t n'⇙› have "∥tid∥⇘t ⟨tid → t⟩⇘n⇙⇙" using nxtActI by simp ultimately show ?thesis using baEANow[of tid t t' "⟨tid → t⟩⇘n⇙" ?check] by simp qed lemma bhv_hn_in: fixes t and t'::"nat ⇒ 'ND" and tid assumes "honest tid" and "∃n'≥n. ∥tid∥⇘t n'⇙" and "∃n'<n. ∥tid∥⇘t n'⇙" and "¬ (∃b∈pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙). length b > length (bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)))" shows "¬ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) ∨ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) @ [b])" proof - let ?cond = "λnd. bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) = (if (∃b∈pin nd. length b > length (bc nd)) then (MAX (pin nd)) else (bc nd))" let ?check = "λnd. ¬ mining nd ∧ bc nd = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) ∨ mining nd ∧ (∃b. bc nd = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) @ [b])" from ‹honest tid› have "eval tid t t' 0 ((□⇩_{b}([?cond]⇩_{b}⟶⇧^{b}○⇩_{b}[?check]⇩_{b})))" using consensus[of tid _ _ "bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)"] by simp moreover from assms have "∃i≥0. ∥tid∥⇘t i⇙" by auto moreover have "⟨tid ⇐ t⟩⇘0⇙ ≤ ⟨tid ← t⟩⇘n⇙" by simp ultimately have "eval tid t t' ⟨tid ← t⟩⇘n⇙ ([?cond]⇩_{b}⟶⇧^{b}○⇩_{b}[?check]⇩_{b})" using globEA[of 0 tid t t' "[?cond]⇩_{b}⟶⇧^{b}○⇩_{b}[?check]⇩_{b}" "⟨tid ← t⟩⇘n⇙"] by fastforce moreover have "eval tid t t' ⟨tid ← t⟩⇘n⇙ [?cond]⇩_{b}" proof (rule baIA) from ‹∃n'<n. ∥tid∥⇘t n'⇙› show "∃i≥⟨tid ← t⟩⇘n⇙. ∥tid∥⇘t i⇙" using latestAct_prop(1) by blast from assms(3) assms(4) show "?cond (σ⇘tid⇙t ⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙)" using latestActNxt by simp qed ultimately have "eval tid t t' ⟨tid ← t⟩⇘n⇙ (○⇩_{b}[?check]⇩_{b})" using impE[of tid t t' _ "[?cond]⇩_{b}" "○⇩_{b}[?check]⇩_{b}"] by simp moreover have "∃i>⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙. ∥tid∥⇘t i⇙" proof - from assms have "⟨tid → t⟩⇘n⇙>⟨tid ← t⟩⇘n⇙" using latestActNxtAct by simp with assms(3) have "⟨tid → t⟩⇘n⇙>⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙" using latestActNxt by simp moreover from ‹∃n'≥n. ∥tid∥⇘t n'⇙› have "∥tid∥⇘t ⟨tid → t⟩⇘n⇙⇙" using nxtActI by simp ultimately show ?thesis by auto qed moreover from assms have "⟨tid ← t⟩⇘n⇙ ≤ ⟨tid → t⟩⇘n⇙" using latestActNxtAct by (simp add: order.strict_implies_order) moreover from assms have "∃!i. ⟨tid ← t⟩⇘n⇙ ≤ i ∧ i < ⟨tid → t⟩⇘n⇙ ∧ ∥tid∥⇘t i⇙" using onlyone by simp ultimately have "eval tid t t' ⟨tid → t⟩⇘n⇙ [?check]⇩_{b}" using nxtEA1[of tid t "⟨tid ← t⟩⇘n⇙" t' "[?check]⇩_{b}" "⟨tid → t⟩⇘n⇙"] by simp moreover from ‹∃n'≥n. ∥tid∥⇘t n'⇙› have "∥tid∥⇘t ⟨tid → t⟩⇘n⇙⇙" using nxtActI by simp ultimately show ?thesis using baEANow[of tid t t' "⟨tid → t⟩⇘n⇙" ?check] by simp qed lemma bhv_hn_context: assumes "honest tid" and "∥tid∥⇘t n⇙" and "∃n'<n. ∥tid∥⇘t n'⇙" shows "∃nid'. ∥nid'∥⇘t ⟨tid ← t⟩⇘n⇙⇙ ∧ (mining (σ⇘tid⇙t n) ∧ (∃b. bc (σ⇘tid⇙t n) = bc (σ⇘nid'⇙t ⟨tid ← t⟩⇘n⇙) @ [b]) ∨ ¬ mining (σ⇘tid⇙t n) ∧ bc (σ⇘tid⇙t n) = bc (σ⇘nid'⇙t ⟨tid ← t⟩⇘n⇙))" proof cases assume casmp: "∃b∈pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙). length b > length (bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))" moreover from assms(2) have "∃n'≥n. ∥tid∥⇘t n'⇙" by auto moreover from assms(3) have "∃n'<n. ∥tid∥⇘t n'⇙" by auto ultimately have "¬ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∨ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) @ [b])" using assms(1) bhv_hn_ex by auto moreover from assms(2) have "⟨tid → t⟩⇘n⇙ = n" using nxtAct_active by simp ultimately have "¬ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ bc (σ⇘tid⇙t n) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∨ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘tid⇙t n) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) @ [b])" by simp moreover from assms(2) have "⟨tid → t⟩⇘n⇙ = n" using nxtAct_active by simp ultimately have "¬ mining (σ⇘tid⇙t n) ∧ bc (σ⇘tid⇙t n) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∨ mining (σ⇘tid⇙t n) ∧ (∃b. bc (σ⇘tid⇙t n) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) @ [b])" by simp moreover have "Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∈ pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)" proof - from ‹∃n'<n. ∥tid∥⇘t n'⇙› have "∥tid∥⇘t ⟨tid ← t⟩⇘n⇙⇙" using latestAct_prop(1) by simp hence "finite (pin (σ⇘tid⇙(t ⟨tid ← t⟩⇘n⇙)))" using finite_input[of tid t "⟨tid ← t⟩⇘n⇙"] by simp moreover from casmp obtain b where "b ∈ pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)" and "length b > length (bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))" by auto ultimately show ?thesis using max_prop(1) by auto qed with ‹∃n'<n. ∥tid∥⇘t n'⇙› obtain nid where "∥nid∥⇘t ⟨tid ← t⟩⇘n⇙⇙" and "bc (σ⇘nid⇙t ⟨tid ← t⟩⇘n⇙) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))" using closed[of tid t "⟨tid ← t⟩⇘n⇙" "MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))"] latestAct_prop(1) by auto ultimately show ?thesis by auto next assume "¬ (∃b∈pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙). length b > length (bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)))" moreover from assms(2) have "∃n'≥n. ∥tid∥⇘t n'⇙" by auto moreover from assms(3) have "∃n'<n. ∥tid∥⇘t n'⇙" by auto ultimately have "¬ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) ∨ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) @ [b])" using assms(1) bhv_hn_in[of tid n t] by auto moreover from assms(2) have "⟨tid → t⟩⇘n⇙ = n" using nxtAct_active by simp ultimately have "¬ mining (σ⇘tid⇙t n) ∧ bc (σ⇘tid⇙t n) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) ∨ mining (σ⇘tid⇙t n) ∧ (∃b. bc (σ⇘tid⇙t n) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) @ [b])" by simp moreover from ‹∃n'. latestAct_cond tid t n n'› have "∥tid∥⇘t ⟨tid ← t⟩⇘n⇙⇙" using latestAct_prop(1) by simp ultimately show ?thesis by auto qed lemma bhv_dn: fixes t and t'::"nat ⇒ 'ND" and uid assumes "¬ honest uid" and "∃n'≥n. ∥uid∥⇘t n'⇙" and "∃n'<n. ∥uid∥⇘t n'⇙" shows "¬ mining (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) ∧ prefix (bc (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙)) (SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}) ∨ mining (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) = (SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}) @ [b])" proof - let ?cond = "λnd. (SOME b. b ∈ (pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)})) = (SOME b. b ∈ pin nd ∪ {bc nd})" let ?check = "λnd. ¬ mining nd ∧ prefix (bc nd) (SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}) ∨ mining nd ∧ (∃b. bc nd = (SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}) @ [b])" from ‹¬ honest uid› have "eval uid t t' 0 ((□⇩_{b}([?cond]⇩_{b}⟶⇧^{b}○⇩_{b}[?check]⇩_{b})))" using attacker[of uid _ _ "(SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)})"] by simp moreover from assms have "∃i≥0. ∥uid∥⇘t i⇙" by auto moreover have "⟨uid ⇐ t⟩⇘0⇙ ≤ ⟨uid ← t⟩⇘n⇙" by simp ultimately have "eval uid t t' ⟨uid ← t⟩⇘n⇙ ([?cond]⇩_{b}⟶⇧^{b}○⇩_{b}[?check]⇩_{b})" using globEA[of 0 uid t t' "([?cond]⇩_{b}⟶⇧^{b}○⇩_{b}[?check]⇩_{b})" "⟨uid ← t⟩⇘n⇙"] by fastforce moreover have "eval uid t t' ⟨uid ← t⟩⇘n⇙ [?cond]⇩_{b}" proof (rule baIA) from ‹∃n'<n. ∥uid∥⇘t n'⇙› show "∃i≥⟨uid ← t⟩⇘n⇙. ∥uid∥⇘t i⇙" using latestAct_prop(1) by blast with assms(3) show "?cond (σ⇘uid⇙t ⟨uid → t⟩⇘⟨uid ← t⟩⇘n⇙⇙)" using latestActNxt by simp qed ultimately have "eval uid t t' ⟨uid ← t⟩⇘n⇙ (○⇩_{b}[?check]⇩_{b})" using impE[of uid t t' _ "[?cond]⇩_{b}" "○⇩_{b}[?check]⇩_{b}"] by simp moreover have "∃i>⟨uid → t⟩⇘⟨uid ← t⟩⇘n⇙⇙. ∥uid∥⇘t i⇙" proof - from assms have "⟨uid → t⟩⇘n⇙>⟨uid ← t⟩⇘n⇙" using latestActNxtAct by simp with assms(3) have "⟨uid → t⟩⇘n⇙>⟨uid → t⟩⇘⟨uid ← t⟩⇘n⇙⇙" using latestActNxt by simp moreover from ‹∃n'≥n. ∥uid∥⇘t n'⇙› have "∥uid∥⇘t ⟨uid → t⟩⇘n⇙⇙" using nxtActI by simp ultimately show ?thesis by auto qed moreover from assms have "⟨uid ← t⟩⇘n⇙ ≤ ⟨uid → t⟩⇘n⇙" using latestActNxtAct by (simp add: order.strict_implies_order) moreover from assms have "∃!i. ⟨uid ← t⟩⇘n⇙ ≤ i ∧ i < ⟨uid → t⟩⇘n⇙ ∧ ∥uid∥⇘t i⇙" using onlyone by simp ultimately have "eval uid t t' ⟨uid → t⟩⇘n⇙ [?check]⇩_{b}" using nxtEA1[of uid t "⟨uid ← t⟩⇘n⇙" t' "[?check]⇩_{b}" "⟨uid → t⟩⇘n⇙"] by simp moreover from ‹∃n'≥n. ∥uid∥⇘t n'⇙› have "∥uid∥⇘t ⟨uid → t⟩⇘n⇙⇙" using nxtActI by simp ultimately show ?thesis using baEANow[of uid t t' "⟨uid → t⟩⇘n⇙" ?check] by simp qed lemma bhv_dn_context: assumes "¬ honest uid" and "∥uid∥⇘t n⇙" and "∃n'<n. ∥uid∥⇘t n'⇙" shows "∃nid'. ∥nid'∥⇘t ⟨uid ← t⟩⇘n⇙⇙ ∧ (mining (σ⇘uid⇙t n) ∧ (∃b. prefix (bc (σ⇘uid⇙t n)) (bc (σ⇘nid'⇙t ⟨uid ← t⟩⇘n⇙) @ [b])) ∨ ¬ mining (σ⇘uid⇙t n) ∧ prefix (bc (σ⇘uid⇙t n)) (bc (σ⇘nid'⇙t ⟨uid ← t⟩⇘n⇙)))" proof - let ?bc="SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}" have bc_ex: "?bc ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∨ ?bc ∈ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}" proof - have "∃b. b∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}" by auto hence "?bc ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}" using someI_ex by simp thus ?thesis by auto qed from assms(2) have "∃n'≥n. ∥uid∥⇘t n'⇙" by auto moreover from assms(3) have "∃n'<n. ∥uid∥⇘t n'⇙" by auto ultimately have "¬ mining (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) ∧ prefix (bc (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙)) ?bc ∨ mining (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) = ?bc @ [b])" using bhv_dn[of uid n t] assms(1) by simp moreover from assms(2) have "⟨uid → t⟩⇘n⇙ = n" using nxtAct_active by simp ultimately have casmp: "¬ mining (σ⇘uid⇙t n) ∧ prefix (bc (σ⇘uid⇙t n)) ?bc ∨ mining (σ⇘uid⇙t n) ∧ (∃b. bc (σ⇘uid⇙t n) = ?bc @ [b])" by simp from bc_ex have "?bc ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∨ ?bc ∈ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}" . thus ?thesis proof assume "?bc ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)" moreover from ‹∃n'<n. ∥uid∥⇘t n'⇙› have "∥uid∥⇘t ⟨uid ← t⟩⇘n⇙⇙" using latestAct_prop(1) by simp ultimately obtain nid where "∥nid∥⇘t ⟨uid ← t⟩⇘n⇙⇙" and "bc (σ⇘nid⇙t ⟨uid ← t⟩⇘n⇙) = ?bc" using closed by blast with casmp have "¬ mining (σ⇘uid⇙t n) ∧ prefix (bc (σ⇘uid⇙t n)) (bc (σ⇘nid⇙t ⟨uid ← t⟩⇘n⇙)) ∨ mining (σ⇘uid⇙t n) ∧ (∃b. bc (σ⇘uid⇙t n) = (bc (σ⇘nid⇙t ⟨uid ← t⟩⇘n⇙)) @ [b])" by simp with ‹∥nid∥⇘t ⟨uid ← t⟩⇘n⇙⇙› show ?thesis by auto next assume "?bc ∈ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}" hence "?bc = bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)" by simp moreover from ‹∃n'. latestAct_cond uid t n n'› have "∥uid∥⇘t ⟨uid ← t⟩⇘n⇙⇙" using latestAct_prop(1) by simp ultimately show ?thesis using casmp by auto qed qed subsubsection "Maximal Honest Blockchains" abbreviation mbc_cond:: "trace ⇒ nat ⇒ 'nid ⇒ bool" where "mbc_cond t n nid ≡ nid∈actHn (t n) ∧ (∀nid'∈actHn (t n). length (bc (σ⇘nid'⇙(t n))) ≤ length (bc (σ⇘nid⇙(t n))))" lemma mbc_ex: fixes t n shows "∃x. mbc_cond t n x" proof - let ?ALL="{b. ∃nid∈actHn (t n). b = bc (σ⇘nid⇙(t n))}" have "MAX ?ALL ∈ ?ALL" proof (rule max_prop) from actHn have "actHn (t n) ≠ {}" using actHn_def by blast thus "?ALL≠{}" by auto from act have "finite (actHn (t n))" using actHn_def by simp thus "finite ?ALL" by simp qed then obtain nid where "nid ∈ actHn (t n) ∧ bc (σ⇘nid⇙(t n)) = MAX ?ALL" by auto moreover have "∀nid'∈actHn (t n). length (bc (σ⇘nid'⇙(t n))) ≤ length (MAX ?ALL)" proof fix nid assume "nid ∈ actHn (t n)" hence "bc (σ⇘nid⇙(t n)) ∈ ?ALL" by auto moreover have "∀b'∈?ALL. length b' ≤ length (MAX ?ALL)" proof (rule max_prop) from ‹bc (σ⇘nid⇙(t n)) ∈ ?ALL› show "?ALL≠{}" by auto from act have "finite (actHn (t n))" using actHn_def by simp thus "finite ?ALL" by simp qed ultimately show "length (bc (σ⇘nid⇙t n)) ≤ length (Blockchain.MAX {b. ∃nid∈actHn (t n). b = bc (σ⇘nid⇙t n)})" by simp qed ultimately show ?thesis by auto qed definition MBC:: "trace ⇒ nat ⇒ 'nid" where "MBC t n = (SOME b. mbc_cond t n b)" lemma mbc_prop[simp]: shows "mbc_cond t n (MBC t n)" using someI_ex[OF mbc_ex] MBC_def by simp subsubsection "Honest Proof of Work" text ‹ An important construction is the maximal proof of work available in the honest community. The construction was already introduces in the locale itself since it was used to express some of the locale assumptions. › abbreviation pow_cond:: "trace ⇒ nat ⇒ nat ⇒ bool" where "pow_cond t n n' ≡ ∀nid∈actHn (t n). length (bc (σ⇘nid⇙(t n))) ≤ n'" lemma pow_ex: fixes t n shows "pow_cond t n (length (bc (σ⇘MBC t n⇙(t n))))" and "∀x'. pow_cond t n x' ⟶ x'≥length (bc (σ⇘MBC t n⇙(t n)))" using mbc_prop by auto lemma pow_prop: "pow_cond t n (PoW t n)" proof - from pow_ex have "pow_cond t n (LEAST x. pow_cond t n x)" using LeastI_ex[of "pow_cond t n"] by blast thus ?thesis using PoW_def by simp qed lemma pow_eq: fixes n assumes "∃tid∈actHn (t n). length (bc (σ⇘tid⇙(t n))) = x" and "∀tid∈actHn (t n). length (bc (σ⇘tid⇙(t n))) ≤ x" shows "PoW t n = x" proof - have "(LEAST x. pow_cond t n x) = x" proof (rule Least_equality) from assms(2) show "∀nid∈actHn (t n). length (bc (σ⇘nid⇙t n)) ≤ x" by simp next fix y assume "∀nid∈actHn (t n). length (bc (σ⇘nid⇙t n)) ≤ y" thus "x ≤ y" using assms(1) by auto qed with PoW_def show ?thesis by simp qed lemma pow_mbc: shows "length (bc (σ⇘MBC t n⇙t n)) = PoW t n" by (metis mbc_prop pow_eq) lemma pow_less: fixes t n nid assumes "pow_cond t n x" shows "PoW t n ≤ x" proof - from pow_ex assms have "(LEAST x. pow_cond t n x) ≤ x" using Least_le[of "pow_cond t n"] by blast thus ?thesis using PoW_def by simp qed lemma pow_le_max: assumes "honest tid" and "∥tid∥⇘t n⇙" shows "PoW t n ≤ length (MAX (pin (σ⇘tid⇙t n)))" proof - from mbc_prop have "honest (MBC t n)" and "∥MBC t n∥⇘t n⇙" using actHn_def by auto hence "pout (σ⇘MBC t n⇙t n) = bc (σ⇘MBC t n⇙t n)" using forward globEANow[THEN baEANow[of "MBC t n" t t' n "λnd. pout nd = bc nd"]] by auto with assms ‹∥MBC t n∥⇘t n⇙› ‹honest (MBC t n)› have "bc (σ⇘MBC t n⇙t n) ∈ pin (σ⇘tid⇙t n)" using conn actHn_def by auto moreover from assms (2) have "finite (pin (σ⇘tid⇙t n))" using finite_input[of tid t n] by simp ultimately have "length (bc (σ⇘MBC t n⇙t n)) ≤ length (MAX (pin (σ⇘tid⇙t n)))" using max_prop(2) by auto with pow_mbc show ?thesis by simp qed lemma pow_ge_lgth: assumes "honest tid" and "∥tid∥⇘t n⇙" shows "length (bc (σ⇘tid⇙t n)) ≤ PoW t n" proof - from assms have "tid ∈ actHn (t n)" using actHn_def by simp thus ?thesis using pow_prop by simp qed lemma pow_le_lgth: assumes "honest tid" and "∥tid∥⇘t n⇙" and "¬(∃b∈pin (σ⇘tid⇙t n). length b > length (bc (σ⇘tid⇙t n)))" shows "length (bc (σ⇘tid⇙t n)) ≥ PoW t n" proof - from assms (3) have "∀b∈pin (σ⇘tid⇙t n). length b ≤ length (bc (σ⇘tid⇙t n))" by auto moreover from assms nempty_input[of tid t n] finite_input[of tid t n] have "MAX (pin (σ⇘tid⇙t n)) ∈ pin (σ⇘tid⇙t n)" using max_prop(1)[of "pin (σ⇘tid⇙t n)"] by simp ultimately have "length (MAX (pin (σ⇘tid⇙t n))) ≤ length (bc (σ⇘tid⇙t n))" by simp moreover from assms have "PoW t n ≤ length (MAX (pin (σ⇘tid⇙t n)))" using pow_le_max by simp ultimately show ?thesis by simp qed lemma pow_mono: shows "n'≥n ⟹ PoW t n' ≥ PoW t n" proof (induction n' rule: dec_induct) case base then show ?case by simp next case (step n') hence "PoW t n ≤ PoW t n'" by simp moreover have "PoW t (Suc n') ≥ PoW t n'" proof - from actHn obtain tid where "honest tid" and "∥tid∥⇘t n'⇙" and "∥tid∥⇘t (Suc n')⇙" by auto show ?thesis proof cases assume "∃b∈pin (σ⇘tid⇙t n'). length b > length (bc (σ⇘tid⇙t n'))" moreover from ‹∥tid∥⇘t (Suc n')⇙› have "⟨tid → t⟩⇘Suc n'⇙ = Suc n'" using nxtAct_active by simp moreover from ‹∥tid∥⇘t n'⇙› have "⟨tid ← t⟩⇘Suc n'⇙ = n'" using latestAct_prop(2) latestActless le_less_Suc_eq by blast moreover from ‹∥tid∥⇘t n'⇙› have "∃n''<Suc n'. ∥tid∥⇘t n''⇙" by blast moreover from ‹∥tid∥⇘t (Suc n')⇙› have "∃n''≥Suc n'. ∥tid∥⇘t n''⇙" by auto ultimately have "bc (σ⇘tid⇙t (Suc n')) = Blockchain.MAX (pin (σ⇘tid⇙t n')) ∨ (∃b. bc (σ⇘tid⇙t (Suc n')) = Blockchain.MAX (pin (σ⇘tid⇙t n')) @ b)" using ‹honest tid› bhv_hn_ex[of tid "Suc n'" t] by auto hence "length (bc (σ⇘tid⇙t (Suc n'))) ≥ length (Blockchain.MAX (pin (σ⇘tid⇙t n')))" by auto moreover from ‹honest tid› ‹∥tid∥⇘t n'⇙› have "length (Blockchain.MAX (pin (σ⇘tid⇙t n'))) ≥ PoW t n'" using pow_le_max by simp ultimately have "PoW t n' ≤ length (bc (σ⇘tid⇙t (Suc n')))" by simp moreover from ‹honest tid› ‹∥tid∥⇘t (Suc n')⇙› have "length (bc (σ⇘tid⇙t (Suc n'))) ≤ PoW t (Suc n')" using pow_ge_lgth by simp ultimately show ?thesis by simp next assume asmp: "¬(∃b∈pin (σ⇘tid⇙t n'). length b > length (bc (σ⇘tid⇙t n')))" moreover from ‹∥tid∥⇘t (Suc n')⇙› have "⟨tid → t⟩⇘Suc n'⇙ = Suc n'" using nxtAct_active by simp moreover from ‹∥tid∥⇘t n'⇙› have "⟨tid ← t⟩⇘Suc n'⇙ = n'" using latestAct_prop(2) latestActless le_less_Suc_eq by blast moreover from ‹∥tid∥⇘t n'⇙› have "∃n''<Suc n'. ∥tid∥⇘t n''⇙" by blast moreover from ‹∥tid∥⇘t (Suc n')⇙› have "∃n''≥Suc n'. ∥tid∥⇘t n''⇙" by auto ultimately have "bc (σ⇘tid⇙t (Suc n')) = bc (σ⇘tid⇙t n') ∨ (∃b. bc (σ⇘tid⇙t (Suc n')) = bc (σ⇘tid⇙t n') @ b)" using ‹honest tid› bhv_hn_in[of tid "Suc n'" t] by auto hence "length (bc (σ⇘tid⇙t (Suc n'))) ≥ length (bc (σ⇘tid⇙t n'))" by auto moreover from ‹honest tid› ‹∥tid∥⇘t n'⇙› asmp have "length (bc (σ⇘tid⇙t n')) ≥ PoW t n'" using pow_le_lgth by simp moreover from ‹honest tid› ‹∥tid∥⇘t (Suc n')⇙› have "length (bc (σ⇘tid⇙t (Suc n'))) ≤ PoW t (Suc n')" using pow_ge_lgth by simp ultimately show ?thesis by simp qed qed ultimately show ?case by auto qed lemma pow_equals: assumes "PoW t n = PoW t n'" and "n'≥n" and "n''≥n" and "n''≤n'" shows "PoW t n = PoW t n''" by (metis pow_mono assms(1) assms(3) assms(4) eq_iff) lemma pow_mining_suc: assumes "hmining t (Suc n)" shows "PoW t n < PoW t (Suc n)" proof - from assms obtain nid where "nid∈actHn (t (Suc n))" and "mining (σ⇘nid⇙(t (Suc n)))" using hmining_def by auto show ?thesis proof cases assume asmp: "(∃b∈pin (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙). length b > length (bc (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙)))" moreover from ‹nid∈actHn (t (Suc n))› have "honest nid" and "∥nid∥⇘t (Suc n)⇙" using actHn_def by auto moreover from ‹honest nid› ‹mining (σ⇘nid⇙(t (Suc n)))› ‹∥nid∥⇘t (Suc n)⇙› have "∥nid∥⇘t n⇙" using mine by simp hence "∃n'. latestAct_cond nid t (Suc n) n'" by auto ultimately have "¬ mining (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) ∧ bc (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) = MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙)) ∨ mining (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) ∧ (∃b. bc (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) = MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙)) @ [b])" using bhv_hn_ex[of nid "Suc n"] by auto moreover from ‹∥nid∥⇘t (Suc n)⇙› have "⟨nid → t⟩⇘Suc n⇙ = Suc n" using nxtAct_active by simp moreover have "⟨nid ← t⟩⇘Suc n⇙ = n" proof (rule latestActEq) from ‹∥nid∥⇘t n⇙› show "∥nid∥⇘t n⇙" by simp show "¬ (∃n''>n. n'' < Suc n ∧ ∥nid∥⇘t n⇙)" by simp show "n < Suc n" by simp qed hence "⟨nid ← t⟩⇘Suc n⇙ = n" using latestAct_def by simp ultimately have "¬ mining (σ⇘nid⇙t (Suc n)) ∧ bc (σ⇘nid⇙t (Suc n)) = MAX (pin (σ⇘nid⇙t n)) ∨ mining (σ⇘nid⇙t (Suc n)) ∧ (∃b. bc (σ⇘nid⇙t (Suc n)) = MAX (pin (σ⇘nid⇙t n)) @ [b])" by simp with ‹mining (σ⇘nid⇙(t (Suc n)))› have "∃b. bc (σ⇘nid⇙t (Suc n)) = MAX (pin (σ⇘nid⇙t n)) @ [b]" by auto moreover from ‹honest nid› ‹∥nid∥⇘t (Suc n)⇙› have "length (bc (σ⇘nid⇙t (Suc n))) ≤ PoW t (Suc n)" using pow_ge_lgth[of nid t "Suc n"] by simp ultimately have "length (MAX (pin (σ⇘nid⇙t n))) < PoW t (Suc n)" by auto moreover from ‹honest nid› ‹∥nid∥⇘t n⇙› have "length (MAX (pin (σ⇘nid⇙t n))) ≥ PoW t n" using pow_le_max by simp ultimately show ?thesis by simp next assume asmp: "¬ (∃b∈pin (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙). length b > length (bc (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙)))" moreover from ‹nid∈actHn (t (Suc n))› have "honest nid" and "∥nid∥⇘t (Suc n)⇙" using actHn_def by auto moreover from ‹honest nid› ‹mining (σ⇘nid⇙(t (Suc n)))› ‹∥nid∥⇘t (Suc n)⇙› have "∥nid∥⇘t n⇙" using mine by simp hence "∃n'. latestAct_cond nid t (Suc n) n'" by auto ultimately have "¬ mining (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) ∧ bc (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) = bc (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙) ∨ mining (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) ∧ (∃b. bc (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) = bc (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙) @ [b])" using bhv_hn_in[of nid "Suc n"] by auto moreover from ‹∥nid∥⇘t (Suc n)⇙› have "⟨nid → t⟩⇘Suc n⇙ = Suc n" using nxtAct_active by simp moreover have "⟨nid ← t⟩⇘Suc n⇙ = n" proof (rule latestActEq) from ‹∥nid∥⇘t n⇙› show "∥nid∥⇘t n⇙" by simp show "¬ (∃n''>n. n'' < Suc n ∧ ∥nid∥⇘t n⇙)" by simp show "n < Suc n" by simp qed hence "⟨nid ← t⟩⇘Suc n⇙ = n" using latestAct_def by simp ultimately have "¬ mining (σ⇘nid⇙t (Suc n)) ∧ bc (σ⇘nid⇙t (Suc n)) = bc (σ⇘nid⇙t n) ∨ mining (σ⇘nid⇙t (Suc n)) ∧ (∃b. bc (σ⇘nid⇙t (Suc n)) = bc (σ⇘nid⇙t n) @ [b])" by simp with ‹mining (σ⇘nid⇙(t (Suc n)))› have "∃b. bc (σ⇘nid⇙t (Suc n)) = bc (σ⇘nid⇙t n) @ [b]" by simp moreover from ‹⟨nid ← t⟩⇘Suc n⇙ = n› have "¬ (∃b∈pin (σ⇘nid⇙t n). length (bc (σ⇘nid⇙t n)) < length b)" using asmp by simp with ‹honest nid› ‹∥nid∥⇘t n⇙› have "length (bc (σ⇘nid⇙t n)) ≥ PoW t n" using pow_le_lgth[of nid t n] by simp moreover from ‹honest nid› ‹∥nid∥⇘t (Suc n)⇙› have "length (bc (σ⇘nid⇙t (Suc n))) ≤ PoW t (Suc n)" using pow_ge_lgth[of nid t "Suc n"] by simp ultimately show ?thesis by auto qed qed subsubsection "History" text ‹ In the following we introduce an operator which extracts the development of a blockchain up to a time point @{term n}. › abbreviation "his_prop t n nid n' nid' x ≡ (∃n. latestAct_cond nid' t n' n) ∧ ∥snd x∥⇘t (fst x)⇙ ∧ fst x = ⟨nid' ← t⟩⇘n'⇙ ∧ (prefix (bc (σ⇘nid'⇙(t n'))) (bc (σ⇘snd x⇙(t (fst x)))) ∨ (∃b. bc (σ⇘nid'⇙(t n')) = (bc (σ⇘snd x⇙(t (fst x)))) @ [b] ∧ mining (σ⇘nid'⇙(t n'))))" inductive_set his:: "trace ⇒ nat ⇒ 'nid ⇒ (nat × 'nid) set" for t::trace and n::nat and nid::'nid where "⟦∥nid∥⇘t n⇙⟧ ⟹ (n,nid) ∈ his t n nid" | "⟦(n',nid') ∈ his t n nid; ∃x. his_prop t n nid n' nid' x⟧ ⟹ (SOME x. his_prop t n nid n' nid' x) ∈ his t n nid" lemma his_act: assumes "(n',nid') ∈ his t n nid" shows "∥nid'∥⇘t n'⇙" using assms proof (rule his.cases) assume "(n', nid') = (n, nid)" and "∥nid∥⇘t n⇙" thus "∥nid'∥⇘t n'⇙" by simp next fix n'' nid'' assume asmp: "(n', nid') = (SOME x. his_prop t n nid n'' nid'' x)" and "(n'', nid'') ∈ his t n nid" and "∃x. his_prop t n nid n'' nid'' x" hence "his_prop t n nid n'' nid'' (SOME x. his_prop t n nid n'' nid'' x)" using someI_ex[of "λx. his_prop t n nid n'' nid'' x"] by auto hence "∥snd (SOME x. his_prop t n nid n'' nid'' x)∥⇘t (fst (SOME x. his_prop t n nid n'' nid'' x))⇙" by blast moreover from asmp have "fst (SOME x. his_prop t n nid n'' nid'' x) = fst (n', nid')" by simp moreover from asmp have "snd (SOME x. his_prop t n nid n'' nid'' x) = snd (n', nid')" by simp ultimately show ?thesis by simp qed text ‹ In addition we also introduce an operator to obtain the predecessor of a blockchains development. › definition "hisPred" where "hisPred t n nid n' ≡ (GREATEST n''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n')" lemma hisPrev_prop: assumes "∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid" shows "hisPred t n nid n' < n'" and "∃nid'. (hisPred t n nid n',nid')∈ his t n nid" proof - from assms obtain n'' where "∃nid'. (n'',nid')∈ his t n nid ∧ n''<n'" by auto moreover from ‹∃nid'. (n'',nid')∈ his t n nid ∧ n''<n'› have "∃i'≤n'. (∃nid'. (i', nid') ∈ his t n nid ∧ i' < n') ∧ (∀n'a. (∃nid'. (n'a, nid') ∈ his t n nid ∧ n'a < n') ⟶ n'a ≤ i')" using boundedGreatest[of "λn''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n'" n'' n'] by simp then obtain i' where "∀n'a. (∃nid'. (n'a, nid') ∈ his t n nid ∧ n'a < n') ⟶ n'a ≤ i'" by auto ultimately show "hisPred t n nid n' < n'" and "∃nid'. (hisPred t n nid n',nid')∈ his t n nid" using GreatestI_nat[of "λn''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n'" n'' i'] hisPred_def by auto qed lemma hisPrev_nex_less: assumes "∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid" shows "¬(∃x∈his t n nid. fst x < n' ∧ fst x>hisPred t n nid n')" proof (rule ccontr) assume "¬¬(∃x∈his t n nid. fst x < n' ∧ fst x>hisPred t n nid n')" then obtain n'' nid'' where "(n'',nid'')∈his t n nid" and "n''< n'" and "n''>hisPred t n nid n'" by auto moreover have "n''≤hisPred t n nid n'" proof - from ‹(n'',nid'')∈his t n nid› ‹n''< n'› have "∃nid'. (n'',nid')∈ his t n nid ∧ n''<n'" by auto moreover from ‹∃nid'. (n'',nid')∈ his t n nid ∧ n''<n'› have "∃i'≤n'. (∃nid'. (i', nid') ∈ his t n nid ∧ i' < n') ∧ (∀n'a. (∃nid'. (n'a, nid') ∈ his t n nid ∧ n'a < n') ⟶ n'a ≤ i')" using boundedGreatest[of "λn''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n'" n'' n'] by simp then obtain i' where "∀n'a. (∃nid'. (n'a, nid') ∈ his t n nid ∧ n'a < n') ⟶ n'a ≤ i'" by auto ultimately show ?thesis using Greatest_le_nat[of "λn''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n'" n'' i'] hisPred_def by simp qed ultimately show False by simp qed lemma his_le: assumes "x ∈ his t n nid" shows "fst x≤n" using assms proof (induction rule: his.induct) case 1 then show ?case by simp next case (2 n' nid') moreover have "fst (SOME x. his_prop t n nid n' nid' x) ≤ n'" proof - from "2.hyps" have "∃x. his_prop t n nid n' nid' x" by simp hence "his_prop t n nid n' nid' (SOME x. his_prop t n nid n' nid' x)" using someI_ex[of "λx. his_prop t n nid n' nid' x"] by auto hence "fst (SOME x. his_prop t n nid n' nid' x) = ⟨nid' ← t⟩⇘n'⇙" by force moreover from ‹his_prop t n nid n' nid' (SOME x. his_prop t n nid n' nid' x)› have "∃n. latestAct_cond nid' t n' n" by simp ultimately show ?thesis using latestAct_prop(2)[of n' nid' t] by simp qed ultimately show ?case by simp qed lemma his_determ_base: shows "(n, nid') ∈ his t n nid ⟹ nid'=nid" proof (rule his.cases) assume "(n, nid') = (n, nid)" thus ?thesis by simp next fix n' nid'a assume "(n, nid') ∈ his t n nid" and "(n, nid') = (SOME x. his_prop t n nid n' nid'a x)" and "(n', nid'a) ∈ his t n nid" and "∃x. his_prop t n nid n' nid'a x" hence "his_prop t n nid n' nid'a (SOME x. his_prop t n nid n' nid'a x)" using someI_ex[of "λx. his_prop t n nid n' nid'a x"] by auto hence "fst (SOME x. his_prop t n nid n' nid'a x) = ⟨nid'a ← t⟩⇘n'⇙" by force moreover from ‹his_prop t n nid n' nid'a (SOME x. his_prop t n nid n' nid'a x)› have "∃n. latestAct_cond nid'a t n' n" by simp ultimately have "fst (SOME x. his_prop t n nid n' nid'a x) < n'" using latestAct_prop(2)[of n' nid'a t] by simp with ‹(n, nid') = (SOME x. his_prop t n nid n' nid'a x)› have "fst (n, nid')<n'" by simp hence "n<n'" by simp moreover from ‹(n', nid'a) ∈ his t n nid› have "n'≤n" using his_le by auto ultimately show "nid' = nid" by simp qed lemma hisPrev_same: assumes "∃n'<n''. ∃nid'. (n',nid')∈ his t n nid" and "∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid" and "(n',nid')∈ his t n nid" and "(n'',nid'')∈ his t n nid" and "hisPred t n nid n'=hisPred t n nid n''" shows "n'=n''" proof (rule ccontr) assume "¬ n'=n''" hence "n'>n'' ∨ n'<n''" by auto thus False proof assume "n'<n''" hence "fst (n',nid')<n''" by simp moreover from assms(2) have "hisPred t n nid n'<n'" using hisPrev_prop(1) by simp with assms have "hisPred t n nid n''<n'" by simp hence "hisPred t n nid n''<fst (n',nid')" by simp ultimately show False using hisPrev_nex_less[of n'' t n nid] assms by auto next (*Symmetric*) assume "n'>n''" hence "fst (n'',nid')<n'" by simp moreover from assms(1) have "hisPred t n nid n''<n''" using hisPrev_prop(1) by simp with assms have "hisPred t n nid n'<n''" by simp hence "hisPred t n nid n'<fst (n'',nid')" by simp ultimately show False using hisPrev_nex_less[of n' t n nid] assms by auto qed qed lemma his_determ_ext: shows "n'≤n ⟹ (∃nid'. (n',nid')∈his t n nid) ⟹ (∃!nid'. (n',nid')∈his t n nid) ∧ ((∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid) ⟶ (∃x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x) ∧ (hisPred t n nid n', (SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x))" proof (induction n' rule: my_induct) case base then obtain nid' where "(n, nid') ∈ his t n nid" by auto hence "∃!nid'. (n, nid') ∈ his t n nid" proof fix nid'' assume "(n, nid'') ∈ his t n nid" with his_determ_base have "nid''=nid" by simp moreover from ‹(n, nid') ∈ his t n nid› have "nid'=nid" using his_determ_base by simp ultimately show "nid'' = nid'" by simp qed moreover have "(∃n''<n. ∃nid'. (n'',nid')∈ his t n nid) ⟶ (∃x. his_prop t n nid n (THE nid'. (n,nid')∈his t n nid) x) ∧ (hisPred t n nid n, (SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n (THE nid'. (n,nid')∈his t n nid) x)" proof assume "∃n''<n. ∃nid'. (n'',nid')∈ his t n nid" hence "∃nid'. (hisPred t n nid n, nid')∈ his t n nid" using hisPrev_prop(2) by simp hence "(hisPred t n nid n, (SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid)) ∈ his t n nid" using someI_ex[of "λnid'. (hisPred t n nid n, nid') ∈ his t n nid"] by simp thus "(∃x. his_prop t n nid n (THE nid'. (n,nid')∈his t n nid) x) ∧ (hisPred t n nid n, (SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n (THE nid'. (n,nid')∈his t n nid) x)" proof (rule his.cases) assume "(hisPred t n nid n, SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid) = (n, nid)" hence "hisPred t n nid n=n" by simp with ‹∃n''<n. ∃nid'. (n'',nid')∈ his t n nid› show ?thesis using hisPrev_prop(1)[of n t n nid] by force next fix n'' nid'' assume asmp: "(hisPred t n nid n, SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid) = (SOME x. his_prop t n nid n'' nid'' x)" and "(n'', nid'') ∈ his t n nid" and "∃x. his_prop t n nid n'' nid'' x" moreover have "n''=n" proof (rule antisym) show "n''≥n" proof (rule ccontr) assume "(¬n''≥n)" hence "n''<n" by simp moreover have "n''>hisPred t n nid n" proof - let ?x="λx. his_prop t n nid n'' nid'' x" from ‹∃x. his_prop t n nid n'' nid'' x› have "his_prop t n nid n'' nid'' (SOME x. ?x x)" using someI_ex[of ?x] by auto hence "n''>fst (SOME x. ?x x)" using latestAct_prop(2)[of n'' nid'' t] by force moreover from asmp have "fst (hisPred t n nid n, SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid) = fst (SOME x. ?x x)" by simp ultimately show ?thesis by simp qed moreover from ‹∃n''<n. ∃nid'. (n'',nid')∈ his t n nid› have "¬(∃x∈his t n nid. fst x < n ∧ fst x > hisPred t n nid n)" using hisPrev_nex_less by simp ultimately show False using ‹(n'', nid'') ∈ his t n nid› by auto qed next from ‹(n'', nid'') ∈ his t n nid› show "n'' ≤ n" using his_le by auto qed ultimately have "(hisPred t n nid n, SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid) = (SOME x. his_prop t n nid n nid'' x)" by simp moreover from ‹n''=n› ‹(n'', nid'') ∈ his t n nid› have "(n, nid'') ∈ his t n nid" by simp with ‹∃!nid'. (n,nid') ∈ his t n nid› have "nid''=(THE nid'. (n,nid')∈his t n nid)" using the1_equality[of "λnid'. (n, nid') ∈ his t n nid"] by simp moreover from ‹∃x. his_prop t n nid n'' nid'' x› ‹n''=n› ‹nid''=(THE nid'. (n,nid')∈his t n nid)› have "∃x. his_prop t n nid n (THE nid'. (n,nid')∈his t n nid) x" by simp ultimately show ?thesis by simp qed qed ultimately show ?case by simp next case (step n') then obtain nid' where "(n', nid') ∈ his t n nid" by auto hence "∃!nid'. (n', nid') ∈ his t n nid" proof (rule his.cases) assume "(n', nid') = (n, nid)" hence "n'=n" by simp with step.hyps show ?thesis by simp next fix n'''' nid'''' assume "(n'''', nid'''') ∈ his t n nid" and n'nid': "(n', nid') = (SOME x. his_prop t n nid n'''' nid'''' x)" and "(n'''', nid'''') ∈ his t n nid" and "∃x. his_prop t n nid n'''' nid'''' x" from ‹(n', nid') ∈ his t n nid› show ?thesis proof fix nid'' assume "(n', nid'') ∈ his t n nid" thus "nid'' = nid'" proof (rule his.cases) assume "(n', nid'') = (n, nid)" hence "n'=n" by simp with step.hyps show ?thesis by simp next fix n''' nid''' assume "(n''', nid''') ∈ his t n nid" and n'nid'': "(n', nid'') = (SOME x. his_prop t n nid n''' nid''' x)" and "(n''', nid''') ∈ his t n nid" and "∃x. his_prop t n nid n''' nid''' x" moreover have "n'''=n''''" proof - have "hisPred t n nid n''' = n'" proof - from n'nid'' ‹∃x. his_prop t n nid n''' nid''' x› have "his_prop t n nid n''' nid''' (n',nid'')" using someI_ex[of "λx. his_prop t n nid n''' nid''' x"] by auto hence "n'''>n'" using latestAct_prop(2) by simp moreover from ‹(n''', nid''') ∈ his t n nid› have "n'''≤ n" using his_le by auto moreover from ‹(n''', nid''') ∈ his t n nid› have "∃nid'. (n''', nid') ∈ his t n nid" by auto ultimately have "(∃n'<n'''. ∃nid'. (n',nid')∈ his t n nid) ⟶ (∃!nid'. (n''',nid') ∈ his t n nid) ∧ (hisPred t n nid n''', (SOME nid'. (hisPred t n nid n''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n''' (THE nid'. (n''',nid')∈his t n nid) x)" using step.IH by auto with ‹n'''>n'› ‹(n', nid') ∈ his t n nid› have "∃!nid'. (n''',nid') ∈ his t n nid" and "(hisPred t n nid n''', (SOME nid'. (hisPred t n nid n''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n''' (THE nid'. (n''',nid')∈his t n nid) x)" by auto moreover from ‹∃!nid'. (n''',nid') ∈ his t n nid› ‹(n''', nid''') ∈ his t n nid› have "nid'''=(THE nid'. (n''',nid')∈his t n nid)" using the1_equality[of "λnid'. (n''', nid') ∈ his t n nid"] by simp ultimately have "(hisPred t n nid n''', (SOME nid'. (hisPred t n nid n''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n''' nid''' x)" by simp with n'nid'' have "(n', nid'') = (hisPred t n nid n''', (SOME nid'. (hisPred t n nid n''', nid') ∈ his t n nid))" by simp thus ?thesis by simp qed moreover have "hisPred t n nid n'''' = n'" (*Symmetric*) proof - from n'nid' ‹∃x. his_prop t n nid n'''' nid'''' x› have "his_prop t n nid n'''' nid'''' (n',nid')" using someI_ex[of "λx. his_prop t n nid n'''' nid'''' x"] by auto hence "n''''>n'" using latestAct_prop(2) by simp moreover from ‹(n'''', nid'''') ∈ his t n nid› have "n''''≤ n" using his_le by auto moreover from ‹(n'''', nid'''') ∈ his t n nid› have "∃nid'. (n'''', nid') ∈ his t n nid" by auto ultimately have "(∃n'<n''''. ∃nid'. (n',nid')∈ his t n nid) ⟶ (∃!nid'. (n'''',nid') ∈ his t n nid) ∧ (hisPred t n nid n'''', (SOME nid'. (hisPred t n nid n'''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n'''' (THE nid'. (n'''',nid')∈his t n nid) x)" using step.IH by auto with ‹n''''>n'› ‹(n', nid') ∈ his t n nid› have "∃!nid'. (n'''',nid') ∈ his t n nid" and "(hisPred t n nid n'''', (SOME nid'. (hisPred t n nid n'''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n'''' (THE nid'. (n'''',nid')∈his t n nid) x)" by auto moreover from ‹∃!nid'. (n'''',nid') ∈ his t n nid› ‹(n'''', nid'''') ∈ his t n nid› have "nid''''=(THE nid'. (n'''',nid')∈his t n nid)" using the1_equality[of "λnid'. (n'''', nid') ∈ his t n nid"] by simp ultimately have "(hisPred t n nid n'''', (SOME nid'. (hisPred t n nid n'''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n'''' nid'''' x)" by simp with n'nid' have "(n', nid') = (hisPred t n nid n'''', (SOME nid'. (hisPred t n nid n'''', nid') ∈ his t n nid))" by simp thus ?thesis by simp qed ultimately have "hisPred t n nid n'''=hisPred t n nid n''''" .. moreover have "∃n'<n'''. ∃nid'. (n',nid')∈ his t n nid" proof - from n'nid'' ‹∃x. his_prop t n nid n''' nid''' x› have "his_prop t n nid n''' nid''' (n',nid'')" using someI_ex[of "λx. his_prop t n nid n''' nid''' x"] by auto hence "n'''>n'" using latestAct_prop(2) by simp with ‹(n', nid') ∈ his t n nid› show ?thesis by auto qed moreover have "∃n'<n''''. ∃nid'. (n',nid')∈ his t n nid" proof - from n'nid' ‹∃x. his_prop t n nid n'''' nid'''' x› have "his_prop t n nid n'''' nid'''' (n',nid')" using someI_ex[of "λx. his_prop t n nid n'''' nid'''' x"] by auto hence "n''''>n'" using latestAct_prop(2) by simp with ‹(n', nid') ∈ his t n nid› show ?thesis by auto qed ultimately show ?thesis using hisPrev_same ‹(n''', nid''') ∈ his t n nid› ‹(n'''', nid'''') ∈ his t n nid› by blast qed moreover have "nid'''=nid''''" proof - from n'nid'' ‹∃x. his_prop t n nid n''' nid''' x› have "his_prop t n nid n''' nid''' (n',nid'')" using someI_ex[of "λx. his_prop t n nid n''' nid''' x"] by auto hence "n'''>n'" using latestAct_prop(2) by simp moreover from ‹(n''', nid''') ∈ his t n nid› have "n'''≤ n" using his_le by auto moreover from ‹(n''', nid''') ∈ his t n nid› have "∃nid'. (n''', nid') ∈ his t n nid" by auto ultimately have "∃!nid'. (n''', nid') ∈ his t n nid" using step.IH by auto with ‹(n''', nid''') ∈ his t n nid› ‹(n'''', nid'''') ∈ his t n nid› ‹n'''=n''''› show ?thesis by auto qed ultimately have "(n', nid') = (n', nid'')" using n'nid' by simp thus "nid'' = nid'" by simp qed qed qed moreover have "(∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid) ⟶ (∃x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x) ∧ (hisPred t n nid n', (SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x)" proof assume "∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid" hence "∃nid'. (hisPred t n nid n', nid')∈ his t n nid" using hisPrev_prop(2) by simp hence "(hisPred t n nid n', (SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid)) ∈ his t n nid" using someI_ex[of "λnid'. (hisPred t n nid n', nid') ∈ his t n nid"] by simp thus "(∃x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x) ∧ (hisPred t n nid n', (SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x)" proof (rule his.cases) assume "(hisPred t n nid n', SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid) = (n, nid)" hence "hisPred t n nid n'=n" by simp moreover from ‹∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid› have "hisPred t n nid n'<n'" using hisPrev_prop(1)[of n'] by force ultimately show ?thesis using step.hyps by simp next fix n'' nid'' assume asmp: "(hisPred t n nid n', SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid) = (SOME x. his_prop t n nid n'' nid'' x)" and "(n'', nid'') ∈ his t n nid" and "∃x. his_prop t n nid n'' nid'' x" moreover have "n''=n'" proof (rule antisym) show "n''≥n'" proof (rule ccontr) assume "(¬n''≥n')" hence "n''<n'" by simp moreover have "n''>hisPred t n nid n'" proof - let ?x="λx. his_prop t n nid n'' nid'' x" from ‹∃x. his_prop t n nid n'' nid'' x› have "his_prop t n nid n'' nid'' (SOME x. ?x x)" using someI_ex[of ?x] by auto hence "n''>fst (SOME x. ?x x)" using latestAct_prop(2)[of n'' nid'' t] by force moreover from asmp have "fst (hisPred t n nid n', SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid) = fst (SOME x. ?x x)" by simp ultimately show ?thesis by simp qed moreover from ‹∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid› have "¬(∃x∈his t n nid. fst x < n' ∧ fst x > hisPred t n nid n')" using hisPrev_nex_less by simp ultimately show False using ‹