Theory Proofchain

Up to index of Isabelle/HOL/ribbonproofs

theory Proofchain
imports JHelper
header {* Proof chains *}

theory Proofchain imports

text {* An (@{typ 'a}, @{typ 'c}) chain is a sequence of alternating
@{typ 'a}'s and @{typ 'c}'s, beginning and ending with an @{typ 'a}. Usually
@{typ 'a} represents some sort of assertion, and @{typ 'c} represents some
sort of command. Proof chains are useful for stating the SMain proof rule,
and for conducting the proof of soundness. *}

datatype ('a,'c) chain =
cNil "'a" ("\<lbrace> _ \<rbrace>")
| cCons "'a" "'c" "('a,'c) chain" ("\<lbrace> _ \<rbrace> · _ · _" [0,0,0] 60)

text {* For example, @{term "\<lbrace> a \<rbrace> · proof · \<lbrace> chain \<rbrace> · might · \<lbrace> look \<rbrace> ·
like · \<lbrace> this \<rbrace>"}. *}

subsection {* Projections *}

text {* Project first assertion. *}
pre :: "('a,'c) chain => 'a"
"pre \<lbrace> P \<rbrace> = P"
| "pre (\<lbrace> P \<rbrace> · _ · _) = P"

text {* Project final assertion. *}
post :: "('a,'c) chain => 'a"
"post \<lbrace> P \<rbrace> = P"
| "post (\<lbrace> _ \<rbrace> · _ · Π) = post Π"

text {* Project list of commands. *}
comlist :: "('a,'c) chain => 'c list"
"comlist \<lbrace> _ \<rbrace> = []"
| "comlist (\<lbrace> _ \<rbrace> · x · Π) = x # (comlist Π)"

subsection {* Chain length *}

chainlen :: "('a,'c) chain => nat"
"chainlen \<lbrace> _ \<rbrace> = 0"
| "chainlen (\<lbrace> _ \<rbrace> · _ · Π) = 1 + (chainlen Π)"

lemma len_comlist_chainlen:
"length (comlist Π) = chainlen Π"
by (induct Π, auto)

subsection {* Extracting triples from chains *}

text {* @{term "nthtriple Π n"} extracts the @{term n}th triple of @{term Π},
counting from 0. The function is well-defined when @{term "chainlen Π > n"}.

nthtriple :: "('a,'c) chain => nat => ('a * 'c * 'a)"
"nthtriple (\<lbrace> P \<rbrace> · x · Π) 0 = (P, x, pre Π)"
| "nthtriple (\<lbrace> P \<rbrace> · x · Π) (Suc n) = nthtriple Π n"

text {* The list of middle components of @{term Π}'s triples is the list of
@{term Π}'s commands. *}

lemma snds_of_triples_form_comlist:
fixes Π i
shows "i < chainlen Π ==> snd3 (nthtriple Π i) = (comlist Π)!i"
apply (induct Π arbitrary: i)
apply simp
apply (case_tac i)
apply (auto simp add: snd3_def)

subsection {* Evaluating a predicate on each triple of a chain *}

text {* @{term "chain_all φ"} holds of @{term Π} iff @{term φ} holds for each
of @{term Π}'s individual triples. *}

chain_all :: "(('a × 'c × 'a) => bool) => ('a,'c) chain => bool"
"chain_all φ \<lbrace> σ \<rbrace> = True"
| "chain_all φ (\<lbrace> σ \<rbrace> · x · Π) = (φ (σ,x,pre Π) ∧ chain_all φ Π)"

lemma chain_all_mono [mono]:
"x ≤ y ==> chain_all x ≤ chain_all y"
proof (intro le_funI le_boolI)
fix f g :: "('a × 'b × 'a) => bool"
fix Π :: "('a, 'b) chain"
assume "f ≤ g"
assume "chain_all f Π"
thus "chain_all g Π"
apply (induct Π)
apply simp
apply (metis `f ≤ g` chain_all.simps(2) predicate1D)

lemma chain_all_nthtriple:
"(chain_all φ Π) = (∀i < chainlen Π. φ (nthtriple Π i))"
proof (intro iffI allI impI)
fix i
assume "chain_all φ Π" and "i < chainlen Π"
thus "φ (nthtriple Π i)"
proof (induct i arbitrary: Π)
case 0
then obtain σ x Π' where Π_def: "Π = \<lbrace> σ \<rbrace> · x · Π'"
by (metis chain.exhaust chainlen.simps(1) less_nat_zero_code)
show ?case
by (insert "0.prems"(1), unfold Π_def, auto)
case (Suc i)
then obtain σ x Π' where Π_def: "Π = \<lbrace> σ \<rbrace> · x · Π'"
by (metis chain.exhaust chainlen.simps(1) less_nat_zero_code)
show ?case
apply (unfold Π_def nthtriple.simps)
apply (intro Suc.hyps, insert Suc.prems, auto simp add: Π_def)
assume "∀i<chainlen Π. φ (nthtriple Π i)"
hence "!!i. i < chainlen Π ==> φ (nthtriple Π i)" by auto
thus "chain_all φ Π"
proof (induct Π)
case (cCons σ x Π')
show ?case
apply (simp, intro conjI)
apply (subgoal_tac "φ (nthtriple (\<lbrace> σ \<rbrace> · x · Π') 0)", simp)
apply (intro cCons.prems, simp)
apply (intro cCons.hyps)
proof -
fix i
assume "i < chainlen Π'"
hence "Suc i < chainlen (\<lbrace> σ \<rbrace> · x · Π')" by auto
from cCons.prems[OF this] show "φ (nthtriple Π' i)" by auto

subsection {* A map function for proof chains *}

text {* @{term "chainmap f g Π"} maps @{term f} over each of @{term Π}'s
assertions, and @{term g} over each of @{term Π}'s commands. *}

chainmap :: "('a => 'b) => ('c => 'd) => ('a,'c) chain => ('b,'d) chain"
"chainmap f g \<lbrace> P \<rbrace> = \<lbrace> f P \<rbrace>"
| "chainmap f g (\<lbrace> P \<rbrace> · x · Π) = \<lbrace> f P \<rbrace> · g x · chainmap f g Π"

text {* Mapping over a chain preserves its length. *}
lemma chainmap_preserves_length:
"chainlen (chainmap f g Π) = chainlen Π"
by (induct Π, auto)

lemma pre_chainmap:
"pre (chainmap f g Π) = f (pre Π)"
by (induct Π, auto)

lemma post_chainmap:
"post (chainmap f g Π) = f (post Π)"
by (induct Π, auto)

lemma nthtriple_chainmap:
assumes "i < chainlen Π"
shows "nthtriple (chainmap f g Π) i
= (λt. (f (fst3 t), g (snd3 t), f (thd3 t))) (nthtriple Π i)"

using assms
proof (induct Π arbitrary: i)
case cCons
thus ?case
by (induct i, auto simp add: pre_chainmap fst3_def snd3_def thd3_def)
qed (auto)

subsection {* Extending a chain on its right-hand side *}

cSnoc :: "('a,'c) chain => 'c => 'a => ('a,'c) chain"
"cSnoc \<lbrace> σ \<rbrace> y τ = \<lbrace> σ \<rbrace> · y · \<lbrace> τ \<rbrace>"
| "cSnoc (\<lbrace> σ \<rbrace> · x · Π) y τ = \<lbrace> σ \<rbrace> · x · (cSnoc Π y τ)"

lemma len_snoc:
fixes Π x P
shows "chainlen (cSnoc Π x P) = 1 + (chainlen Π)"
by (induct Π, auto)

lemma pre_snoc:
"pre (cSnoc Π x P) = pre Π"
by (induct Π, auto)

lemma post_snoc:
"post (cSnoc Π x P) = P"
by (induct Π, auto)

lemma comlist_snoc:
"comlist (cSnoc Π x p) = comlist Π @ [x]"
by (induct Π, auto)