theory Ribbons_Graphical imports Ribbons_Basic begin text {* We introduce several concepts that are required for the soundness and completeness results (proved in ribbons_rast.thy, ribbons_completeness.thy and ribbons_soundness.thy). We introduce interfaces, the graphical syntax of diagrams, and how to extract commands and interfaces from diagrams. *} subsection {* Syntax and semantics of interfaces *} text {* An interface is obtained by extracting a single row from a diagram. *} datatype interface = Ribbon "assertion" | HComp_int "interface" "interface" (infixr "\" 50) | Emp_int | Exists_int "string" "interface" text {* 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 HComp_int. The final two make Emp_int the left and right unit of HComp_int. *} inductive equiv_int :: "interface \ interface \ bool" where refl: "equiv_int P P" | sym: "equiv_int P Q \ equiv_int Q P" | trans: "\equiv_int P Q; equiv_int Q R\ \ equiv_int P R" | cong_hcomp1: "equiv_int P Q \ equiv_int (P' \ P) (P' \ Q)" | cong_hcomp2: "equiv_int P Q \ equiv_int (P \ P') (Q \ P')" | cong_exists: "equiv_int P Q \ equiv_int (Exists_int x P) (Exists_int x Q)" | hcomp_assoc: "equiv_int (P \ (Q \ R)) ((P \ Q) \ R)" | hcomp_comm: "equiv_int (P \ Q) (Q \ P)" | hcomp_unit1: "equiv_int (Emp_int \ P) P" | hcomp_unit2: "equiv_int (P \ Emp_int) P" text {* The semantics of an interface is an assertion. *} primrec ass :: "interface \ assertion" where "ass (Ribbon p) = p" | "ass (P \ Q) = (ass P) \ (ass Q)" | "ass (Emp_int) = Emp" | "ass (Exists_int x P) = Exists x (ass P)" text {* The equivalence on interfaces is sound for this semantics. *} lemma equiv_int_sound: "equiv_int P1 P2 \ ass P1 = ass P2" proof - fix P1 P2 assume "equiv_int P1 P2" thus "ass P1 = ass P2" proof (induct rule:equiv_int.induct) case (hcomp_assoc P Q R) thus ?case by (auto simp add: star_assoc) next case (hcomp_comm P Q) thus ?case by (auto simp add: star_comm) next case (hcomp_unit1 P) thus ?case by (auto simp add: emp_star) next case (hcomp_unit2 P) thus ?case by (auto simp add: star_emp) qed auto qed text {* Program variables mentioned in an interface. *} primrec rd_int :: "interface \ string set" where "rd_int (Ribbon p) = rd_ass p" | "rd_int (P \ Q) = rd_int P \ rd_int Q" | "rd_int (Emp_int) = {}" | "rd_int (Exists_int x P) = rd_int P" text {* The program variables read by an interface are the same as those read by its corresponding assertion. (In fact, this lemma would suffice as a definition of rd_int.) *} lemma rd_int_is_rd_ass: "rd_ass (ass P) = rd_int P" by (induct P, auto simp add: rd_star rd_exists rd_emp) subsection {* Syntax, provability and semantics of diagrams *} subsubsection {* Some general purpose lemmas *} lemma nth_in_set: "\ i < length xs ; xs ! i = x \ \ x \ set xs" by auto lemma exI3: "P a b c \ \a b c. P a b c" by auto text {* Fix a type for node identifiers. Pick v01 and v02 as distinct nodes. *} typedecl node axiomatization v01 :: node and v02 :: node where v01_neq_v02 [simp]: "v01 \ v02" and v02_neq_v01 [simp]: "v02 \ v01" text {* Syntax of diagrams *} datatype assnode = Rib "assertion" | Exists_dia "string" "diagram" and comnode = Com "command" | Choose_dia "diagram" "diagram" | Loop_dia "diagram" and diagram = Graph "node list" "node \ assnode" "(node list \ comnode \ node list) list" type_synonym labelling = "node \ assnode" type_synonym edge = "node list \ comnode \ node list" subsubsection {* Projection functions on triples *} definition fst3 :: "'a \ 'b \ 'c \ 'a" where "fst3 \ fst" definition snd3 :: "'a \ 'b \ 'c \ 'b" where "snd3 \ fst \ snd" definition thd3 :: "'a \ 'b \ 'c \ 'c" where "thd3 \ snd \ snd" lemma fst3_comp: "\f g h T. fst3 ((\(x,y,z). (f x, g y, h z)) T) = f (fst3 T)" unfolding fst3_def by auto lemma snd3_comp: "\f g h T. snd3 ((\(x,y,z). (f x, g y, h z)) T) = g (snd3 T)" unfolding snd3_def by auto lemma thd3_comp: "\f g h T. thd3 ((\(x,y,z). (f x, g y, h z)) T) = h (thd3 T)" unfolding thd3_def by auto lemma fst3_simp: "\a b c. fst3 (a,b,c) = a" unfolding fst3_def by auto lemma snd3_simp: "\a b c. snd3 (a,b,c) = b" unfolding snd3_def by auto lemma thd3_simp: "\a b c. thd3 (a,b,c) = c" unfolding thd3_def by auto lemma tripleI: fixes T U assumes "fst3 T = fst3 U" and "snd3 T = snd3 U" and "thd3 T = thd3 U" shows "T = U" using assms unfolding fst3_def snd3_def thd3_def by (metis o_def surjective_pairing) subsubsection {* Well formedness of graphs *} definition acyclicity :: "edge list \ bool" where "acyclicity E \ acyclic (\e \ set E. \v \ set (fst3 e). \w \ set (thd3 e). {(v,w)})" definition linearity :: "edge list \ bool" where "linearity E \ distinct E \ (\e \ set E. \f \ set E. e \ f \ set (fst3 e) \ set (fst3 f) = {} \ set (thd3 e) \ set (thd3 f) = {})" inductive wf_ass :: "assnode \ bool" and wf_com :: "comnode \ bool" and wf_dia :: "diagram \ bool" where wf_rib: "wf_ass (Rib p)" | wf_exists: "wf_dia G \ wf_ass (Exists_dia x G)" | wf_basic: "wf_com (Com c)" | wf_choice: "\ wf_dia G; wf_dia H \ \ wf_com (Choose_dia G H)" | wf_loop: "wf_dia G \ wf_com (Loop_dia G)" | wf_dia: "\ distinct V; acyclicity E; linearity E; \e. e \ set E \ distinct (fst3 e) \ set (fst3 e) \ set V ; \e. e \ set E \ distinct (thd3 e) \ set (thd3 e) \ set V \ \ wf_dia (Graph V \ E)" inductive_cases wf_dia_inv': "wf_dia (Graph V \ E)" lemma wf_dia_inv: fixes V \ E assumes "wf_dia (Graph V \ E)" shows "distinct V" and "acyclicity E" and "linearity E" and "\e. e \ set E \ distinct (fst3 e) \ set (fst3 e) \ set V" and "\e. e \ set E \ distinct (thd3 e) \ set (thd3 e) \ set V" proof - show "distinct V" using wf_dia_inv'[OF assms] by blast next show "acyclicity E" using wf_dia_inv'[OF assms] by blast next show "linearity E" using wf_dia_inv'[OF assms] by blast next show "\e. e \ set E \ distinct (fst3 e) \ set (fst3 e) \ set V" using wf_dia_inv'[OF assms] unfolding fst3_def by blast next show "\e. e \ set E \ distinct (thd3 e) \ set (thd3 e) \ set V" using wf_dia_inv'[OF assms] unfolding thd3_def comp_def by blast qed subsubsection {* Initial and terminal nodes *} fun initials :: "diagram \ node list" where "initials (Graph V _ E) = [v \ V. v \ set (concat (map thd3 E))]" fun terminals :: "diagram \ node list" where "terminals (Graph V _ E) = [v \ V. v \ set (concat (map fst3 E))]" lemma no_edges_imp_all_nodes_initial: "initials (Graph V \ []) = V" by auto lemma no_edges_imp_all_nodes_terminal: "terminals (Graph V \ []) = V" by auto subsubsection {* Top and bottom interfaces *} primrec top_dia :: "diagram \ interface" and top_ass :: "assnode \ interface" where "top_dia (Graph V \ E) = foldl (op \) Emp_int [ top_ass (\ v) . v \ initials (Graph V \ E) ]" | "top_ass (Rib p) = Ribbon p" | "top_ass (Exists_dia x G) = Exists_int x (top_dia G)" primrec bot_dia :: "diagram \ interface" and bot_ass :: "assnode \ interface" where "bot_dia (Graph V \ E) = foldl (op \) Emp_int [ bot_ass (\ v) . v \ terminals (Graph V \ E) ]" | "bot_ass (Rib p) = Ribbon p" | "bot_ass (Exists_dia x G) = Exists_int x (bot_dia G)" subsubsection {* Provability of diagrams *} inductive prov_dia :: "[diagram, interface, interface] \ bool" and prov_com :: "[comnode, interface, interface] \ bool" and prov_ass :: "assnode \ bool" where Skip: "prov_ass (Rib p)" | Exists: "prov_dia G _ _ \ prov_ass (Exists_dia x G)" | Basic: "prov_triple (ass P, c, ass Q) \ prov_com (Com c) P Q" | Choice: "\ prov_dia G P Q ; prov_dia H P Q \ \ prov_com (Choose_dia G H) P Q" | Loop: "prov_dia G P P \ prov_com (Loop_dia G) P P" | Main: "\\v. v \ set V \ prov_ass (\ v) ; \e. e \ set E \ prov_com (snd3 e) (foldl (op \) Emp_int [bot_ass (\ v) . v \ fst3 e]) (foldl (op \) Emp_int [top_ass (\ v) . v \ thd3 e]) ; wf_dia (Graph V \ E) \ \ prov_dia (Graph V \ E) (top_dia (Graph V \ E)) (bot_dia (Graph V \ E))" inductive_cases main_inv: "prov_dia (Graph V \ E) P Q" inductive_cases loop_inv: "prov_com (Loop_dia G) P Q" inductive_cases choice_inv: "prov_com (Choose_dia G H) P Q" inductive_cases basic_inv: "prov_com (Com c) P Q" inductive_cases exists_inv: "prov_ass (Exists_dia x G)" inductive_cases skip_inv: "prov_ass (Rib p)" subsubsection {* Extracting commands from diagrams *} fun lins :: "diagram \ ((node + edge) list) set" where "lins (Graph V \ E) = {\ . (distinct \) \ (set \ = ((Inl ` (set V)) \ (Inr ` (set E)))) \ (\i j v e. i < length \ \ j < length \ \ \!i = Inl v \ \!j = Inr e \ v \ set (fst3 e) \ i (\j k w e. j < length \ \ k < length \ \ \!j = Inr e \ \!k = Inl w \ w \ set (thd3 e) \ j defn. And the corresponding defn cannot be proved to terminate. So we use the defn that follows. primrec coms_dia :: "diagram \ command set" and coms_ass :: "assnode \ command set" and coms_com :: "comnode \ command set" where "coms_ass (Rib p) = {Skip}" | "coms_ass (Exists_dia x G) = coms_dia G" | "coms_com (Com c) = {c}" | "coms_com (Choose_dia G H) = {Choose c d | c d . c \ coms_dia G \ d \ coms_dia H}" | "coms_com (Loop_dia G) = {Loop c | c . c \ coms_dia G}" | "coms_dia (Graph V \ E) = { foldr (op ;;) cs Skip | cs . \X \ lin (Graph V \ E) . \i (case (X!i) of Inl A \ coms_ass A | Inr C \ coms_com C) }" *) inductive coms_dia :: "[diagram, command] \ bool" and coms_ass :: "[assnode, command] \ bool" and coms_com :: "[comnode, command] \ bool" where coms_skip: "coms_ass (Rib p) Skip" | coms_exists: "coms_dia G c \ coms_ass (Exists_dia x G) c" | coms_basic: "coms_com (Com c) c" | coms_choice: "\ coms_dia G c; coms_dia H d \ \ coms_com (Choose_dia G H) (Choose c d)" | coms_loop: "coms_dia G c \ coms_com (Loop_dia G) (Loop c)" (* In the following clause we would prefer to write... \i. i \ (case (\!i) of Inl v \ coms_ass (\ v) | Inr e \ coms_com (snd3 e) ) (cs!i) ... or maybe even ... \i. i \ (sum_case (coms_ass \ \) (coms_com \ snd3) (\!i)) (cs!i) ... but in either case, monotonicity fails. Need to help via a lemma annotated as [mono]. *) | coms_main: "\ \ \ lins (Graph V \ E); length cs = length \; \i. \ i ; \v. (\!i) = Inl v \ \ coms_ass (\ (Sum_Type.Projl (\!i))) (cs!i) ; \i. \ i ; \e. (\!i) = Inr e \ \ coms_com (snd3 (Sum_Type.Projr (\!i))) (cs!i) \ \ coms_dia (Graph V \ E) (foldr (op ;;) cs Skip)" inductive_cases coms_skip_inv: "coms_ass (Rib p) c" inductive_cases coms_exists_inv: "coms_ass (Exists_dia x G) c" inductive_cases coms_basic_inv: "coms_com (Com c') c" inductive_cases coms_choice_inv: "coms_com (Choose_dia G H) c" inductive_cases coms_loop_inv: "coms_com (Loop_dia G) c" lemma coms_main_inv: fixes G c assumes "coms_dia G c" shows "\V \ E \ cs. (G = Graph V \ E) \ (\ \ lins (Graph V \ E)) \ (length cs = length \) \ (\i. (\v. (\!i) = Inl v) \ coms_ass (\ (Sum_Type.Projl (\!i))) (cs!i)) \ (\i. (\e. (\!i) = Inr e) \ coms_com (snd3 (Sum_Type.Projr (\!i))) (cs!i)) \ (c = foldr (op ;;) cs Skip)" proof - have "(coms_dia G c \ (\V \ E \ cs. (G = Graph V \ E) \ (\ \ lins (Graph V \ E)) \ (length cs = length \) \ (\i. (\v. (\!i) = Inl v) \ coms_ass (\ (Sum_Type.Projl (\!i))) (cs!i)) \ (\i. (\e. (\!i) = Inr e) \ coms_com (snd3 (Sum_Type.Projr (\!i))) (cs!i)) \ (c = foldr (op ;;) cs Skip))) \ (coms_ass A c \ True) \ (coms_com C c \ True)" proof (induct rule: coms_dia_coms_ass_coms_com.induct) qed (simp, simp, simp, simp, simp, metis) with assms show ?thesis by auto qed end