diff --git a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy @@ -1,108 +1,108 @@ section \Deterministic Büchi Automata Combinations\ theory DBA_Combine imports DBA DGBA begin global_interpretation degeneralization: automaton_degeneralization_run dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\ P w r p. gen infs P (p ## r)" dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" fst id defines degeneralize = degeneralization.degeneralize by (unfold_locales) (auto simp flip: sscan_smap) lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded DBA.language_def] lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded DBA.nodes_def] lemmas degeneralize_nodes_card = degeneralization.degeneralize_nodes_card[folded DBA.nodes_def] global_interpretation intersection: automaton_intersection_run dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" dgba.dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\ P w r p. gen infs P (p ## r)" "\ c\<^sub>1 c\<^sub>2. [c\<^sub>1 \ fst, c\<^sub>2 \ snd]" - defines intersect' = intersection.combine + defines intersect' = intersection.product by unfold_locales auto - lemmas intersect'_language[simp] = intersection.combine_language[folded DGBA.language_def] - lemmas intersect'_nodes_finite = intersection.combine_nodes_finite[folded DGBA.nodes_def] - lemmas intersect'_nodes_card = intersection.combine_nodes_card[folded DGBA.nodes_def] + lemmas intersect'_language[simp] = intersection.product_language[folded DGBA.language_def] + lemmas intersect'_nodes_finite = intersection.product_nodes_finite[folded DGBA.nodes_def] + lemmas intersect'_nodes_card = intersection.product_nodes_card[folded DGBA.nodes_def] global_interpretation union: automaton_union_run dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" "\ c\<^sub>1 c\<^sub>2 pq. (c\<^sub>1 \ fst) pq \ (c\<^sub>2 \ snd) pq" - defines union = union.combine + defines union = union.product by (unfold_locales) (simp del: comp_apply) - lemmas union_language = union.combine_language - lemmas union_nodes_finite = union.combine_nodes_finite - lemmas union_nodes_card = union.combine_nodes_card + lemmas union_language = union.product_language + lemmas union_nodes_finite = union.product_nodes_finite + lemmas union_nodes_card = union.product_nodes_card global_interpretation intersection_list: automaton_intersection_list_run dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" dgba.dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\ P w r p. gen infs P (p ## r)" "\ cs. map (\ k pp. (cs ! k) (pp ! k)) [0 ..< length cs]" - defines intersect_list' = intersection_list.combine + defines intersect_list' = intersection_list.product by (unfold_locales) (auto simp: gen_def comp_def) - lemmas intersect_list'_language[simp] = intersection_list.combine_language[folded DGBA.language_def] - lemmas intersect_list'_nodes_finite = intersection_list.combine_nodes_finite[folded DGBA.nodes_def] - lemmas intersect_list'_nodes_card = intersection_list.combine_nodes_card[folded DGBA.nodes_def] + lemmas intersect_list'_language[simp] = intersection_list.product_language[folded DGBA.language_def] + lemmas intersect_list'_nodes_finite = intersection_list.product_nodes_finite[folded DGBA.nodes_def] + lemmas intersect_list'_nodes_card = intersection_list.product_nodes_card[folded DGBA.nodes_def] global_interpretation union_list: automaton_union_list_run dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" "\ cs pp. \ k < length cs. (cs ! k) (pp ! k)" - defines union_list = union_list.combine + defines union_list = union_list.product by (unfold_locales) (simp add: comp_def) - lemmas union_list_language = union_list.combine_language - lemmas union_list_nodes_finite = union_list.combine_nodes_finite - lemmas union_list_nodes_card = union_list.combine_nodes_card + lemmas union_list_language = union_list.product_language + lemmas union_list_nodes_finite = union_list.product_nodes_finite + lemmas union_list_nodes_card = union_list.product_nodes_card (* TODO: these compound definitions are annoying, can we move those into Deterministic theory *) abbreviation intersect where "intersect A B \ degeneralize (intersect' A B)" lemma intersect_language[simp]: "DBA.language (intersect A B) = DBA.language A \ DBA.language B" by simp lemma intersect_nodes_finite: assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)" shows "finite (DBA.nodes (intersect A B))" using intersect'_nodes_finite assms by simp lemma intersect_nodes_card: assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)" shows "card (DBA.nodes (intersect A B)) \ 2 * card (DBA.nodes A) * card (DBA.nodes B)" proof - have "card (DBA.nodes (intersect A B)) \ max 1 (length (dgba.accepting (intersect' A B))) * card (DGBA.nodes (intersect' A B))" using degeneralize_nodes_card by this also have "length (dgba.accepting (intersect' A B)) = 2" by simp also have "card (DGBA.nodes (intersect' A B)) \ card (DBA.nodes A) * card (DBA.nodes B)" using intersect'_nodes_card assms by this finally show ?thesis by simp qed abbreviation intersect_list where "intersect_list AA \ degeneralize (intersect_list' AA)" lemma intersect_list_language[simp]: "DBA.language (intersect_list AA) = \ (DBA.language ` set AA)" by simp lemma intersect_list_nodes_finite: assumes "list_all (finite \ DBA.nodes) AA" shows "finite (DBA.nodes (intersect_list AA))" using intersect_list'_nodes_finite assms by simp lemma intersect_list_nodes_card: assumes "list_all (finite \ DBA.nodes) AA" shows "card (DBA.nodes (intersect_list AA)) \ max 1 (length AA) * prod_list (map (card \ DBA.nodes) AA)" proof - have "card (DBA.nodes (intersect_list AA)) \ max 1 (length (dgba.accepting (intersect_list' AA))) * card (DGBA.nodes (intersect_list' AA))" using degeneralize_nodes_card by this also have "length (dgba.accepting (intersect_list' AA)) = length AA" by simp also have "card (DGBA.nodes (intersect_list' AA)) \ prod_list (map (card \ DBA.nodes) AA)" using intersect_list'_nodes_card assms by this finally show ?thesis by simp qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DBTA/DBTA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DBTA/DBTA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DBTA/DBTA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DBTA/DBTA_Combine.thy @@ -1,115 +1,115 @@ section \Deterministic Büchi Transition Automata Combinations\ theory DBTA_Combine imports DBTA DGBTA begin (* TODO: exact copy-paste from NBTA, abstract *) global_interpretation degeneralization: automaton_degeneralization_run dgbta dgbta.alphabet dgbta.initial dgbta.transition dgbta.accepting "\ P w r p. gen infs P (p ## r ||| w ||| r)" dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" id "\ ((p, k), a, (q, l)). ((p, a, q), k)" defines degeneralize = degeneralization.degeneralize proof fix w :: "'a stream" fix r :: "'b stream" fix cs p k let ?f = "\ ((p, k), a, (q, l)). ((p, a, q), k)" let ?s = "sscan (count cs \ id) (p ## r ||| w ||| r) k" have "infs (degen cs \ ?f) ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) \ infs (degen cs) (smap ?f ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)))" by (simp add: comp_def) also have "smap ?f ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) = (p ## r ||| w ||| r) ||| k ## ?s" by (coinduction arbitrary: p k r w) (auto simp: eq_scons simp flip: szip_unfold sscan_scons) also have "\ = (p ## r ||| w ||| r) ||| k ## sscan (count cs) (p ## r ||| w ||| r) k" by simp also have "infs (degen cs) \ = gen infs cs (p ## r ||| w ||| r)" using degen_infs by this finally show "infs (degen cs \ ?f) ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) \ gen infs cs (p ## r ||| w ||| r)" by this qed lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded DBTA.language_def] lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded DBTA.nodes_def] lemmas degeneralize_nodes_card = degeneralization.degeneralize_nodes_card[folded DBTA.nodes_def] global_interpretation intersection: automaton_intersection_run dbta.dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" dbta.dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" dgbta.dgbta dgbta.alphabet dgbta.initial dgbta.transition dgbta.accepting "\ P w r p. gen infs P (p ## r ||| w ||| r)" "\ c\<^sub>1 c\<^sub>2. [c\<^sub>1 \ (\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1)), c\<^sub>2 \ (\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2))]" - defines intersect' = intersection.combine + defines intersect' = intersection.product proof fix w :: "'a stream" fix u :: "'b stream" fix v :: "'c stream" fix c\<^sub>1 c\<^sub>2 p q let ?tfst = "\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1)" let ?tsnd = "\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2)" have "gen infs [c\<^sub>1 \ ?tfst, c\<^sub>2 \ ?tsnd] ((p, q) ## (u ||| v) ||| w ||| u ||| v) \ infs c\<^sub>1 (smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v)) \ infs c\<^sub>2 (smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v))" unfolding gen_def by (simp add: comp_def) also have "smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v) = p ## u ||| w ||| u" by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse) also have "smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v) = q ## v ||| w ||| v" by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse) finally show "gen infs [c\<^sub>1 \ ?tfst, c\<^sub>2 \ ?tsnd] ((p, q) ## (u ||| v) ||| w ||| u ||| v) \ infs c\<^sub>1 (p ## u ||| w ||| u) \ infs c\<^sub>2 (q ## v ||| w ||| v)" by this qed - lemmas intersect'_language[simp] = intersection.combine_language[folded DGBTA.language_def] - lemmas intersect'_nodes_finite = intersection.combine_nodes_finite[folded DGBTA.nodes_def] - lemmas intersect'_nodes_card = intersection.combine_nodes_card[folded DGBTA.nodes_def] + lemmas intersect'_language[simp] = intersection.product_language[folded DGBTA.language_def] + lemmas intersect'_nodes_finite = intersection.product_nodes_finite[folded DGBTA.nodes_def] + lemmas intersect'_nodes_card = intersection.product_nodes_card[folded DGBTA.nodes_def] global_interpretation union: automaton_union_run dbta.dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" dbta.dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" dbta.dbta dbta.alphabet dbta.initial dbta.transition dbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" "\ c\<^sub>1 c\<^sub>2 pq. (c\<^sub>1 \ (\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1))) pq \ (c\<^sub>2 \ (\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2))) pq" - defines union = union.combine + defines union = union.product proof fix w :: "'a stream" fix u :: "'b stream" fix v :: "'c stream" fix c\<^sub>1 c\<^sub>2 p q let ?tfst = "\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1)" let ?tsnd = "\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2)" have "infs (\ pq. (c\<^sub>1 \ (\ ((p\<^sub>1, p\<^sub>2), a, q\<^sub>1, q\<^sub>2). (p\<^sub>1, a, q\<^sub>1))) pq \ (c\<^sub>2 \ (\ ((p\<^sub>1, p\<^sub>2), a, q\<^sub>1, q\<^sub>2). (p\<^sub>2, a, q\<^sub>2))) pq) ((p, q) ## (u ||| v) ||| w ||| (u ||| v)) \ infs c\<^sub>1 (smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v)) \ infs c\<^sub>2 (smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v))" by (simp add: comp_def) also have "smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v) = p ## u ||| w ||| u" by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse) also have "smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v) = q ## v ||| w ||| v" by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse) finally show "infs (\ pq. (c\<^sub>1 \ (\ ((p\<^sub>1, p\<^sub>2), a, q\<^sub>1, q\<^sub>2). (p\<^sub>1, a, q\<^sub>1))) pq \ (c\<^sub>2 \ (\ ((p\<^sub>1, p\<^sub>2), a, q\<^sub>1, q\<^sub>2). (p\<^sub>2, a, q\<^sub>2))) pq) ((p, q) ## (u ||| v) ||| w ||| (u ||| v)) \ infs c\<^sub>1 (p ## u ||| w ||| u) \ infs c\<^sub>2 (q ## v ||| w ||| v)" by this qed - lemmas union_language = union.combine_language - lemmas union_nodes_finite = union.combine_nodes_finite - lemmas union_nodes_card = union.combine_nodes_card + lemmas union_language = union.product_language + lemmas union_nodes_finite = union.product_nodes_finite + lemmas union_nodes_card = union.product_nodes_card abbreviation intersect where "intersect A B \ degeneralize (intersect' A B)" lemma intersect_language[simp]: "DBTA.language (intersect A B) = DBTA.language A \ DBTA.language B" by simp lemma intersect_nodes_finite: assumes "finite (DBTA.nodes A)" "finite (DBTA.nodes B)" shows "finite (DBTA.nodes (intersect A B))" using intersect'_nodes_finite assms by simp lemma intersect_nodes_card: assumes "finite (DBTA.nodes A)" "finite (DBTA.nodes B)" shows "card (DBTA.nodes (intersect A B)) \ 2 * card (DBTA.nodes A) * card (DBTA.nodes B)" proof - have "card (DBTA.nodes (intersect A B)) \ max 1 (length (dgbta.accepting (intersect' A B))) * card (DGBTA.nodes (intersect' A B))" using degeneralize_nodes_card by this also have "length (dgbta.accepting (intersect' A B)) = 2" by simp also have "card (DGBTA.nodes (intersect' A B)) \ card (DBTA.nodes A) * card (DBTA.nodes B)" using intersect'_nodes_card assms by this finally show ?thesis by simp qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy @@ -1,110 +1,110 @@ section \Deterministic Co-Büchi Automata Combinations\ theory DCA_Combine imports DCA DGCA begin global_interpretation degeneralization: automaton_degeneralization_run dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\ P w r p. cogen fins P (p ## r)" dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" fst id defines degeneralize = degeneralization.degeneralize by (unfold_locales) (auto simp flip: sscan_smap) lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded DCA.language_def] lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded DCA.nodes_def] lemmas degeneralize_nodes_card = degeneralization.degeneralize_nodes_card[folded DCA.nodes_def] global_interpretation intersection: automaton_intersection_run dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" "\ c\<^sub>1 c\<^sub>2 pq. (c\<^sub>1 \ fst) pq \ (c\<^sub>2 \ snd) pq" - defines intersect = intersection.combine + defines intersect = intersection.product by (unfold_locales) (simp del: comp_apply) - lemmas intersect_language = intersection.combine_language - lemmas intersect_nodes_finite = intersection.combine_nodes_finite - lemmas intersect_nodes_card = intersection.combine_nodes_card + lemmas intersect_language = intersection.product_language + lemmas intersect_nodes_finite = intersection.product_nodes_finite + lemmas intersect_nodes_card = intersection.product_nodes_card global_interpretation union: automaton_union_run dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" dgca.dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\ P w r p. cogen fins P (p ## r)" "\ c\<^sub>1 c\<^sub>2. [c\<^sub>1 \ fst, c\<^sub>2 \ snd]" - defines union' = union.combine + defines union' = union.product by unfold_locales auto - lemmas union'_language[simp] = union.combine_language[folded DGCA.language_def] - lemmas union'_nodes_finite = union.combine_nodes_finite[folded DGCA.nodes_def] - lemmas union'_nodes_card = union.combine_nodes_card[folded DGCA.nodes_def] + lemmas union'_language[simp] = union.product_language[folded DGCA.language_def] + lemmas union'_nodes_finite = union.product_nodes_finite[folded DGCA.nodes_def] + lemmas union'_nodes_card = union.product_nodes_card[folded DGCA.nodes_def] global_interpretation intersection_list: automaton_intersection_list_run dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" "\ cs pp. \ k < length cs. (cs ! k) (pp ! k)" - defines intersect_list = intersection_list.combine + defines intersect_list = intersection_list.product by (unfold_locales) (simp add: comp_def) - lemmas intersect_list_language = intersection_list.combine_language - lemmas intersect_list_nodes_finite = intersection_list.combine_nodes_finite - lemmas intersect_list_nodes_card = intersection_list.combine_nodes_card + lemmas intersect_list_language = intersection_list.product_language + lemmas intersect_list_nodes_finite = intersection_list.product_nodes_finite + lemmas intersect_list_nodes_card = intersection_list.product_nodes_card global_interpretation union_list: automaton_union_list_run dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" dgca.dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\ P w r p. cogen fins P (p ## r)" "\ cs. map (\ k pp. (cs ! k) (pp ! k)) [0 ..< length cs]" - defines union_list' = union_list.combine + defines union_list' = union_list.product by (unfold_locales) (auto simp: cogen_def comp_def) - lemmas union_list'_language[simp] = union_list.combine_language[folded DGCA.language_def] - lemmas union_list'_nodes_finite = union_list.combine_nodes_finite[folded DGCA.nodes_def] - lemmas union_list'_nodes_card = union_list.combine_nodes_card[folded DGCA.nodes_def] + lemmas union_list'_language[simp] = union_list.product_language[folded DGCA.language_def] + lemmas union_list'_nodes_finite = union_list.product_nodes_finite[folded DGCA.nodes_def] + lemmas union_list'_nodes_card = union_list.product_nodes_card[folded DGCA.nodes_def] abbreviation union where "union A B \ degeneralize (union' A B)" lemma union_language[simp]: assumes "dca.alphabet A = dca.alphabet B" shows "DCA.language (union A B) = DCA.language A \ DCA.language B" using assms by simp lemma union_nodes_finite: assumes "finite (DCA.nodes A)" "finite (DCA.nodes B)" shows "finite (DCA.nodes (union A B))" using union'_nodes_finite assms by simp lemma union_nodes_card: assumes "finite (DCA.nodes A)" "finite (DCA.nodes B)" shows "card (DCA.nodes (union A B)) \ 2 * card (DCA.nodes A) * card (DCA.nodes B)" proof - have "card (DCA.nodes (union A B)) \ max 1 (length (dgca.rejecting (union' A B))) * card (DGCA.nodes (union' A B))" using degeneralize_nodes_card by this also have "length (dgca.rejecting (union' A B)) = 2" by simp also have "card (DGCA.nodes (union' A B)) \ card (DCA.nodes A) * card (DCA.nodes B)" using union'_nodes_card assms by this finally show ?thesis by simp qed abbreviation union_list where "union_list AA \ degeneralize (union_list' AA)" lemma union_list_language[simp]: assumes "\ (dca.alphabet ` set AA) = \ (dca.alphabet ` set AA)" shows "DCA.language (union_list AA) = \ (DCA.language ` set AA)" using assms by simp lemma union_list_nodes_finite: assumes "list_all (finite \ DCA.nodes) AA" shows "finite (DCA.nodes (union_list AA))" using union_list'_nodes_finite assms by simp lemma union_list_nodes_card: assumes "list_all (finite \ DCA.nodes) AA" shows "card (DCA.nodes (union_list AA)) \ max 1 (length AA) * prod_list (map (card \ DCA.nodes) AA)" proof - have "card (DCA.nodes (union_list AA)) \ max 1 (length (dgca.rejecting (union_list' AA))) * card (DGCA.nodes (union_list' AA))" using degeneralize_nodes_card by this also have "length (dgca.rejecting (union_list' AA)) = length AA" by simp also have "card (DGCA.nodes (union_list' AA)) \ prod_list (map (card \ DCA.nodes) AA)" using union_list'_nodes_card assms by this finally show ?thesis by simp qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DFA/DFA.thy b/thys/Transition_Systems_and_Automata/Automata/DFA/DFA.thy --- a/thys/Transition_Systems_and_Automata/Automata/DFA/DFA.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DFA/DFA.thy @@ -1,48 +1,48 @@ section \Deterministic Finite Automata\ theory DFA imports "../Deterministic" begin datatype ('label, 'state) dfa = dfa (alphabet: "'label set") (initial: "'state") (transition: "'label \ 'state \ 'state") (accepting: "'state pred") global_interpretation dfa: automaton dfa alphabet initial transition accepting defines path = dfa.path and run = dfa.run and reachable = dfa.reachable and nodes = dfa.nodes by unfold_locales auto global_interpretation dfa: automaton_path dfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" defines language = dfa.language by standard abbreviation target where "target \ dfa.target" abbreviation states where "states \ dfa.states" abbreviation trace where "trace \ dfa.trace" abbreviation successors where "successors \ dfa.successors TYPE('label)" global_interpretation intersection: automaton_intersection_path dfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" dfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" dfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" "\ c\<^sub>1 c\<^sub>2 (p, q). c\<^sub>1 p \ c\<^sub>2 q" - defines intersect = intersection.combine + defines intersect = intersection.product by (unfold_locales) (auto simp: zip_eq_Nil_iff) global_interpretation union: automaton_union_path dfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" dfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" dfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" "\ c\<^sub>1 c\<^sub>2 (p, q). c\<^sub>1 p \ c\<^sub>2 q" - defines union = union.combine + defines union = union.product by (unfold_locales) (auto simp: zip_eq_Nil_iff) global_interpretation complement: automaton_complement_path dfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" dfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" "\ c p. \ c p" defines complement = complement.complement by unfold_locales auto end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy @@ -1,33 +1,33 @@ section \Deterministic Rabin Automata Combinations\ theory DRA_Combine imports "DRA" "../DBA/DBA" "../DCA/DCA" begin global_interpretation intersection_bc: automaton_intersection_run dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\ P w r p. infs P (p ## r)" dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\ P w r p. fins P (p ## r)" dra.dra dra.alphabet dra.initial dra.transition dra.condition "\ P w r p. cogen rabin P (p ## r)" "\ c\<^sub>1 c\<^sub>2. [(c\<^sub>1 \ fst, c\<^sub>2 \ snd)]" - defines intersect_bc = intersection_bc.combine + defines intersect_bc = intersection_bc.product by (unfold_locales) (simp add: cogen_def rabin_def) (* TODO: why are only the constants of the first interpretation folded back correctly? *) - lemmas intersect_bc_language[simp] = intersection_bc.combine_language[folded DCA.language_def DRA.language_def] - lemmas intersect_bc_nodes_finite = intersection_bc.combine_nodes_finite[folded DCA.nodes_def DRA.nodes_def] - lemmas intersect_bc_nodes_card = intersection_bc.combine_nodes_card[folded DCA.nodes_def DRA.nodes_def] + lemmas intersect_bc_language[simp] = intersection_bc.product_language[folded DCA.language_def DRA.language_def] + lemmas intersect_bc_nodes_finite = intersection_bc.product_nodes_finite[folded DCA.nodes_def DRA.nodes_def] + lemmas intersect_bc_nodes_card = intersection_bc.product_nodes_card[folded DCA.nodes_def DRA.nodes_def] (* TODO: are there some statements about the rabin constant hidden in here? same for gen/cogen, also in other combinations, shouldn't have to unfold those *) global_interpretation union_list: automaton_union_list_run dra.dra dra.alphabet dra.initial dra.transition dra.condition "\ P w r p. cogen rabin P (p ## r)" dra.dra dra.alphabet dra.initial dra.transition dra.condition "\ P w r p. cogen rabin P (p ## r)" "\ cs. do { k \ [0 ..< length cs]; (f, g) \ cs ! k; [(\ pp. f (pp ! k), \ pp. g (pp ! k))] }" - defines union_list = union_list.combine + defines union_list = union_list.product by (unfold_locales) (auto simp: cogen_def rabin_def comp_def split_beta) - lemmas union_list_language = union_list.combine_language - lemmas union_list_nodes_finite = union_list.combine_nodes_finite - lemmas union_list_nodes_card = union_list.combine_nodes_card + lemmas union_list_language = union_list.product_language + lemmas union_list_nodes_finite = union_list.product_nodes_finite + lemmas union_list_nodes_card = union_list.product_nodes_card end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy b/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy --- a/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy +++ b/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy @@ -1,589 +1,589 @@ section \Deterministic Automata\ theory Deterministic imports "../Transition_Systems/Transition_System" "../Transition_Systems/Transition_System_Extra" "../Transition_Systems/Transition_System_Construction" "../Basic/Degeneralization" begin locale automaton = fixes automaton :: "'label set \ 'state \ ('label \ 'state \ 'state) \ 'condition \ 'automaton" fixes alphabet initial transition condition assumes automaton[simp]: "automaton (alphabet A) (initial A) (transition A) (condition A) = A" assumes alphabet[simp]: "alphabet (automaton a i t c) = a" assumes initial[simp]: "initial (automaton a i t c) = i" assumes transition[simp]: "transition (automaton a i t c) = t" assumes condition[simp]: "condition (automaton a i t c) = c" begin (* TODO: is there a way to use defines without renaming the constants? *) sublocale transition_system_initial "transition A" "\ a p. a \ alphabet A" "\ p. p = initial A" for A defines path' = path and run' = run and reachable' = reachable and nodes' = nodes by this lemma path_alt_def: "path A w p \ w \ lists (alphabet A)" proof show "w \ lists (alphabet A)" if "path A w p" using that by (induct arbitrary: p) (auto) show "path A w p" if "w \ lists (alphabet A)" using that by (induct arbitrary: p) (auto) qed lemma run_alt_def: "run A w p \ w \ streams (alphabet A)" proof show "w \ streams (alphabet A)" if "run A w p" using that by (coinduction arbitrary: w p) (force elim: run.cases) show "run A w p" if "w \ streams (alphabet A)" using that by (coinduction arbitrary: w p) (force elim: streams.cases) qed end locale automaton_path = automaton automaton alphabet initial transition condition for automaton :: "'label set \ 'state \ ('label \ 'state \ 'state) \ 'condition \ 'automaton" and alphabet initial transition condition + fixes test :: "'condition \ 'label list \ 'state list \ 'state \ bool" begin definition language :: "'automaton \ 'label list set" where "language A \ {w. path A w (initial A) \ test (condition A) w (states A w (initial A)) (initial A)}" lemma language[intro]: assumes "path A w (initial A)" "test (condition A) w (states A w (initial A)) (initial A)" shows "w \ language A" using assms unfolding language_def by auto lemma language_elim[elim]: assumes "w \ language A" obtains "path A w (initial A)" "test (condition A) w (states A w (initial A)) (initial A)" using assms unfolding language_def by auto lemma language_alphabet: "language A \ lists (alphabet A)" using path_alt_def by auto end locale automaton_run = automaton automaton alphabet initial transition condition for automaton :: "'label set \ 'state \ ('label \ 'state \ 'state) \ 'condition \ 'automaton" and alphabet initial transition condition + fixes test :: "'condition \ 'label stream \ 'state stream \ 'state \ bool" begin definition language :: "'automaton \ 'label stream set" where "language A \ {w. run A w (initial A) \ test (condition A) w (trace A w (initial A)) (initial A)}" lemma language[intro]: assumes "run A w (initial A)" "test (condition A) w (trace A w (initial A)) (initial A)" shows "w \ language A" using assms unfolding language_def by auto lemma language_elim[elim]: assumes "w \ language A" obtains "run A w (initial A)" "test (condition A) w (trace A w (initial A)) (initial A)" using assms unfolding language_def by auto lemma language_alphabet: "language A \ streams (alphabet A)" using run_alt_def by auto end locale automaton_degeneralization = a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 + b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 for automaton\<^sub>1 :: "'label set \ 'state \ ('label \ 'state \ 'state) \ 'item pred gen \ 'automaton\<^sub>1" and alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 and automaton\<^sub>2 :: "'label set \ 'state degen \ ('label \ 'state degen \ 'state degen) \ 'item_degen pred \ 'automaton\<^sub>2" and alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 + fixes item :: "'state \ 'label \ 'state \ 'item" fixes translate :: "'item_degen \ 'item degen" begin definition degeneralize :: "'automaton\<^sub>1 \ 'automaton\<^sub>2" where "degeneralize A \ automaton\<^sub>2 (alphabet\<^sub>1 A) (initial\<^sub>1 A, 0) (\ a (p, k). (transition\<^sub>1 A a p, count (condition\<^sub>1 A) (item (p, a, transition\<^sub>1 A a p)) k)) (degen (condition\<^sub>1 A) \ translate)" lemma degeneralize_simps[simp]: "alphabet\<^sub>2 (degeneralize A) = alphabet\<^sub>1 A" "initial\<^sub>2 (degeneralize A) = (initial\<^sub>1 A, 0)" "transition\<^sub>2 (degeneralize A) a (p, k) = (transition\<^sub>1 A a p, count (condition\<^sub>1 A) (item (p, a, transition\<^sub>1 A a p)) k)" "condition\<^sub>2 (degeneralize A) = degen (condition\<^sub>1 A) \ translate" unfolding degeneralize_def by auto lemma degeneralize_target[simp]: "b.target (degeneralize A) w (p, k) = (a.target A w p, fold (count (condition\<^sub>1 A) \ item) (p # a.states A w p || w || a.states A w p) k)" by (induct w arbitrary: p k) (auto) lemma degeneralize_states[simp]: "b.states (degeneralize A) w (p, k) = a.states A w p || scan (count (condition\<^sub>1 A) \ item) (p # a.states A w p || w || a.states A w p) k" by (induct w arbitrary: p k) (auto) lemma degeneralize_trace[simp]: "b.trace (degeneralize A) w (p, k) = a.trace A w p ||| sscan (count (condition\<^sub>1 A) \ item) (p ## a.trace A w p ||| w ||| a.trace A w p) k" by (coinduction arbitrary: w p k) (auto, metis sscan.code) lemma degeneralize_path[iff]: "b.path (degeneralize A) w (p, k) \ a.path A w p" unfolding a.path_alt_def b.path_alt_def by simp lemma degeneralize_run[iff]: "b.run (degeneralize A) w (p, k) \ a.run A w p" unfolding a.run_alt_def b.run_alt_def by simp lemma degeneralize_reachable_fst[simp]: "fst ` b.reachable (degeneralize A) (p, k) = a.reachable A p" unfolding a.reachable_alt_def b.reachable_alt_def image_def by simp lemma degeneralize_reachable_snd_empty[simp]: assumes "condition\<^sub>1 A = []" shows "snd ` b.reachable (degeneralize A) (p, k) = {k}" proof - have "snd ql = k" if "ql \ b.reachable (degeneralize A) (p, k)" for ql using that assms by induct auto then show ?thesis by auto qed lemma degeneralize_reachable_empty[simp]: assumes "condition\<^sub>1 A = []" shows "b.reachable (degeneralize A) (p, k) = a.reachable A p \ {k}" using degeneralize_reachable_fst degeneralize_reachable_snd_empty assms by (metis prod_singleton(2)) lemma degeneralize_reachable_snd: "snd ` b.reachable (degeneralize A) (p, k) \ insert k {0 ..< length (condition\<^sub>1 A)}" by (cases "condition\<^sub>1 A = []") (auto) lemma degeneralize_reachable: "b.reachable (degeneralize A) (p, k) \ a.reachable A p \ insert k {0 ..< length (condition\<^sub>1 A)}" by (cases "condition\<^sub>1 A = []") (auto 0 3) lemma degeneralize_nodes_fst[simp]: "fst ` b.nodes (degeneralize A) = a.nodes A" unfolding a.nodes_alt_def b.nodes_alt_def by simp lemma degeneralize_nodes_snd_empty: assumes "condition\<^sub>1 A = []" shows "snd ` b.nodes (degeneralize A) = {0}" using assms unfolding b.nodes_alt_def by auto lemma degeneralize_nodes_empty: assumes "condition\<^sub>1 A = []" shows "b.nodes (degeneralize A) = a.nodes A \ {0}" using assms unfolding b.nodes_alt_def by auto lemma degeneralize_nodes_snd: "snd ` b.nodes (degeneralize A) \ insert 0 {0 ..< length (condition\<^sub>1 A)}" using degeneralize_reachable_snd unfolding b.nodes_alt_def by auto lemma degeneralize_nodes: "b.nodes (degeneralize A) \ a.nodes A \ insert 0 {0 ..< length (condition\<^sub>1 A)}" using degeneralize_reachable unfolding a.nodes_alt_def b.nodes_alt_def by simp lemma degeneralize_nodes_finite[iff]: "finite (b.nodes (degeneralize A)) \ finite (a.nodes A)" proof show "finite (a.nodes A)" if "finite (b.nodes (degeneralize A))" using that by (auto simp flip: degeneralize_nodes_fst) show "finite (b.nodes (degeneralize A))" if "finite (a.nodes A)" using finite_subset degeneralize_nodes that by blast qed lemma degeneralize_nodes_card: "card (b.nodes (degeneralize A)) \ max 1 (length (condition\<^sub>1 A)) * card (a.nodes A)" proof (cases "finite (a.nodes A)") case True have "card (b.nodes (degeneralize A)) \ card (a.nodes A \ insert 0 {0 ..< length (condition\<^sub>1 A)})" using degeneralize_nodes True by (blast intro: card_mono) also have "\ = card (insert 0 {0 ..< length (condition\<^sub>1 A)}) * card (a.nodes A)" unfolding card_cartesian_product by simp also have "card (insert 0 {0 ..< length (condition\<^sub>1 A)}) = max 1 (length (condition\<^sub>1 A))" by (simp add: card_insert_if Suc_leI max_absorb2) finally show ?thesis by this next case False then have "card (a.nodes A) = 0" "card (b.nodes (degeneralize A)) = 0" by auto then show ?thesis by simp qed end locale automaton_degeneralization_run = automaton_degeneralization automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 item translate + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and item translate + assumes test[iff]: "test\<^sub>2 (degen cs \ translate) w (r ||| sscan (count cs \ item) (p ## r ||| w ||| r) k) (p, k) \ test\<^sub>1 cs w r p" begin lemma degeneralize_language[simp]: "b.language (degeneralize A) = a.language A" by force end - locale automaton_combination = + locale automaton_product = a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 + b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 + c: automaton automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 for automaton\<^sub>1 :: "'label set \ 'state\<^sub>1 \ ('label \ 'state\<^sub>1 \ 'state\<^sub>1) \ 'condition\<^sub>1 \ 'automaton\<^sub>1" and alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 and automaton\<^sub>2 :: "'label set \ 'state\<^sub>2 \ ('label \ 'state\<^sub>2 \ 'state\<^sub>2) \ 'condition\<^sub>2 \ 'automaton\<^sub>2" and alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 and automaton\<^sub>3 :: "'label set \ 'state\<^sub>1 \ 'state\<^sub>2 \ ('label \ 'state\<^sub>1 \ 'state\<^sub>2 \ 'state\<^sub>1 \ 'state\<^sub>2) \ 'condition\<^sub>3 \ 'automaton\<^sub>3" and alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 + fixes condition :: "'condition\<^sub>1 \ 'condition\<^sub>2 \ 'condition\<^sub>3" begin - definition combine :: "'automaton\<^sub>1 \ 'automaton\<^sub>2 \ 'automaton\<^sub>3" where - "combine A B \ automaton\<^sub>3 + definition product :: "'automaton\<^sub>1 \ 'automaton\<^sub>2 \ 'automaton\<^sub>3" where + "product A B \ automaton\<^sub>3 (alphabet\<^sub>1 A \ alphabet\<^sub>2 B) (initial\<^sub>1 A, initial\<^sub>2 B) (\ a (p, q). (transition\<^sub>1 A a p, transition\<^sub>2 B a q)) (condition (condition\<^sub>1 A) (condition\<^sub>2 B))" - lemma combine_simps[simp]: - "alphabet\<^sub>3 (combine A B) = alphabet\<^sub>1 A \ alphabet\<^sub>2 B" - "initial\<^sub>3 (combine A B) = (initial\<^sub>1 A, initial\<^sub>2 B)" - "transition\<^sub>3 (combine A B) a (p, q) = (transition\<^sub>1 A a p, transition\<^sub>2 B a q)" - "condition\<^sub>3 (combine A B) = condition (condition\<^sub>1 A) (condition\<^sub>2 B)" - unfolding combine_def by auto + lemma product_simps[simp]: + "alphabet\<^sub>3 (product A B) = alphabet\<^sub>1 A \ alphabet\<^sub>2 B" + "initial\<^sub>3 (product A B) = (initial\<^sub>1 A, initial\<^sub>2 B)" + "transition\<^sub>3 (product A B) a (p, q) = (transition\<^sub>1 A a p, transition\<^sub>2 B a q)" + "condition\<^sub>3 (product A B) = condition (condition\<^sub>1 A) (condition\<^sub>2 B)" + unfolding product_def by auto - lemma combine_target[simp]: "c.target (combine A B) w (p, q) = (a.target A w p, b.target B w q)" + lemma product_target[simp]: "c.target (product A B) w (p, q) = (a.target A w p, b.target B w q)" by (induct w arbitrary: p q) (auto) - lemma combine_states[simp]: "c.states (combine A B) w (p, q) = a.states A w p || b.states B w q" + lemma product_states[simp]: "c.states (product A B) w (p, q) = a.states A w p || b.states B w q" by (induct w arbitrary: p q) (auto) - lemma combine_trace[simp]: "c.trace (combine A B) w (p, q) = a.trace A w p ||| b.trace B w q" + lemma product_trace[simp]: "c.trace (product A B) w (p, q) = a.trace A w p ||| b.trace B w q" by (coinduction arbitrary: w p q) (auto) - lemma combine_path[iff]: "c.path (combine A B) w (p, q) \ a.path A w p \ b.path B w q" + lemma product_path[iff]: "c.path (product A B) w (p, q) \ a.path A w p \ b.path B w q" unfolding a.path_alt_def b.path_alt_def c.path_alt_def by simp - lemma combine_run[iff]: "c.run (combine A B) w (p, q) \ a.run A w p \ b.run B w q" + lemma product_run[iff]: "c.run (product A B) w (p, q) \ a.run A w p \ b.run B w q" unfolding a.run_alt_def b.run_alt_def c.run_alt_def by simp - lemma combine_reachable[simp]: "c.reachable (combine A B) (p, q) \ a.reachable A p \ b.reachable B q" + lemma product_reachable[simp]: "c.reachable (product A B) (p, q) \ a.reachable A p \ b.reachable B q" unfolding c.reachable_alt_def by auto - lemma combine_nodes[simp]: "c.nodes (combine A B) \ a.nodes A \ b.nodes B" + lemma product_nodes[simp]: "c.nodes (product A B) \ a.nodes A \ b.nodes B" unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def by auto - lemma combine_reachable_fst[simp]: + lemma product_reachable_fst[simp]: assumes "alphabet\<^sub>1 A \ alphabet\<^sub>2 B" - shows "fst ` c.reachable (combine A B) (p, q) = a.reachable A p" - using assms - unfolding a.reachable_alt_def a.path_alt_def - unfolding b.reachable_alt_def b.path_alt_def - unfolding c.reachable_alt_def c.path_alt_def - by auto force - lemma combine_reachable_snd[simp]: - assumes "alphabet\<^sub>1 A \ alphabet\<^sub>2 B" - shows "snd ` c.reachable (combine A B) (p, q) = b.reachable B q" + shows "fst ` c.reachable (product A B) (p, q) = a.reachable A p" using assms unfolding a.reachable_alt_def a.path_alt_def unfolding b.reachable_alt_def b.path_alt_def unfolding c.reachable_alt_def c.path_alt_def by auto force - lemma combine_nodes_fst[simp]: + lemma product_reachable_snd[simp]: + assumes "alphabet\<^sub>1 A \ alphabet\<^sub>2 B" + shows "snd ` c.reachable (product A B) (p, q) = b.reachable B q" + using assms + unfolding a.reachable_alt_def a.path_alt_def + unfolding b.reachable_alt_def b.path_alt_def + unfolding c.reachable_alt_def c.path_alt_def + by auto force + lemma product_nodes_fst[simp]: assumes "alphabet\<^sub>1 A \ alphabet\<^sub>2 B" - shows "fst ` c.nodes (combine A B) = a.nodes A" - using assms combine_reachable_fst + shows "fst ` c.nodes (product A B) = a.nodes A" + using assms product_reachable_fst unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def by fastforce - lemma combine_nodes_snd[simp]: + lemma product_nodes_snd[simp]: assumes "alphabet\<^sub>1 A \ alphabet\<^sub>2 B" - shows "snd ` c.nodes (combine A B) = b.nodes B" - using assms combine_reachable_snd + shows "snd ` c.nodes (product A B) = b.nodes B" + using assms product_reachable_snd unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def by fastforce - lemma combine_nodes_finite[intro]: + lemma product_nodes_finite[intro]: assumes "finite (a.nodes A)" "finite (b.nodes B)" - shows "finite (c.nodes (combine A B))" + shows "finite (c.nodes (product A B))" proof (rule finite_subset) - show "c.nodes (combine A B) \ a.nodes A \ b.nodes B" using combine_nodes by this + show "c.nodes (product A B) \ a.nodes A \ b.nodes B" using product_nodes by this show "finite (a.nodes A \ b.nodes B)" using assms by simp qed - lemma combine_nodes_finite_strong[iff]: + lemma product_nodes_finite_strong[iff]: assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B" - shows "finite (c.nodes (combine A B)) \ finite (a.nodes A) \ finite (b.nodes B)" + shows "finite (c.nodes (product A B)) \ finite (a.nodes A) \ finite (b.nodes B)" proof safe - show "finite (a.nodes A)" if "finite (c.nodes (combine A B))" - using combine_nodes_fst assms that by (metis finite_imageI equalityD1) - show "finite (b.nodes B)" if "finite (c.nodes (combine A B))" - using combine_nodes_snd assms that by (metis finite_imageI equalityD2) - show "finite (c.nodes (combine A B))" if "finite (a.nodes A)" "finite (b.nodes B)" + show "finite (a.nodes A)" if "finite (c.nodes (product A B))" + using product_nodes_fst assms that by (metis finite_imageI equalityD1) + show "finite (b.nodes B)" if "finite (c.nodes (product A B))" + using product_nodes_snd assms that by (metis finite_imageI equalityD2) + show "finite (c.nodes (product A B))" if "finite (a.nodes A)" "finite (b.nodes B)" using that by rule qed - lemma combine_nodes_card[intro]: + lemma product_nodes_card[intro]: assumes "finite (a.nodes A)" "finite (b.nodes B)" - shows "card (c.nodes (combine A B)) \ card (a.nodes A) * card (b.nodes B)" + shows "card (c.nodes (product A B)) \ card (a.nodes A) * card (b.nodes B)" proof - - have "card (c.nodes (combine A B)) \ card (a.nodes A \ b.nodes B)" + have "card (c.nodes (product A B)) \ card (a.nodes A \ b.nodes B)" proof (rule card_mono) show "finite (a.nodes A \ b.nodes B)" using assms by simp - show "c.nodes (combine A B) \ a.nodes A \ b.nodes B" using combine_nodes by this + show "c.nodes (product A B) \ a.nodes A \ b.nodes B" using product_nodes by this qed also have "\ = card (a.nodes A) * card (b.nodes B)" using card_cartesian_product by this finally show ?thesis by this qed - lemma combine_nodes_card_strong[intro]: + lemma product_nodes_card_strong[intro]: assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B" - shows "card (c.nodes (combine A B)) \ card (a.nodes A) * card (b.nodes B)" + shows "card (c.nodes (product A B)) \ card (a.nodes A) * card (b.nodes B)" proof (cases "finite (a.nodes A) \ finite (b.nodes B)") case True show ?thesis using True by auto next case False - have 1: "card (c.nodes (combine A B)) = 0" using False assms by simp + have 1: "card (c.nodes (product A B)) = 0" using False assms by simp have 2: "card (a.nodes A) * card (b.nodes B) = 0" using False by auto show ?thesis using 1 2 by simp qed end locale automaton_intersection_path = - automaton_combination + automaton_product automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition + a: automaton_path automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_path automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 + c: automaton_path automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 and condition + assumes test[iff]: "length r = length s \ test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (r || s) (p, q) \ test\<^sub>1 c\<^sub>1 w r p \ test\<^sub>2 c\<^sub>2 w s q" begin - lemma combine_language[simp]: "c.language (combine A B) = a.language A \ b.language B" by force + lemma product_language[simp]: "c.language (product A B) = a.language A \ b.language B" by force end locale automaton_union_path = - automaton_combination + automaton_product automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition + a: automaton_path automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_path automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 + c: automaton_path automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 and condition + assumes test[iff]: "length r = length s \ test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (r || s) (p, q) \ test\<^sub>1 c\<^sub>1 w r p \ test\<^sub>2 c\<^sub>2 w s q" begin - lemma combine_language[simp]: + lemma product_language[simp]: assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B" - shows "c.language (combine A B) = a.language A \ b.language B" + shows "c.language (product A B) = a.language A \ b.language B" using assms by (force simp: a.path_alt_def b.path_alt_def) end locale automaton_intersection_run = - automaton_combination + automaton_product automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 + c: automaton_run automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 and condition + assumes test[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (r ||| s) (p, q) \ test\<^sub>1 c\<^sub>1 w r p \ test\<^sub>2 c\<^sub>2 w s q" begin - lemma combine_language[simp]: "c.language (combine A B) = a.language A \ b.language B" by force + lemma product_language[simp]: "c.language (product A B) = a.language A \ b.language B" by force end locale automaton_union_run = - automaton_combination + automaton_product automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 + c: automaton_run automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 and condition + assumes test[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (r ||| s) (p, q) \ test\<^sub>1 c\<^sub>1 w r p \ test\<^sub>2 c\<^sub>2 w s q" begin - lemma combine_language[simp]: + lemma product_language[simp]: assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B" - shows "c.language (combine A B) = a.language A \ b.language B" + shows "c.language (product A B) = a.language A \ b.language B" using assms by (force simp: a.run_alt_def b.run_alt_def) end (* TODO: complete this in analogy to the pair case *) - locale automaton_combination_list = + locale automaton_product_list = a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 + b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 for automaton\<^sub>1 :: "'label set \ 'state \ ('label \ 'state \ 'state) \ 'condition\<^sub>1 \ 'automaton\<^sub>1" and alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 and automaton\<^sub>2 :: "'label set \ 'state list \ ('label \ 'state list \ 'state list) \ 'condition\<^sub>2 \ 'automaton\<^sub>2" and alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 + fixes condition :: "'condition\<^sub>1 list \ 'condition\<^sub>2" begin - definition combine :: "'automaton\<^sub>1 list \ 'automaton\<^sub>2" where - "combine AA \ automaton\<^sub>2 + definition product :: "'automaton\<^sub>1 list \ 'automaton\<^sub>2" where + "product AA \ automaton\<^sub>2 (\ (alphabet\<^sub>1 ` set AA)) (map initial\<^sub>1 AA) (\ a ps. map2 (\ A p. transition\<^sub>1 A a p) AA ps) (condition (map condition\<^sub>1 AA))" - lemma combine_simps[simp]: - "alphabet\<^sub>2 (combine AA) = \ (alphabet\<^sub>1 ` set AA)" - "initial\<^sub>2 (combine AA) = map initial\<^sub>1 AA" - "transition\<^sub>2 (combine AA) a ps = map2 (\ A p. transition\<^sub>1 A a p) AA ps" - "condition\<^sub>2 (combine AA) = condition (map condition\<^sub>1 AA)" - unfolding combine_def by auto + lemma product_simps[simp]: + "alphabet\<^sub>2 (product AA) = \ (alphabet\<^sub>1 ` set AA)" + "initial\<^sub>2 (product AA) = map initial\<^sub>1 AA" + "transition\<^sub>2 (product AA) a ps = map2 (\ A p. transition\<^sub>1 A a p) AA ps" + "condition\<^sub>2 (product AA) = condition (map condition\<^sub>1 AA)" + unfolding product_def by auto (* TODO: get rid of indices, express this using stranspose and listset *) - lemma combine_trace_smap: + lemma product_trace_smap: assumes "length ps = length AA" "k < length AA" - shows "smap (\ ps. ps ! k) (b.trace (combine AA) w ps) = a.trace (AA ! k) w (ps ! k)" + shows "smap (\ ps. ps ! k) (b.trace (product AA) w ps) = a.trace (AA ! k) w (ps ! k)" using assms by (coinduction arbitrary: w ps) (force) - lemma combine_nodes: "b.nodes (combine AA) \ listset (map a.nodes AA)" + lemma product_nodes: "b.nodes (product AA) \ listset (map a.nodes AA)" proof - show "ps \ listset (map a.nodes AA)" if "ps \ b.nodes (combine AA)" for ps + show "ps \ listset (map a.nodes AA)" if "ps \ b.nodes (product AA)" for ps using that by (induct) (auto simp: listset_member list_all2_conv_all_nth) qed - lemma combine_nodes_finite[intro]: + lemma product_nodes_finite[intro]: assumes "list_all (finite \ a.nodes) AA" - shows "finite (b.nodes (combine AA))" - using list.pred_map combine_nodes assms by (blast dest: finite_subset) - lemma combine_nodes_card: + shows "finite (b.nodes (product AA))" + using list.pred_map product_nodes assms by (blast dest: finite_subset) + lemma product_nodes_card: assumes "list_all (finite \ a.nodes) AA" - shows "card (b.nodes (combine AA)) \ prod_list (map (card \ a.nodes) AA)" + shows "card (b.nodes (product AA)) \ prod_list (map (card \ a.nodes) AA)" proof - - have "card (b.nodes (combine AA)) \ card (listset (map a.nodes AA))" - using list.pred_map combine_nodes assms by (blast intro: card_mono) + have "card (b.nodes (product AA)) \ card (listset (map a.nodes AA))" + using list.pred_map product_nodes assms by (blast intro: card_mono) also have "\ = prod_list (map (card \ a.nodes) AA)" by simp finally show ?thesis by this qed end locale automaton_intersection_list_run = - automaton_combination_list + automaton_product_list automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 condition + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and condition + assumes test[iff]: "test\<^sub>2 (condition cs) w rs ps \ (\ k < length cs. test\<^sub>1 (cs ! k) w (smap (\ ps. ps ! k) rs) (ps ! k))" begin - lemma combine_language[simp]: "b.language (combine AA) = \ (a.language ` set AA)" + lemma product_language[simp]: "b.language (product AA) = \ (a.language ` set AA)" unfolding a.language_def b.language_def unfolding a.run_alt_def b.run_alt_def streams_iff_sset - by (fastforce simp: set_conv_nth combine_trace_smap) + by (fastforce simp: set_conv_nth product_trace_smap) end locale automaton_union_list_run = - automaton_combination_list + automaton_product_list automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 condition + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and condition + assumes test[iff]: "test\<^sub>2 (condition cs) w rs ps \ (\ k < length cs. test\<^sub>1 (cs ! k) w (smap (\ ps. ps ! k) rs) (ps ! k))" begin - lemma combine_language[simp]: + lemma product_language[simp]: assumes "\ (alphabet\<^sub>1 ` set AA) = \ (alphabet\<^sub>1 ` set AA)" - shows "b.language (combine AA) = \ (a.language ` set AA)" + shows "b.language (product AA) = \ (a.language ` set AA)" using assms unfolding a.language_def b.language_def unfolding a.run_alt_def b.run_alt_def streams_iff_sset - by (fastforce simp: set_conv_nth combine_trace_smap) + by (fastforce simp: set_conv_nth product_trace_smap) end locale automaton_complement = a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 + b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 for automaton\<^sub>1 :: "'label set \ 'state \ ('label \ 'state \ 'state) \ 'condition\<^sub>1 \ 'automaton\<^sub>1" and alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 and automaton\<^sub>2 :: "'label set \ 'state \ ('label \ 'state \ 'state) \ 'condition\<^sub>2 \ 'automaton\<^sub>2" and alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 + fixes condition :: "'condition\<^sub>1 \ 'condition\<^sub>2" begin definition complement :: "'automaton\<^sub>1 \ 'automaton\<^sub>2" where "complement A \ automaton\<^sub>2 (alphabet\<^sub>1 A) (initial\<^sub>1 A) (transition\<^sub>1 A) (condition (condition\<^sub>1 A))" lemma combine_simps[simp]: "alphabet\<^sub>2 (complement A) = alphabet\<^sub>1 A" "initial\<^sub>2 (complement A) = initial\<^sub>1 A" "transition\<^sub>2 (complement A) = transition\<^sub>1 A" "condition\<^sub>2 (complement A) = condition (condition\<^sub>1 A)" unfolding complement_def by auto end locale automaton_complement_path = automaton_complement automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 condition + a: automaton_path automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_path automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and condition + assumes test[iff]: "test\<^sub>2 (condition c) w r p \ \ test\<^sub>1 c w r p" begin lemma complement_language[simp]: "b.language (complement A) = lists (alphabet\<^sub>1 A) - a.language A" unfolding a.language_def b.language_def a.path_alt_def b.path_alt_def by auto end locale automaton_complement_run = automaton_complement automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 condition + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and condition + assumes test[iff]: "test\<^sub>2 (condition c) w r p \ \ test\<^sub>1 c w r p" begin lemma complement_language[simp]: "b.language (complement A) = streams (alphabet\<^sub>1 A) - a.language A" unfolding a.language_def b.language_def a.run_alt_def b.run_alt_def by auto end end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy @@ -1,90 +1,90 @@ section \Nondeterministic Büchi Automata Combinations\ theory NBA_Combine imports NBA NGBA begin global_interpretation degeneralization: automaton_degeneralization_run ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "\ P w r p. gen infs P (p ## r)" nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" fst id defines degeneralize = degeneralization.degeneralize by (unfold_locales) (auto simp flip: sscan_smap) lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded NBA.language_def] lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded NBA.nodes_def] global_interpretation intersection: automaton_intersection_run nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "\ P w r p. gen infs P (p ## r)" "\ c\<^sub>1 c\<^sub>2. [c\<^sub>1 \ fst, c\<^sub>2 \ snd]" - defines intersect' = intersection.intersect + defines intersect' = intersection.product by unfold_locales auto - lemmas intersect'_language[simp] = intersection.intersect_language[folded NGBA.language_def] - lemmas intersect'_nodes_finite[intro] = intersection.intersect_nodes_finite[folded NGBA.nodes_def] + lemmas intersect'_language[simp] = intersection.product_language[folded NGBA.language_def] + lemmas intersect'_nodes_finite[intro] = intersection.product_nodes_finite[folded NGBA.nodes_def] global_interpretation union: automaton_union_run nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" case_sum - defines union = union.union + defines union = union.sum by (unfold_locales) (auto simp: comp_def) - lemmas union_language = union.union_language - lemmas union_nodes_finite = union.union_nodes_finite + lemmas union_language = union.sum_language + lemmas union_nodes_finite = union.sum_nodes_finite global_interpretation intersection_list: automaton_intersection_list_run nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "\ P w r p. gen infs P (p ## r)" "\ cs. map (\ k ps. (cs ! k) (ps ! k)) [0 ..< length cs]" - defines intersect_list' = intersection_list.intersect + defines intersect_list' = intersection_list.product proof unfold_locales fix cs :: "('b \ bool) list" and rs :: "'b stream list" and w :: "'a stream" and ps :: "'b list" assume 1: "length rs = length cs" "length ps = length cs" have "gen infs (map (\ k pp. (cs ! k) (pp ! k)) [0 ..< length cs]) (ps ## stranspose rs) \ (\ k < length cs. infs (\ pp. (cs ! k) (pp ! k)) (ps ## stranspose rs))" by (auto simp: gen_def) also have "\ \ (\ k < length cs. infs (cs ! k) (smap (\ pp. pp ! k) (ps ## stranspose rs)))" by (simp add: comp_def) also have "\ \ (\ k < length cs. infs (cs ! k) (rs ! k))" using 1 by simp also have "\ \ list_all (\ (c, r, p). infs c (p ## r)) (cs || rs || ps)" using 1 unfolding list_all_length by simp finally show "gen infs (map (\ k ps. (cs ! k) (ps ! k)) [0 ..< length cs]) (ps ## stranspose rs) \ list_all (\ (c, r, p). infs c (p ## r)) (cs || rs || ps)" by this qed - lemmas intersect_list'_language[simp] = intersection_list.intersect_language[folded NGBA.language_def] - lemmas intersect_list'_nodes_finite[intro] = intersection_list.intersect_nodes_finite[folded NGBA.nodes_def] + lemmas intersect_list'_language[simp] = intersection_list.product_language[folded NGBA.language_def] + lemmas intersect_list'_nodes_finite[intro] = intersection_list.product_nodes_finite[folded NGBA.nodes_def] global_interpretation union_list: automaton_union_list_run nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" nba nba.alphabet nba.initial nba.transition nba.accepting "\ P w r p. infs P (p ## r)" "\ cs (k, p). (cs ! k) p" - defines union_list = union_list.union + defines union_list = union_list.sum by (unfold_locales) (auto simp: szip_sconst_smap_fst comp_def) - lemmas union_list_language = union_list.union_language - lemmas union_list_nodes_finite = union_list.union_nodes_finite + lemmas union_list_language = union_list.sum_language + lemmas union_list_nodes_finite = union_list.sum_nodes_finite abbreviation intersect where "intersect A B \ degeneralize (intersect' A B)" lemma intersect_language[simp]: "NBA.language (intersect A B) = NBA.language A \ NBA.language B" by simp lemma intersect_nodes_finite[intro]: assumes "finite (NBA.nodes A)" "finite (NBA.nodes B)" shows "finite (NBA.nodes (intersect A B))" using intersect'_nodes_finite assms by simp abbreviation intersect_list where "intersect_list AA \ degeneralize (intersect_list' AA)" lemma intersect_list_language[simp]: "NBA.language (intersect_list AA) = \ (NBA.language ` set AA)" by simp lemma intersect_list_nodes_finite[intro]: assumes "list_all (finite \ NBA.nodes) AA" shows "finite (NBA.nodes (intersect_list AA))" using intersect_list'_nodes_finite assms by simp end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NGBA_Algorithms.thy @@ -1,61 +1,61 @@ section \Algorithms on Nondeterministic Generalized Büchi Automata\ theory NGBA_Algorithms imports NBA_Algorithms NGBA_Implement NBA_Combine begin subsection \Implementations\ context begin interpretation autoref_syn by this (* TODO: move *) lemma degen_param[param, autoref_rules]: "(degen, degen) \ \S \ bool_rel\ list_rel \ S \\<^sub>r nat_rel \ bool_rel" proof (intro fun_relI) fix cs ds ak bl assume "(cs, ds) \ \S \ bool_rel\ list_rel" "(ak, bl) \ S \\<^sub>r nat_rel" then show "(degen cs ak, degen ds bl) \ bool_rel" unfolding degen_def list_rel_def fun_rel_def list_all2_conv_all_nth by (cases "snd ak < length cs") (auto 0 3) qed (* TODO: move *) lemmas [param] = null_transfer[unfolded pred_bool_Id, to_set] (* TODO: move *) lemma count_param[param, autoref_rules]: "(Degeneralization.count, Degeneralization.count) \ \A \ bool_rel\ list_rel \ A \ nat_rel \ nat_rel" unfolding count_def null_def[symmetric] by parametricity (* TODO: why do we need this? *) lemma degeneralize_alt_def: "degeneralize A = nba (ngba.alphabet A) ((\ p. (p, 0)) ` ngba.initial A) (\ a (p, k). (\ q. (q, Degeneralization.count (ngba.accepting A) p k)) ` ngba.transition A a p) (degen (ngba.accepting A))" unfolding degeneralization.degeneralize_def by auto schematic_goal ngba_degeneralize: "(?f :: ?'a, degeneralize) \ ?R" unfolding degeneralize_alt_def by autoref concrete_definition ngba_degeneralize uses ngba_degeneralize lemmas ngba_degeneralize_refine[autoref_rules] = ngba_degeneralize.refine schematic_goal nba_intersect': assumes [autoref_rules]: "(seq, HOL.eq) \ L \ L \ bool_rel" shows "(?f, intersect') \ \L, S\ nbai_nba_rel \ \L, T\ nbai_nba_rel \ \L, S \\<^sub>r T\ ngbai_ngba_rel" - unfolding intersection.intersect_def by autoref + unfolding intersection.product_def by autoref concrete_definition nba_intersect' uses nba_intersect' lemma nba_intersect'_refine[autoref_rules]: assumes "GEN_OP seq HOL.eq (L \ L \ bool_rel)" shows "(nba_intersect' seq, intersect') \ \L, S\ nbai_nba_rel \ \L, T\ nbai_nba_rel \ \L, S \\<^sub>r T\ ngbai_ngba_rel" using nba_intersect'.refine assms unfolding autoref_tag_defs by this end end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NBTA/NBTA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/NBTA/NBTA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/NBTA/NBTA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NBTA/NBTA_Combine.thy @@ -1,80 +1,80 @@ section \Nondeterministic Büchi Transition Automata Combinations\ theory NBTA_Combine imports NBTA NGBTA begin global_interpretation degeneralization: automaton_degeneralization_run ngbta ngbta.alphabet ngbta.initial ngbta.transition ngbta.accepting "\ P w r p. gen infs P (p ## r ||| w ||| r)" nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" id "\ ((p, k), a, (q, l)). ((p, a, q), k)" defines degeneralize = degeneralization.degeneralize proof fix w :: "'a stream" fix r :: "'b stream" fix cs p k let ?f = "\ ((p, k), a, (q, l)). ((p, a, q), k)" let ?s = "sscan (count cs \ id) (p ## r ||| w ||| r) k" have "infs (degen cs \ ?f) ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) \ infs (degen cs) (smap ?f ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)))" by (simp add: comp_def) also have "smap ?f ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) = (p ## r ||| w ||| r) ||| k ## ?s" by (coinduction arbitrary: p k r w) (auto simp: eq_scons simp flip: szip_unfold sscan_scons) also have "\ = (p ## r ||| w ||| r) ||| k ## sscan (count cs) (p ## r ||| w ||| r) k" by simp also have "infs (degen cs) \ = gen infs cs (p ## r ||| w ||| r)" using degen_infs by this finally show "infs (degen cs \ ?f) ((p, k) ## (r ||| ?s) ||| w ||| (r ||| ?s)) \ gen infs cs (p ## r ||| w ||| r)" by this qed lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded NBTA.language_def] lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded NBTA.nodes_def] global_interpretation intersection: automaton_intersection_run nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" ngbta ngbta.alphabet ngbta.initial ngbta.transition ngbta.accepting "\ P w r p. gen infs P (p ## r ||| w ||| r)" "\ c\<^sub>1 c\<^sub>2. [c\<^sub>1 \ (\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1)), c\<^sub>2 \ (\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2))]" - defines intersect' = intersection.intersect + defines intersect' = intersection.product proof fix w :: "'a stream" fix u :: "'b stream" fix v :: "'c stream" fix c\<^sub>1 c\<^sub>2 p q let ?tfst = "\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>1, a, q\<^sub>1)" let ?tsnd = "\ ((p\<^sub>1, p\<^sub>2), a, (q\<^sub>1, q\<^sub>2)). (p\<^sub>2, a, q\<^sub>2)" have "gen infs [c\<^sub>1 \ ?tfst, c\<^sub>2 \ ?tsnd] ((p, q) ## (u ||| v) ||| w ||| u ||| v) \ infs c\<^sub>1 (smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v)) \ infs c\<^sub>2 (smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v))" unfolding gen_def by (simp add: comp_def) also have "smap ?tfst ((p, q) ## (u ||| v) ||| w ||| u ||| v) = p ## u ||| w ||| u" by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse) also have "smap ?tsnd ((p, q) ## (u ||| v) ||| w ||| u ||| v) = q ## v ||| w ||| v" by (coinduction arbitrary: p q u v w) (auto simp flip: szip_unfold, metis stream.collapse) finally show "gen infs [c\<^sub>1 \ ?tfst, c\<^sub>2 \ ?tsnd] ((p, q) ## (u ||| v) ||| w ||| u ||| v) \ infs c\<^sub>1 (p ## u ||| w ||| u) \ infs c\<^sub>2 (q ## v ||| w ||| v)" by this qed - lemmas intersect'_language[simp] = intersection.intersect_language[folded NGBTA.language_def] - lemmas intersect'_nodes_finite[intro] = intersection.intersect_nodes_finite[folded NGBTA.nodes_def] + lemmas intersect'_language[simp] = intersection.product_language[folded NGBTA.language_def] + lemmas intersect'_nodes_finite[intro] = intersection.product_nodes_finite[folded NGBTA.nodes_def] global_interpretation union: automaton_union_run nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" nbta nbta.alphabet nbta.initial nbta.transition nbta.accepting "\ P w r p. infs P (p ## r ||| w ||| r)" "\ c\<^sub>1 c\<^sub>2 m. case m of (Inl p, a, Inl q) \ c\<^sub>1 (p, a, q) | (Inr p, a, Inr q) \ c\<^sub>2 (p, a, q)" - defines union = union.union + defines union = union.sum by (unfold_locales) (auto simp add: szip_smap_fold comp_def case_prod_unfold simp flip: stream.map) - lemmas union_language = union.union_language - lemmas union_nodes_finite = union.union_nodes_finite + lemmas union_language = union.sum_language + lemmas union_nodes_finite = union.sum_nodes_finite abbreviation intersect where "intersect A B \ degeneralize (intersect' A B)" lemma intersect_language[simp]: "NBTA.language (intersect A B) = NBTA.language A \ NBTA.language B" by simp lemma intersect_nodes_finite[intro]: assumes "finite (NBTA.nodes A)" "finite (NBTA.nodes B)" shows "finite (NBTA.nodes (intersect A B))" using intersect'_nodes_finite assms by simp end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/NFA/NFA.thy b/thys/Transition_Systems_and_Automata/Automata/NFA/NFA.thy --- a/thys/Transition_Systems_and_Automata/Automata/NFA/NFA.thy +++ b/thys/Transition_Systems_and_Automata/Automata/NFA/NFA.thy @@ -1,42 +1,42 @@ section \Nondeterministic Finite Automata\ theory NFA imports "../Nondeterministic" begin datatype ('label, 'state) nfa = nfa (alphabet: "'label set") (initial: "'state set") (transition: "'label \ 'state \ 'state set") (accepting: "'state pred") global_interpretation nfa: automaton nfa alphabet initial transition accepting defines path = nfa.path and run = nfa.run and reachable = nfa.reachable and nodes = nfa.nodes by unfold_locales auto global_interpretation nfa: automaton_path nfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" defines language = nfa.language by standard abbreviation target where "target \ nfa.target" abbreviation states where "states \ nfa.states" abbreviation trace where "trace \ nfa.trace" abbreviation successors where "successors \ nfa.successors TYPE('label)" (* TODO: going from target to last requires states as intermediate step, used in other places too *) global_interpretation nfa: automaton_intersection_path nfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" nfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" nfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" "\ c\<^sub>1 c\<^sub>2 (p, q). c\<^sub>1 p \ c\<^sub>2 q" - defines intersect = nfa.intersect + defines intersect = nfa.product by (unfold_locales) (auto simp: zip_eq_Nil_iff) global_interpretation nfa: automaton_union_path nfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" nfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" nfa alphabet initial transition accepting "\ P w r p. P (last (p # r))" case_sum - defines union = nfa.union + defines union = nfa.sum by (unfold_locales) (auto simp: last_map) end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/Nondeterministic.thy b/thys/Transition_Systems_and_Automata/Automata/Nondeterministic.thy --- a/thys/Transition_Systems_and_Automata/Automata/Nondeterministic.thy +++ b/thys/Transition_Systems_and_Automata/Automata/Nondeterministic.thy @@ -1,761 +1,761 @@ section \Nondeterministic Automata\ theory Nondeterministic imports "../Transition_Systems/Transition_System" "../Transition_Systems/Transition_System_Extra" "../Transition_Systems/Transition_System_Construction" "../Basic/Degeneralization" begin locale automaton = fixes automaton :: "'label set \ 'state set \ ('label \ 'state \ 'state set) \ 'condition \ 'automaton" fixes alphabet initial transition condition assumes automaton[simp]: "automaton (alphabet A) (initial A) (transition A) (condition A) = A" assumes alphabet[simp]: "alphabet (automaton a i t c) = a" assumes initial[simp]: "initial (automaton a i t c) = i" assumes transition[simp]: "transition (automaton a i t c) = t" assumes condition[simp]: "condition (automaton a i t c) = c" begin sublocale transition_system_initial "\ a p. snd a" "\ a p. fst a \ alphabet A \ snd a \ transition A (fst a) p" "\ p. p \ initial A" for A defines path' = path and run' = run and reachable' = reachable and nodes' = nodes by this lemma states_alt_def: "states r p = map snd r" by (induct r arbitrary: p) (auto) lemma trace_alt_def: "trace r p = smap snd r" by (coinduction arbitrary: r p) (auto) lemma successors_alt_def: "successors A p = (\ a \ alphabet A. transition A a p)" by auto lemma reachable_transition[intro]: assumes "a \ alphabet A" "q \ reachable A p" "r \ transition A a q" shows "r \ reachable A p" using reachable.execute assms by force lemma nodes_transition[intro]: assumes "a \ alphabet A" "p \ nodes A" "q \ transition A a p" shows "q \ nodes A" using nodes.execute assms by force lemma path_alphabet: assumes "length r = length w" "path A (w || r) p" shows "w \ lists (alphabet A)" using assms by (induct arbitrary: p rule: list_induct2) (auto) lemma run_alphabet: assumes "run A (w ||| r) p" shows "w \ streams (alphabet A)" using assms by (coinduction arbitrary: w r p) (metis run.cases stream.map szip_smap szip_smap_fst) definition restrict :: "'automaton \ 'automaton" where "restrict A \ automaton (alphabet A) (initial A) (\ a p. if a \ alphabet A then transition A a p else {}) (condition A)" lemma restrict_simps[simp]: "alphabet (restrict A) = alphabet A" "initial (restrict A) = initial A" "transition (restrict A) a p = (if a \ alphabet A then transition A a p else {})" "condition (restrict A) = condition A" unfolding restrict_def by auto lemma restrict_path[simp]: "path (restrict A) = path A" proof (intro ext iffI) show "path A wr p" if "path (restrict A) wr p" for wr p using that by induct auto show "path (restrict A) wr p" if "path A wr p" for wr p using that by induct auto qed lemma restrict_run[simp]: "run (restrict A) = run A" proof (intro ext iffI) show "run A wr p" if "run (restrict A) wr p" for wr p using that by coinduct auto show "run (restrict A) wr p" if "run A wr p" for wr p using that by coinduct auto qed end locale automaton_path = automaton automaton alphabet initial transition condition for automaton :: "'label set \ 'state set \ ('label \ 'state \ 'state set) \ 'condition \ 'automaton" and alphabet initial transition condition + fixes test :: "'condition \ 'label list \ 'state list \ 'state \ bool" begin definition language :: "'automaton \ 'label list set" where "language A \ {w |w r p. length r = length w \ p \ initial A \ path A (w || r) p \ test (condition A) w r p}" lemma language[intro]: assumes "length r = length w" "p \ initial A" "path A (w || r) p" "test (condition A) w r p" shows "w \ language A" using assms unfolding language_def by auto lemma language_elim[elim]: assumes "w \ language A" obtains r p where "length r = length w" "p \ initial A" "path A (w || r) p" "test (condition A) w r p" using assms unfolding language_def by auto lemma language_alphabet: "language A \ lists (alphabet A)" by (auto dest: path_alphabet) lemma restrict_language[simp]: "language (restrict A) = language A" by force end locale automaton_run = automaton automaton alphabet initial transition condition for automaton :: "'label set \ 'state set \ ('label \ 'state \ 'state set) \ 'condition \ 'automaton" and alphabet initial transition condition + fixes test :: "'condition \ 'label stream \ 'state stream \ 'state \ bool" begin definition language :: "'automaton \ 'label stream set" where "language A \ {w |w r p. p \ initial A \ run A (w ||| r) p \ test (condition A) w r p}" lemma language[intro]: assumes "p \ initial A" "run A (w ||| r) p" "test (condition A) w r p" shows "w \ language A" using assms unfolding language_def by auto lemma language_elim[elim]: assumes "w \ language A" obtains r p where "p \ initial A" "run A (w ||| r) p" "test (condition A) w r p" using assms unfolding language_def by auto lemma language_alphabet: "language A \ streams (alphabet A)" by (auto dest: run_alphabet) lemma restrict_language[simp]: "language (restrict A) = language A" by force end locale automaton_degeneralization = a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 + b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 for automaton\<^sub>1 :: "'label set \ 'state set \ ('label \ 'state \ 'state set) \ 'item pred gen \ 'automaton\<^sub>1" and alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 and automaton\<^sub>2 :: "'label set \ 'state degen set \ ('label \ 'state degen \ 'state degen set) \ 'item_degen pred \ 'automaton\<^sub>2" and alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 + fixes item :: "'state \ 'label \ 'state \ 'item" fixes translate :: "'item_degen \ 'item degen" begin definition degeneralize :: "'automaton\<^sub>1 \ 'automaton\<^sub>2" where "degeneralize A \ automaton\<^sub>2 (alphabet\<^sub>1 A) (initial\<^sub>1 A \ {0}) (\ a (p, k). {(q, count (condition\<^sub>1 A) (item (p, a, q)) k) |q. q \ transition\<^sub>1 A a p}) (degen (condition\<^sub>1 A) \ translate)" lemma degeneralize_simps[simp]: "alphabet\<^sub>2 (degeneralize A) = alphabet\<^sub>1 A" "initial\<^sub>2 (degeneralize A) = initial\<^sub>1 A \ {0}" "transition\<^sub>2 (degeneralize A) a (p, k) = {(q, count (condition\<^sub>1 A) (item (p, a, q)) k) |q. q \ transition\<^sub>1 A a p}" "condition\<^sub>2 (degeneralize A) = degen (condition\<^sub>1 A) \ translate" unfolding degeneralize_def by auto lemma run_degeneralize: assumes "a.run A (w ||| r) p" shows "b.run (degeneralize A) (w ||| r ||| sscan (count (condition\<^sub>1 A) \ item) (p ## r ||| w ||| r) k) (p, k)" using assms by (coinduction arbitrary: w r p k) (force elim: a.run.cases) lemma degeneralize_run: assumes "b.run (degeneralize A) (w ||| rs) pk" obtains r s p k where "rs = r ||| s" "pk = (p, k)" "a.run A (w ||| r) p" "s = sscan (count (condition\<^sub>1 A) \ item) (p ## r ||| w ||| r) k" proof - obtain r s p k where 1: "rs = r ||| s" "pk = (p, k)" using szip_smap surjective_pairing by metis show ?thesis proof show "rs = r ||| s" "pk = (p, k)" using 1 by this show "a.run A (w ||| r) p" using assms unfolding 1 by (coinduction arbitrary: w r s p k) (force elim: b.run.cases) show "s = sscan (count (condition\<^sub>1 A) \ item) (p ## r ||| w ||| r) k" using assms unfolding 1 by (coinduction arbitrary: w r s p k) (erule b.run.cases, force) qed qed lemma degeneralize_nodes: "b.nodes (degeneralize A) \ a.nodes A \ insert 0 {0 ..< length (condition\<^sub>1 A)}" proof fix pk assume "pk \ b.nodes (degeneralize A)" then show "pk \ a.nodes A \ insert 0 {0 ..< length (condition\<^sub>1 A)}" by (induct) (force, cases "condition\<^sub>1 A = []", auto) qed lemma nodes_degeneralize: "a.nodes A \ fst ` b.nodes (degeneralize A)" proof fix p assume "p \ a.nodes A" then show "p \ fst ` b.nodes (degeneralize A)" proof induct case (initial p) have "(p, 0) \ b.nodes (degeneralize A)" using initial by auto then show ?case using image_iff fst_conv by force next case (execute p aq) obtain k where "(p, k) \ b.nodes (degeneralize A)" using execute(2) by auto then have "(snd aq, count (condition\<^sub>1 A) (item (p, aq)) k) \ b.nodes (degeneralize A)" using execute(3) by auto then show ?case using image_iff snd_conv by force qed qed lemma degeneralize_nodes_finite[iff]: "finite (b.nodes (degeneralize A)) \ finite (a.nodes A)" proof show "finite (a.nodes A)" if "finite (b.nodes (degeneralize A))" using finite_subset nodes_degeneralize that by blast show "finite (b.nodes (degeneralize A))" if "finite (a.nodes A)" using finite_subset degeneralize_nodes that by blast qed end locale automaton_degeneralization_run = automaton_degeneralization automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 item translate + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and item translate + assumes test[iff]: "test\<^sub>2 (degen cs \ translate) w (r ||| sscan (count cs \ item) (p ## r ||| w ||| r) k) (p, k) \ test\<^sub>1 cs w r p" begin lemma degeneralize_language[simp]: "b.language (degeneralize A) = a.language A" unfolding a.language_def b.language_def by (auto dest: run_degeneralize elim!: degeneralize_run) end - locale automaton_intersection = + locale automaton_product = a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 + b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 + c: automaton automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 for automaton\<^sub>1 :: "'label set \ 'state\<^sub>1 set \ ('label \ 'state\<^sub>1 \ 'state\<^sub>1 set) \ 'condition\<^sub>1 \ 'automaton\<^sub>1" and alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 and automaton\<^sub>2 :: "'label set \ 'state\<^sub>2 set \ ('label \ 'state\<^sub>2 \ 'state\<^sub>2 set) \ 'condition\<^sub>2 \ 'automaton\<^sub>2" and alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 and automaton\<^sub>3 :: "'label set \ ('state\<^sub>1 \ 'state\<^sub>2) set \ ('label \ 'state\<^sub>1 \ 'state\<^sub>2 \ ('state\<^sub>1 \ 'state\<^sub>2) set) \ 'condition\<^sub>3 \ 'automaton\<^sub>3" and alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 + fixes condition :: "'condition\<^sub>1 \ 'condition\<^sub>2 \ 'condition\<^sub>3" begin - definition intersect :: "'automaton\<^sub>1 \ 'automaton\<^sub>2 \ 'automaton\<^sub>3" where - "intersect A B \ automaton\<^sub>3 + definition product :: "'automaton\<^sub>1 \ 'automaton\<^sub>2 \ 'automaton\<^sub>3" where + "product A B \ automaton\<^sub>3 (alphabet\<^sub>1 A \ alphabet\<^sub>2 B) (initial\<^sub>1 A \ initial\<^sub>2 B) (\ a (p, q). transition\<^sub>1 A a p \ transition\<^sub>2 B a q) (condition (condition\<^sub>1 A) (condition\<^sub>2 B))" - lemma intersect_simps[simp]: - "alphabet\<^sub>3 (intersect A B) = alphabet\<^sub>1 A \ alphabet\<^sub>2 B" - "initial\<^sub>3 (intersect A B) = initial\<^sub>1 A \ initial\<^sub>2 B" - "transition\<^sub>3 (intersect A B) a (p, q) = transition\<^sub>1 A a p \ transition\<^sub>2 B a q" - "condition\<^sub>3 (intersect A B) = condition (condition\<^sub>1 A) (condition\<^sub>2 B)" - unfolding intersect_def by auto + lemma product_simps[simp]: + "alphabet\<^sub>3 (product A B) = alphabet\<^sub>1 A \ alphabet\<^sub>2 B" + "initial\<^sub>3 (product A B) = initial\<^sub>1 A \ initial\<^sub>2 B" + "transition\<^sub>3 (product A B) a (p, q) = transition\<^sub>1 A a p \ transition\<^sub>2 B a q" + "condition\<^sub>3 (product A B) = condition (condition\<^sub>1 A) (condition\<^sub>2 B)" + unfolding product_def by auto - lemma intersect_target[simp]: + lemma product_target[simp]: assumes "length w = length r" "length r = length s" shows "c.target (w || r || s) (p, q) = (a.target (w || r) p, b.target (w || s) q)" using assms by (induct arbitrary: p q rule: list_induct3) (auto) - lemma intersect_path[iff]: + lemma product_path[iff]: assumes "length w = length r" "length r = length s" - shows "c.path (intersect A B) (w || r || s) (p, q) \ + shows "c.path (product A B) (w || r || s) (p, q) \ a.path A (w || r) p \ b.path B (w || s) q" using assms by (induct arbitrary: p q rule: list_induct3) (auto) - lemma intersect_run[iff]: "c.run (intersect A B) (w ||| r ||| s) (p, q) \ + lemma product_run[iff]: "c.run (product A B) (w ||| r ||| s) (p, q) \ a.run A (w ||| r) p \ b.run B (w ||| s) q" proof safe - show "a.run A (w ||| r) p" if "c.run (intersect A B) (w ||| r ||| s) (p, q)" + show "a.run A (w ||| r) p" if "c.run (product A B) (w ||| r ||| s) (p, q)" using that by (coinduction arbitrary: w r s p q) (force elim: c.run.cases) - show "b.run B (w ||| s) q" if "c.run (intersect A B) (w ||| r ||| s) (p, q)" + show "b.run B (w ||| s) q" if "c.run (product A B) (w ||| r ||| s) (p, q)" using that by (coinduction arbitrary: w r s p q) (force elim: c.run.cases) - show "c.run (intersect A B) (w ||| r ||| s) (p, q)" if "a.run A (w ||| r) p" "b.run B (w ||| s) q" + show "c.run (product A B) (w ||| r ||| s) (p, q)" if "a.run A (w ||| r) p" "b.run B (w ||| s) q" using that by (coinduction arbitrary: w r s p q) (auto elim: a.run.cases b.run.cases) qed - lemma intersect_nodes: "c.nodes (intersect A B) \ a.nodes A \ b.nodes B" + lemma product_nodes: "c.nodes (product A B) \ a.nodes A \ b.nodes B" proof fix pq - assume "pq \ c.nodes (intersect A B)" + assume "pq \ c.nodes (product A B)" then show "pq \ a.nodes A \ b.nodes B" by induct auto qed - lemma intersect_nodes_finite[intro]: + lemma product_nodes_finite[intro]: assumes "finite (a.nodes A)" "finite (b.nodes B)" - shows "finite (c.nodes (intersect A B))" - using finite_subset intersect_nodes assms by blast + shows "finite (c.nodes (product A B))" + using finite_subset product_nodes assms by blast end locale automaton_intersection_path = - automaton_intersection + automaton_product automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition + a: automaton_path automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_path automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 + c: automaton_path automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 and condition + - assumes test[iff]: "length u = length w \ length v = length w \ - test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (u || v) (p, q) \ test\<^sub>1 c\<^sub>1 w u p \ test\<^sub>2 c\<^sub>2 w v q" + assumes test[iff]: "length r = length w \ length s = length w \ + test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (r || s) (p, q) \ test\<^sub>1 c\<^sub>1 w r p \ test\<^sub>2 c\<^sub>2 w s q" begin - lemma intersect_language[simp]: "c.language (intersect A B) = a.language A \ b.language B" + lemma product_language[simp]: "c.language (product A B) = a.language A \ b.language B" unfolding a.language_def b.language_def c.language_def by (force iff: split_zip) end locale automaton_intersection_run = - automaton_intersection + automaton_product automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 + c: automaton_run automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 and condition + - assumes test[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (u ||| v) (p, q) \ test\<^sub>1 c\<^sub>1 w u p \ test\<^sub>2 c\<^sub>2 w v q" + assumes test[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (r ||| s) (p, q) \ test\<^sub>1 c\<^sub>1 w r p \ test\<^sub>2 c\<^sub>2 w s q" begin - lemma intersect_language[simp]: "c.language (intersect A B) = a.language A \ b.language B" + lemma product_language[simp]: "c.language (product A B) = a.language A \ b.language B" unfolding a.language_def b.language_def c.language_def by (fastforce iff: split_szip) end - locale automaton_union = + locale automaton_sum = a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 + b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 + c: automaton automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 for automaton\<^sub>1 :: "'label set \ 'state\<^sub>1 set \ ('label \ 'state\<^sub>1 \ 'state\<^sub>1 set) \ 'condition\<^sub>1 \ 'automaton\<^sub>1" and alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 and automaton\<^sub>2 :: "'label set \ 'state\<^sub>2 set \ ('label \ 'state\<^sub>2 \ 'state\<^sub>2 set) \ 'condition\<^sub>2 \ 'automaton\<^sub>2" and alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 and automaton\<^sub>3 :: "'label set \ ('state\<^sub>1 + 'state\<^sub>2) set \ ('label \ 'state\<^sub>1 + 'state\<^sub>2 \ ('state\<^sub>1 + 'state\<^sub>2) set) \ 'condition\<^sub>3 \ 'automaton\<^sub>3" and alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 + fixes condition :: "'condition\<^sub>1 \ 'condition\<^sub>2 \ 'condition\<^sub>3" begin - definition union :: "'automaton\<^sub>1 \ 'automaton\<^sub>2 \ 'automaton\<^sub>3" where - "union A B \ automaton\<^sub>3 + definition sum :: "'automaton\<^sub>1 \ 'automaton\<^sub>2 \ 'automaton\<^sub>3" where + "sum A B \ automaton\<^sub>3 (alphabet\<^sub>1 A \ alphabet\<^sub>2 B) (initial\<^sub>1 A <+> initial\<^sub>2 B) (\ a. \ Inl p \ Inl ` transition\<^sub>1 A a p | Inr q \ Inr ` transition\<^sub>2 B a q) (condition (condition\<^sub>1 A) (condition\<^sub>2 B))" - lemma union_simps[simp]: - "alphabet\<^sub>3 (union A B) = alphabet\<^sub>1 A \ alphabet\<^sub>2 B" - "initial\<^sub>3 (union A B) = initial\<^sub>1 A <+> initial\<^sub>2 B" - "transition\<^sub>3 (union A B) a (Inl p) = Inl ` transition\<^sub>1 A a p" - "transition\<^sub>3 (union A B) a (Inr q) = Inr ` transition\<^sub>2 B a q" - "condition\<^sub>3 (union A B) = condition (condition\<^sub>1 A) (condition\<^sub>2 B)" - unfolding union_def by auto + lemma sum_simps[simp]: + "alphabet\<^sub>3 (sum A B) = alphabet\<^sub>1 A \ alphabet\<^sub>2 B" + "initial\<^sub>3 (sum A B) = initial\<^sub>1 A <+> initial\<^sub>2 B" + "transition\<^sub>3 (sum A B) a (Inl p) = Inl ` transition\<^sub>1 A a p" + "transition\<^sub>3 (sum A B) a (Inr q) = Inr ` transition\<^sub>2 B a q" + "condition\<^sub>3 (sum A B) = condition (condition\<^sub>1 A) (condition\<^sub>2 B)" + unfolding sum_def by auto - lemma path_union_a: + lemma path_sum_a: assumes "length r = length w" "a.path A (w || r) p" - shows "c.path (union A B) (w || map Inl r) (Inl p)" + shows "c.path (sum A B) (w || map Inl r) (Inl p)" using assms by (induct arbitrary: p rule: list_induct2) (auto) - lemma path_union_b: + lemma path_sum_b: assumes "length s = length w" "b.path B (w || s) q" - shows "c.path (union A B) (w || map Inr s) (Inr q)" + shows "c.path (sum A B) (w || map Inr s) (Inr q)" using assms by (induct arbitrary: q rule: list_induct2) (auto) - lemma union_path: + lemma sum_path: assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B" - assumes "length rs = length w" "c.path (union A B) (w || rs) pq" + assumes "length rs = length w" "c.path (sum A B) (w || rs) pq" obtains (a) r p where "rs = map Inl r" "pq = Inl p" "a.path A (w || r) p" | (b) s q where "rs = map Inr s" "pq = Inr q" "b.path B (w || s) q" proof (cases pq) case (Inl p) have 1: "rs = map Inl (map projl rs)" using assms(2, 3) unfolding Inl by (induct arbitrary: p rule: list_induct2) (auto) have 2: "a.path A (w || map projl rs) p" using assms(2, 1, 3) unfolding Inl by (induct arbitrary: p rule: list_induct2) (auto) show ?thesis using a 1 Inl 2 by this next case (Inr q) have 1: "rs = map Inr (map projr rs)" using assms(2, 3) unfolding Inr by (induct arbitrary: q rule: list_induct2) (auto) have 2: "b.path B (w || map projr rs) q" using assms(2, 1, 3) unfolding Inr by (induct arbitrary: q rule: list_induct2) (auto) show ?thesis using b 1 Inr 2 by this qed - lemma run_union_a: + lemma run_sum_a: assumes "a.run A (w ||| r) p" - shows "c.run (union A B) (w ||| smap Inl r) (Inl p)" + shows "c.run (sum A B) (w ||| smap Inl r) (Inl p)" using assms by (coinduction arbitrary: w r p) (force elim: a.run.cases) - lemma run_union_b: + lemma run_sum_b: assumes "b.run B (w ||| s) q" - shows "c.run (union A B) (w ||| smap Inr s) (Inr q)" + shows "c.run (sum A B) (w ||| smap Inr s) (Inr q)" using assms by (coinduction arbitrary: w s q) (force elim: b.run.cases) - lemma union_run: + lemma sum_run: assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B" - assumes "c.run (union A B) (w ||| rs) pq" + assumes "c.run (sum A B) (w ||| rs) pq" obtains (a) r p where "rs = smap Inl r" "pq = Inl p" "a.run A (w ||| r) p" | (b) s q where "rs = smap Inr s" "pq = Inr q" "b.run B (w ||| s) q" proof (cases pq) case (Inl p) have 1: "rs = smap Inl (smap projl rs)" using assms(2) unfolding Inl by (coinduction arbitrary: w rs p) (force elim: c.run.cases) have 2: "a.run A (w ||| smap projl rs) p" using assms unfolding Inl by (coinduction arbitrary: w rs p) (force elim: c.run.cases) show ?thesis using a 1 Inl 2 by this next case (Inr q) have 1: "rs = smap Inr (smap projr rs)" using assms(2) unfolding Inr by (coinduction arbitrary: w rs q) (force elim: c.run.cases) have 2: "b.run B (w ||| smap projr rs) q" using assms unfolding Inr by (coinduction arbitrary: w rs q) (force elim: c.run.cases) show ?thesis using b 1 Inr 2 by this qed - lemma union_nodes: + lemma sum_nodes: assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B" - shows "c.nodes (union A B) \ a.nodes A <+> b.nodes B" + shows "c.nodes (sum A B) \ a.nodes A <+> b.nodes B" proof fix pq - assume "pq \ c.nodes (union A B)" + assume "pq \ c.nodes (sum A B)" then show "pq \ a.nodes A <+> b.nodes B" using assms by (induct) (auto 0 3) qed - lemma union_nodes_finite[intro]: + lemma sum_nodes_finite[intro]: assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B" assumes "finite (a.nodes A)" "finite (b.nodes B)" - shows "finite (c.nodes (union A B))" - using finite_subset union_nodes assms by (auto intro: finite_Plus) + shows "finite (c.nodes (sum A B))" + using finite_subset sum_nodes assms by (auto intro: finite_Plus) end locale automaton_union_path = - automaton_union + automaton_sum automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition + a: automaton_path automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_path automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 + c: automaton_path automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 and condition + - assumes test\<^sub>1[iff]: "length u = length w \ test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (map Inl u) (Inl p) \ test\<^sub>1 c\<^sub>1 w u p" - assumes test\<^sub>2[iff]: "length v = length w \ test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (map Inr v) (Inr q) \ test\<^sub>2 c\<^sub>2 w v q" + assumes test\<^sub>1[iff]: "length r = length w \ test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (map Inl r) (Inl p) \ test\<^sub>1 c\<^sub>1 w r p" + assumes test\<^sub>2[iff]: "length s = length w \ test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (map Inr s) (Inr q) \ test\<^sub>2 c\<^sub>2 w s q" begin - lemma union_language[simp]: + lemma sum_language[simp]: assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B" - shows "c.language (union A B) = a.language A \ b.language B" + shows "c.language (sum A B) = a.language A \ b.language B" using assms unfolding a.language_def b.language_def c.language_def - by (force intro: path_union_a path_union_b elim!: union_path) + by (force intro: path_sum_a path_sum_b elim!: sum_path) end locale automaton_union_run = - automaton_union + automaton_sum automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 + c: automaton_run automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3 and condition + - assumes test\<^sub>1[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (smap Inl u) (Inl p) \ test\<^sub>1 c\<^sub>1 w u p" - assumes test\<^sub>2[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (smap Inr v) (Inr q) \ test\<^sub>2 c\<^sub>2 w v q" + assumes test\<^sub>1[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (smap Inl r) (Inl p) \ test\<^sub>1 c\<^sub>1 w r p" + assumes test\<^sub>2[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (smap Inr s) (Inr q) \ test\<^sub>2 c\<^sub>2 w s q" begin - lemma union_language[simp]: + lemma sum_language[simp]: assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B" - shows "c.language (union A B) = a.language A \ b.language B" + shows "c.language (sum A B) = a.language A \ b.language B" using assms unfolding a.language_def b.language_def c.language_def - by (auto intro: run_union_a run_union_b elim!: union_run) + by (auto intro: run_sum_a run_sum_b elim!: sum_run) end - locale automaton_intersection_list = + locale automaton_product_list = a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 + b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 for automaton\<^sub>1 :: "'label set \ 'state set \ ('label \ 'state \ 'state set) \ 'condition\<^sub>1 \ 'automaton\<^sub>1" and alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 and automaton\<^sub>2 :: "'label set \ 'state list set \ ('label \ 'state list \ 'state list set) \ 'condition\<^sub>2 \ 'automaton\<^sub>2" and alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 + fixes condition :: "'condition\<^sub>1 list \ 'condition\<^sub>2" begin - definition intersect :: "'automaton\<^sub>1 list \ 'automaton\<^sub>2" where - "intersect AA \ automaton\<^sub>2 + definition product :: "'automaton\<^sub>1 list \ 'automaton\<^sub>2" where + "product AA \ automaton\<^sub>2 (\ (alphabet\<^sub>1 ` set AA)) (listset (map initial\<^sub>1 AA)) (\ a ps. listset (map2 (\ A p. transition\<^sub>1 A a p) AA ps)) (condition (map condition\<^sub>1 AA))" - lemma intersect_simps[simp]: - "alphabet\<^sub>2 (intersect AA) = \ (alphabet\<^sub>1 ` set AA)" - "initial\<^sub>2 (intersect AA) = listset (map initial\<^sub>1 AA)" - "transition\<^sub>2 (intersect AA) a ps = listset (map2 (\ A p. transition\<^sub>1 A a p) AA ps)" - "condition\<^sub>2 (intersect AA) = condition (map condition\<^sub>1 AA)" - unfolding intersect_def by auto + lemma product_simps[simp]: + "alphabet\<^sub>2 (product AA) = \ (alphabet\<^sub>1 ` set AA)" + "initial\<^sub>2 (product AA) = listset (map initial\<^sub>1 AA)" + "transition\<^sub>2 (product AA) a ps = listset (map2 (\ A p. transition\<^sub>1 A a p) AA ps)" + "condition\<^sub>2 (product AA) = condition (map condition\<^sub>1 AA)" + unfolding product_def by auto - lemma intersect_run_length: + lemma product_run_length: assumes "length ps = length AA" - assumes "b.run (intersect AA) (w ||| r) ps" + assumes "b.run (product AA) (w ||| r) ps" assumes "qs \ sset r" shows "length qs = length AA" proof - have "pred_stream (\ qs. length qs = length AA) r" using assms(1, 2) by (coinduction arbitrary: w r ps) (force elim: b.run.cases simp: listset_member list_all2_conv_all_nth) then show ?thesis using assms(3) unfolding stream.pred_set by auto qed - lemma intersect_run_stranspose: + lemma product_run_stranspose: assumes "length ps = length AA" - assumes "b.run (intersect AA) (w ||| r) ps" + assumes "b.run (product AA) (w ||| r) ps" obtains rs where "r = stranspose rs" "length rs = length AA" proof define rs where "rs \ map (\ k. smap (\ ps. ps ! k) r) [0 ..< length AA]" - have "length qs = length AA" if "qs \ sset r" for qs using intersect_run_length assms that by this + have "length qs = length AA" if "qs \ sset r" for qs using product_run_length assms that by this then show "r = stranspose rs" unfolding rs_def by (coinduction arbitrary: r) (auto intro: nth_equalityI simp: comp_def) show "length rs = length AA" unfolding rs_def by auto qed - lemma run_intersect: + lemma run_product: assumes "length rs = length AA" "length ps = length AA" assumes "\ k. k < length AA \ a.run (AA ! k) (w ||| rs ! k) (ps ! k)" - shows "b.run (intersect AA) (w ||| stranspose rs) ps" + shows "b.run (product AA) (w ||| stranspose rs) ps" using assms proof (coinduction arbitrary: w rs ps) case (run ap r) then show ?case proof (intro conjI exI) - show "fst ap \ alphabet\<^sub>2 (intersect AA)" + show "fst ap \ alphabet\<^sub>2 (product AA)" using run by (force elim: a.run.cases simp: set_conv_nth) - show "snd ap \ transition\<^sub>2 (intersect AA) (fst ap) ps" + show "snd ap \ transition\<^sub>2 (product AA) (fst ap) ps" using run by (force elim: a.run.cases simp: listset_member list_all2_conv_all_nth) show "\ k < length AA. a.run' (AA ! k) (stl w ||| map stl rs ! k) (map shd rs ! k)" using run by (force elim: a.run.cases) qed auto qed - lemma intersect_run: + lemma product_run: assumes "length rs = length AA" "length ps = length AA" - assumes "b.run (intersect AA) (w ||| stranspose rs) ps" + assumes "b.run (product AA) (w ||| stranspose rs) ps" shows "k < length AA \ a.run (AA ! k) (w ||| rs ! k) (ps ! k)" using assms proof (coinduction arbitrary: w rs ps) case (run ap wr) then show ?case proof (intro exI conjI) show "fst ap \ alphabet\<^sub>1 (AA ! k)" using run by (force elim: b.run.cases) show "snd ap \ transition\<^sub>1 (AA ! k) (fst ap) (ps ! k)" using run by (force elim: b.run.cases simp: listset_member list_all2_conv_all_nth) - show "b.run' (intersect AA) (stl w ||| stranspose (map stl rs)) (shd (stranspose rs))" + show "b.run' (product AA) (stl w ||| stranspose (map stl rs)) (shd (stranspose rs))" using run by (force elim: b.run.cases) qed auto qed - lemma intersect_nodes: "b.nodes (intersect AA) \ listset (map a.nodes AA)" + lemma product_nodes: "b.nodes (product AA) \ listset (map a.nodes AA)" proof - show "ps \ listset (map a.nodes AA)" if "ps \ b.nodes (intersect AA)" for ps + show "ps \ listset (map a.nodes AA)" if "ps \ b.nodes (product AA)" for ps using that by (induct) (auto 0 3 simp: listset_member list_all2_conv_all_nth) qed - lemma intersect_nodes_finite[intro]: + lemma product_nodes_finite[intro]: assumes "list_all (finite \ a.nodes) AA" - shows "finite (b.nodes (intersect AA))" - using list.pred_map intersect_nodes assms by (blast dest: finite_subset) - lemma intersect_nodes_card: + shows "finite (b.nodes (product AA))" + using list.pred_map product_nodes assms by (blast dest: finite_subset) + lemma product_nodes_card: assumes "list_all (finite \ a.nodes) AA" - shows "card (b.nodes (intersect AA)) \ prod_list (map (card \ a.nodes) AA)" + shows "card (b.nodes (product AA)) \ prod_list (map (card \ a.nodes) AA)" proof - - have "card (b.nodes (intersect AA)) \ card (listset (map a.nodes AA))" - using list.pred_map intersect_nodes assms by (blast intro: card_mono) + have "card (b.nodes (product AA)) \ card (listset (map a.nodes AA))" + using list.pred_map product_nodes assms by (blast intro: card_mono) also have "\ = prod_list (map (card \ a.nodes) AA)" by simp finally show ?thesis by this qed end locale automaton_intersection_list_run = - automaton_intersection_list + automaton_product_list automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 condition + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and condition + assumes test[iff]: "length rs = length cs \ length ps = length cs \ test\<^sub>2 (condition cs) w (stranspose rs) ps \ list_all (\ (c, r, p). test\<^sub>1 c w r p) (cs || rs || ps)" begin - lemma intersect_language[simp]: "b.language (intersect AA) = \ (a.language ` set AA)" + lemma product_language[simp]: "b.language (product AA) = \ (a.language ` set AA)" proof safe fix A w - assume 1: "w \ b.language (intersect AA)" "A \ set AA" + assume 1: "w \ b.language (product AA)" "A \ set AA" obtain r ps where 2: - "ps \ initial\<^sub>2 (intersect AA)" - "b.run (intersect AA) (w ||| r) ps" - "test\<^sub>2 (condition\<^sub>2 (intersect AA)) w r ps" + "ps \ initial\<^sub>2 (product AA)" + "b.run (product AA) (w ||| r) ps" + "test\<^sub>2 (condition\<^sub>2 (product AA)) w r ps" using 1(1) by auto have 3: "length ps = length AA" using 2(1) by (simp add: listset_member list_all2_conv_all_nth) obtain rs where 4: "r = stranspose rs" "length rs = length AA" - using intersect_run_stranspose 3 2(2) by this + using product_run_stranspose 3 2(2) by this obtain k where 5: "k < length AA" "A = AA ! k" using 1(2) unfolding set_conv_nth by auto show "w \ a.language A" proof show "ps ! k \ initial\<^sub>1 A" using 2(1) 5 by (auto simp: listset_member list_all2_conv_all_nth) - show "a.run A (w ||| rs ! k) (ps ! k)" using 2(2) 3 4 5 by (auto intro: intersect_run) + show "a.run A (w ||| rs ! k) (ps ! k)" using 2(2) 3 4 5 by (auto intro: product_run) show "test\<^sub>1 (condition\<^sub>1 A) w (rs ! k) (ps ! k)" using 2(3) 3 4 5 by (simp add: list_all_length) qed next fix w assume 1: "w \ \ (a.language ` set AA)" have 2: "\ A \ set AA. \ r p. p \ initial\<^sub>1 A \ a.run A (w ||| r) p \ test\<^sub>1 (condition\<^sub>1 A) w r p" using 1 by blast obtain rs ps where 3: "length rs = length AA" "length ps = length AA" "\ k. k < length AA \ ps ! k \ initial\<^sub>1 (AA ! k)" "\ k. k < length AA \ a.run (AA ! k) (w ||| rs ! k) (ps ! k)" "\ k. k < length AA \ test\<^sub>1 (condition\<^sub>1 (AA ! k)) w (rs ! k) (ps ! k)" using 2 unfolding Ball_set list_choice_zip list_choice_pair unfolding list.pred_set set_conv_nth by force - show "w \ b.language (intersect AA)" + show "w \ b.language (product AA)" proof - show "ps \ initial\<^sub>2 (intersect AA)" using 3 by (auto simp: listset_member list_all2_conv_all_nth) - show "b.run (intersect AA) (w ||| stranspose rs) ps" using 3 by (auto intro: run_intersect) - show "test\<^sub>2 (condition\<^sub>2 (intersect AA)) w (stranspose rs) ps" using 3 by (auto simp: list_all_length) + show "ps \ initial\<^sub>2 (product AA)" using 3 by (auto simp: listset_member list_all2_conv_all_nth) + show "b.run (product AA) (w ||| stranspose rs) ps" using 3 by (auto intro: run_product) + show "test\<^sub>2 (condition\<^sub>2 (product AA)) w (stranspose rs) ps" using 3 by (auto simp: list_all_length) qed qed end - locale automaton_union_list = + locale automaton_sum_list = a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 + b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 for automaton\<^sub>1 :: "'label set \ 'state set \ ('label \ 'state \ 'state set) \ 'condition\<^sub>1 \ 'automaton\<^sub>1" and alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 and automaton\<^sub>2 :: "'label set \ (nat \ 'state) set \ ('label \ nat \ 'state \ (nat \ 'state) set) \ 'condition\<^sub>2 \ 'automaton\<^sub>2" and alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 + fixes condition :: "'condition\<^sub>1 list \ 'condition\<^sub>2" begin - definition union :: "'automaton\<^sub>1 list \ 'automaton\<^sub>2" where - "union AA \ automaton\<^sub>2 + definition sum :: "'automaton\<^sub>1 list \ 'automaton\<^sub>2" where + "sum AA \ automaton\<^sub>2 (\ (alphabet\<^sub>1 ` set AA)) (\ k < length AA. {k} \ initial\<^sub>1 (AA ! k)) (\ a (k, p). {k} \ transition\<^sub>1 (AA ! k) a p) (condition (map condition\<^sub>1 AA))" - lemma union_simps[simp]: - "alphabet\<^sub>2 (union AA) = \ (alphabet\<^sub>1 ` set AA)" - "initial\<^sub>2 (union AA) = (\ k < length AA. {k} \ initial\<^sub>1 (AA ! k))" - "transition\<^sub>2 (union AA) a (k, p) = {k} \ transition\<^sub>1 (AA ! k) a p" - "condition\<^sub>2 (union AA) = condition (map condition\<^sub>1 AA)" - unfolding union_def by auto + lemma sum_simps[simp]: + "alphabet\<^sub>2 (sum AA) = \ (alphabet\<^sub>1 ` set AA)" + "initial\<^sub>2 (sum AA) = (\ k < length AA. {k} \ initial\<^sub>1 (AA ! k))" + "transition\<^sub>2 (sum AA) a (k, p) = {k} \ transition\<^sub>1 (AA ! k) a p" + "condition\<^sub>2 (sum AA) = condition (map condition\<^sub>1 AA)" + unfolding sum_def by auto - lemma run_union: + lemma run_sum: assumes "\ (alphabet\<^sub>1 ` set AA) = \ (alphabet\<^sub>1 ` set AA)" assumes "A \ set AA" assumes "a.run A (w ||| s) p" - obtains k where "k < length AA" "A = AA ! k" "b.run (union AA) (w ||| sconst k ||| s) (k, p)" + obtains k where "k < length AA" "A = AA ! k" "b.run (sum AA) (w ||| sconst k ||| s) (k, p)" proof - obtain k where 1: "k < length AA" "A = AA ! k" using assms(2) unfolding set_conv_nth by auto show ?thesis proof show "k < length AA" "A = AA ! k" using 1 by this - show "b.run (union AA) (w ||| sconst k ||| s) (k, p)" + show "b.run (sum AA) (w ||| sconst k ||| s) (k, p)" using assms 1(2) by (coinduction arbitrary: w s p) (force elim: a.run.cases) qed qed - lemma union_run: + lemma sum_run: assumes "\ (alphabet\<^sub>1 ` set AA) = \ (alphabet\<^sub>1 ` set AA)" assumes "k < length AA" - assumes "b.run (union AA) (w ||| r) (k, p)" + assumes "b.run (sum AA) (w ||| r) (k, p)" obtains s where "r = sconst k ||| s" "a.run (AA ! k) (w ||| s) p" proof show "r = sconst k ||| smap snd r" using assms by (coinduction arbitrary: w r p) (force elim: b.run.cases) show "a.run (AA ! k) (w ||| smap snd r) p" using assms by (coinduction arbitrary: w r p) (force elim: b.run.cases) qed - lemma union_nodes: + lemma sum_nodes: assumes "\ (alphabet\<^sub>1 ` set AA) = \ (alphabet\<^sub>1 ` set AA)" - shows "b.nodes (union AA) \ (\ k < length AA. {k} \ a.nodes (AA ! k))" + shows "b.nodes (sum AA) \ (\ k < length AA. {k} \ a.nodes (AA ! k))" proof - show "kp \ (\ k < length AA. {k} \ a.nodes (AA ! k))" if "kp \ b.nodes (union AA)" for kp + show "kp \ (\ k < length AA. {k} \ a.nodes (AA ! k))" if "kp \ b.nodes (sum AA)" for kp using that assms by (induct) (auto 0 4) qed - lemma union_nodes_finite[intro]: + lemma sum_nodes_finite[intro]: assumes "\ (alphabet\<^sub>1 ` set AA) = \ (alphabet\<^sub>1 ` set AA)" assumes "list_all (finite \ a.nodes) AA" - shows "finite (b.nodes (union AA))" + shows "finite (b.nodes (sum AA))" proof (rule finite_subset) - show "b.nodes (union AA) \ (\ k < length AA. {k} \ a.nodes (AA ! k))" - using union_nodes assms(1) by this + show "b.nodes (sum AA) \ (\ k < length AA. {k} \ a.nodes (AA ! k))" + using sum_nodes assms(1) by this show "finite (\ k < length AA. {k} \ a.nodes' (AA ! k))" using assms(2) unfolding list_all_length by auto qed end locale automaton_union_list_run = - automaton_union_list + automaton_sum_list automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 condition + a: automaton_run automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 + b: automaton_run automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 for automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 and automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 and condition + assumes test[iff]: "k < length cs \ test\<^sub>2 (condition cs) w (sconst k ||| r) (k, p) \ test\<^sub>1 (cs ! k) w r p" begin - lemma union_language[simp]: + lemma sum_language[simp]: assumes "\ (alphabet\<^sub>1 ` set AA) = \ (alphabet\<^sub>1 ` set AA)" - shows "b.language (union AA) = \ (a.language ` set AA)" + shows "b.language (sum AA) = \ (a.language ` set AA)" proof - show "b.language (union AA) \ \ (a.language ` set AA)" - using assms unfolding a.language_def b.language_def by (force elim: union_run) - show "\ (a.language ` set AA) \ b.language (union AA)" - using assms unfolding a.language_def b.language_def by (force elim!: run_union) + show "b.language (sum AA) \ \ (a.language ` set AA)" + using assms unfolding a.language_def b.language_def by (force elim: sum_run) + show "\ (a.language ` set AA) \ b.language (sum AA)" + using assms unfolding a.language_def b.language_def by (force elim!: run_sum) qed end end \ No newline at end of file