Theory Ribbons_Interfaces

header {* Ribbon proof interfaces *}

theory Ribbons_Interfaces imports
  Ribbons_Basic
  Proofchain
  "~~/src/HOL/Quotient_Examples/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 {* Some extra lemmas about finite sets *}

lemma filter_subset: 
  "filter_fset p X |⊆| X"
by (descending, auto)

lemma fset_diff_union: 
  "A - (B |∪| C) = A - B - C"
by (descending, auto)

lemma fset_diff_union2:
  assumes "B |⊆| A" 
  shows "A - B |∪| B = A"
using assms by (descending, auto)

lemma rsp_fold_o:
  assumes "rsp_fold f"
  shows "rsp_fold (f o g)"
using assms by (smt o_apply rsp_fold_def)

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 "op ⊗⇩c"} 
  The final two make @{term "ε⇩c"} the left and right unit of @{term "op ⊗⇩c"}. 
  *}
inductive
  equiv_int :: "conc_interface => conc_interface => bool" (infix "\<simeq>" 45)
where
  refl: "P \<simeq> P"
| sym: "P \<simeq> Q ==> Q \<simeq> P"
| trans: "[|P \<simeq> Q; Q \<simeq> R|] ==> P \<simeq> R"
| cong_hcomp1: "P \<simeq> Q ==> P' ⊗⇩c P \<simeq> P' ⊗⇩c Q"
| cong_hcomp2: "P \<simeq> Q ==> P ⊗⇩c P' \<simeq> Q ⊗⇩c P'"
| cong_exists: "P \<simeq> Q ==> Exists_int_conc x P \<simeq> Exists_int_conc x Q"
| hcomp_conc_assoc: "P ⊗⇩c (Q ⊗⇩c R) \<simeq> (P ⊗⇩c Q) ⊗⇩c R"
| hcomp_conc_comm: "P ⊗⇩c Q \<simeq> Q ⊗⇩c P"
| hcomp_conc_unit1: "ε⇩c ⊗⇩c P \<simeq> P"
| hcomp_conc_unit2: "P ⊗⇩c ε⇩c \<simeq> P"

lemma equiv_int_cong_hcomp: 
  "[| P \<simeq> Q ; P' \<simeq> Q' |] ==> P ⊗⇩c P' \<simeq> 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

quotient_definition 
  "Ribbon :: assertion => interface" 
is "Ribbon_conc"
done

quotient_definition
  "Emp_int :: interface"
is "ε⇩c"
done
notation Emp_int ("ε")

quotient_definition
  "Exists_int :: string => interface => interface"
is "Exists_int_conc"
by (rule equiv_int.cong_exists)

quotient_definition
  "HComp_int :: interface => interface => interface" 
is "HComp_int_conc"
by (auto simp add: equiv_int_cong_hcomp)
notation HComp_int (infix "⊗" 50)

lemma hcomp_comm: 
  "(P ⊗ Q) = (Q ⊗ P)"
by (lifting hcomp_conc_comm)

lemma hcomp_assoc:
  "(P ⊗ (Q ⊗ R)) = ((P ⊗ Q) ⊗ R)"
by (lifting hcomp_conc_assoc)

lemma emp_hcomp:
  "ε ⊗ P = P"
by (lifting hcomp_conc_unit1)

lemma hcomp_emp:
  "P ⊗ ε = P"
by (lifting hcomp_conc_unit2)

lemma rsp_hcomp:
  "rsp_fold (op ⊗)"
by (auto simp add:rsp_fold_def o_def, metis hcomp_comm hcomp_assoc)

subsection {* An iterated horizontal-composition operator *}

definition iter_hcomp :: "('a fset) => ('a => interface) => interface"
where
  "iter_hcomp X f ≡ fold_fset (op ⊗ o f) X ε"

syntax "iter_hcomp_syntax" :: 
  "'a => ('a fset) => ('a => interface) => interface"
      ("(\<Otimes>_|∈|_. _)" [0,0,10] 10)
translations "\<Otimes>x|∈|M. e" == "CONST iter_hcomp M (λx. e)"

term "\<Otimes>P|∈|Ps. f P" -- "this is eta-expanded, so prints in expanded form"
term "\<Otimes>P|∈|Ps. f" -- "this isn't eta-expanded, so prints as written"

lemma iter_hcomp_cong:
  assumes "∀v ∈ fset vs. φ v = φ' v"
  shows "(\<Otimes>v|∈|vs. φ v) = (\<Otimes>v|∈|vs. φ' v)"
proof -
  have "!!f g e. (!!v. v |∈| vs ==> f v = g v) ==>
    rsp_fold f ==> rsp_fold g ==> fold_fset f vs e = fold_fset g vs e"
  by (descending, unfold fold_once_def, auto, metis fold_cong set_remdups)
  thus ?thesis 
  by (smt assms in_fset iter_hcomp_def o_apply rsp_fold_o rsp_hcomp)
qed

lemma iter_hcomp_empty:
  shows "(\<Otimes>x |∈| {||}. p x) = ε"
by (metis iter_hcomp_def fold_empty_fset id_apply)

lemma iter_hcomp_insert:
  assumes "v |∉| ws"
  shows "(\<Otimes>x |∈| insert_fset v ws. p x) = (p v ⊗ (\<Otimes>x |∈| ws. p x))"
proof -
  have "!!f v ws e. rsp_fold f ==> v |∉| ws ==> 
    fold_fset f (insert_fset v ws) e = (f v (fold_fset f ws e))"
  apply (induct ws)
  apply (descending, unfold fold_once_def, auto)[1]
  apply (descending, unfold fold_once_def rsp_fold_def, auto)
  apply (metis (hide_lams, no_types) fold_Cons fold_rev foldr_Cons
    foldr_conv_fold o_eq_dest_lhs)
  done
  thus "?thesis"
  by (metis iter_hcomp_def assms o_apply rsp_fold_o rsp_hcomp)
qed

lemma iter_hcomp_union:
  assumes "vs |∩| ws = {||}"
  shows "(\<Otimes>x |∈| vs |∪| ws. p x) = ((\<Otimes>x |∈| vs. p x) ⊗ (\<Otimes>x |∈| ws. p x))"
apply (insert assms, induct vs)
apply (metis emp_hcomp iter_hcomp_empty sup_bot_left)
apply (subgoal_tac "x |∉| (vs |∪| ws)")
apply (unfold union_insert_fset iter_hcomp_insert)
apply (subgoal_tac "vs |∩| ws = {||}")
apply (metis hcomp_assoc)
apply (metis in_union_fset inter_insert_fset)
apply (metis in_inter_fset in_union_fset insert_fsetI1 notin_empty_fset)
done

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)"

quotient_definition 
  "asn :: interface => assertion"
is "conc_asn"
apply (induct_tac rule:equiv_int.induct)
apply (auto simp add: star_assoc star_comm star_rot emp_star)
done

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 (descending, 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"

quotient_definition
  "rd_int :: interface => string set"
is "rd_conc_int"
apply (induct_tac rule: equiv_int.induct)
apply auto
done
  
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 (descending, 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 (op ;;) 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: "Π = cCons 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 (smt Cons.prems(4) Π_def chainlen.simps(2) 
    nth_Cons_0 nthtriple.simps(1) fst3_simp thd3_simp)
  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), auto simp add: Π_def)
  done
qed

end