Theory Ribbons_Interfaces

Up to index of Isabelle/HOL/ribbonproofs

theory Ribbons_Interfaces
imports Ribbons_Basic Proofchain FSet
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: cc 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