Theory Ribbons_Interfaces

section ‹Ribbon proof interfaces›

theory Ribbons_Interfaces imports
  Ribbons_Basic
  Proofchain
  "HOL-Library.FSet"
begin

text ‹Interfaces are the top and bottom boundaries through which diagrams 
  can be connected into a surrounding context. For instance, when composing two 
  diagrams vertically, the bottom interface of the upper diagram must match the 
  top interface of the lower diagram. 

  We define a datatype of concrete interfaces. We then quotient by the 
  associativity, commutativity and unity properties of our 
  horizontal-composition operator.›

subsection ‹Syntax of interfaces›

datatype conc_interface =
  Ribbon_conc "assertion"
| HComp_int_conc "conc_interface" "conc_interface" (infix ‹⊗⇩c› 50)
| Emp_int_conc (‹ε⇩c›)
| Exists_int_conc "string" "conc_interface"

text ‹We define an equivalence on interfaces. The first three rules make this 
  an equivalence relation. The next three make it a congruence. The next two 
  identify interfaces up to associativity and commutativity of @{term "(⊗⇩c)"} 
  The final two make @{term "ε⇩c"} the left and right unit of @{term "(⊗⇩c)"}. 
›
inductive
  equiv_int :: "conc_interface ⇒ conc_interface ⇒ bool" (infix ‹≃› 45)
where
  refl: "P ≃ P"
| sym: "P ≃ Q ⟹ Q ≃ P"
| trans: "⟦P ≃ Q; Q ≃ R⟧ ⟹ P ≃ R"
| cong_hcomp1: "P ≃ Q ⟹ P' ⊗⇩c P ≃ P' ⊗⇩c Q"
| cong_hcomp2: "P ≃ Q ⟹ P ⊗⇩c P' ≃ Q ⊗⇩c P'"
| cong_exists: "P ≃ Q ⟹ Exists_int_conc x P ≃ Exists_int_conc x Q"
| hcomp_conc_assoc: "P ⊗⇩c (Q ⊗⇩c R) ≃ (P ⊗⇩c Q) ⊗⇩c R"
| hcomp_conc_comm: "P ⊗⇩c Q ≃ Q ⊗⇩c P"
| hcomp_conc_unit1: "ε⇩c ⊗⇩c P ≃ P"
| hcomp_conc_unit2: "P ⊗⇩c ε⇩c ≃ P"

lemma equiv_int_cong_hcomp: 
  "⟦ P ≃ Q ; P' ≃ Q' ⟧ ⟹ P ⊗⇩c P' ≃ Q ⊗⇩c Q'"
by (metis cong_hcomp1 cong_hcomp2 equiv_int.trans)

quotient_type interface = "conc_interface" / "equiv_int"
apply (intro equivpI)
apply (intro reflpI, simp add: equiv_int.refl)
apply (intro sympI, simp add: equiv_int.sym)
apply (intro transpI, elim equiv_int.trans, simp add: equiv_int.refl)
done

lift_definition 
  Ribbon :: "assertion ⇒ interface" 
is "Ribbon_conc" .


lift_definition
  Emp_int :: "interface" (‹ε›)
is "ε⇩c" .

lift_definition
  Exists_int :: "string ⇒ interface ⇒ interface"
is "Exists_int_conc"
by (rule equiv_int.cong_exists)

lift_definition
  HComp_int :: "interface ⇒ interface ⇒ interface" (infix ‹⊗› 50)
is "HComp_int_conc" by (rule equiv_int_cong_hcomp)

lemma hcomp_comm: 
  "(P ⊗ Q) = (Q ⊗ P)"
by (rule hcomp_conc_comm[Transfer.transferred])

lemma hcomp_assoc:
  "(P ⊗ (Q ⊗ R)) = ((P ⊗ Q) ⊗ R)"
by (rule hcomp_conc_assoc[Transfer.transferred])

lemma emp_hcomp:
  "ε ⊗ P = P"
by (rule hcomp_conc_unit1[Transfer.transferred])

lemma hcomp_emp:
  "P ⊗ ε = P"
by (rule hcomp_conc_unit2[Transfer.transferred])

lemma comp_fun_commute_hcomp:
  "comp_fun_commute (⊗)"
by standard (simp add: hcomp_assoc fun_eq_iff, metis hcomp_comm)

subsection ‹An iterated horizontal-composition operator›

definition iter_hcomp :: "('a fset) ⇒ ('a ⇒ interface) ⇒ interface"
where
  "iter_hcomp X f ≡ ffold ((⊗) ∘ f) ε X"

syntax "iter_hcomp_syntax" :: 
  "'a ⇒ ('a fset) ⇒ ('a ⇒ interface) ⇒ interface"
      (‹(⨂_|∈|_. _)› [0,0,10] 10)
syntax_consts "iter_hcomp_syntax" == iter_hcomp  
translations "⨂x|∈|M. e" == "CONST iter_hcomp M (λx. e)"

term "⨂P|∈|Ps. f P" ― ‹this is eta-expanded, so prints in expanded form›
term "⨂P|∈|Ps. f" ― ‹this isn't eta-expanded, so prints as written›

lemma iter_hcomp_cong:
  assumes "∀v ∈ fset vs. φ v = φ' v"
  shows "(⨂v|∈|vs. φ v) = (⨂v|∈|vs. φ' v)"
using assms unfolding iter_hcomp_def  
by (auto simp add: comp_fun_commute.comp_comp_fun_commute comp_fun_commute_hcomp 
  intro: ffold_cong)

lemma iter_hcomp_empty:
  shows "(⨂x |∈| {||}. p x) = ε"
  by (simp add: comp_fun_commute.comp_comp_fun_commute comp_fun_commute.ffold_empty
      comp_fun_commute_hcomp iter_hcomp_def)

lemma iter_hcomp_insert:
  assumes "v |∉| ws"
  shows "(⨂x |∈| finsert v ws. p x) = (p v ⊗ (⨂x |∈| ws. p x))"
proof -
  interpret comp_fun_commute "((⊗) ∘ p)"
  by (metis comp_fun_commute.comp_comp_fun_commute comp_fun_commute_hcomp)
  from assms show ?thesis unfolding iter_hcomp_def by auto
qed

lemma iter_hcomp_union:
  assumes "vs |∩| ws = {||}"
  shows "(⨂x |∈| vs |∪| ws. p x) = ((⨂x |∈| vs. p x) ⊗ (⨂x |∈| ws. p x))"
using assms
by (induct vs) (auto simp add: emp_hcomp iter_hcomp_empty iter_hcomp_insert hcomp_assoc)


subsection ‹Semantics of interfaces›

text ‹The semantics of an interface is an assertion.›
fun
  conc_asn :: "conc_interface ⇒ assertion"
where
  "conc_asn (Ribbon_conc p) = p"
| "conc_asn (P ⊗⇩c Q) = (conc_asn P) ⋆ (conc_asn Q)"
| "conc_asn (ε⇩c) = Emp"
| "conc_asn (Exists_int_conc x P) = Exists x (conc_asn P)"

lift_definition 
  asn :: "interface ⇒ assertion"
is "conc_asn"
by (induct_tac rule:equiv_int.induct) (auto simp add: star_assoc star_comm star_rot emp_star)

lemma asn_simps [simp]:
  "asn (Ribbon p) = p"
  "asn (P ⊗ Q) = (asn P) ⋆ (asn Q)"
  "asn ε = Emp"
  "asn (Exists_int x P) = Exists x (asn P)"
by (transfer, simp)+

subsection ‹Program variables mentioned in an interface.›

fun
  rd_conc_int :: "conc_interface ⇒ string set"
where
  "rd_conc_int (Ribbon_conc p) = rd_ass p"
| "rd_conc_int (P ⊗⇩c Q) = rd_conc_int P ∪ rd_conc_int Q"
| "rd_conc_int (ε⇩c) = {}"
| "rd_conc_int (Exists_int_conc x P) = rd_conc_int P"

lift_definition
  rd_int :: "interface ⇒ string set"
is "rd_conc_int"
by (induct_tac rule: equiv_int.induct) auto
  
text ‹The program variables read by an interface are the same as those read 
  by its corresponding assertion.›

lemma rd_int_is_rd_ass:
  "rd_ass (asn P) = rd_int P"
by (transfer, induct_tac P, auto simp add: rd_star rd_exists rd_emp) 

text ‹Here is an iterated version of the Hoare logic sequencing rule.›

lemma seq_fold: 
  "⋀Π. ⟦ length cs = chainlen Π ; p1 = asn (pre Π) ; p2 = asn (post Π) ; 
  ⋀i. i < chainlen Π ⟹ prov_triple 
  (asn (fst3 (nthtriple Π i)), cs ! i, asn (thd3 (nthtriple Π i))) ⟧
  ⟹ prov_triple (p1, foldr (;;) cs Skip, p2)"
proof (induct cs arbitrary: p1 p2)
  case Nil
  thus ?case 
  by (cases Π, auto simp add: prov_triple.skip)
next
  case (Cons c cs)
  obtain p x Π' where Π_def: "Π = ⦃ p ⦄ ⋅ x ⋅ Π'" 
  by (metis Cons.prems(1) chain.exhaust chainlen.simps(1) impossible_Cons le0)
  show ?case 
  apply (unfold foldr_Cons o_def)
  apply (rule prov_triple.seq[where q = "asn (pre Π')"])
  apply (unfold Cons.prems(2) Cons.prems(3) Π_def pre.simps post.simps)
  apply (subst nth_Cons_0[of c cs, symmetric])
  apply (subst fst3_simp[of p x "pre Π'", symmetric])
  apply (subst(2) thd3_simp[of p x "pre Π'", symmetric])
  apply (subst(1 2) nthtriple.simps(1)[of p x "Π'", symmetric])
  apply (fold Π_def, intro Cons.prems(4), simp add: Π_def)
  apply (intro Cons.hyps, insert Π_def Cons.prems(1), auto)
  apply (fold nth_Cons_Suc[of c cs] nthtriple.simps(2)[of p x "Π'"])
  apply (fold Π_def, intro Cons.prems(4), simp add: Π_def)
  done
qed

end