Theory Proofchain

section ‹Proof chains›

theory Proofchain imports
  JHelper  
begin

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"                         ("⦃ _ ⦄")
| cCons "'a" "'c" "('a,'c) chain"   ("⦃ _ ⦄ ⋅ _ ⋅ _" [0,0,0] 60) 

text ‹For example, @{term "⦃ a ⦄ ⋅ proof ⋅ ⦃ chain ⦄ ⋅ might ⋅ ⦃ look ⦄ ⋅ 
  like ⋅ ⦃ this ⦄"}.›

subsection ‹Projections›

text ‹Project first assertion.›
fun
  pre :: "('a,'c) chain ⇒ 'a"
where
  "pre ⦃ P ⦄ = P"
| "pre (⦃ P ⦄ ⋅ _ ⋅ _) = P"

text ‹Project final assertion.›
fun 
  post :: "('a,'c) chain ⇒ 'a"
where
  "post ⦃ P ⦄  = P"
| "post (⦃ _ ⦄ ⋅ _ ⋅ Π) = post Π"

text ‹Project list of commands.›
fun
  comlist :: "('a,'c) chain ⇒ 'c list"
where
  "comlist ⦃ _ ⦄ = []"
| "comlist (⦃ _ ⦄ ⋅ x ⋅ Π) = x # (comlist Π)" 


subsection ‹Chain length›

fun
  chainlen :: "('a,'c) chain ⇒ nat"
where
  "chainlen ⦃ _ ⦄ = 0"
| "chainlen (⦃ _ ⦄ ⋅ _ ⋅ Π) = 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"}. 
›
fun
  nthtriple :: "('a,'c) chain ⇒ nat ⇒ ('a * 'c * 'a)"
where
  "nthtriple (⦃ P ⦄ ⋅ x ⋅ Π) 0 = (P, x, pre Π)"
| "nthtriple (⦃ P ⦄ ⋅ 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)
done

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.› 
fun
  chain_all :: "(('a × 'c × 'a) ⇒ bool) ⇒ ('a,'c) chain ⇒ bool"
where
  "chain_all φ ⦃ σ ⦄ = True"
| "chain_all φ (⦃ σ ⦄ ⋅ 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)
  done
qed
  
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: "Π = ⦃ σ ⦄ ⋅ x ⋅ Π'"
    by (metis chain.exhaust chainlen.simps(1) less_nat_zero_code)
    show ?case 
    by (insert "0.prems"(1), unfold Π_def, auto)
  next
    case (Suc i)
    then obtain σ x Π' where Π_def: "Π = ⦃ σ ⦄ ⋅ 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)
    done
  qed
next
  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 (⦃ σ ⦄ ⋅ x ⋅ Π') 0)", simp)
    apply (intro cCons.prems, simp)
    apply (intro cCons.hyps)
    proof -
      fix i
      assume "i < chainlen Π'"
      hence "Suc i < chainlen (⦃ σ ⦄ ⋅ x ⋅ Π')" by auto
      from cCons.prems[OF this] show "φ (nthtriple Π' i)" by auto
    qed
  qed(auto)
qed

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.›
fun
  chainmap :: "('a ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒ ('a,'c) chain ⇒ ('b,'d) chain"
where
  "chainmap f g ⦃ P ⦄ = ⦃ f P ⦄"
| "chainmap f g (⦃ P ⦄ ⋅ x ⋅ Π) = ⦃ f P ⦄ ⋅ 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›

fun
  cSnoc :: "('a,'c) chain ⇒ 'c ⇒ 'a ⇒ ('a,'c) chain"
where
  "cSnoc ⦃ σ ⦄ y τ = ⦃ σ ⦄ ⋅ y ⋅ ⦃ τ ⦄"
| "cSnoc (⦃ σ ⦄ ⋅ x ⋅ Π) y τ = ⦃ σ ⦄ ⋅ 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)



end