Theory Input_Output_Language_Conformance
theory Input_Output_Language_Conformance
imports "HOL-Library.Sublist"
begin
section ‹Preliminaries›
type_synonym ('a) alphabet = "'a set"
type_synonym ('x,'y) word = "('x × 'y) list"
type_synonym ('x,'y) language = "('x,'y) word set"
type_synonym ('y) output_relation = "('y set × 'y set) set"
fun is_language :: "'x alphabet ⇒ 'y alphabet ⇒ ('x,'y) language ⇒ bool" where
"is_language X Y L = (
(L ≠ {}) ∧
(∀ π ∈ L .
(∀ xy ∈ set π . fst xy ∈ X ∧ snd xy ∈ Y) ∧
(∀ π' . prefix π' π ⟶ π' ∈ L)))"
lemma language_contains_nil :
assumes "is_language X Y L"
shows "[] ∈ L"
using assms by auto
lemma language_intersection_is_language :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "is_language X Y (L1 ∩ L2)"
using assms
using language_contains_nil[OF assms(1)] language_contains_nil[OF assms(2)]
unfolding is_language.simps
by (metis IntD1 IntD2 IntI disjoint_iff)
fun language_for_state :: "('x,'y) language ⇒ ('x,'y) word ⇒ ('x,'y) language" where
"language_for_state L π = {τ . π@τ ∈ L}"
notation language_for_state ("ℒ[_,_]")
lemma language_for_state_is_language :
assumes "is_language X Y L"
and "π ∈ L"
shows "is_language X Y ℒ[L,π]"
proof -
have "⋀ τ . τ ∈ ℒ[L,π] ⟹ (∀ xy ∈ set τ . fst xy ∈ X ∧ snd xy ∈ Y) ∧ (∀ τ' . prefix τ' τ ⟶ τ' ∈ ℒ[L,π])"
proof -
fix τ assume "τ ∈ ℒ[L,π]"
then have "π@τ ∈ L" by auto
then have "⋀ xy . xy ∈ set (π@τ) ⟹ fst xy ∈ X ∧ snd xy ∈ Y"
and "⋀ π' . prefix π' (π@τ) ⟹ π' ∈ L"
using assms(1) by auto
have "⋀ xy . xy ∈ set τ ⟹ fst xy ∈ X ∧ snd xy ∈ Y"
using ‹⋀ xy . xy ∈ set (π@τ) ⟹ fst xy ∈ X ∧ snd xy ∈ Y› by auto
moreover have "⋀ τ' . prefix τ' τ ⟹ τ' ∈ ℒ[L,π]"
by (simp add: ‹⋀π'. prefix π' (π @ τ) ⟹ π' ∈ L›)
ultimately show "(∀ xy ∈ set τ . fst xy ∈ X ∧ snd xy ∈ Y) ∧ (∀ τ' . prefix τ' τ ⟶ τ' ∈ ℒ[L,π])"
by simp
qed
moreover have "ℒ[L,π] ≠ {}"
using assms(2)
by (metis (no_types, lifting) append.right_neutral empty_Collect_eq language_for_state.simps)
ultimately show ?thesis
by simp
qed
lemma language_of_state_empty_iff :
assumes "is_language X Y L"
shows "(ℒ[L,π] = {}) ⟷ (π ∉ L)"
using assms unfolding is_language.simps language_for_state.simps
by (metis Collect_empty_eq append.right_neutral prefixI)
fun are_equivalent_for_language :: "('x,'y) language ⇒ ('x,'y) word ⇒ ('x,'y) word ⇒ bool" where
"are_equivalent_for_language L α β = (ℒ[L,α] = ℒ[L,β])"
abbreviation(input) "input_projection π ≡ map fst π"
abbreviation(input) "output_projection π ≡ map snd π"
notation input_projection ("[_]⇩I")
notation output_projection ("[_]⇩O")
fun is_executable :: "('x,'y) language ⇒ ('x,'y) word ⇒ 'x list ⇒ bool" where
"is_executable L π xs = (∃ τ ∈ ℒ[L,π] . [τ]⇩I = xs)"
fun executable_sequences :: "('x,'y) language ⇒ ('x,'y) word ⇒ 'x list set" where
"executable_sequences L π = {xs . is_executable L π xs}"
fun executable_inputs :: "('x,'y) language ⇒ ('x,'y) word ⇒ 'x set" where
"executable_inputs L π = {x . is_executable L π [x]}"
notation executable_inputs ("exec[_,_]")
lemma executable_sequences_alt_def : "executable_sequences L π = {xs . ∃ ys . length ys = length xs ∧ zip xs ys ∈ ℒ[L,π]}"
proof -
have *:"⋀ A xs . (∃τ∈A. map fst τ = xs) = (∃ys. length ys = length xs ∧ zip xs ys ∈ A)"
by (metis length_map map_fst_zip zip_map_fst_snd)
show ?thesis
unfolding executable_sequences.simps is_executable.simps
unfolding *
by simp
qed
lemma executable_inputs_alt_def : "executable_inputs L π = {x . ∃ y . [(x,y)] ∈ ℒ[L,π]}"
proof -
have *:"⋀ A xs . (∃τ∈A. map fst τ = xs) = (∃ys. length ys = length xs ∧ zip xs ys ∈ A)"
by (metis length_map map_fst_zip zip_map_fst_snd)
have **: "⋀ A x . (∃ys. length ys = length [x] ∧ zip [x] ys ∈ A) = (∃ y . [(x,y)] ∈ A)"
by (metis length_Suc_conv length_map zip_Cons_Cons zip_Nil)
show ?thesis
unfolding executable_inputs.simps is_executable.simps
unfolding *
unfolding **
by fastforce
qed
lemma executable_inputs_in_alphabet :
assumes "is_language X Y L"
and "x ∈ exec[L,π]"
shows "x ∈ X"
using assms unfolding executable_inputs_alt_def by auto
fun output_sequences :: "('x,'y) language ⇒ ('x,'y) word ⇒ 'x list ⇒ 'y list set" where
"output_sequences L π xs = output_projection ` {τ ∈ ℒ[L,π] . [τ]⇩I = xs}"
lemma prefix_closure_no_member :
assumes "is_language X Y L"
and "π ∉ L"
shows "π@τ ∉ L"
by (meson assms(1) assms(2) is_language.elims(2) prefixI)
lemma output_sequences_empty_iff :
assumes "is_language X Y L"
shows "(output_sequences L π xs = {}) = ((π ∉ L) ∨ (¬ is_executable L π xs))"
unfolding output_sequences.simps is_executable.simps language_for_state.simps
using Collect_empty_eq assms image_empty mem_Collect_eq prefix_closure_no_member by auto
fun outputs :: "('x,'y) language ⇒ ('x,'y) word ⇒ 'x ⇒ 'y set" where
"outputs L π x = {y . [(x,y)] ∈ ℒ[L,π]}"
notation outputs ("out[_,_,_]")
lemma outputs_in_alphabet :
assumes "is_language X Y L"
shows "out[L,π,x] ⊆ Y"
using assms by auto
lemma outputs_executable : "(out[L,π,x] = {}) ⟷ (x ∉ exec[L,π])"
by auto
fun is_completely_specified_for :: "'x set ⇒ ('x,'y) language ⇒ bool" where
"is_completely_specified_for X L = (∀ π ∈ L . ∀ x ∈ X . out[L,π,x] ≠ {})"
lemma prefix_executable :
assumes "is_language X Y L"
and "π ∈ L"
and "i < length π"
shows "fst (π ! i) ∈ exec[L,take i π]"
proof -
define π' where "π' = take i π"
moreover define π'' where "π'' = drop (Suc i) π"
moreover define xy where "xy = π ! i"
ultimately have "π = π'@[xy]@π''"
by (simp add: Cons_nth_drop_Suc assms(3))
then have "π'@[xy] ∈ L"
using assms(1,2) by auto
then show ?thesis
unfolding π'_def xy_def
unfolding executable_inputs_alt_def language_for_state.simps
by (metis (mono_tags, lifting) CollectI eq_fst_iff)
qed
section ‹Conformance Relations›
definition language_equivalence :: "('x,'y) language ⇒ ('x,'y) language ⇒ bool" where
"language_equivalence L1 L2 = (L1 = L2)"
definition language_inclusion :: "('x,'y) language ⇒ ('x,'y) language ⇒ bool" where
"language_inclusion L1 L2 = (L1 ⊆ L2)"
abbreviation(input) "reduction L1 L2 ≡ language_inclusion L1 L2"
definition quasi_equivalence :: "('x,'y) language ⇒ ('x,'y) language ⇒ bool" where
"quasi_equivalence L1 L2 = (∀ π ∈ L1 ∩ L2 . ∀ x ∈ exec[L2,π] . out[L1,π,x] = out[L2,π,x])"
definition quasi_reduction :: "('x,'y) language ⇒ ('x,'y) language ⇒ bool" where
"quasi_reduction L1 L2 = (∀ π ∈ L1 ∩ L2 . ∀ x ∈ exec[L2,π] . (out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x]))"
definition strong_reduction :: "('x,'y) language ⇒ ('x,'y) language ⇒ bool" where
"strong_reduction L1 L2 = (quasi_reduction L1 L2 ∧ (∀ π ∈ L1 ∩ L2 . ∀ x . out[L2,π,x] = {} ⟶ out[L1,π,x] = {}))"
definition semi_equivalence :: "('x,'y) language ⇒ ('x,'y) language ⇒ bool" where
"semi_equivalence L1 L2 = (∀ π ∈ L1 ∩ L2 . ∀ x ∈ exec[L2,π] .
(out[L1,π,x] = {} ∨ out[L1,π,x] = out[L2,π,x]) ∧
(∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}))"
definition semi_reduction :: "('x,'y) language ⇒ ('x,'y) language ⇒ bool" where
"semi_reduction L1 L2 = (∀ π ∈ L1 ∩ L2 . ∀ x ∈ exec[L2,π] .
(out[L1,π,x] ⊆ out[L2,π,x]) ∧
(∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}))"
definition strong_semi_equivalence :: "('x,'y) language ⇒ ('x,'y) language ⇒ bool" where
"strong_semi_equivalence L1 L2 = (∀ π ∈ L1 ∩ L2 . ∀ x .
(x ∈ exec[L2,π] ⟶ ((out[L1,π,x] = {} ∨ out[L1,π,x] = out[L2,π,x]) ∧ (∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}))) ∧
(x ∉ exec[L2,π] ⟶ out[L1,π,x] = {}))"
definition strong_semi_reduction :: "('x,'y) language ⇒ ('x,'y) language ⇒ bool" where
"strong_semi_reduction L1 L2 = (∀ π ∈ L1 ∩ L2 . ∀ x .
(x ∈ exec[L2,π] ⟶ (out[L1,π,x] ⊆ out[L2,π,x] ∧ (∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}))) ∧
(x ∉ exec[L2,π] ⟶ out[L1,π,x] = {}))"
section ‹Unifying Characterisations›
subsection ‹$\preceq$ Conformance›
fun type_1_conforms :: "('x,'y) language ⇒ 'x alphabet ⇒ 'y output_relation ⇒ ('x,'y) language ⇒ bool" where
"type_1_conforms L1 X H L2 = (∀ π ∈ L1 ∩ L2 . ∀ x ∈ X . (out[L1,π,x],out[L2,π,x]) ∈ H)"
notation type_1_conforms ("_ ≼[_,_] _")
fun equiv :: "'y alphabet ⇒ 'y output_relation" where
"equiv Y = {(A,A) | A . A ⊆ Y}"
fun red :: "'y alphabet ⇒ 'y output_relation" where
"red Y = {(A,B) | A B . A ⊆ B ∧ B ⊆ Y}"
fun quasieq :: "'y alphabet ⇒ 'y output_relation" where
"quasieq Y = {(A,A) | A . A ⊆ Y} ∪ {(A,{}) | A . A ⊆ Y}"
fun quasired :: "'y alphabet ⇒ 'y output_relation" where
"quasired Y = {(A,B) | A B . A ≠ {} ∧ A ⊆ B ∧ B ⊆ Y} ∪ {(C,{}) | C . C ⊆ Y}"
fun strongred :: "'y alphabet ⇒ 'y output_relation" where
"strongred Y = {(A,B) | A B . A ≠ {} ∧ A ⊆ B ∧ B ⊆ Y} ∪ {({},{})}"
lemma red_type_1 :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "reduction L1 L2 ⟷ (L1 ≼[X,red Y] L2)"
unfolding language_inclusion_def proof
show "L1 ⊆ L2 ⟹ L1 ≼[X,red Y] L2"
using outputs_in_alphabet[OF assms(2)]
unfolding type_1_conforms.simps red.simps
by auto
show "L1 ≼[X,red Y] L2 ⟹ L1 ⊆ L2"
proof
fix π assume "π ∈ L1" and "L1 ≼[X,red Y] L2"
then show "π ∈ L2" proof (induction π rule: rev_induct)
case Nil
then show ?case using assms(2) by auto
next
case (snoc xy π)
then have "π ∈ L1" and "π ∈ L1 ∩ L2"
using assms(1) by auto
obtain x y where "xy = (x,y)"
by fastforce
then have "y ∈ out[L1,π,x]"
using snoc.prems(1)
by simp
moreover have "x ∈ X" and "y ∈ Y"
using snoc.prems(1) assms(1) unfolding ‹xy = (x,y)› by auto
ultimately have "y ∈ out[L2,π,x]"
using snoc.prems(2) ‹π ∈ L1 ∩ L2›
unfolding type_1_conforms.simps
by fastforce
then show ?case
using ‹xy = (x, y)› by auto
qed
qed
qed
lemma equiv_by_reduction : "(L1 ≼[X,equiv Y] L2) ⟷ ((L1 ≼[X,red Y] L2) ∧ (L2 ≼[X,red Y] L1))"
by fastforce
lemma equiv_type_1 :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "(L1 = L2) ⟷ (L1 ≼[X,equiv Y] L2)"
unfolding equiv_by_reduction
unfolding red_type_1[OF assms(1,2), symmetric]
unfolding red_type_1[OF assms(2,1), symmetric]
unfolding language_inclusion_def
by blast
lemma quasired_type_1 :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "quasi_reduction L1 L2 ⟷ (L1 ≼[X,quasired Y] L2)"
proof
have "⋀ π x . quasi_reduction L1 L2 ⟹ π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x], out[L2,π,x]) ∈ quasired Y"
proof -
fix π x assume "quasi_reduction L1 L2" and "π ∈ L1 ∩ L2" and "x ∈ X"
show "(out[L1,π,x], out[L2,π,x]) ∈ quasired Y"
proof (cases "x ∈ exec[L2,π]")
case False
then show ?thesis
by (metis (mono_tags, lifting) CollectI UnCI assms(1) outputs_executable outputs_in_alphabet quasired.elims)
next
case True
then obtain y where "y ∈ out[L2,π,x]" by auto
then have "out[L1,π,x] ⊆ out[L2,π,x]" and "out[L1,π,x] ≠ {}"
using ‹π ∈ L1 ∩ L2› ‹x ∈ X› ‹quasi_reduction L1 L2›
unfolding quasi_reduction_def by force+
moreover have "out[L2,π,x] ⊆ Y"
by (meson assms(2) outputs_in_alphabet)
ultimately show ?thesis
unfolding quasired.simps by blast
qed
qed
then show "quasi_reduction L1 L2 ⟹ (L1 ≼[X,quasired Y] L2)"
by auto
have "⋀ π x . L1 ≼[X,quasired Y] L2 ⟹ π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ out[L1,π,x] ⊆ out[L2,π,x]"
and "⋀ π x . L1 ≼[X,quasired Y] L2 ⟹ π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ out[L1,π,x] ≠ {}"
proof -
fix π x assume "L1 ≼[X,quasired Y] L2" and "π ∈ L1 ∩ L2" and "x ∈ exec[L2,π]"
then have "x ∈ X"
using executable_inputs_in_alphabet[OF assms(2)] by auto
have "out[L2,π,x] ≠ {}"
using ‹x ∈ exec[L2,π]›
by (meson outputs_executable)
moreover have "(out[L1,π,x],out[L2,π,x]) ∈ quasired Y"
by (meson ‹L1 ≼[X,quasired Y] L2› ‹π ∈ L1 ∩ L2› ‹x ∈ X› type_1_conforms.elims(2))
ultimately show "out[L1,π,x] ⊆ out[L2,π,x]"
and "out[L1,π,x] ≠ {}"
unfolding quasired.simps
by blast+
qed
then show "L1 ≼[X,quasired Y] L2 ⟹ quasi_reduction L1 L2"
by (meson quasi_reduction_def)
qed
lemma quasieq_type_1 :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "quasi_equivalence L1 L2 ⟷ (L1 ≼[X,quasieq Y] L2)"
proof
have "⋀ π x . quasi_equivalence L1 L2 ⟹ π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x], out[L2,π,x]) ∈ quasieq Y"
proof -
fix π x assume "quasi_equivalence L1 L2" and "π ∈ L1 ∩ L2" and "x ∈ X"
show "(out[L1,π,x], out[L2,π,x]) ∈ quasieq Y"
proof (cases "x ∈ exec[L2,π]")
case False
then show ?thesis
by (metis (mono_tags, lifting) CollectI UnCI assms(1) outputs_executable outputs_in_alphabet quasieq.simps)
next
case True
then show ?thesis
by (metis (mono_tags, lifting) CollectI UnCI ‹π ∈ L1 ∩ L2› ‹quasi_equivalence L1 L2› assms(1) outputs_in_alphabet quasi_equivalence_def quasieq.simps)
qed
qed
then show "quasi_equivalence L1 L2 ⟹ (L1 ≼[X,quasieq Y] L2)"
by auto
have "⋀ π x . L1 ≼[X,quasieq Y] L2 ⟹ π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ out[L1,π,x] = out[L2,π,x]"
proof -
fix π x assume "L1 ≼[X,quasieq Y] L2" and "π ∈ L1 ∩ L2" and "x ∈ exec[L2,π]"
then have "x ∈ X"
using executable_inputs_in_alphabet[OF assms(2)] by auto
have "out[L2,π,x] ≠ {}"
using ‹x ∈ exec[L2,π]›
by (meson outputs_executable)
moreover have "(out[L1,π,x],out[L2,π,x]) ∈ quasieq Y"
by (meson ‹L1 ≼[X,quasieq Y] L2› ‹π ∈ L1 ∩ L2› ‹x ∈ X› type_1_conforms.elims(2))
ultimately show "out[L1,π,x] = out[L2,π,x]"
unfolding quasieq.simps
by blast
qed
then show "L1 ≼[X,quasieq Y] L2 ⟹ quasi_equivalence L1 L2"
by (meson quasi_equivalence_def)
qed
lemma strongred_type_1 :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "strong_reduction L1 L2 ⟷ (L1 ≼[X,strongred Y] L2)"
proof
have "⋀ π x . strong_reduction L1 L2 ⟹ π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x], out[L2,π,x]) ∈ strongred Y"
proof -
fix π x assume "strong_reduction L1 L2" and "π ∈ L1 ∩ L2" and "x ∈ X"
have "out[L2,π,x] ⊆ Y"
using outputs_in_alphabet[OF assms(2)] .
show "(out[L1,π,x], out[L2,π,x]) ∈ strongred Y"
proof (cases "x ∈ exec[L2,π]")
case False
then have "out[L2,π,x] = {}"
using outputs_executable by force
then have "out[L1,π,x] = {}"
using ‹strong_reduction L1 L2› ‹π ∈ L1 ∩ L2›
unfolding strong_reduction_def by blast
then show ?thesis
using ‹out[L2,π,x] = {}› by auto
next
case True
then have "out[L1,π,x] ≠ {}"
using ‹strong_reduction L1 L2› ‹π ∈ L1 ∩ L2›
unfolding strong_reduction_def
by (meson quasi_reduction_def)
moreover have "out[L1,π,x] ⊆ out[L2,π,x]"
by (meson True ‹π ∈ L1 ∩ L2› ‹strong_reduction L1 L2› quasi_reduction_def strong_reduction_def)
ultimately show ?thesis
unfolding strongred.simps
using outputs_executable outputs_in_alphabet[OF assms(2)]
by force
qed
qed
then show "strong_reduction L1 L2 ⟹ (L1 ≼[X,strongred Y] L2)"
by auto
have "⋀ π x . L1 ≼[X,strongred Y] L2 ⟹ π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ out[L1,π,x] ≠ {}"
and "⋀ π x . L1 ≼[X,strongred Y] L2 ⟹ π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ out[L1,π,x] ⊆ out[L2,π,x]"
proof -
fix π x y assume "L1 ≼[X,strongred Y] L2" and "π ∈ L1 ∩ L2" and "x ∈ exec[L2,π]"
then have "x ∈ X"
using executable_inputs_in_alphabet[OF assms(2)] by auto
have "out[L2,π,x] ≠ {}"
using ‹x ∈ exec[L2,π]›
by (meson outputs_executable)
moreover have "(out[L1,π,x],out[L2,π,x]) ∈ strongred Y"
by (meson ‹L1 ≼[X,strongred Y] L2› ‹π ∈ L1 ∩ L2› ‹x ∈ X› type_1_conforms.elims(2))
ultimately show "out[L1,π,x] ≠ {}" and "out[L1,π,x] ⊆ out[L2,π,x]"
unfolding strongred.simps
by blast+
qed
moreover have "⋀ π x . L1 ≼[X,strongred Y] L2 ⟹ π ∈ L1 ∩ L2 ⟹ out[L2,π,x] = {} ⟹ out[L1,π,x] = {}"
proof -
fix π x assume "L1 ≼[X,strongred Y] L2" and "π ∈ L1 ∩ L2" and "out[L2,π,x] = {}"
show "out[L1,π,x] = {}"
proof (rule ccontr)
assume "out[L1,π,x] ≠ {}"
then have "x ∈ X"
by (meson assms(1) executable_inputs_in_alphabet outputs_executable)
then have "out[L2,π,x] ≠ {}"
using ‹L1 ≼[X,strongred Y] L2› ‹π ∈ L1 ∩ L2› ‹out[L1,π,x] ≠ {}› by fastforce
then show False
using ‹out[L2,π,x] = {}› by simp
qed
qed
ultimately show "L1 ≼[X,strongred Y] L2 ⟹ strong_reduction L1 L2"
unfolding strong_reduction_def quasi_reduction_def by blast
qed
subsection ‹$\le$ Conformance›
fun type_2_conforms :: "('x,'y) language ⇒ 'x alphabet ⇒ 'y output_relation ⇒ ('x,'y) language ⇒ bool" where
"type_2_conforms L1 X H L2 = (
(∀ π ∈ L1 ∩ L2 . ∀ x ∈ X . (out[L1,π,x],out[L2,π,x]) ∈ H) ∧
(∀ π ∈ L1 ∩ L2 . exec[L2,π] ≠ {} ⟶ (∃ x . out[L1,π,x] ∩ out[L2,π,x] ≠ {})))"
notation type_2_conforms ("_ ≤[_,_] _")
fun semieq :: "'y alphabet ⇒ 'y output_relation" where
"semieq Y = {(A,A) | A . A ⊆ Y} ∪ {({},A) | A . A ⊆ Y} ∪ {(A,{}) | A . A ⊆ Y}"
fun semired :: "'y alphabet ⇒ 'y output_relation" where
"semired Y = {(A,B) | A B . A ⊆ B ∧ B ⊆ Y} ∪ {(C,{}) | C . C ⊆ Y}"
fun strongsemieq :: "'y alphabet ⇒ 'y output_relation" where
"strongsemieq Y = {(A,A) | A . A ⊆ Y} ∪ {({},A) | A . A ⊆ Y}"
fun strongsemired :: "'y alphabet ⇒ 'y output_relation" where
"strongsemired Y = {(A,B) | A B . A ⊆ B ∧ B ⊆ Y}"
lemma strongsemieq_alt_def : "strongsemieq Y = semieq Y ∩ red Y"
by auto
lemma strongsemired_alt_def : "strongsemired Y = red Y"
by auto
lemma semired_type_2 :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "(semi_reduction L1 L2) ⟷ (L1 ≤[X, semired Y] L2)"
proof
show "semi_reduction L1 L2 ⟹ L1 ≤[X, semired Y] L2"
proof -
assume "semi_reduction L1 L2"
then have p1: "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ (out[L1,π,x] ⊆ out[L2,π,x])"
and p2: "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ ∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}"
unfolding semi_reduction_def by blast+
have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x], out[L2,π,x]) ∈ semired Y"
by (metis (mono_tags, lifting) CollectI UnCI assms(1) assms(2) outputs_executable outputs_in_alphabet p1 semired.simps)
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ exec[L2,π] ≠ {} ⟹ ∃x. out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
using p2 by fastforce
ultimately show "L1 ≤[X, semired Y] L2"
by auto
qed
show "L1 ≤[X,semired Y] L2 ⟹ semi_reduction L1 L2"
proof -
assume "L1 ≤[X,semired Y] L2"
then have p1 : "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x],out[L2,π,x]) ∈ semired Y"
and p2 : "⋀ π x . π ∈ L1 ∩ L2 ⟹ exec[L2,π] ≠ {} ⟹ ∃ x . out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
by auto
have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ (out[L1,π,x] ⊆ out[L2,π,x])"
proof -
fix π x assume "π ∈ L1 ∩ L2" and "x ∈ exec[L2,π]"
then have "(out[L1,π,x],out[L2,π,x]) ∈ semired Y"
using p1 executable_inputs_in_alphabet[OF assms(2)] by auto
moreover have "out[L2,π,x] ≠ {}"
using ‹x ∈ exec[L2,π]› by auto
ultimately show "(out[L1,π,x] ⊆ out[L2,π,x])"
unfolding semired.simps by blast
qed
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ ∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}"
using p2 by blast
ultimately show ?thesis
unfolding semi_reduction_def by blast
qed
qed
lemma semieq_type_2 :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "(semi_equivalence L1 L2) ⟷ (L1 ≤[X, semieq Y] L2)"
proof
show "semi_equivalence L1 L2 ⟹ L1 ≤[X, semieq Y] L2"
proof -
assume "semi_equivalence L1 L2"
then have p1: "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ out[L1,π,x] = {} ∨ out[L1,π,x] = out[L2,π,x]"
and p2: "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ ∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}"
unfolding semi_equivalence_def by blast+
have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x], out[L2,π,x]) ∈ semieq Y"
proof -
fix π x assume "π ∈ L1 ∩ L2" and "x ∈ X"
show "(out[L1,π,x], out[L2,π,x]) ∈ semieq Y"
proof (cases "x ∈ exec[L2,π]")
case True
then have "out[L2,π,x] ≠ {}" by auto
then show ?thesis
using p1[OF ‹π ∈ L1 ∩ L2› True]
using outputs_in_alphabet[OF assms(2)]
unfolding semieq.simps
by fastforce
next
case False
then show ?thesis
by (metis (mono_tags, lifting) CollectI UnI2 assms(1) outputs_executable outputs_in_alphabet semieq.elims)
qed
qed
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ exec[L2,π] ≠ {} ⟹ ∃x. out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
using p2 by fastforce
ultimately show "L1 ≤[X, semieq Y] L2"
by auto
qed
show "L1 ≤[X,semieq Y] L2 ⟹ semi_equivalence L1 L2"
proof -
assume "L1 ≤[X,semieq Y] L2"
then have p1 : "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x],out[L2,π,x]) ∈ semieq Y"
and p2 : "⋀ π x . π ∈ L1 ∩ L2 ⟹ exec[L2,π] ≠ {} ⟹ ∃ x . out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
by auto
have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ out[L1,π,x] = {} ∨ out[L1,π,x] = out[L2,π,x]"
proof -
fix π x assume "π ∈ L1 ∩ L2" and "x ∈ exec[L2,π]"
then have "(out[L1,π,x],out[L2,π,x]) ∈ semieq Y"
using p1 executable_inputs_in_alphabet[OF assms(2)] by auto
moreover have "out[L2,π,x] ≠ {}"
using ‹x ∈ exec[L2,π]› by auto
ultimately show "out[L1,π,x] = {} ∨ out[L1,π,x] = out[L2,π,x]"
unfolding semieq.simps
by blast
qed
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ ∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}"
using p2 by blast
ultimately show ?thesis
unfolding semi_equivalence_def by blast
qed
qed
lemma strongsemired_type_2 :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "(strong_semi_reduction L1 L2) ⟷ (L1 ≤[X, strongsemired Y] L2)"
proof
show "strong_semi_reduction L1 L2 ⟹ L1 ≤[X, strongsemired Y] L2"
proof -
assume "strong_semi_reduction L1 L2"
then have p1: "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ (out[L1,π,x] ⊆ out[L2,π,x])"
and p2: "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ ∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}"
and p3: "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∉ exec[L2,π] ⟹ out[L1,π,x] = {}"
unfolding strong_semi_reduction_def by blast+
have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x], out[L2,π,x]) ∈ strongsemired Y"
unfolding strongsemired.simps
by (metis (mono_tags, lifting) CollectI assms(2) outputs_executable outputs_in_alphabet p1 p3 set_eq_subset)
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ exec[L2,π] ≠ {} ⟹ ∃x. out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
using p2 by fastforce
ultimately show "L1 ≤[X, strongsemired Y] L2"
by auto
qed
show "L1 ≤[X,strongsemired Y] L2 ⟹ strong_semi_reduction L1 L2"
proof -
assume "L1 ≤[X,strongsemired Y] L2"
then have p1 : "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x],out[L2,π,x]) ∈ strongsemired Y"
and p2 : "⋀ π x . π ∈ L1 ∩ L2 ⟹ exec[L2,π] ≠ {} ⟹ ∃ x . out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
by auto
have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ (out[L1,π,x] ⊆ out[L2,π,x])"
proof -
fix π x assume "π ∈ L1 ∩ L2" and "x ∈ exec[L2,π]"
then have "(out[L1,π,x],out[L2,π,x]) ∈ semired Y"
using p1 executable_inputs_in_alphabet[OF assms(2)] by auto
moreover have "out[L2,π,x] ≠ {}"
using ‹x ∈ exec[L2,π]› by auto
ultimately show "(out[L1,π,x] ⊆ out[L2,π,x])"
unfolding semired.simps by blast
qed
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ ∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}"
using p2 by blast
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∉ exec[L2,π] ⟹ out[L1,π,x] = {}"
proof -
fix π x assume "π ∈ L1 ∩ L2" and "x ∉ exec[L2,π]"
have "(out[L1,π,x],out[L2,π,x]) ∈ strongsemired Y"
proof (cases "x ∈ exec[L1,π]")
case True
then show ?thesis
by (meson ‹π ∈ L1 ∩ L2› assms(1) executable_inputs_in_alphabet p1)
next
case False
then show ?thesis
using ‹x ∉ exec[L2,π]› by fastforce
qed
moreover have "out[L2,π,x] = {}"
using ‹x ∉ exec[L2,π]› by auto
ultimately show "out[L1,π,x] = {}"
unfolding strongsemired.simps
by blast
qed
ultimately show ?thesis
unfolding strong_semi_reduction_def by blast
qed
qed
lemma strongsemieq_type_2 :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "(strong_semi_equivalence L1 L2) ⟷ (L1 ≤[X, strongsemieq Y] L2)"
proof
show "strong_semi_equivalence L1 L2 ⟹ L1 ≤[X, strongsemieq Y] L2"
proof -
assume "strong_semi_equivalence L1 L2"
then have p1: "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ out[L1,π,x] = {} ∨ out[L1,π,x] = out[L2,π,x]"
and p2: "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ ∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}"
and p3: "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∉ exec[L2,π] ⟹ out[L1,π,x] = {}"
unfolding strong_semi_equivalence_def by blast+
have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x], out[L2,π,x]) ∈ strongsemieq Y"
proof -
fix π x assume "π ∈ L1 ∩ L2" and "x ∈ X"
show "(out[L1,π,x], out[L2,π,x]) ∈ strongsemieq Y"
proof (cases "x ∈ exec[L2,π]")
case True
then have "out[L2,π,x] ≠ {}" by auto
then show ?thesis
using p1[OF ‹π ∈ L1 ∩ L2› True]
using outputs_in_alphabet[OF assms(2)]
by fastforce
next
case False
then show ?thesis
using ‹π ∈ L1 ∩ L2› p3 by fastforce
qed
qed
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ exec[L2,π] ≠ {} ⟹ ∃x. out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
using p2 by fastforce
ultimately show "L1 ≤[X, strongsemieq Y] L2"
by auto
qed
show "L1 ≤[X,strongsemieq Y] L2 ⟹ strong_semi_equivalence L1 L2"
proof -
assume "L1 ≤[X,strongsemieq Y] L2"
then have p1 : "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x],out[L2,π,x]) ∈ strongsemieq Y"
and p2 : "⋀ π x . π ∈ L1 ∩ L2 ⟹ exec[L2,π] ≠ {} ⟹ ∃ x . out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
by auto
have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ out[L1,π,x] = {} ∨ out[L1,π,x] = out[L2,π,x]"
proof -
fix π x assume "π ∈ L1 ∩ L2" and "x ∈ exec[L2,π]"
then have "(out[L1,π,x],out[L2,π,x]) ∈ semieq Y"
using p1 executable_inputs_in_alphabet[OF assms(2)] by auto
moreover have "out[L2,π,x] ≠ {}"
using ‹x ∈ exec[L2,π]› by auto
ultimately show "out[L1,π,x] = {} ∨ out[L1,π,x] = out[L2,π,x]"
unfolding semieq.simps
by blast
qed
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ ∃ x' . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}"
using p2 by blast
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∉ exec[L2,π] ⟹ out[L1,π,x] = {}"
proof -
fix π x assume "π ∈ L1 ∩ L2" and "x ∉ exec[L2,π]"
have "(out[L1,π,x],out[L2,π,x]) ∈ strongsemieq Y"
proof (cases "x ∈ exec[L1,π]")
case True
then show ?thesis
by (meson ‹π ∈ L1 ∩ L2› assms(1) executable_inputs_in_alphabet p1)
next
case False
then show ?thesis
using ‹x ∉ exec[L2,π]› by fastforce
qed
moreover have "out[L2,π,x] = {}"
using ‹x ∉ exec[L2,π]› by auto
ultimately show "out[L1,π,x] = {}"
unfolding strongsemieq.simps
by blast
qed
ultimately show ?thesis
unfolding strong_semi_equivalence_def by blast
qed
qed
section ‹Comparing Conformance Relations›
lemma type_1_subset :
assumes "L1 ≼[X,H1] L2"
and "H1 ⊆ H2"
shows "L1 ≼[X,H2] L2"
using assms by auto
lemma type_1_subsets :
shows "equiv Y ⊆ strongred Y"
and "equiv Y ⊆ quasieq Y"
and "strongred Y ⊆ red Y"
and "strongred Y ⊆ quasired Y"
and "quasieq Y ⊆ quasired Y"
by auto
lemma type_1_implications :
shows "L1 ≼[X, equiv Y] L2 ⟹ L1 ≼[X, strongred Y] L2"
and "L1 ≼[X, equiv Y] L2 ⟹ L1 ≼[X, red Y] L2"
and "L1 ≼[X, equiv Y] L2 ⟹ L1 ≼[X, quasired Y] L2"
and "L1 ≼[X, equiv Y] L2 ⟹ L1 ≼[X, quasieq Y] L2"
and "L1 ≼[X, strongred Y] L2 ⟹ L1 ≼[X, red Y] L2"
and "L1 ≼[X, strongred Y] L2 ⟹ L1 ≼[X, quasired Y] L2"
and "L1 ≼[X, quasieq Y] L2 ⟹ L1 ≼[X, quasired Y] L2"
using type_1_subset[OF _ type_1_subsets(4), of L1 X Y L2]
using type_1_subset[OF _ type_1_subsets(5), of L1 X Y L2]
by auto
lemma type_2_subset :
assumes "L1 ≤[X,H1] L2"
and "H1 ⊆ H2"
shows "L1 ≤[X,H2] L2"
using assms by auto
lemma type_2_subsets :
shows "strongsemieq Y ⊆ strongsemired Y"
and "strongsemieq Y ⊆ semieq Y"
and "semieq Y ⊆ semired Y"
and "strongsemired Y ⊆ semired Y"
and "strongsemired Y ⊆ red Y"
by auto
lemma type_2_implications :
shows "L1 ≤[X, strongsemieq Y] L2 ⟹ L1 ≤[X, strongsemired Y] L2"
and "L1 ≤[X, strongsemieq Y] L2 ⟹ L1 ≤[X, semieq Y] L2"
and "L1 ≤[X, strongsemieq Y] L2 ⟹ L1 ≤[X, semired Y] L2"
and "L1 ≤[X, strongsemired Y] L2 ⟹ L1 ≤[X, semired Y] L2"
and "L1 ≤[X, semieq Y] L2 ⟹ L1 ≤[X, semired Y] L2"
by auto
lemma type_1_conformance_to_type_2 :
assumes "is_language X Y L2"
and "L1 ≼[X,H1] L2"
and "H1 ⊆ H2"
and "⋀ A B . (A,B) ∈ H1 ⟹ B ≠ {} ⟹ A ∩ B ≠ {}"
shows "L1 ≤[X,H2] L2"
proof -
have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x], out[L2,π,x]) ∈ H2"
using assms(2,3) by auto
moreover have "⋀ π . π ∈ L1 ∩ L2 ⟹ exec[L2,π] ≠ {} ⟹ ∃x. out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
proof -
fix π assume "π ∈ L1 ∩ L2" and "exec[L2,π] ≠ {}"
then obtain x where "x ∈ exec[L2,π]"
by blast
then have "x ∈ X"
by (meson assms(1) executable_inputs_in_alphabet)
then have "(out[L1,π,x], out[L2,π,x]) ∈ H1"
using ‹π ∈ L1 ∩ L2› assms(2) by auto
moreover have "out[L2,π,x] ≠ {}"
by (meson ‹x ∈ exec[L2,π]› outputs_executable)
ultimately have "out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
using assms(4) by blast
then show "∃x. out[L1,π,x] ∩ out[L2,π,x] ≠ {}"
by blast
qed
ultimately show ?thesis
by auto
qed
lemma type_1_and_2_mixed_implications :
assumes "is_language X Y L2"
shows "L1 ≤[X, strongsemieq Y] L2 ⟹ L1 ≼[X, red Y] L2"
and "L1 ≤[X, strongsemired Y] L2 ⟹ L1 ≼[X, red Y] L2"
and "L1 ≼[X, quasieq Y] L2 ⟹ L1 ≤[X, semieq Y] L2"
and "L1 ≼[X, quasired Y] L2 ⟹ L1 ≤[X, semired Y] L2"
and "L1 ≼[X, equiv Y] L2 ⟹ L1 ≤[X, strongsemieq Y] L2"
and "L1 ≼[X, strongred Y] L2 ⟹ L1 ≤[X, strongsemired Y] L2"
proof -
show "L1 ≤[X, strongsemieq Y] L2 ⟹ L1 ≼[X, red Y] L2"
and "L1 ≤[X, strongsemired Y] L2 ⟹ L1 ≼[X, red Y] L2"
by auto
have "⋀ A B . (A,B) ∈ quasieq Y ⟹ B ≠ {} ⟹ A ∩ B ≠ {}"
by auto
moreover have "quasieq Y ⊆ semieq Y"
by auto
ultimately show "L1 ≼[X, quasieq Y] L2 ⟹ L1 ≤[X, semieq Y] L2"
using type_1_conformance_to_type_2[OF assms] by blast
have "⋀ A B . (A,B) ∈ quasired Y ⟹ B ≠ {} ⟹ A ∩ B ≠ {}"
by auto
moreover have "quasired Y ⊆ semired Y"
unfolding quasired.simps semired.simps by blast
ultimately show "L1 ≼[X, quasired Y] L2 ⟹ L1 ≤[X, semired Y] L2"
using type_1_conformance_to_type_2[OF assms] by blast
have "⋀ A B . (A,B) ∈ equiv Y ⟹ B ≠ {} ⟹ A ∩ B ≠ {}"
by auto
moreover have "equiv Y ⊆ strongsemieq Y"
unfolding equiv.simps strongsemieq.simps by blast
ultimately show "L1 ≼[X, equiv Y] L2 ⟹ L1 ≤[X, strongsemieq Y] L2"
using type_1_conformance_to_type_2[OF assms] by blast
have "⋀ A B . (A,B) ∈ strongred Y ⟹ B ≠ {} ⟹ A ∩ B ≠ {}"
by auto
moreover have "strongred Y ⊆ strongsemired Y"
unfolding strongred.simps strongsemired.simps by blast
ultimately show "L1 ≼[X, strongred Y] L2 ⟹ L1 ≤[X, strongsemired Y] L2"
using type_1_conformance_to_type_2[OF assms] by blast
qed
subsection ‹Completely Specified Languages›
definition partiality_component :: "'y set ⇒ 'y output_relation" where
"partiality_component Y = {(A,{}) | A . A ⊆ Y} ∪ {({},A) | A . A ⊆ Y}"
abbreviation(input) "Π Y ≡ partiality_component Y"
lemma conformance_without_partiality :
shows "strongsemieq Y - Π Y = semieq Y - Π Y"
and "semieq Y - Π Y = equiv Y - Π Y"
and "strongsemired Y - Π Y = semired Y - Π Y"
and "semired Y - Π Y = red Y - Π Y"
unfolding partiality_component_def
by fastforce+
section ‹Conformance Testing›
type_synonym ('x,'y) state_cover = "('x,'y) language"
type_synonym ('x,'y) transition_cover = "('x,'y) state_cover × 'x set"
fun is_state_cover :: "('x,'y) language ⇒ ('x,'y) language ⇒ ('x,'y) state_cover ⇒ bool" where
"is_state_cover L1 L2 V = (∀ π ∈ L1 ∩ L2 . ∃ α ∈ V . ℒ[L1,π] = ℒ[L1,α] ∧ ℒ[L2,π] = ℒ[L2,α])"
lemma state_cover_subset :
assumes "is_language X Y L1"
and "is_language X Y L2"
and "is_state_cover L1 L2 V"
and "π ∈ L1 ∩ L2"
obtains α where "α ∈ V"
and "α ∈ L1 ∩ L2"
and "ℒ[L1,π] = ℒ[L1,α]"
and "ℒ[L2,π] = ℒ[L2,α]"
proof -
obtain α where "α ∈ V"
and "ℒ[L1,π] = ℒ[L1,α]"
and "ℒ[L2,π] = ℒ[L2,α]"
using assms
by (meson is_state_cover.elims(2))
moreover have "ℒ[L1,π] ≠ {}" and "ℒ[L2,π] ≠ {}"
by (metis Collect_empty_eq_bot Int_iff append.right_neutral assms(4) empty_def language_for_state.elims)+
ultimately have "α ∈ L1 ∩ L2"
using language_of_state_empty_iff[OF assms(1)] language_of_state_empty_iff[OF assms(2)]
by blast
then show ?thesis using that[OF ‹α ∈ V› _ ‹ℒ[L1,π] = ℒ[L1,α]› ‹ℒ[L2,π] = ℒ[L2,α]›]
by blast
qed
theorem sufficient_condition_for_type_1_conformance :
assumes "is_language X Y L1"
and "is_language X Y L2"
and "is_state_cover L1 L2 V"
shows "(L1 ≼[X,H] L2) ⟷ (∀ π ∈ V . ∀ x ∈ X . π ∈ L1 ∩ L2 ⟶ (out[L1,π,x], out[L2,π,x]) ∈ H)"
proof
show "(L1 ≼[X,H] L2) ⟹ (∀ π ∈ V . ∀ x ∈ X . π ∈ L1 ∩ L2 ⟶ (out[L1,π,x], out[L2,π,x]) ∈ H)"
by auto
have "(⋀ π x . π ∈ V ⟹ x ∈ X ⟹ π ∈ L1 ∩ L2 ⟹ (out[L1,π,x], out[L2,π,x]) ∈ H) ⟹ (⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x], out[L2,π,x]) ∈ H)"
proof -
fix π x assume "(⋀ π x . π ∈ V ⟹ x ∈ X ⟹ π ∈ L1 ∩ L2 ⟹ (out[L1,π,x], out[L2,π,x]) ∈ H)"
and "π ∈ L1 ∩ L2"
and "x ∈ X"
obtain α where "α ∈ V" and "α ∈ L1 ∩ L2" and "ℒ[L1,π] = ℒ[L1,α]" and "ℒ[L2,π] = ℒ[L2,α]"
using state_cover_subset[OF assms ‹π ∈ L1 ∩ L2›] by auto
then have "out[L1,π,x] = out[L1,α,x]" and "out[L2,π,x] = out[L2,α,x]"
by force+
moreover have "(out[L1,α,x], out[L2,α,x]) ∈ H"
using ‹(⋀ π x . π ∈ V ⟹ x ∈ X ⟹ π ∈ L1 ∩ L2 ⟹ (out[L1,π,x], out[L2,π,x]) ∈ H)› ‹α ∈ V› ‹x ∈ X› ‹α ∈ L1 ∩ L2›
by blast
ultimately show "(out[L1,π,x], out[L2,π,x]) ∈ H"
by simp
qed
then show "∀π∈V. ∀x∈X. π ∈ L1 ∩ L2 ⟶ (out[L1,π,x], out[L2,π,x]) ∈ H ⟹ L1 ≼[X,H] L2"
by auto
qed
theorem sufficient_condition_for_type_2_conformance :
assumes "is_language X Y L1"
and "is_language X Y L2"
and "is_state_cover L1 L2 V"
shows "(L1 ≤[X,H] L2) ⟷ (∀ π ∈ V . ∀ x ∈ X . π ∈ L1 ∩ L2 ⟶ (out[L1,π,x], out[L2,π,x]) ∈ H ∧ (out[L2,π,x] ≠ {} ⟶ (∃ x' ∈ X . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {})))"
proof
have "⋀ π x . (L1 ≤[X,H] L2) ⟹ π ∈ V ⟹ x ∈ X ⟹ π ∈ L1 ∩ L2 ⟹ (out[L1,π,x], out[L2,π,x]) ∈ H ∧ (out[L2,π,x] ≠ {} ⟶ (∃ x' ∈ X . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}))"
proof -
fix π x assume "L1 ≤[X,H] L2" and "π ∈ V" and "x ∈ X" and "π ∈ L1 ∩ L2"
have "(out[L1,π,x], out[L2,π,x]) ∈ H"
using ‹L1 ≤[X,H] L2› ‹π ∈ L1 ∩ L2› ‹x ∈ X› by force
moreover have "out[L2,π,x] ≠ {} ⟹ (∃ x' ∈ X . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {})"
by (metis (no_types, lifting) ‹L1 ≤[X,H] L2› ‹π ∈ L1 ∩ L2› assms(2) empty_iff executable_inputs_in_alphabet inf_bot_right outputs_executable type_2_conforms.elims(2))
ultimately show "(out[L1,π,x], out[L2,π,x]) ∈ H ∧ (out[L2,π,x] ≠ {} ⟶ (∃ x' ∈ X . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}))"
by blast
qed
then show "(L1 ≤[X,H] L2) ⟹ (∀ π ∈ V . ∀ x ∈ X . π ∈ L1 ∩ L2 ⟶ (out[L1,π,x], out[L2,π,x]) ∈ H ∧ (out[L2,π,x] ≠ {} ⟶ (∃ x' ∈ X . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {})))"
by auto
have "(⋀ π x . π ∈ V ⟹ x ∈ X ⟹ π ∈ L1 ∩ L2 ⟹ (out[L1,π,x], out[L2,π,x]) ∈ H ∧ (out[L2,π,x] ≠ {} ⟶ (∃ x' ∈ X . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}))) ⟹ (⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x], out[L2,π,x]) ∈ H)"
by (meson assms(1) assms(2) assms(3) sufficient_condition_for_type_1_conformance type_1_conforms.elims(2))
moreover have "(⋀ π x . π ∈ V ⟹ x ∈ X ⟹ π ∈ L1 ∩ L2 ⟹ (out[L1,π,x], out[L2,π,x]) ∈ H ∧ (out[L2,π,x] ≠ {} ⟶ (∃ x' ∈ X . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}))) ⟹ (⋀ π . π ∈ L1 ∩ L2 ⟹ exec[L2,π] ≠ {} ⟹ (∃ x . out[L1,π,x] ∩ out[L2,π,x] ≠ {}))"
proof -
fix π assume "π ∈ L1 ∩ L2"
and "exec[L2,π] ≠ {}"
and *: "(⋀ π x . π ∈ V ⟹ x ∈ X ⟹ π ∈ L1 ∩ L2 ⟹ (out[L1,π,x], out[L2,π,x]) ∈ H ∧ (out[L2,π,x] ≠ {} ⟶ (∃ x' ∈ X . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {})))"
then obtain x where "x ∈ X" and "out[L2,π,x] ≠ {}"
by (metis all_not_in_conv assms(2) executable_inputs_in_alphabet outputs_executable)
moreover obtain α where "α ∈ V"
and "α ∈ L1 ∩ L2"
and "ℒ[L1,π] = ℒ[L1,α]"
and "ℒ[L2,π] = ℒ[L2,α]"
using state_cover_subset[OF assms ‹π ∈ L1 ∩ L2›] by blast
ultimately show "(∃ x . out[L1,π,x] ∩ out[L2,π,x] ≠ {})"
using *
by (metis outputs.elims)
qed
ultimately show "(∀ π ∈ V . ∀ x ∈ X . π ∈ L1 ∩ L2 ⟶ (out[L1,π,x], out[L2,π,x]) ∈ H ∧ (out[L2,π,x] ≠ {} ⟶ (∃ x' ∈ X . out[L1,π,x'] ∩ out[L2,π,x'] ≠ {}))) ⟹ (L1 ≤[X,H] L2)"
by auto
qed
lemma intersections_card_helper :
assumes "finite X"
and "finite Y"
shows "card {A ∩ B | A B . A ∈ X ∧ B ∈ Y} ≤ card X * card Y"
proof -
have "{A ∩ B | A B . A ∈ X ∧ B ∈ Y} = (λ (A,B) . A ∩ B) ` (X × Y)"
by auto
then have "card {A ∩ B | A B . A ∈ X ∧ B ∈ Y} ≤ card (X × Y)"
by (metis (no_types, lifting) assms(1) assms(2) card_image_le finite_SigmaI)
then show ?thesis
by (simp add: card_cartesian_product)
qed
lemma prefix_length_take :
"(prefix xs ys ∧ length xs ≤ k) ⟷ (prefix xs (take k ys))"
proof
show "prefix xs ys ∧ length xs ≤ k ⟹ prefix xs (take k ys)"
using prefix_length_prefix take_is_prefix by fastforce
show "prefix xs (take k ys) ⟹ prefix xs ys ∧ length xs ≤ k"
by (metis le_trans length_take min.cobounded2 prefix_length_le prefix_order.order_trans take_is_prefix)
qed
lemma brute_force_state_cover :
assumes "is_language X Y L1"
and "is_language X Y L2"
and "finite {ℒ[L1,π] | π . π ∈ L1}"
and "finite {ℒ[L2,π] | π . π ∈ L2}"
and "card {ℒ[L1,π] | π . π ∈ L1} ≤ n"
and "card {ℒ[L2,π] | π . π ∈ L2} ≤ m"
shows "is_state_cover L1 L2 {α . length α ≤ m * n - 1 ∧ (∀ xy ∈ set α . fst xy ∈ X ∧ snd xy ∈ Y)}"
proof (rule ccontr)
let ?V = "{α. length α ≤ m * n - 1 ∧ (∀xy∈set α. fst xy ∈ X ∧ snd xy ∈ Y)}"
assume "¬ is_state_cover L1 L2 ?V"
define is_covered where "is_covered = (λ π . ∃ α ∈ ?V . ℒ[L1,π] = ℒ[L1,α] ∧ ℒ[L2,π] = ℒ[L2,α])"
define missing_traces where "missing_traces = {τ . τ ∈ L1 ∩ L2 ∧ ¬is_covered τ}"
define τ where "τ = arg_min length (λ π . π ∈ missing_traces)"
have "missing_traces ≠ {}"
using ‹¬ is_state_cover L1 L2 ?V›
using is_covered_def missing_traces_def by fastforce
then have "τ ∈ missing_traces"
"⋀ τ' . τ' ∈ missing_traces ⟹ length τ ≤ length τ'"
using arg_min_nat_lemma[where P="(λ π . π ∈ missing_traces)" and m=length]
unfolding τ_def[symmetric] by blast+
then have τ_props: "τ ∈ L1 ∩ L2"
"⋀ α . α ∈ ?V ⟹ ¬(ℒ[L1,τ] = ℒ[L1,α] ∧ ℒ[L2,τ] = ℒ[L2,α])"
unfolding missing_traces_def is_covered_def by blast+
have "⋀ xy . xy ∈ set τ ⟹ fst xy ∈ X ∧ snd xy ∈ Y"
using ‹τ ∈ L1 ∩ L2› assms(1) by auto
moreover have "τ ∉ ?V"
using τ_props(2) by blast
ultimately have "length τ > m*n-1"
by simp
let ?L12 = "{ℒ[L1,π] | π . π ∈ L1} × {ℒ[L2,π] | π . π ∈ L2}"
have "finite ?L12"
using assms(3,4)
by blast
have "card ?L12 ≤ m*n"
using assms(3,4,5,6)
by (metis (no_types, lifting) Sigma_cong card_cartesian_product mult.commute mult_le_mono)
let ?visited_states = "{(ℒ[L1,τ'],ℒ[L2,τ']) | τ' . τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1}"
have "⋀ τ' . τ' ∈ set (prefixes τ) ⟹ τ' ∈ L1 ∩ L2"
by (meson τ_props(1) assms(1) assms(2) in_set_prefixes is_language.elims(2) language_intersection_is_language)
then have "?visited_states ⊆ ?L12"
by blast
then have "card ?visited_states ≤ m * n"
using ‹finite ?L12› ‹card ?L12 ≤ m * n›
by (meson card_mono dual_order.trans)
have no_index_loop : "⋀ i j . i < j ⟹ j ≤ length τ ⟹ ℒ[L1, take i τ] ≠ ℒ[L1, take j τ] ∨ ℒ[L2, take i τ] ≠ ℒ[L2, take j τ]"
proof (rule ccontr)
fix i j
assume "i < j" and "j ≤ length τ" and "¬ (ℒ[L1,take i τ] ≠ ℒ[L1,take j τ] ∨ ℒ[L2,take i τ] ≠ ℒ[L2,take j τ])"
then have "ℒ[L1,take i τ] = ℒ[L1,take j τ]" and "ℒ[L2,take i τ] = ℒ[L2,take j τ]"
by auto
have "{τ'. τ @ τ' ∈ L1} = {τ'. take j τ @ drop j τ @ τ' ∈ L1}"
by (metis append.assoc append_take_drop_id)
have "{τ'. τ @ τ' ∈ L2} = {τ'. take j τ @ drop j τ @ τ' ∈ L2}"
by (metis append.assoc append_take_drop_id)
have "ℒ[L1,take i τ @ drop j τ] = ℒ[L1,τ]"
using ‹ℒ[L1,take i τ] = ℒ[L1,take j τ]›
unfolding language_for_state.simps
unfolding ‹{τ'. τ @ τ' ∈ L1} = {τ'. take j τ @ drop j τ @ τ' ∈ L1}› append.assoc by blast
moreover have "ℒ[L2,take i τ @ drop j τ] = ℒ[L2,τ]"
using ‹ℒ[L2,take i τ] = ℒ[L2,take j τ]›
unfolding language_for_state.simps
unfolding ‹{τ'. τ @ τ' ∈ L2} = {τ'. take j τ @ drop j τ @ τ' ∈ L2}› append.assoc by blast
have "(take i τ @ drop j τ) ∈ missing_traces"
proof (rule ccontr)
assume "take i τ @ drop j τ ∉ missing_traces"
moreover have "take i τ @ drop j τ ∈ L1 ∩ L2"
by (metis IntD1 IntD2 IntI ‹ℒ[L1,take i τ] = ℒ[L1,take j τ]› ‹ℒ[L2,take i τ] = ℒ[L2,take j τ]› τ_props(1) append_take_drop_id language_for_state.elims mem_Collect_eq)
ultimately obtain α where "length α ≤ m * n - 1"
"(∀xy∈set α. fst xy ∈ X ∧ snd xy ∈ Y)"
"ℒ[L1,take i τ @ drop j τ] = ℒ[L1,α]"
"ℒ[L2,take i τ @ drop j τ] = ℒ[L2,α]"
unfolding missing_traces_def is_covered_def
by blast
then have "τ ∉ missing_traces"
unfolding missing_traces_def is_covered_def
using ‹τ ∈ L1 ∩ L2›
unfolding ‹ℒ[L1,take i τ @ drop j τ] = ℒ[L1,τ]›
unfolding ‹ℒ[L2,take i τ @ drop j τ] = ℒ[L2,τ]›
by blast
then show False
using ‹τ ∈ missing_traces› by simp
qed
moreover have "length (take i τ @ drop j τ) < length τ"
using ‹i < j› ‹j ≤ length τ›
by (induction τ arbitrary: i j; auto)
ultimately show False
using ‹⋀ τ' . τ' ∈ missing_traces ⟹ length τ ≤ length τ'›
using leD by blast
qed
have no_prefix_loop : "⋀ τ' τ'' . τ' ∈ set (prefixes τ) ⟹ τ'' ∈ set (prefixes τ) ⟹ τ' ≠ τ'' ⟹ (ℒ[L1,τ'],ℒ[L2,τ']) ≠ (ℒ[L1,τ''],ℒ[L2,τ''])"
proof -
fix τ' τ'' assume "τ' ∈ set (prefixes τ)" and "τ'' ∈ set (prefixes τ)" and "τ' ≠ τ''"
obtain i where "τ' = take i τ" and "i ≤ length τ"
using ‹τ' ∈ set (prefixes τ)›
by (metis append_eq_conv_conj in_set_prefixes linorder_linear prefix_def take_all_iff)
obtain j where "τ'' = take j τ" and "j ≤ length τ"
using ‹τ'' ∈ set (prefixes τ)›
by (metis append_eq_conv_conj in_set_prefixes linorder_linear prefix_def take_all_iff)
have "i ≠ j"
using ‹τ' = take i τ› ‹τ' ≠ τ''› ‹τ'' = take j τ› by blast
then consider (a) "i < j" | (b) "j < i"
using nat_neq_iff by blast
then show "(ℒ[L1,τ'],ℒ[L2,τ']) ≠ (ℒ[L1,τ''],ℒ[L2,τ''])"
using no_index_loop
using ‹j ≤ length τ› ‹i ≤ length τ›
unfolding ‹τ' = take i τ› ‹τ'' = take j τ›
by (cases; blast)
qed
then have "inj_on (λ τ' . (ℒ[L1,τ'], ℒ[L2,τ'])) {τ' . τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1}"
using inj_onI
by (metis (mono_tags, lifting) mem_Collect_eq)
then have "card ((λ τ' . (ℒ[L1,τ'], ℒ[L2,τ'])) ` {τ' . τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1}) = card {τ' . τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1}"
using card_image by blast
moreover have "?visited_states = (λ τ' . (ℒ[L1,τ'], ℒ[L2,τ'])) ` {τ' . τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1}"
by auto
ultimately have "card ?visited_states = card {τ' . τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1}"
by simp
moreover have "card {τ' . τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1} = m*n"
proof -
have "{τ' . τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1} = set (prefixes (take (m*n-1) τ))"
unfolding in_set_prefixes prefix_length_take
by auto
moreover have "length (take (m*n-1) τ) = m*n-1"
using ‹length τ > m*n-1› by auto
ultimately show ?thesis
using length_prefixes distinct_prefixes
by (metis ‹card {(ℒ[L1,τ'], ℒ[L2,τ']) |τ'. τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1} = card {τ' ∈ set (prefixes τ). length τ' ≤ m * n - 1}› ‹card {(ℒ[L1,τ'], ℒ[L2,τ']) |τ'. τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1} ≤ m * n› distinct_card less_diff_conv not_less_iff_gr_or_eq order_le_less)
qed
ultimately have "card ?visited_states = m*n"
by simp
then have "?visited_states = ?L12"
by (metis (no_types, lifting) ‹card ({ℒ[L1,π] |π. π ∈ L1} × {ℒ[L2,π] |π. π ∈ L2}) ≤ m * n› ‹finite ({ℒ[L1,π] |π. π ∈ L1} × {ℒ[L2,π] |π. π ∈ L2})› ‹{(ℒ[L1,τ'], ℒ[L2,τ']) |τ'. τ' ∈ set (prefixes τ) ∧ length τ' ≤ m * n - 1} ⊆ {ℒ[L1,π] |π. π ∈ L1} × {ℒ[L2,π] |π. π ∈ L2}› card_seteq)
have "(ℒ[L1,τ], ℒ[L2,τ]) ∈ ?L12"
using ‹τ ∈ L1 ∩ L2›
by blast
moreover have "(ℒ[L1,τ], ℒ[L2,τ]) ∉ ?visited_states"
proof
assume "(ℒ[L1,τ], ℒ[L2,τ]) ∈ ?visited_states"
then obtain τ' where "(ℒ[L1,τ], ℒ[L2,τ]) = (ℒ[L1,τ'],ℒ[L2,τ'])"
and "τ' ∈ set (prefixes τ)"
and "length τ' ≤ m * n - 1"
by blast
then have "τ ≠ τ'"
using ‹length τ > m*n-1› by auto
show False
using ‹(ℒ[L1,τ], ℒ[L2,τ]) = (ℒ[L1,τ'],ℒ[L2,τ'])›
using no_prefix_loop[OF _ ‹τ' ∈ set (prefixes τ)› ‹τ ≠ τ'›]
by simp
qed
ultimately show False
unfolding ‹?visited_states = ?L12›
by blast
qed
section ‹Reductions Between Relations›
subsection ‹Quasi-Equivalence via Quasi-Reduction and Absences›
fun absence_completion :: "'x alphabet ⇒ 'y alphabet ⇒ ('x,'y) language ⇒ ('x, 'y × bool) language" where
"absence_completion X Y L =
((λ π . map (λ(x,y) . (x,(y,True))) π) ` L)
∪ {(map (λ(x,y) . (x,(y,True))) π)@[(x,(y,False))]@τ | π x y τ . π ∈ L ∧ out[L,π,x] ≠ {} ∧ y ∈ Y ∧ y ∉ out[L,π,x] ∧ (∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)}"
lemma absence_completion_is_language :
assumes "is_language X Y L"
shows "is_language X (Y × UNIV) (absence_completion X Y L)"
proof -
let ?L = "(absence_completion X Y L)"
have "[] ∈ ?L"
using language_contains_nil[OF assms] by auto
have "?L ≠ {}"
using language_contains_nil[OF assms] by auto
moreover have "⋀ γ xy . γ ∈ ?L ⟹ xy ∈ set γ ⟹ fst xy ∈ X ∧ snd xy ∈ (Y × UNIV)"
and "⋀ γ γ' . γ ∈ ?L ⟹ prefix γ' γ ⟹ γ' ∈ ?L"
proof -
fix γ xy γ' assume "γ ∈ ?L"
then consider (a) "γ ∈ ((λ π . map (λ(x,y) . (x,(y,True))) π) ` L)" |
(b) "γ ∈ {(map (λ(x,y) . (x,(y,True))) π)@[(x,(y,False))]@τ | π x y τ . π ∈ L ∧ out[L,π,x] ≠ {} ∧ y ∈ Y ∧ y ∉ out[L,π,x] ∧ (∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)}"
unfolding absence_completion.simps by blast
then have "(xy ∈ set γ ⟶ fst xy ∈ X ∧ snd xy ∈ (Y × UNIV)) ∧ (prefix γ' γ ⟶ γ' ∈ ?L)"
proof cases
case a
then obtain π where *:"γ = map (λ(x,y) . (x,(y,True))) π" and "π ∈ L"
by auto
then have p1: "⋀ xy . xy ∈ set π ⟹ fst xy ∈ X ∧ snd xy ∈ Y"
and p2: "⋀ π' . prefix π' π ⟹ π' ∈ L"
using assms by auto
have "xy ∈ set γ ⟹ fst xy ∈ X ∧ snd xy ∈ (Y × UNIV)"
proof -
assume "xy ∈ set γ"
then have "(fst xy, fst (snd xy)) ∈ set π" and "snd (snd xy) = True"
unfolding * by auto
then show "fst xy ∈ X ∧ snd xy ∈ (Y × UNIV)"
by (metis p1 SigmaI UNIV_I fst_conv prod.collapse snd_conv)
qed
moreover have "prefix γ' γ ⟹ γ' ∈ ?L"
proof -
assume "prefix γ' γ"
then obtain i where "γ' = take i γ"
by (metis append_eq_conv_conj prefix_def)
then have "γ' = map (λ(x,y) . (x,(y,True))) (take i π)"
unfolding * using take_map by blast
moreover have "take i π ∈ L"
using p2 ‹π ∈ L› take_is_prefix by blast
ultimately have "γ' ∈ ((λ π . map (λ(x,y) . (x,(y,True))) π) ` L)"
by simp
then show "γ' ∈ ?L"
by auto
qed
ultimately show ?thesis by blast
next
case b
then obtain π x y τ where *: "γ = (map (λ(x,y) . (x,(y,True))) π)@[(x,(y,False))]@τ"
and "π ∈ L"
and "out[L,π,x] ≠ {}"
and "y ∈ Y"
and "y ∉ out[L,π,x]"
and "(∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)"
by blast
then have p1: "⋀ xy . xy ∈ set π ⟹ fst xy ∈ X ∧ snd xy ∈ Y"
and p2: "⋀ π' . prefix π' π ⟹ π' ∈ L"
using assms by auto
have "x ∈ X"
using ‹out[L,π,x] ≠ {}› assms
by (meson executable_inputs_in_alphabet outputs_executable)
have "xy ∈ set γ ⟹ fst xy ∈ X ∧ snd xy ∈ (Y × UNIV)"
proof -
assume "xy ∈ set γ"
then consider (b1) "xy ∈ set (map (λ(x,y) . (x,(y,True))) π)" |
(b2) "xy = (x,(y,False))" |
(b3) "xy ∈ set τ"
unfolding * by force
then show ?thesis proof cases
case b1
then have "(fst xy, fst (snd xy)) ∈ set π" and "snd (snd xy) = True"
unfolding * by auto
then show "fst xy ∈ X ∧ snd xy ∈ (Y × UNIV)"
by (metis p1 SigmaI UNIV_I fst_conv prod.collapse snd_conv)
next
case b2
then show ?thesis
using ‹x ∈ X› ‹y ∈ Y› by simp
next
case b3
then show ?thesis
using ‹(∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)› by force
qed
qed
moreover have "prefix γ' γ ⟹ γ' ∈ ?L"
proof -
assume "prefix γ' γ"
then obtain i where "γ' = take i γ"
by (metis append_eq_conv_conj prefix_def)
then consider (b1) "i ≤ length π" |
(b2) "i > length π"
by linarith
then show "γ' ∈ ?L" proof cases
case b1
then have "i ≤ length (map (λ(x, y). (x, y, True)) π)"
by auto
then have "γ' = map (λ(x,y) . (x,(y,True))) (take i π)"
unfolding * ‹γ' = take i γ›
by (simp add: take_map)
moreover have "take i π ∈ L"
using p2 ‹π ∈ L› take_is_prefix by blast
ultimately have "γ' ∈ ((λ π . map (λ(x,y) . (x,(y,True))) π) ` L)"
by simp
then show "γ' ∈ ?L"
by auto
next
case b2
then have "i > length (map (λ(x, y). (x, y, True)) π)"
by auto
have "⋀ k xs ys . k > length xs ⟹ take k (xs@ys) = xs@(take (k - length xs) ys)"
by simp
have take_helper: "⋀ k xs y zs . k > length xs ⟹ take k (xs@[y]@zs) = xs@[y]@(take (k - length xs - 1) zs)"
by (metis One_nat_def Suc_pred ‹⋀ys xs k. length xs < k ⟹ take k (xs @ ys) = xs @ take (k - length xs) ys› append_Cons append_Nil take_Suc_Cons zero_less_diff)
have **: "γ' = (map (λ(x,y) . (x,(y,True))) π)@[(x,(y,False))]@(take (i - length π - 1) τ)"
unfolding * ‹γ' = take i γ›
using take_helper[OF ‹i > length (map (λ(x, y). (x, y, True)) π)›] by simp
have "(∀ (x,(y,a)) ∈ set (take (i - length π - 1) τ) . x ∈ X ∧ y ∈ Y)"
using ‹(∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)›
by (meson in_set_takeD)
then show ?thesis
unfolding ** absence_completion.simps
using ‹π ∈ L› ‹out[L,π,x] ≠ {}› ‹y ∈ Y› ‹y ∉ out[L,π,x]›
by blast
qed
qed
ultimately show ?thesis by simp
qed
then show "xy ∈ set γ ⟹ fst xy ∈ X ∧ snd xy ∈ (Y × UNIV)"
and "prefix γ' γ ⟹ γ' ∈ ?L"
by blast+
qed
ultimately show ?thesis
unfolding is_language.simps by blast
qed
lemma absence_completion_inclusion_R :
assumes "is_language X Y L"
and "π ∈ absence_completion X Y L"
shows "(map (λ(x,y,a) . (x,y)) π ∈ L) ⟷ (∀ (x,y,a) ∈ set π . a = True)"
proof -
define L'a where "L'a = ((λ π . map (λ(x,y) . (x,(y,True))) π) ` L)"
define L'b where "L'b = {(map (λ(x,y) . (x,(y,True))) π)@[(x,(y,False))]@τ | π x y τ . π ∈ L ∧ out[L,π,x] ≠ {} ∧ y ∈ Y ∧ y ∉ out[L,π,x] ∧ (∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)}"
have "⋀ π xya . π ∈ L'a ⟹ xya ∈ set π ⟹ snd (snd xya) = True"
unfolding L'a_def by auto
moreover have "⋀ π . π ∈ L'b ⟹ ∃ xya ∈ set π . snd (snd xya) = False"
unfolding L'b_def by auto
moreover have "π ∈ L'a ∪ L'b"
using assms(2) unfolding absence_completion.simps L'a_def L'b_def .
ultimately have "(∀ (x,y,a) ∈ set π . a = True) = (π ∈ L'a)"
by fastforce
show ?thesis proof (cases "(∀ (x,y,a) ∈ set π . a = True)")
case True
then obtain τ where "π = map (λ(x, y). (x, y, True)) τ"
and "τ ∈ L"
unfolding ‹(∀ (x,y,a) ∈ set π . a = True) = (π ∈ L'a)› L'a_def
by blast
have "map (λ(x, y, a). (x, y)) π = τ"
unfolding ‹π = map (λ(x, y). (x, y, True)) τ›
by (induction τ; auto)
show ?thesis
using True ‹τ ∈ L›
unfolding ‹(∀ (x,y,a) ∈ set π . a = True) = (π ∈ L'a)› L'a_def
unfolding ‹map (λ(x, y, a). (x, y)) π = τ›
unfolding ‹π = map (λ(x, y). (x, y, True)) τ›
by blast
next
case False
then have "π ∈ L'b"
using ‹(∀ (x,y,a) ∈ set π . a = True) = (π ∈ L'a)› ‹π ∈ L'a ∪ L'b› by blast
then obtain τ x y τ' where "π = (map (λ(x,y) . (x,(y,True))) τ)@[(x,(y,False))]@τ'"
and "τ ∈ L"
and "out[L,τ,x] ≠ {}"
and "y ∈ Y"
and "y ∉ out[L,τ,x]"
and "(∀ (x,(y,a)) ∈ set τ' . x ∈ X ∧ y ∈ Y)"
unfolding L'b_def by blast
then have "τ@[(x,y)] ∉ L"
by fastforce
then have "τ@[(x,y)]@(map (λ(x, y, a). (x, y)) τ') ∉ L"
using assms(1)
by (metis append.assoc prefix_closure_no_member)
moreover have "map (λ(x, y, a). (x, y)) π = τ@[(x,y)]@(map (λ(x, y, a). (x, y)) τ')"
unfolding ‹π = (map (λ(x,y) . (x,(y,True))) τ)@[(x,(y,False))]@τ'›
by (induction τ; auto)
ultimately have "map (λ(x, y, a). (x, y)) π ∉ L"
by simp
then show ?thesis
using False by blast
qed
qed
lemma absence_completion_inclusion_L :
"(π ∈ L) ⟷ (map (λ(x,y) . (x,y,True)) π ∈ absence_completion X Y L)"
proof -
let ?L = "absence_completion X Y L"
define L'a where "L'a = ((λ π . map (λ(x,y) . (x,(y,True))) π) ` L)"
define L'b where "L'b = {(map (λ(x,y) . (x,(y,True))) π)@[(x,(y,False))]@τ | π x y τ . π ∈ L ∧ out[L,π,x] ≠ {} ∧ y ∈ Y ∧ y ∉ out[L,π,x] ∧ (∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)}"
have "?L = L'a ∪ L'b"
unfolding L'a_def L'b_def absence_completion.simps by blast
have "⋀ π . π ∈ L'b ⟹ ∃ xya ∈ set π . snd (snd xya) = False"
unfolding L'b_def by auto
then have "(map (λ(x,y) . (x,y,True)) π ∈ ?L) = (map (λ(x,y) . (x,y,True)) π ∈ L'a)"
unfolding ‹?L = L'a ∪ L'b›
by fastforce
have "inj (λ π . map (λ(x,y) . (x,(y,True))) π)"
by (simp add: inj_def)
then show ?thesis
unfolding ‹(map (λ(x,y) . (x,y,True)) π ∈ ?L) = (map (λ(x,y) . (x,y,True)) π ∈ L'a)›
unfolding L'a_def
by (simp add: image_iff inj_def)
qed
fun is_present :: "('x,'y × bool) word ⇒ ('x,'y) language ⇒ bool" where
"is_present π L = (π ∈ map (λ(x, y). (x, y, True)) ` L)"
lemma is_present_rev :
assumes "is_present π L"
shows "map (λ(x, y, a). (x, y)) π ∈ L"
proof -
obtain π' where "π = map (λ(x, y). (x, y, True)) π'" and "π' ∈ L"
using assms by auto
moreover have "map (λ(x, y, a). (x, y)) (map (λ(x, y). (x, y, True)) π') = π'"
by (induction π'; auto)
ultimately show ?thesis
by force
qed
lemma absence_completion_out :
assumes "is_language X Y L"
and "x ∈ X"
and "π ∈ absence_completion X Y L"
shows "is_present π L ⟹ out[L,map (λ(x, y, a). (x, y)) π,x] ≠ {} ⟹ out[absence_completion X Y L, π, x] = {(y,True) | y . y ∈ out[L,map (λ(x, y, a). (x, y)) π,x]} ∪ {(y,False) | y . y ∈ Y ∧ y ∉ out[L,map (λ(x, y, a). (x, y)) π,x]}"
and "is_present π L ⟹ out[L,map (λ(x, y, a). (x, y)) π,x] = {} ⟹ out[absence_completion X Y L, π, x] = {}"
and "¬ is_present π L ⟹ out[absence_completion X Y L, π, x] = Y × UNIV"
proof -
let ?L = "absence_completion X Y L"
define L'a where "L'a = ((λ π . map (λ(x,y) . (x,(y,True))) π) ` L)"
define L'b where "L'b = {(map (λ(x,y) . (x,(y,True))) π)@[(x,(y,False))]@τ | π x y τ . π ∈ L ∧ out[L,π,x] ≠ {} ∧ y ∈ Y ∧ y ∉ out[L,π,x] ∧ (∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)}"
have "?L = L'a ∪ L'b"
unfolding L'a_def L'b_def absence_completion.simps by blast
then have "out[?L, π, x] = {y. π @ [(x, y)] ∈ L'a} ∪ {y. π @ [(x, y)] ∈ L'b}"
unfolding outputs.simps language_for_state.simps by blast
show "is_present π L ⟹ out[L,map (λ(x, y, a). (x, y)) π,x] ≠ {} ⟹ out[?L, π, x] = {(y,True) | y . y ∈ out[L,map (λ(x, y, a). (x, y)) π,x]} ∪ {(y,False) | y . y ∈ Y ∧ y ∉ out[L,map (λ(x, y, a). (x, y)) π,x]}"
proof -
assume "is_present π L" and "out[L,map (λ(x, y, a). (x, y)) π,x] ≠ {}"
then have "map (λ(x, y, a). (x, y)) π ∈ L"
using assms(1) by auto
have "{y. π @ [(x, y)] ∈ L'a} = {(y,True) | y . y ∈ out[L,map (λ(x, y, a). (x, y)) π,x]}"
proof
show "{y. π @ [(x, y)] ∈ L'a} ⊆ {(y, True) |y. y ∈ out[L,map (λ(x, y, a). (x, y)) π,x]}"
proof
fix ya assume "ya ∈ {y. π @ [(x, y)] ∈ L'a}"
then have "π @ [(x, ya)] ∈ map (λ(x, y). (x, y, True)) ` L"
unfolding L'a_def by blast
then obtain γ where "γ ∈ L" and "π @ [(x, ya)] = map (λ(x, y). (x, y, True)) γ"
by blast
then have "length (π @ [(x, ya)]) = length γ"
by auto
then obtain γ' xy where "γ = γ'@[xy]"
by (metis add.right_neutral dual_order.strict_iff_not length_append_singleton less_add_Suc2 rev_exhaust take0 take_all_iff)
then have "(x,ya) = (λ(x, y). (x, y, True)) xy"
using ‹π @ [(x, ya)] = map (λ(x, y). (x, y, True)) γ› unfolding ‹γ = γ'@[xy]› by auto
then have "ya = (snd xy, True)" and "xy = (x,snd xy)"
by (simp add: split_beta)+
moreover define y where "y = snd xy"
ultimately have "ya = (y, True)" and "xy = (x,y)"
by auto
have "π = map (λ(x, y). (x, y, True)) γ'"
using ‹π @ [(x, ya)] = map (λ(x, y). (x, y, True)) γ› unfolding ‹γ = γ'@[xy]› by auto
then have "map (λ(x, y, a). (x, y)) π = γ'"
by (induction π arbitrary: γ'; auto)
have "[(x, y)] ∈ {τ. map (λ(x, y, a). (x, y)) π @ τ ∈ L}"
using ‹γ ∈ L›
unfolding ‹γ = γ'@[xy]› ‹ya = (y, True)› ‹xy = (x,y)›
unfolding ‹map (λ(x, y, a). (x, y)) π = γ'›
by auto
then show "ya ∈ {(y, True) |y. y ∈ out[L,map (λ(x, y, a). (x, y)) π,x]}"
unfolding ‹ya = (snd xy, True)› outputs.simps language_for_state.simps
unfolding ‹ya = (y, True)› ‹xy = (x,y)› ‹map (λ(x, y, a). (x, y)) π = γ'›
by auto
qed
show "{(y, True) |y. y ∈ out[L,map (λ(x, y, a). (x, y)) π,x]} ⊆ {y. π @ [(x, y)] ∈ L'a}"
proof
fix ya assume "ya ∈ {(y, True) |y. y ∈ out[L,map (λ(x, y, a). (x, y)) π,x]}"
then obtain y where "ya = (y,True)" and "y ∈ out[L,map (λ(x, y, a). (x, y)) π,x]"
by blast
then have "[(x, y)] ∈ {τ. map (λ(x, y, a). (x, y)) π @ τ ∈ L}"
unfolding outputs.simps language_for_state.simps by auto
then have "(map (λ(x, y, a). (x, y)) π) @ [(x,y)] ∈ L"
by auto
moreover have "map (λ(x, y). (x, y, True)) ((map (λ(x, y, a). (x, y)) π) @ [(x,y)]) = π @ [(x, (y, True))]"
using ‹is_present π L› unfolding is_present.simps
by (induction π arbitrary: x y; auto)
ultimately have "π @ [(x, (y, True))] ∈ L'a"
unfolding L'a_def
by force
then show "ya ∈ {y. π @ [(x, y)] ∈ L'a}"
unfolding ‹ya = (y,True)›
by blast
qed
qed
moreover have "{y. π @ [(x, y)] ∈ L'b} = {(y,False) | y . y ∈ Y ∧ y ∉ out[L,map (λ(x, y, a). (x, y)) π,x]}"
proof
show "{y. π @ [(x, y)] ∈ L'b} ⊆ {(y, False) |y. y ∈ Y ∧ y ∉ out[L,map (λ(x, y, a). (x, y)) π,x]}"
proof
fix ya assume "ya ∈ {y. π @ [(x, y)] ∈ L'b}"
then have "π @ [(x,ya)] ∈ L'b"
by auto
then obtain π' x' y' τ where "π @ [(x,ya)] = map (λ(x, y). (x, y, True)) π' @ [(x', y', False)] @ τ"
and "π' ∈ L"
and "out[L,π',x'] ≠ {}"
and "y' ∈ Y"
and "y' ∉ out[L,π',x']"
and "(∀(x, y, a)∈set τ. x ∈ X ∧ y ∈ Y)"
unfolding L'b_def by blast
obtain π'' where "π = map (λ(x, y). (x, y, True)) π''" and "π'' ∈ L"
using ‹is_present π L› by auto
then have "⋀ xya . xya ∈ set π ⟹ snd (snd xya) = True"
by (induction π; auto)
have "τ = []"
proof (rule ccontr)
assume "τ ≠ []"
then obtain τ' xyz where "τ = τ'@[xyz]"
by (metis append_butlast_last_id)
then have "π = map (λ(x, y). (x, y, True)) π' @ [(x', y', False)] @ τ'"
using ‹π @ [(x,ya)] = map (λ(x, y). (x, y, True)) π' @ [(x', y', False)] @ τ›
by auto
then have "(x', y', False) ∈ set π"
by auto
then show False
using ‹⋀ xya . xya ∈ set π ⟹ snd (snd xya) = True› by force
qed
then have "x' = x" and "ya = (y', False)" and "π = map (λ(x, y). (x, y, True)) π'"
using ‹π @ [(x,ya)] = map (λ(x, y). (x, y, True)) π' @ [(x', y', False)] @ τ›
by auto
have *: "map (λ(x, y, a). (x, y)) (map (λ(x, y). (x, y, True)) π') = π'"
by (induction π'; auto)
have "y' ∉ out[L,map (λ(x, y, a). (x, y)) π,x]"
using ‹y' ∉ out[L,π',x']›
unfolding outputs.simps language_for_state.simps
unfolding ‹π = map (λ(x, y). (x, y, True)) π'› ‹x' = x›
unfolding * .
then show "ya ∈ {(y, False) |y. y ∈ Y ∧ y ∉ out[L,map (λ(x, y, a). (x, y)) π,x]}"
using ‹y' ∈ Y›
unfolding ‹ya = (y', False)› by auto
qed
show "{(y, False) |y. y ∈ Y ∧ y ∉ out[L,map (λ(x, y, a). (x, y)) π,x]} ⊆ {y. π @ [(x, y)] ∈ L'b}"
proof
fix ya assume "ya ∈ {(y, False) |y. y ∈ Y ∧ y ∉ out[L,map (λ(x, y, a). (x, y)) π,x]}"
then obtain y where "ya = (y,False)"
and "y ∈ Y"
and "y ∉ out[L,map (λ(x, y, a). (x, y)) π,x]"
by blast
obtain π' where "π = map (λ(x, y). (x, y, True)) π'" and "π' ∈ L"
using ‹is_present π L› by auto
have *: "map (λ(x, y, a). (x, y)) (map (λ(x, y). (x, y, True)) π') = π'"
by (induction π'; auto)
have "out[L,π',x] ≠ {}"
using ‹out[L,map (λ(x, y, a). (x, y)) π,x] ≠ {}›
unfolding ‹π = map (λ(x, y). (x, y, True)) π'› * .
have "y ∉ out[L,π',x]"
using ‹y ∉ out[L,map (λ(x, y, a). (x, y)) π,x]›
unfolding ‹π = map (λ(x, y). (x, y, True)) π'› * .
have "π@[(x,ya)] = map (λ(x, y). (x, y, True)) π' @ [(x, y, False)]"
unfolding ‹ya = (y,False)› ‹π = map (λ(x, y). (x, y, True)) π'›
by auto
then show "ya ∈ {y. π @ [(x, y)] ∈ L'b}"
unfolding L'b_def
using ‹π' ∈ L› ‹out[L,π',x] ≠ {}› ‹y ∈ Y› ‹y ∉ out[L,π',x]›
by force
qed
qed
ultimately show ?thesis
unfolding ‹out[?L, π, x] = {y. π @ [(x, y)] ∈ L'a} ∪ {y. π @ [(x, y)] ∈ L'b}›
by blast
qed
show "is_present π L ⟹ out[L,map (λ(x, y, a). (x, y)) π,x] = {} ⟹ out[absence_completion X Y L, π, x] = {}"
proof -
assume "is_present π L" and "out[L,map (λ(x, y, a). (x, y)) π,x] = {}"
obtain π' where "π = map (λ(x, y). (x, y, True)) π'" and "π' ∈ L"
using ‹is_present π L› by auto
have *: "map (λ(x, y, a). (x, y)) (map (λ(x, y). (x, y, True)) π') = π'"
by (induction π'; auto)
then have "map (λ(x, y, a). (x, y)) π = π'"
using ‹π = map (λ(x, y). (x, y, True)) π'› by blast
have "{y. π @ [(x, y)] ∈ L'a} = {}"
proof -
have "∄ y . π @ [(x, y)] ∈ L'a"
proof
assume "∃y. π @ [(x, y)] ∈ L'a"
then obtain ya where "π @ [(x, ya)] ∈ L'a"
by blast
then obtain π'' where "π'' ∈ L" and "map (λ(x, y). (x, y, True)) π'' = π @ [(x, ya)]"
unfolding L'a_def by force
then have "(x,ya) = (λ(x, y). (x, y, True)) (last π'')"
by (metis (mono_tags, lifting) append_is_Nil_conv last_map last_snoc list.map_disc_iff not_Cons_self2)
then obtain y where "ya = (y,True)"
by (simp add: split_beta)
have "map (λ(x, y). (x, y, True)) π'' = map (λ(x, y). (x, y, True)) (π' @ [(x, y)])"
using ‹map (λ(x, y). (x, y, True)) π'' = π @ [(x, ya)]›
unfolding ‹π = map (λ(x, y). (x, y, True)) π'› ‹ya = (y,True)› by auto
moreover have "inj (λ(x, y). (x, y, True))"
by (simp add: inj_def)
ultimately have "π'' = π' @ [(x,y)]"
using inj_map_eq_map by blast
show False
using ‹π'' ∈ L› ‹out[L,map (λ(x, y, a). (x, y)) π,x] = {}›
unfolding ‹map (λ(x, y, a). (x, y)) π = π'› ‹π'' = π' @ [(x,y)]›
by simp
qed
then show ?thesis
by blast
qed
moreover have "{y. π @ [(x, y)] ∈ L'b} = {}"
proof -
have "∄ y . π @ [(x, y)] ∈ L'b"
proof
assume "∃y. π @ [(x, y)] ∈ L'b"
then obtain ya where "π @ [(x, ya)] ∈ L'b"
by blast
then obtain π'' x' y' τ where "π @ [(x,ya)] = map (λ(x, y). (x, y, True)) π'' @ [(x', y', False)] @ τ"
and "π'' ∈ L"
and "out[L,π'',x'] ≠ {}"
and "y' ∈ Y"
and "y' ∉ out[L,π'',x']"
and "(∀(x, y, a)∈set τ. x ∈ X ∧ y ∈ Y)"
unfolding L'b_def by blast
have "⋀ xya . xya ∈ set π ⟹ snd (snd xya) = True"
using ‹π = map (λ(x, y). (x, y, True)) π'›
by (induction π; auto)
have "τ = []"
proof (rule ccontr)
assume "τ ≠ []"
then obtain τ' xyz where "τ = τ'@[xyz]"
by (metis append_butlast_last_id)
then have "π = map (λ(x, y). (x, y, True)) π'' @ [(x', y', False)] @ τ'"
using ‹π @ [(x,ya)] = map (λ(x, y). (x, y, True)) π'' @ [(x', y', False)] @ τ›
by auto
then have "(x', y', False) ∈ set π"
by auto
then show False
using ‹⋀ xya . xya ∈ set π ⟹ snd (snd xya) = True› by force
qed
then have "x' = x" and "ya = (y', False)" and "π = map (λ(x, y). (x, y, True)) π''"
using ‹π @ [(x,ya)] = map (λ(x, y). (x, y, True)) π'' @ [(x', y', False)] @ τ›
by auto
moreover have "inj (λ(x, y). (x, y, True))"
by (simp add: inj_def)
ultimately have "π'' = π'"
unfolding ‹π = map (λ(x, y). (x, y, True)) π'›
using map_injective by blast
then show False
using ‹out[L,π'',x'] ≠ {}› ‹out[L,map (λ(x, y, a). (x, y)) π,x] = {}›
unfolding ‹map (λ(x, y, a). (x, y)) π = π'› ‹x' = x›
by blast
qed
then show ?thesis
by blast
qed
ultimately show ?thesis
unfolding ‹out[?L, π, x] = {y. π @ [(x, y)] ∈ L'a} ∪ {y. π @ [(x, y)] ∈ L'b}›
by blast
qed
show "¬ is_present π L ⟹ out[absence_completion X Y L,π,x] = Y × UNIV"
proof
show "out[absence_completion X Y L,π,x] ⊆ Y × UNIV"
using absence_completion_is_language[OF assms(1)]
by (meson outputs_in_alphabet)
assume "¬ is_present π L"
then have "π ∉ L'a"
unfolding L'a_def by auto
then have "π ∈ L'b"
using ‹π ∈ ?L› ‹?L = L'a ∪ L'b› by blast
then obtain π' x' y' τ where "π = map (λ(x, y). (x, y, True)) π' @ [(x', y', False)] @ τ"
and "π' ∈ L"
and "out[L,π',x'] ≠ {}"
and "y' ∈ Y"
and "y' ∉ out[L,π',x']"
and "(∀(x, y, a)∈set τ. x ∈ X ∧ y ∈ Y)"
unfolding L'b_def by blast
show "Y × UNIV ⊆ out[absence_completion X Y L,π,x]"
proof
fix ya assume "ya ∈ Y × (UNIV :: bool set)"
have "π@[(x,ya)] = map (λ(x, y). (x, y, True)) π' @ [(x', y', False)] @ (τ @ [(x,ya)])"
using ‹π = map (λ(x, y). (x, y, True)) π' @ [(x', y', False)] @ τ›
by auto
moreover have ‹(∀(x, y, a)∈set (τ @ [(x,ya)]) . x ∈ X ∧ y ∈ Y)›
using ‹(∀(x, y, a)∈set τ. x ∈ X ∧ y ∈ Y)› ‹x ∈ X› ‹ya ∈ Y × (UNIV :: bool set)›
by auto
ultimately have "π@[(x,ya)] ∈ L'b"
unfolding L'b_def
using ‹π' ∈ L› ‹out[L,π',x'] ≠ {}› ‹y' ∈ Y› ‹y' ∉ out[L,π',x']›
by blast
then show "ya ∈ out[?L,π,x]"
unfolding ‹out[?L, π, x] = {y. π @ [(x, y)] ∈ L'a} ∪ {y. π @ [(x, y)] ∈ L'b}›
by blast
qed
qed
qed
theorem quasieq_via_quasired :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "(L1 ≼[X,quasieq Y] L2) ⟷ ((absence_completion X Y L1) ≼[X, quasired (Y × UNIV)] (absence_completion X Y L2))"
proof
define L1' where "L1' = absence_completion X Y L1"
define L2' where "L2' = absence_completion X Y L2"
define L1'a where "L1'a = ((λ π . map (λ(x,y) . (x,(y,True))) π) ` L1)"
define L1'b where "L1'b = {(map (λ(x,y) . (x,(y,True))) π)@[(x,(y,False))]@τ | π x y τ . π ∈ L1 ∧ out[L1,π,x] ≠ {} ∧ y ∈ Y ∧ y ∉ out[L1,π,x] ∧ (∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)}"
define L2'a where "L2'a = ((λ π . map (λ(x,y) . (x,(y,True))) π) ` L2)"
define L2'b where "L2'b = {(map (λ(x,y) . (x,(y,True))) π)@[(x,(y,False))]@τ | π x y τ . π ∈ L2 ∧ out[L2,π,x] ≠ {} ∧ y ∈ Y ∧ y ∉ out[L2,π,x] ∧ (∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)}"
have "⋀ π xya . π ∈ L1'a ⟹ xya ∈ set π ⟹ snd (snd xya) = True"
unfolding L1'a_def by auto
moreover have "⋀ π xya . π ∈ L2'a ⟹ xya ∈ set π ⟹ snd (snd xya) = True"
unfolding L2'a_def by auto
moreover have "⋀ π . π ∈ L1'b ⟹ ∃ xya ∈ set π . snd (snd xya) = False"
unfolding L1'b_def by auto
moreover have "⋀ π . π ∈ L2'b ⟹ ∃ xya ∈ set π . snd (snd xya) = False"
unfolding L2'b_def by auto
ultimately have "L1'a ∩ L2'b = {}" and "L1'b ∩ L2'a = {}"
by blast+
moreover have "L1' = L1'a ∪ L1'b"
unfolding L1'_def L1'a_def L1'b_def by auto
moreover have "L2' = L2'a ∪ L2'b"
unfolding L2'_def L2'a_def L2'b_def by auto
ultimately have "L1' ∩ L2' = (L1'a ∩ L2'a) ∪ (L1'b ∩ L2'b)"
by blast
have "inj (λ π . map (λ(x,y) . (x,(y,True))) π)"
by (simp add: inj_def)
then have "L1'a ∩ L2'a = ((λ π . map (λ(x,y) . (x,(y,True))) π) ` (L1 ∩ L2))"
unfolding L1'a_def L2'a_def
using image_Int by blast
have intersection_b: "L1'b ∩ L2'b = {(map (λ(x,y) . (x,(y,True))) π)@[(x,(y,False))]@τ | π x y τ . π ∈ L1 ∩ L2 ∧ out[L1,π,x] ≠ {} ∧ out[L2,π,x] ≠ {} ∧ y ∈ Y ∧ y ∉ out[L1,π,x] ∧ y ∉ out[L2,π,x] ∧ (∀ (x,(y,a)) ∈ set τ . x ∈ X ∧ y ∈ Y)}"
(is "L1'b ∩ L2'b = ?L12'b")
proof
show "?L12'b ⊆ L1'b ∩ L2'b"
unfolding L1'b_def L2'b_def by blast
show "L1'b ∩ L2'b ⊆ ?L12'b"
proof
fix γ assume "γ ∈ L1'b ∩ L2'b"
obtain π1 x1 y1 τ1 where "γ = (map (λ(x,y) . (x,(y,True))) π1)@[(x1,(y1,False))]@τ1"
and "π1 ∈ L1"
and "out[L1,π1,x1] ≠ {}"
and "y1 ∈ Y"
and "y1 ∉ out[L1,π1,x1]"
and "(∀ (x,(y,a)) ∈ set τ1 . x ∈ X ∧ y ∈ Y)"
using ‹γ ∈ L1'b ∩ L2'b› unfolding L1'b_def by blast
obtain π2 x2 y2 τ2 where "γ = (map (λ(x,y) . (x,(y,True))) π2)@[(x2,(y2,False))]@τ2"
and "π2 ∈ L2"
and "out[L2,π2,x2] ≠ {}"
and "y2 ∈ Y"
and "y2 ∉ out[L2,π2,x2]"
and "(∀ (x,(y,a)) ∈ set τ2 . x ∈ X ∧ y ∈ Y)"
using ‹γ ∈ L1'b ∩ L2'b› unfolding L2'b_def by blast
have "⋀ i . i < length π1 ⟹ snd (snd (γ ! i)) = True"
proof -
fix i assume "i < length π1"
then have "i < length (map (λ(x,y) . (x,(y,True))) π1)" by auto
then have "γ ! i = (map (λ(x,y) . (x,(y,True))) π1) ! i"
unfolding ‹γ = (map (λ(x,y) . (x,(y,True))) π1)@[(x1,(y1,False))]@τ1›
by (simp add: nth_append)
also have "… = (λ(x,y) . (x,(y,True))) (π1 ! i)"
using ‹i < length π1› nth_map by blast
finally show "snd (snd (γ ! i)) = True"
by (metis (no_types, lifting) case_prod_conv old.prod.exhaust snd_conv)
qed
have "γ ! length π1 = (x1,(y1,False))"
unfolding ‹γ = (map (λ(x,y) . (x,(y,True))) π1)@[(x1,(y1,False))]@τ1›
by (metis append_Cons length_map nth_append_length)
have "⋀ i . i < length π2 ⟹ snd (snd (γ ! i)) = True"
proof -
fix i assume "i < length π2"
then have "i < length (map (λ(x,y) . (x,(y,True))) π2)" by auto
then have "γ ! i = (map (λ(x,y) . (x,(y,True))) π2) ! i"
unfolding ‹γ = (map (λ(x,y) . (x,(y,True))) π2)@[(x2,(y2,False))]@τ2›
by (simp add: nth_append)
also have "… = (λ(x,y) . (x,(y,True))) (π2 ! i)"
using ‹i < length π2› nth_map by blast
finally show "snd (snd (γ ! i)) = True"
by (metis (no_types, lifting) case_prod_conv old.prod.exhaust snd_conv)
qed
have "γ ! length π2 = (x2,(y2,False))"
unfolding ‹γ = (map (λ(x,y) . (x,(y,True))) π2)@[(x2,(y2,False))]@τ2›
by (metis append_Cons length_map nth_append_length)
have "length π1 = length π2"
by (metis ‹⋀i. i < length π1 ⟹ snd (snd (γ ! i)) = True› ‹⋀i. i < length π2 ⟹ snd (snd (γ ! i)) = True› ‹γ ! length π1 = (x1, y1, False)› ‹γ ! length π2 = (x2, y2, False)› not_less_iff_gr_or_eq snd_conv)
then have "π1 = π2"
using ‹γ = (map (λ(x,y) . (x,(y,True))) π1)@[(x1,(y1,False))]@τ1› ‹inj (λ π . map (λ(x,y) . (x,(y,True))) π)›
unfolding ‹γ = (map (λ(x,y) . (x,(y,True))) π2)@[(x2,(y2,False))]@τ2›
using map_injective by fastforce
then have "[(x1,(y1,False))]@τ1 = [(x2,(y2,False))]@τ2"
using ‹γ = (map (λ(x,y) . (x,(y,True))) π1)@[(x1,(y1,False))]@τ1›
unfolding ‹γ = (map (λ(x,y) . (x,(y,True))) π2)@[(x2,(y2,False))]@τ2›
by force
then have "x1 = x2" and "y1 = y2" and "τ1 = τ2"
by auto
show "γ ∈ ?L12'b"
using ‹π1 ∈ L1› ‹out[L1,π1,x1] ≠ {}› ‹y1 ∈ Y› ‹y1 ∉ out[L1,π1,x1]› ‹(∀ (x,(y,a)) ∈ set τ1 . x ∈ X ∧ y ∈ Y)›
using ‹π2 ∈ L2› ‹out[L2,π2,x2] ≠ {}› ‹y2 ∈ Y› ‹y2 ∉ out[L2,π2,x2]› ‹(∀ (x,(y,a)) ∈ set τ2 . x ∈ X ∧ y ∈ Y)›
unfolding ‹π1 = π2› ‹x1 = x2› ‹y1 = y2› ‹τ1 = τ2› ‹γ = (map (λ(x,y) . (x,(y,True))) π2)@[(x2,(y2,False))]@τ2›
by blast
qed
qed
have "is_language X (Y × UNIV) L1'"
using absence_completion_is_language[OF assms(1)] unfolding L1'_def .
have "is_language X (Y × UNIV) L2'"
using absence_completion_is_language[OF assms(2)] unfolding L2'_def .
have "(L1 ≼[X,quasieq Y] L2) = quasi_equivalence L1 L2"
using quasieq_type_1[OF assms] by blast
have "(L1' ≼[X,quasired (Y × UNIV)] L2') = quasi_reduction L1' L2'"
using quasired_type_1[OF ‹is_language X (Y × UNIV) L1'› ‹is_language X (Y × UNIV) L2'›] by blast
have "⋀ π x . quasi_equivalence L1 L2 ⟹ π ∈ L1' ∩ L2' ⟹ x ∈ exec[L2',π] ⟹ (out[L1',π,x] ≠ {} ∧ out[L1',π,x] ⊆ out[L2',π,x])"
proof -
fix π x assume "quasi_equivalence L1 L2" and "π ∈ L1' ∩ L2'" and "x ∈ exec[L2',π]"
have "x ∈ X"
using ‹x ∈ exec[L2',π]› absence_completion_is_language[OF assms(2)]
by (metis L2'_def executable_inputs_in_alphabet)
have "π ∈ absence_completion X Y L1" and "π ∈ absence_completion X Y L2"
using ‹π ∈ L1' ∩ L2'› unfolding L1'_def L2'_def by blast+
consider (a) "π ∈ L1'a ∩ L2'a" | (b) "π ∈ (L1'b ∩ L2'b) - (L1'a ∩ L2'a)"
using ‹π ∈ L1' ∩ L2'› ‹L1' ∩ L2' = (L1'a ∩ L2'a) ∪ (L1'b ∩ L2'b)› by blast
then show "(out[L1',π,x] ≠ {} ∧ out[L1',π,x] ⊆ out[L2',π,x])"
proof cases
case a
then obtain τ where "τ ∈ L1 ∩ L2"
and "π = map (λ(x,y) . (x,(y,True))) τ"
using ‹L1'a ∩ L2'a = ((λ π . map (λ(x,y) . (x,(y,True))) π) ` (L1 ∩ L2))› by blast
have "map (λ(x, y, a). (x, y)) π = τ"
unfolding ‹π = map (λ(x,y) . (x,(y,True))) τ› by (induction τ; auto)
have "is_present π L1" and "is_present π L2"
using ‹τ ∈ L1 ∩ L2› unfolding ‹π = map (λ(x,y) . (x,(y,True))) τ› by auto
have "out[L2,map (λ(x, y, a). (x, y)) π,x] ≠ {}"
using ‹x ∈ exec[L2',π]›
using absence_completion_out(2)[OF assms(2) ‹x ∈ X› ‹π ∈ absence_completion X Y L2› ‹is_present π L2›]
unfolding L2'_def[symmetric]
by (meson outputs_executable)
then have "x ∈ exec[L2,map (λ(x, y, a). (x, y)) π]"
by auto
then have "out[L1,map (λ(x, y, a). (x, y)) π,x] ≠ {}" and "out[L1,map (λ(x, y, a). (x, y)) π,x] = out[L2,map (λ(x, y, a). (x, y)) π,x]"
using ‹quasi_equivalence L1 L2› ‹τ ∈ L1 ∩ L2›
unfolding quasi_equivalence_def ‹map (λ(x, y, a). (x, y)) π = τ› by force+
have "out[L1',π,x] = out[L2',π,x]"
unfolding L1'_def L2'_def
unfolding absence_completion_out(1)[OF assms(2) ‹x ∈ X› ‹π ∈ absence_completion X Y L2› ‹is_present π L2› ‹out[L2,map (λ(x, y, a). (x, y)) π,x] ≠ {}›]
unfolding absence_completion_out(1)[OF assms(1) ‹x ∈ X› ‹π ∈ absence_completion X Y L1› ‹is_present π L1› ‹out[L1,map (λ(x, y, a). (x, y)) π,x] ≠ {}›]
using ‹quasi_equivalence L1 L2› ‹τ ∈ L1 ∩ L2› ‹x ∈ exec[L2,map (λ(x, y, a). (x, y)) π]›
unfolding quasi_equivalence_def
unfolding ‹map (λ(x, y, a). (x, y)) π = τ›
by blast
then show ?thesis
by (metis ‹x ∈ exec[L2',π]› dual_order.refl outputs_executable)
next
case b
then obtain π' x' y' τ' where "π = map (λ(x, y). (x, y, True)) π' @ [(x', y', False)] @ τ'"
and "π' ∈ L1 ∩ L2"
and "out[L1,π',x'] ≠ {}"
and "out[L2,π',x'] ≠ {}"
and "y' ∈ Y"
and "y' ∉ out[L1,π',x']"
and "y' ∉ out[L2,π',x']"
and "(∀(x, y, a)∈set τ'. x ∈ X ∧ y ∈ Y)"
unfolding intersection_b
by blast
have "¬ is_present π L1"
using ‹L1'a ≡ map (λ(x, y). (x, y, True)) ` L1› ‹L1'a ∩ L2'b = {}› b by auto
have "¬ is_present π L2"
using ‹L2'a ≡ map (λ(x, y). (x, y, True)) ` L2› ‹L1'b ∩ L2'a = {}› b by auto
show ?thesis
unfolding L1'_def L2'_def
unfolding absence_completion_out(3)[OF assms(1) ‹x ∈ X› ‹π ∈ absence_completion X Y L1› ‹¬ is_present π L1›]
unfolding absence_completion_out(3)[OF assms(2) ‹x ∈ X› ‹π ∈ absence_completion X Y L2› ‹¬ is_present π L2›]
using ‹y' ∈ Y›
by blast
qed
qed
then show "L1 ≼[X,quasieq Y] L2 ⟹ (absence_completion X Y L1) ≼[X,quasired (Y × UNIV)] (absence_completion X Y L2)"
unfolding L1'_def[symmetric] L2'_def[symmetric]
unfolding ‹(L1' ≼[X,quasired (Y × UNIV)] L2') = quasi_reduction L1' L2'›
unfolding ‹(L1 ≼[X,quasieq Y] L2) = quasi_equivalence L1 L2›
unfolding quasi_reduction_def
by blast
have "⋀ π x . quasi_reduction L1' L2' ⟹ π ∈ L1 ∩ L2 ⟹ x ∈ exec[L2,π] ⟹ out[L1,π,x] = out[L2,π,x]"
proof -
fix π x assume "quasi_reduction L1' L2'" and "π ∈ L1 ∩ L2" and "x ∈ exec[L2,π]"
then have "x ∈ X"
by (meson assms(2) executable_inputs_in_alphabet)
let ?π = "map (λ(x, y). (x, y, True)) π"
have "map (λ(x, y, a). (x, y)) ?π = π"
by (induction π; auto)
then have "out[L2,map (λ(x, y, a). (x, y)) ?π,x] ≠ {}"
using ‹x ∈ exec[L2,π]› by auto
have "is_present ?π L1" and "is_present ?π L2"
using ‹π ∈ L1 ∩ L2› by auto
have "?π ∈ L1'a ∩ L2'a"
using L1'a_def ‹L2'a ≡ map (λ(x, y). (x, y, True)) ` L2› ‹is_present (map (λ(x, y). (x, y, True)) π) L1› ‹is_present (map (λ(x, y). (x, y, True)) π) L2› by auto
then have "?π ∈ absence_completion X Y L1" and "?π ∈ absence_completion X Y L2" and "?π ∈ L1' ∩ L2'"
unfolding L1'_def[symmetric] L2'_def[symmetric]
unfolding ‹L1' = L1'a ∪ L1'b› ‹L2' = L2'a ∪ L2'b›
by blast+
have "out[L2',?π,x] = {(y, True) |y. y ∈ out[L2,π,x]} ∪ {(y, False) |y. y ∈ Y ∧ y ∉ out[L2,π,x]}"
using absence_completion_out(1)[OF assms(2) ‹x ∈ X› ‹?π ∈ absence_completion X Y L2› ‹is_present ?π L2› ‹out[L2,map (λ(x, y, a). (x, y)) ?π,x] ≠ {}›]
unfolding L2'_def[symmetric] ‹map (λ(x, y, a). (x, y)) ?π = π› .
then have "x ∈ exec[L2',?π]"
using ‹x ∈ exec[L2,π]› by fastforce
then have "out[L1',?π,x] ≠ {}" and "out[L1',?π,x] ⊆ out[L2',?π,x]"
using ‹quasi_reduction L1' L2'› ‹?π ∈ L1' ∩ L2'›
unfolding quasi_reduction_def
by blast+
have "out[L1,π,x] ≠ {}"
by (metis L1'_def ‹is_present (map (λ(x, y). (x, y, True)) π) L1› ‹map (λ(x, y). (x, y, True)) π ∈ absence_completion X Y L1› ‹map (λ(x, y, a). (x, y)) (map (λ(x, y). (x, y, True)) π) = π› ‹out[L1',map (λ(x, y). (x, y, True)) π,x] ≠ {}› ‹x ∈ X› absence_completion_out(2) assms(1))
then have "out[L1',?π,x] = {(y, True) |y. y ∈ out[L1,π,x]} ∪ {(y, False) |y. y ∈ Y ∧ y ∉ out[L1,π,x]}"
using absence_completion_out(1)[OF assms(1) ‹x ∈ X› ‹?π ∈ absence_completion X Y L1› ‹is_present ?π L1›]
unfolding L1'_def[symmetric] ‹map (λ(x, y, a). (x, y)) ?π = π›
by blast
have "out[L1,π,x] ⊆ Y" and "out[L2,π,x] ⊆ Y"
by (meson assms(1,2) outputs_in_alphabet)+
have "⋀ y . y ∈ out[L1,π,x] ⟹ y ∈ out[L2,π,x]"
proof -
fix y assume "y ∈ out[L1,π,x]"
then have "(y, True) ∈ out[L1',?π,x]"
unfolding ‹out[L1',?π,x] = {(y, True) |y. y ∈ out[L1,π,x]} ∪ {(y, False) |y. y ∈ Y ∧ y ∉ out[L1,π,x]}› by blast
then have "(y, True) ∈ out[L2',?π,x]"
using ‹out[L1',?π,x] ⊆ out[L2',?π,x]› by blast
then show "y ∈ out[L2,π,x]"
unfolding ‹out[L2',?π,x] = {(y, True) |y. y ∈ out[L2,π,x]} ∪ {(y, False) |y. y ∈ Y ∧ y ∉ out[L2,π,x]}›
by fastforce
qed
moreover have "⋀ y . y ∈ out[L2,π,x] ⟹ y ∈ out[L1,π,x]"
proof -
fix y assume "y ∈ out[L2,π,x]"
then have "(y, True) ∈ out[L2',?π,x]" and "(y, False) ∉ out[L2',?π,x]"
unfolding ‹out[L2',?π,x] = {(y, True) |y. y ∈ out[L2,π,x]} ∪ {(y, False) |y. y ∈ Y ∧ y ∉ out[L2,π,x]}› by blast+
moreover have "(y, True) ∈ out[L1',?π,x] ∨ (y, False) ∈ out[L1',?π,x]"
unfolding ‹out[L1',?π,x] = {(y, True) |y. y ∈ out[L1,π,x]} ∪ {(y, False) |y. y ∈ Y ∧ y ∉ out[L1,π,x]}›
using ‹out[L2,π,x] ⊆ Y› ‹y ∈ out[L2,π,x]› by auto
ultimately have "(y, True) ∈ out[L1',?π,x]"
using ‹out[L1',?π,x] ⊆ out[L2',?π,x]› by blast
then show "y ∈ out[L1,π,x]"
unfolding ‹out[L1',?π,x] = {(y, True) |y. y ∈ out[L1,π,x]} ∪ {(y, False) |y. y ∈ Y ∧ y ∉ out[L1,π,x]}›
by fastforce
qed
ultimately show "out[L1,π,x] = out[L2,π,x]"
by blast
qed
then show "(absence_completion X Y L1) ≼[X,quasired (Y × UNIV)] (absence_completion X Y L2) ⟹ L1 ≼[X,quasieq Y] L2"
unfolding L1'_def[symmetric] L2'_def[symmetric]
unfolding ‹(L1' ≼[X,quasired (Y × UNIV)] L2') = quasi_reduction L1' L2'›
unfolding ‹(L1 ≼[X,quasieq Y] L2) = quasi_equivalence L1 L2›
unfolding quasi_reduction_def quasi_equivalence_def
by blast
qed
subsection ‹Quasi-Reduction via Reduction and explicit Undefined Behaviour›
fun bottom_completion :: "'x alphabet ⇒ 'y alphabet ⇒ ('x,'y) language ⇒ ('x, 'y option) language" where
"bottom_completion X Y L =
((λ π . map (λ(x,y) . (x,Some y)) π) ` L)
∪ {(map (λ(x,y) . (x,Some y)) π)@[(x,y)]@τ | π x y τ . π ∈ L ∧ out[L,π,x] = {} ∧ x ∈ X ∧ (y = None ∨ y ∈ Some ` Y) ∧ (∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))}"
lemma bottom_completion_is_language :
assumes "is_language X Y L"
shows "is_language X ({None} ∪ Some ` Y) (bottom_completion X Y L)"
proof -
let ?L = "bottom_completion X Y L"
have "?L ≠ {}"
using language_contains_nil[OF assms] by auto
moreover have "⋀ π . π ∈ ?L ⟹ (∀ xy ∈ set π . fst xy ∈ X ∧ snd xy ∈ ({None} ∪ Some ` Y)) ∧ (∀ π' . prefix π' π ⟶ π' ∈ ?L)"
proof -
fix π assume "π ∈ ?L"
then consider (a) "π ∈ ((λ π . map (λ(x,y) . (x,Some y)) π) ` L)" |
(b) "π ∈ {(map (λ(x,y) . (x,Some y)) π)@[(x,y)]@τ | π x y τ . π ∈ L ∧ out[L,π,x] = {} ∧ x ∈ X ∧ (y = None ∨ y ∈ Some ` Y) ∧ (∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))}"
unfolding bottom_completion.simps by blast
then show "(∀ xy ∈ set π . fst xy ∈ X ∧ snd xy ∈ ({None} ∪ Some ` Y)) ∧ (∀ π' . prefix π' π ⟶ π' ∈ ?L)"
proof cases
case a
then obtain π' where "π = map (λ(x, y). (x, Some y)) π'" and "π' ∈ L"
by auto
then have "(∀ xy ∈ set π' . fst xy ∈ X ∧ snd xy ∈ Y)"
and "(∀ π'' . prefix π'' π' ⟶ π'' ∈ L)"
using assms by auto
have "(∀ π' . prefix π' π ⟶ π' ∈ ((λ π . map (λ(x,y) . (x,Some y)) π) ` L))"
using ‹(∀ π'' . prefix π'' π' ⟶ π'' ∈ L)› unfolding ‹π = map (λ(x, y). (x, Some y)) π'›
using prefix_map_rightE by force
then have "(∀ π' . prefix π' π ⟶ π' ∈ ?L)"
by auto
moreover have "(∀ xy ∈ set π . fst xy ∈ X ∧ snd xy ∈ ({None} ∪ Some ` Y))"
using ‹(∀ xy ∈ set π' . fst xy ∈ X ∧ snd xy ∈ Y)› unfolding ‹π = map (λ(x, y). (x, Some y)) π'›
by (induction π'; auto)
ultimately show ?thesis
by blast
next
case b
then obtain π' x y τ where "π = (map (λ(x,y) . (x,Some y)) π')@[(x,y)]@τ"
and "π' ∈ L"
and "out[L,π',x] = {}"
and "x ∈ X"
and "(y = None ∨ y ∈ Some ` Y)"
and "(∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))"
by blast
then have "(∀ xy ∈ set π' . fst xy ∈ X ∧ snd xy ∈ Y)"
and "(∀ π'' . prefix π'' π' ⟶ π'' ∈ L)"
using assms by auto
have "(∀ xy ∈ set (map (λ(x,y) . (x,Some y)) π') . fst xy ∈ X ∧ snd xy ∈ ({None} ∪ Some ` Y))"
using ‹(∀ xy ∈ set π' . fst xy ∈ X ∧ snd xy ∈ Y)›
by (induction π'; auto)
moreover have "set π = set (map (λ(x,y) . (x,Some y)) π') ∪ {(x,y)} ∪ set τ"
unfolding ‹π = (map (λ(x,y) . (x,Some y)) π')@[(x,y)]@τ›
by simp
ultimately have "(∀ xy ∈ set π . fst xy ∈ X ∧ snd xy ∈ ({None} ∪ Some ` Y))"
using ‹x ∈ X› ‹(y = None ∨ y ∈ Some ` Y)› ‹(∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))›
by auto
moreover have "⋀ π'' . prefix π'' π ⟹ π'' ∈ ?L"
proof -
fix π'' assume "prefix π'' π"
then obtain i where "π'' = take i π"
by (metis append_eq_conv_conj prefix_def)
then consider (b1) "i ≤ length π'" |
(b2) "i > length π'"
by linarith
then show "π'' ∈ ?L" proof cases
case b1
then have "i ≤ length (map (λ(x,y) . (x,Some y)) π')"
by auto
then have "π'' = map (λ(x,y) . (x,Some y)) (take i π')"
unfolding ‹π'' = take i π›
using ‹π = map (λ(x, y). (x, Some y)) π' @ [(x, y)] @ τ› take_map by fastforce
moreover have "take i π' ∈ L"
using ‹π' ∈ L› take_is_prefix
using ‹∀π''. prefix π'' π' ⟶ π'' ∈ L› by blast
ultimately have "π'' ∈ ((λ π . map (λ(x,y) . (x,Some y)) π) ` L)"
by simp
then show "π'' ∈ ?L"
by auto
next
case b2
then have "i > length (map (λ(x,y) . (x,Some y)) π')"
by auto
have "⋀ k xs ys . k > length xs ⟹ take k (xs@ys) = xs@(take (k - length xs) ys)"
by simp
have take_helper: "⋀ k xs y zs . k > length xs ⟹ take k (xs@[y]@zs) = xs@[y]@(take (k - length xs - 1) zs)"
by (metis One_nat_def Suc_pred ‹⋀ys xs k. length xs < k ⟹ take k (xs @ ys) = xs @ take (k - length xs) ys› append_Cons append_Nil take_Suc_Cons zero_less_diff)
have **: "π'' = (map (λ(x,y) . (x,Some y)) π')@[(x,y)]@(take (i - length π' - 1) τ)"
unfolding ‹π = map (λ(x, y). (x, Some y)) π' @ [(x, y)] @ τ› ‹π'' = take i π›
using take_helper[OF ‹i > length (map (λ(x,y) . (x,Some y)) π')›] by simp
have "(∀ (x,y) ∈ set (take (i - length π' - 1) τ) . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))"
using ‹(∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))›
by (meson in_set_takeD)
then show ?thesis
unfolding ** bottom_completion.simps
using ‹π' ∈ L› ‹out[L,π',x] = {}› ‹x ∈ X› ‹(y = None ∨ y ∈ Some ` Y)›
by blast
qed
qed
ultimately show ?thesis by auto
qed
qed
ultimately show ?thesis
unfolding is_language.simps by blast
qed
fun is_not_undefined :: "('x,'y option) word ⇒ ('x,'y) language ⇒ bool" where
"is_not_undefined π L = (π ∈ map (λ(x, y). (x, Some y)) ` L)"
lemma bottom_id : "map (λ(x,y) . (x, the y)) (map (λ(x, y). (x, Some y)) π) = π"
by (induction π; auto)
fun maximum_prefix_with_property :: "('a list ⇒ bool) ⇒ 'a list ⇒ 'a list" where
"maximum_prefix_with_property P xs = (last (filter P (prefixes xs)))"
lemma maximum_prefix_with_property_props :
assumes "∃ ys ∈ set (prefixes xs) . P ys"
shows "P (maximum_prefix_with_property P xs)"
and "(maximum_prefix_with_property P xs) ∈ set (prefixes xs)"
and "⋀ ys . prefix ys xs ⟹ P ys ⟹ length ys ≤ length (maximum_prefix_with_property P xs)"
proof -
have "P (maximum_prefix_with_property P xs) ∧
(maximum_prefix_with_property P xs) ∈ set (prefixes xs) ∧
(∀ ys . prefix ys xs ⟶ P ys ⟶ length ys ≤ length (maximum_prefix_with_property P xs))"
using assms
proof (induction xs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs)
have "prefixes (xs @ [x]) = (prefixes xs)@[xs @ [x]]"
by simp
show ?case proof (cases "P (xs@[x])")
case True
then have "maximum_prefix_with_property P (xs @ [x]) = (xs @ [x])"
unfolding maximum_prefix_with_property.simps ‹prefixes (xs @ [x]) = (prefixes xs)@[xs @ [x]]›
by auto
show ?thesis
using True
unfolding ‹maximum_prefix_with_property P (xs @ [x]) = (xs@[x])›
using in_set_prefixes prefix_length_le by blast
next
case False
then have "maximum_prefix_with_property P (xs@[x]) = maximum_prefix_with_property P xs"
unfolding maximum_prefix_with_property.simps ‹prefixes (xs @ [x]) = (prefixes xs)@[xs @ [x]]›
by auto
have "∃a∈set (prefixes xs). P a"
using snoc.prems False unfolding ‹prefixes (xs @ [x]) = (prefixes xs)@[xs @ [x]]› by auto
show ?thesis
using snoc.IH[OF ‹∃a∈set (prefixes xs). P a›] False
unfolding ‹maximum_prefix_with_property P (xs@[x]) = maximum_prefix_with_property P xs›
unfolding ‹prefixes (xs @ [x]) = (prefixes xs)@[xs @ [x]]› by auto
qed
qed
then show "P (maximum_prefix_with_property P xs)"
and "(maximum_prefix_with_property P xs) ∈ set (prefixes xs)"
and "⋀ ys . prefix ys xs ⟹ P ys ⟹ length ys ≤ length (maximum_prefix_with_property P xs)"
by blast+
qed
lemma bottom_completion_out :
assumes "is_language X Y L"
and "x ∈ X"
and "π ∈ bottom_completion X Y L"
shows "is_not_undefined π L ⟹ out[L,map (λ(x,y) . (x, the y)) π,x] ≠ {} ⟹ out[bottom_completion X Y L, π, x] = Some ` out[L, map (λ(x,y) . (x, the y)) π, x]"
and "is_not_undefined π L ⟹ out[L,map (λ(x,y) . (x, the y)) π,x] = {} ⟹ out[bottom_completion X Y L, π, x] = {None} ∪ Some ` Y"
and "¬ is_not_undefined π L ⟹ out[bottom_completion X Y L, π, x] = {None} ∪ Some ` Y"
proof -
let ?L = "bottom_completion X Y L"
define L'a where "L'a = ((λ π . map (λ(x,y) . (x,Some y)) π) ` L)"
define L'b where "L'b = {(map (λ(x,y) . (x,Some y)) π)@[(x,y)]@τ | π x y τ . π ∈ L ∧ out[L,π,x] = {} ∧ x ∈ X ∧ (y = None ∨ y ∈ Some ` Y) ∧ (∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))}"
have "?L = L'a ∪ L'b"
unfolding L'a_def L'b_def bottom_completion.simps by blast
then have "out[?L, π, x] = {y. π @ [(x, y)] ∈ L'a} ∪ {y. π @ [(x, y)] ∈ L'b}"
unfolding outputs.simps language_for_state.simps by blast
have "is_language X ({None} ∪ Some ` Y) ?L"
using bottom_completion_is_language[OF assms(1)] .
show "is_not_undefined π L ⟹ out[L,map (λ(x,y) . (x, the y)) π,x] ≠ {} ⟹ out[bottom_completion X Y L, π, x] = Some ` out[L, map (λ(x,y) . (x, the y)) π, x]"
and "is_not_undefined π L ⟹ out[L,map (λ(x,y) . (x, the y)) π,x] = {} ⟹ out[bottom_completion X Y L, π, x] = {None} ∪ Some ` Y"
proof -
assume "is_not_undefined π L"
then obtain π' where "π = map (λ(x, y). (x, Some y)) π'" and "π' ∈ L"
by auto
then have "map (λ(x, y). (x, the y)) π = π'"
using bottom_id by auto
have "{y. π @ [(x, y)] ∈ L'a} = Some ` out[L,map (λ(x,y) . (x, the y)) π,x]"
proof
show "{y. π @ [(x, y)] ∈ L'a} ⊆ Some ` out[L,map (λ(x, y). (x, the y)) π,x]"
proof
fix y assume "y ∈ {y. π @ [(x, y)] ∈ L'a}"
then have "π @ [(x, y)] ∈ L'a" by auto
then obtain π' where "π @ [(x, y)] = map (λ(x,y) . (x,Some y)) π'" and "π' ∈ L"
unfolding L'a_def by blast
then have "length (π @ [(x, y)]) = length π'"
by auto
then obtain γ' xy where "π' = γ'@[xy]"
by (metis add.right_neutral dual_order.strict_iff_not length_append_singleton less_add_Suc2 rev_exhaust take0 take_all_iff)
then have "(x,y) = (λ(x, y). (x, Some y)) xy"
using ‹π @ [(x, y)] = map (λ(x, y). (x, Some y)) π'› unfolding ‹π' = γ'@[xy]› by auto
then have "y = Some (snd xy)" and "xy = (x,snd xy)"
by (simp add: split_beta)+
moreover define y' where "y' = snd xy"
ultimately have "y = Some y'" and "xy = (x,y')"
by auto
have "map (λ(x, y). (x, the y)) π = γ'"
using ‹π @ [(x, y)] = map (λ(x,y) . (x,Some y)) π'› unfolding ‹π' = γ'@[xy]›
using bottom_id by auto
have "y' ∈ out[L,map (λ(x, y). (x, the y)) π,x]"
using ‹π' ∈ L›
unfolding ‹map (λ(x, y). (x, the y)) π = γ'› ‹π' = γ'@[xy]› ‹xy = (x,y')› by auto
then show "y ∈ Some ` out[L,map (λ(x, y). (x, the y)) π,x]"
unfolding ‹y = Some y'› by blast
qed
show "Some ` out[L,map (λ(x, y). (x, the y)) π,x] ⊆ {y. π @ [(x, y)] ∈ L'a}"
proof
fix y assume "y ∈ Some ` out[L,map (λ(x, y). (x, the y)) π,x]"
then obtain y' where "y = Some y'" and "y' ∈ out[L,map (λ(x, y). (x, the y)) π,x]"
by blast
then have "π'@[(x,y')] ∈ L"
unfolding ‹map (λ(x, y). (x, the y)) π = π'› by auto
then show "y ∈ {y. π @ [(x, y)] ∈ L'a}"
unfolding L'a_def ‹π = map (λ(x, y). (x, Some y)) π'›
using ‹y = Some y'› image_iff by fastforce
qed
qed
show "out[L,map (λ(x,y) . (x, the y)) π,x] ≠ {} ⟹ out[bottom_completion X Y L, π, x] = Some ` out[L, map (λ(x,y) . (x, the y)) π, x]"
proof -
assume "out[L,map (λ(x,y) . (x, the y)) π,x] ≠ {}"
then obtain ya where "π'@[(x,ya)] ∈ L"
using ‹π' ∈ L› unfolding ‹map (λ(x,y) . (x, the y)) π = π'› by auto
have "{y. π @ [(x, y)] ∈ L'b} = {}"
proof (rule ccontr)
assume "{y. π @ [(x, y)] ∈ L'b} ≠ {}"
then obtain y where "π @ [(x, y)] ∈ L'b" by blast
then obtain π'' x' y' τ where "π @ [(x, y)] = (map (λ(x,y) . (x,Some y)) π'')@[(x',y')]@τ"
and "π'' ∈ L"
and "out[L,π'',x'] = {}"
and "x' ∈ X"
and "(y' = None ∨ y' ∈ Some ` Y)"
and "(∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))"
unfolding L'b_def
by blast
have "⋀ y'' . π''@[(x',y'')] ∉ L"
using ‹π'' ∈ L› ‹out[L,π'',x'] = {}›
unfolding outputs.simps language_for_state.simps by force
have "length π' = length π''"
proof -
have "length π' = length π"
using ‹map (λ(x, y). (x, the y)) π = π'› length_map by blast
have "¬ length π' < length π''"
proof
assume "length π' < length π''"
then have "length π'' = Suc (length π')"
by (metis (no_types, lifting) One_nat_def ‹π @ [(x, y)] = map (λ(x, y). (x, Some y)) π'' @ [(x', y')] @ τ› ‹length π' = length π› add_diff_cancel_left' length_append length_append_singleton length_map list.size(3) not_less_eq plus_1_eq_Suc zero_less_Suc zero_less_diff)
then have "length π'' > length π"
by (simp add: ‹π = map (λ(x, y). (x, Some y)) π'›)
then show False
by (metis (no_types, lifting) One_nat_def ‹π @ [(x, y)] = map (λ(x, y). (x, Some y)) π'' @ [(x', y')] @ τ› length_Cons length_append length_append_singleton length_map less_add_same_cancel1 list.size(3) not_less_eq plus_1_eq_Suc zero_less_Suc)
qed
moreover have "¬ length π'' < length π'"
proof
assume "length π'' < length π'"
then have "prefix ((map (λ(x,y) . (x,Some y)) π'')@[(x',y')]) (map (λ(x,y) . (x,Some y)) π')"
by (metis (no_types, lifting) ‹π = map (λ(x, y). (x, Some y)) π'› ‹π @ [(x, y)] = map (λ(x, y). (x, Some y)) π'' @ [(x', y')] @ τ› append.assoc length_append_singleton length_map linorder_not_le not_less_eq prefixI prefix_length_prefix)
then have "prefix π'' π'"
by (metis append_prefixD bottom_id map_mono_prefix)
then have "take (length π'') π' = π''"
by (metis append_eq_conv_conj prefix_def)
have "(x',y') = (((map (λ(x,y) . (x,Some y)) π'')@[(x',y')])) ! (length π'')"
by (induction π'' arbitrary: x' y'; auto)
then have "(x',y') = (map (λ(x,y) . (x,Some y)) π') ! (length π'')"
by (metis (no_types, lifting) ‹π = map (λ(x, y). (x, Some y)) π'› ‹π @ [(x, y)] = map (λ(x, y). (x, Some y)) π'' @ [(x', y')] @ τ› ‹length π'' < length π'› append_Cons length_map nth_append nth_append_length)
then have "fst (π' ! (length π'')) = x'"
by (simp add: ‹length π'' < length π'› split_beta)
have "out[L, take (length π'') π', fst (π' ! (length π''))] = {}"
unfolding ‹take (length π'') π' = π''› ‹fst (π' ! (length π'')) = x'›
using ‹out[L,π'',x'] = {}› .
moreover have "⋀ i . i < length π' ⟹ out[L, take i π', fst (π' ! i)] ≠ {}"
using prefix_executable[OF assms(1) ‹π' ∈ L›]
by (meson outputs_executable)
ultimately show False
using ‹length π'' < length π'› by blast
qed
ultimately show ?thesis
by simp
qed
then have "π'' = π'"
by (metis ‹π @ [(x, y)] = map (λ(x, y). (x, Some y)) π'' @ [(x', y')] @ τ› ‹map (λ(x, y). (x, the y)) π = π'› append_eq_append_conv bottom_id length_map)
show False
using ‹π @ [(x, y)] = map (λ(x, y). (x, Some y)) π'' @ [(x', y')] @ τ› ‹π'' = π'› ‹map (λ(x, y). (x, the y)) π = π'› ‹out[L,π'',x'] = {}› ‹out[L,map (λ(x, y). (x, the y)) π,x] ≠ {}›
by force
qed
then show ?thesis
using ‹out[bottom_completion X Y L,π,x] = {y. π @ [(x, y)] ∈ L'a} ∪ {y. π @ [(x, y)] ∈ L'b}›
using ‹{y. π @ [(x, y)] ∈ L'a} = Some ` out[L,map (λ(x,y) . (x, the y)) π,x]›
by force
qed
show "out[L,map (λ(x,y) . (x, the y)) π,x] = {} ⟹ out[bottom_completion X Y L, π, x] = {None} ∪ Some ` Y"
proof -
assume "out[L,map (λ(x,y) . (x, the y)) π,x] = {}"
then have "{y. π @ [(x, y)] ∈ L'a} = {}"
unfolding ‹{y. π @ [(x, y)] ∈ L'a} = Some ` out[L,map (λ(x,y) . (x, the y)) π,x]› by blast
moreover have "{y. π @ [(x, y)] ∈ L'b} = {None} ∪ Some ` Y"
proof
show "{y. π @ [(x, y)] ∈ L'b} ⊆ {None} ∪ Some ` Y"
proof
fix y assume "y ∈ {y. π @ [(x, y)] ∈ L'b}"
then have "π @ [(x, y)] ∈ L'b" by blast
then obtain π'' x' y' τ where "π @ [(x, y)] = (map (λ(x,y) . (x,Some y)) π'')@[(x',y')]@τ"
and "π'' ∈ L"
and "out[L,π'',x'] = {}"
and "x' ∈ X"
and "(y' = None ∨ y' ∈ Some ` Y)"
and "(∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))"
unfolding L'b_def
by blast
show "y ∈ {None} ∪ Some ` Y"
by (metis (no_types, lifting) Un_insert_right ‹out[bottom_completion X Y L,π,x] = {y. π @ [(x, y)] ∈ L'a} ∪ {y. π @ [(x, y)] ∈ L'b}› ‹y ∈ {y. π @ [(x, y)] ∈ L'b}› assms(1) bottom_completion_is_language insert_subset mk_disjoint_insert outputs_in_alphabet)
qed
show "{None} ∪ Some ` Y ⊆ {y. π @ [(x, y)] ∈ L'b}"
proof
fix y assume "y ∈ {None} ∪ Some ` Y"
have "π @ [(x, y)] = map (λ(x, y). (x, Some y)) π' @ [(x, y)] @ []"
by (simp add: ‹π = map (λ(x, y). (x, Some y)) π'›)
moreover note ‹π' ∈ L›
moreover have "out[L,π',x] = {}"
using ‹out[L,map (λ(x,y) . (x, the y)) π,x] = {}› unfolding ‹map (λ(x,y) . (x, the y)) π = π'› .
moreover note ‹x ∈ X›
moreover have "(y = None ∨ y ∈ Some ` Y)"
using ‹y ∈ {None} ∪ Some ` Y› by blast
moreover have "(∀(x, y)∈set []. x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))"
by simp
ultimately show "y ∈ {y. π @ [(x, y)] ∈ L'b}"
unfolding L'b_def by blast
qed
qed
ultimately show ?thesis
using ‹out[bottom_completion X Y L,π,x] = {y. π @ [(x, y)] ∈ L'a} ∪ {y. π @ [(x, y)] ∈ L'b}›
using ‹{y. π @ [(x, y)] ∈ L'a} = Some ` out[L,map (λ(x,y) . (x, the y)) π,x]›
by force
qed
qed
show "¬ is_not_undefined π L ⟹ out[bottom_completion X Y L,π,x] = {None} ∪ Some ` Y"
proof -
assume "¬ is_not_undefined π L"
then have "π ∉ L'a"
unfolding L'a_def by auto
have "{y. π @ [(x, y)] ∈ L'a} = {}"
proof (rule ccontr)
assume "{y. π @ [(x, y)] ∈ L'a} ≠ {}"
then obtain y where "π @ [(x, y)] ∈ L'a" by blast
then obtain γ where "π @ [(x, y)] = map (λ(x, y). (x, Some y)) γ" and "γ ∈ L"
unfolding L'a_def by blast
then have "π = map (λ(x, y). (x, Some y)) (butlast γ)"
by (metis (mono_tags, lifting) butlast_snoc map_butlast)
moreover have "butlast γ ∈ L"
using ‹γ ∈ L› assms(1)
by (simp add: prefixeq_butlast)
ultimately show False
using ‹π ∉ L'a›
using L'a_def by blast
qed
then have "out[?L, π, x] = {y. π @ [(x, y)] ∈ L'b}"
using ‹out[bottom_completion X Y L,π,x] = {y. π @ [(x, y)] ∈ L'a} ∪ {y. π @ [(x, y)] ∈ L'b}› by blast
also have "… = {None} ∪ Some ` Y"
proof
show "{y. π @ [(x, y)] ∈ L'b} ⊆ {None} ∪ Some ` Y"
proof
fix y assume "y ∈ {y. π @ [(x, y)] ∈ L'b}"
then obtain π' x' y' τ where "π @ [(x, y)] = (map (λ(x,y) . (x,Some y)) π')@[(x',y')]@τ"
and "π' ∈ L"
and "out[L,π',x'] = {}"
and "x' ∈ X"
and "(y' = None ∨ y' ∈ Some ` Y)"
and "(∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))"
unfolding L'b_def
by blast
have "(x,y) ∈ set ([(x',y')]@τ)"
by (metis ‹π @ [(x, y)] = map (λ(x, y). (x, Some y)) π' @ [(x', y')] @ τ› append_is_Nil_conv last_appendR last_in_set last_snoc length_Cons list.size(3) nat.simps(3))
then show "y ∈ {None} ∪ Some ` Y"
using ‹(y' = None ∨ y' ∈ Some ` Y)› ‹(∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))› by auto
qed
show "{None} ∪ Some ` Y ⊆ {y. π @ [(x, y)] ∈ L'b}"
proof
fix y assume "y ∈ {None} ∪ Some ` Y"
have "π ∈ L'b"
using ‹π ∉ L'a› ‹?L = L'a ∪ L'b› assms(3) by fastforce
then obtain π' x' y' τ where "π = (map (λ(x,y) . (x,Some y)) π')@[(x',y')]@τ"
and "π' ∈ L"
and "out[L,π',x'] = {}"
and "x' ∈ X"
and "(y' = None ∨ y' ∈ Some ` Y)"
and "(∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))"
unfolding L'b_def
by blast
have "π @ [(x,y)] = (map (λ(x,y) . (x,Some y)) π')@[(x',y')]@(τ@[(x,y)])"
unfolding ‹π = (map (λ(x,y) . (x,Some y)) π')@[(x',y')]@τ› by auto
moreover note ‹π' ∈ L› and ‹out[L,π',x'] = {}› and ‹x' ∈ X› and ‹(y' = None ∨ y' ∈ Some ` Y)›
moreover have "(∀ (x,y) ∈ set (τ@[(x,y)]) . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))"
using ‹∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y)› ‹y ∈ {None} ∪ Some ` Y› ‹x ∈ X›
by auto
ultimately show "y ∈ {y. π @ [(x, y)] ∈ L'b}"
unfolding L'b_def by blast
qed
qed
finally show "out[?L,π,x] = {None} ∪ Some ` Y" .
qed
qed
theorem quasired_via_red :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "(L1 ≼[X,quasired Y] L2) ⟷ ((bottom_completion X Y L1) ≼[X, red ({None} ∪ Some ` Y)] (bottom_completion X Y L2))"
proof -
define L1' where "L1' = bottom_completion X Y L1"
define L2' where "L2' = bottom_completion X Y L2"
define L1'a where "L1'a = ((λ π . map (λ(x,y) . (x,Some y)) π) ` L1)"
define L1'b where "L1'b = {(map (λ(x,y) . (x,Some y)) π)@[(x,y)]@τ | π x y τ . π ∈ L1 ∧ out[L1,π,x] = {} ∧ x ∈ X ∧ (y = None ∨ y ∈ Some ` Y) ∧ (∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))}"
define L2'a where "L2'a = ((λ π . map (λ(x,y) . (x,Some y)) π) ` L2)"
define L2'b where "L2'b = {(map (λ(x,y) . (x,Some y)) π)@[(x,y)]@τ | π x y τ . π ∈ L2 ∧ out[L2,π,x] = {} ∧ x ∈ X ∧ (y = None ∨ y ∈ Some ` Y) ∧ (∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))}"
let ?L1 = "bottom_completion X Y L1"
have "?L1 = L1'a ∪ L1'b"
unfolding L1'a_def L1'b_def bottom_completion.simps by blast
then have "⋀ π x . out[?L1, π, x] = {y. π @ [(x, y)] ∈ L1'a} ∪ {y. π @ [(x, y)] ∈ L1'b}"
unfolding outputs.simps language_for_state.simps by blast
let ?L2 = "bottom_completion X Y L2"
have "?L2 = L2'a ∪ L2'b"
unfolding L2'a_def L2'b_def bottom_completion.simps by blast
then have "⋀ π x . out[?L2, π, x] = {y. π @ [(x, y)] ∈ L2'a} ∪ {y. π @ [(x, y)] ∈ L2'b}"
unfolding outputs.simps language_for_state.simps by blast
have "is_language X ({None} ∪ Some ` Y) ?L1"
using bottom_completion_is_language[OF assms(1)] .
have "is_language X ({None} ∪ Some ` Y) ?L2"
using bottom_completion_is_language[OF assms(2)] .
then have "⋀ π x . out[bottom_completion X Y L2,π,x] ⊆ {None} ∪ Some ` Y"
by (meson outputs_in_alphabet)
have "(?L1 ≼[X, red ({None} ∪ Some ` Y)] ?L2) = (∀ π ∈ ?L1 ∩ ?L2 . ∀ x ∈ X . out[?L1,π,x] ⊆ out[?L2,π,x])"
unfolding type_1_conforms.simps red.simps
using ‹⋀ π x . out[bottom_completion X Y L2,π,x] ⊆ {None} ∪ Some ` Y› by force
also have "… = (∀ π ∈ ?L1 ∩ ?L2 . ∀ x ∈ X . (out[?L2,π,x] = {None} ∪ Some ` Y ∨ (out[?L1,π,x] ≠ {} ∧ out[?L1,π,x] ⊆ out[?L2,π,x])))"
by (metis (no_types, lifting) IntD1 ‹is_language X ({None} ∪ Some ` Y) (bottom_completion X Y L1)› ‹is_language X ({None} ∪ Some ` Y) (bottom_completion X Y L2)› assms(1) bottom_completion_out(1) bottom_completion_out(2) bottom_completion_out(3) image_is_empty outputs_in_alphabet subset_antisym)
also have "… = (∀ π ∈ ?L1 ∩ ?L2 . ∀ x ∈ X . (out[?L2,π,x] = {None} ∪ Some ` Y ∨ (is_not_undefined π L1 ∧ is_not_undefined π L2 ∧ out[L1,map (λ(x,y) . (x, the y)) π,x] ≠ {} ∧ out[L1,map (λ(x,y) . (x, the y)) π,x] ⊆ out[L2,map (λ(x,y) . (x, the y)) π,x])))"
proof -
have "⋀ π x . π ∈ ?L1 ∩ ?L2 ⟹ x ∈ X ⟹ out[?L2,π,x] ≠ {None} ∪ Some ` Y ⟹
(out[?L1,π,x] ≠ {} ∧ out[?L1,π,x] ⊆ out[?L2,π,x]) = (is_not_undefined π L1 ∧ is_not_undefined π L2 ∧ out[L1,map (λ(x,y) . (x, the y)) π,x] ≠ {} ∧ out[L1,map (λ(x,y) . (x, the y)) π,x] ⊆ out[L2,map (λ(x,y) . (x, the y)) π,x])"
proof -
fix π x assume "π ∈ ?L1 ∩ ?L2" and "x ∈ X" and "out[?L2,π,x] ≠ {None} ∪ Some ` Y"
then have "π ∈ ?L1" and "π ∈ ?L2" by blast+
have "is_not_undefined π L2"
using bottom_completion_out[OF assms(2) ‹x ∈ X› ‹π ∈ ?L2›]
using ‹out[bottom_completion X Y L2,π,x] ≠ {None} ∪ Some ` Y› by fastforce
have "out[L2,map (λ(x, y). (x, the y)) π,x] ≠ {}"
using bottom_completion_out(1,2)[OF assms(2) ‹x ∈ X› ‹π ∈ ?L2›]
using ‹is_not_undefined π L2› ‹out[bottom_completion X Y L2,π,x] ≠ {None} ∪ Some ` Y› by blast
show "(out[?L1,π,x] ≠ {} ∧ out[?L1,π,x] ⊆ out[?L2,π,x]) = (is_not_undefined π L1 ∧ is_not_undefined π L2 ∧ out[L1,map (λ(x,y) . (x, the y)) π,x] ≠ {} ∧ out[L1,map (λ(x,y) . (x, the y)) π,x] ⊆ out[L2,map (λ(x,y) . (x, the y)) π,x])"
proof (cases "is_not_undefined π L1")
case False
then have "out[?L1,π,x] = {None} ∪ Some ` Y"
by (meson IntD1 ‹π ∈ bottom_completion X Y L1 ∩ bottom_completion X Y L2› ‹x ∈ X› assms(1) bottom_completion_out(3))
then have "¬ (out[?L1,π,x] ⊆ out[?L2,π,x])"
by (metis ‹is_language X ({None} ∪ Some ` Y) (bottom_completion X Y L2)› ‹out[bottom_completion X Y L2,π,x] ≠ {None} ∪ Some ` Y› outputs_in_alphabet subset_antisym)
then show ?thesis
using False by presburger
next
case True
have "(out[?L1,π,x] ≠ {} ∧ out[?L1,π,x] ⊆ out[?L2,π,x]) = (out[L1,map (λ(x,y) . (x, the y)) π,x] ≠ {} ∧ out[L1,map (λ(x,y) . (x, the y)) π,x] ⊆ out[L2,map (λ(x,y) . (x, the y)) π,x])"
proof (cases "out[L1,map (λ(x, y). (x, the y)) π,x] = {}")
case True
have "¬ (out[?L1,π,x] ≠ {} ∧ out[?L1,π,x] ⊆ out[?L2,π,x])"
unfolding bottom_completion_out(2)[OF assms(1) ‹x ∈ X› ‹π ∈ ?L1› ‹is_not_undefined π L1› True]
by (meson ‹⋀x π. out[bottom_completion X Y L2,π,x] ⊆ {None} ∪ Some ` Y› ‹out[bottom_completion X Y L2,π,x] ≠ {None} ∪ Some ` Y› subset_antisym)
moreover have "¬ (out[L1,map (λ(x,y) . (x, the y)) π,x] ≠ {} ∧ out[L1,map (λ(x,y) . (x, the y)) π,x] ⊆ out[L2,map (λ(x,y) . (x, the y)) π,x])"
using True by simp
ultimately show ?thesis by blast
next
case False
show ?thesis
unfolding bottom_completion_out(1)[OF assms(1) ‹x ∈ X› ‹π ∈ ?L1› ‹is_not_undefined π L1› False]
unfolding bottom_completion_out(1)[OF assms(2) ‹x ∈ X› ‹π ∈ ?L2› ‹is_not_undefined π L2› ‹out[L2,map (λ(x, y). (x, the y)) π,x] ≠ {}›]
by blast
qed
then show ?thesis
using ‹is_not_undefined π L1› ‹is_not_undefined π L2›
by blast
qed
qed
then show ?thesis
by meson
qed
also have "… = ( (∀ π ∈ ?L1 ∩ ?L2 . ∀ x ∈ X . ¬ is_not_undefined π L1 ⟶ is_not_undefined π L2 ⟶ out[?L2,π,x] = {None} ∪ Some ` Y)
∧ (∀ π ∈ L1 ∩ L2 . ∀ x ∈ X . out[L2,π,x] = {} ∨ (out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x])))"
(is "?A = ?B")
proof
show "?A ⟹ ?B"
proof -
assume ?A
have "⋀ π x . π ∈ ?L1 ∩ ?L2 ⟹ x ∈ X ⟹ ¬ is_not_undefined π L1 ⟹ is_not_undefined π L2 ⟹ out[?L2,π,x] = {None} ∪ Some ` Y"
using ‹?A› by blast
moreover have "⋀ π x . π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ out[L2,π,x] = {} ∨ (out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x])"
proof -
fix π x assume "π ∈ L1 ∩ L2" and "x ∈ X"
let ?π = "map (λ(x, y). (x, Some y)) π"
have "is_not_undefined ?π L1" and "is_not_undefined ?π L2"
using ‹π ∈ L1 ∩ L2› by auto
then have "?π ∈ ?L1" and "?π ∈ ?L2"
by auto
show "out[L2,π,x] = {} ∨ (out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x])"
proof (cases "out[L2,π,x] = {}")
case True
then show ?thesis by auto
next
case False
then have "out[bottom_completion X Y L2,?π,x] ≠ {None} ∪ Some ` Y"
using bottom_completion_out(1)[OF assms(2) ‹x ∈ X› ‹?π ∈ ?L2› ‹is_not_undefined ?π L2›]
unfolding bottom_id
by force
then have "out[L1,map (λ(x, y). (x, the y)) ?π,x] ≠ {} ∧ out[L1,map (λ(x, y). (x, the y)) ?π,x] ⊆ out[L2,map (λ(x, y). (x, the y)) ?π,x]"
using ‹?A›
using ‹?π ∈ ?L1› ‹?π ∈ ?L2› ‹x ∈ X›
by blast
then show "out[L2,π,x] = {} ∨ (out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x])"
unfolding bottom_id by blast
qed
qed
ultimately show ?B
by meson
qed
show "?B ⟹ ?A"
proof -
assume "?B"
have "⋀ π x . π ∈ ?L1 ∩ ?L2 ⟹ x ∈ X ⟹ out[?L2,π,x] = {None} ∪ Some ` Y ∨ is_not_undefined π L1 ∧ is_not_undefined π L2 ∧ out[L1,map (λ(x, y). (x, the y)) π,x] ≠ {} ∧ out[L1,map (λ(x, y). (x, the y)) π,x] ⊆ out[L2,map (λ(x, y). (x, the y)) π,x]"
proof -
fix π x assume "π ∈ ?L1 ∩ ?L2" and "x ∈ X"
then have "π ∈ ?L1" and "π ∈ ?L2" by auto
show "out[?L2,π,x] = {None} ∪ Some ` Y ∨ is_not_undefined π L1 ∧ is_not_undefined π L2 ∧ out[L1,map (λ(x, y). (x, the y)) π,x] ≠ {} ∧ out[L1,map (λ(x, y). (x, the y)) π,x] ⊆ out[L2,map (λ(x, y). (x, the y)) π,x]"
proof (cases "out[?L2,π,x] = {None} ∪ Some ` Y")
case True
then show ?thesis by blast
next
case False
let ?π = "map (λ(x, y). (x, the y)) π"
have "is_not_undefined π L2"
using False ‹(∀π ∈bottom_completion X Y L1 ∩ bottom_completion X Y L2. ∀x∈X. ¬ is_not_undefined π L1 ⟶ is_not_undefined π L2 ⟶ out[bottom_completion X Y L2,π,x] = {None} ∪ Some ` Y) ∧ (∀π∈L1 ∩ L2. ∀x∈X. out[L2,π,x] = {} ∨ out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x])› ‹π ∈ bottom_completion X Y L1 ∩ bottom_completion X Y L2› ‹x ∈ X›
by (meson ‹π ∈ bottom_completion X Y L2› assms(2) bottom_completion_out(3))
then have "?π ∈ L2"
using bottom_id
by (metis (mono_tags, lifting) imageE is_not_undefined.elims(2))
have "is_not_undefined π L1"
using False ‹(∀π ∈bottom_completion X Y L1 ∩ bottom_completion X Y L2. ∀x∈X. ¬ is_not_undefined π L1 ⟶ is_not_undefined π L2 ⟶ out[bottom_completion X Y L2,π,x] = {None} ∪ Some ` Y) ∧ (∀π∈L1 ∩ L2. ∀x∈X. out[L2,π,x] = {} ∨ out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x])› ‹π ∈ bottom_completion X Y L1 ∩ bottom_completion X Y L2› ‹x ∈ X›
using ‹is_not_undefined π L2› by blast
then have "?π ∈ L1"
using bottom_id
by (metis (mono_tags, lifting) imageE is_not_undefined.elims(2))
have "out[L2,?π,x] ≠ {}"
using False bottom_completion_out(2)[OF assms(2) ‹x ∈ X› ‹π ∈ ?L2› ‹is_not_undefined π L2›]
by blast
then have "out[L1,?π,x] ≠ {}" and "out[L1,?π,x] ⊆ out[L2,?π,x]"
using ‹?B› ‹?π ∈ L1› ‹?π ∈ L2› ‹x ∈ X›
by (meson IntI)+
then show ?thesis
using ‹is_not_undefined π L1› ‹is_not_undefined π L2›
by blast
qed
qed
then show ?A
by blast
qed
qed
also have "… = ( (∀ π ∈ ?L1 ∩ ?L2 . ∀ x ∈ X . ¬ is_not_undefined π L1 ⟶ is_not_undefined π L2 ⟶ out[L2,map (λ(x, y). (x, the y)) π,x] = {})
∧ (∀ π ∈ L1 ∩ L2 . ∀ x ∈ X . out[L2,π,x] = {} ∨ (out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x])))"
(is "(?A ∧ ?B) = (?C ∧ ?B)")
proof -
have "?A = ?C"
by (metis IntD2 None_notin_image_Some UnCI assms(2) bottom_completion_out(1) bottom_completion_out(2) insertCI)
then show ?thesis by meson
qed
also have "… = (∀ π ∈ L1 ∩ L2 . ∀ x ∈ X . out[L2,π,x] = {} ∨ (out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x]))"
(is "(?A ∧ ?B) = ?B")
proof -
have "?B ⟹ ?A"
proof -
assume "?B"
have "⋀ π x . π ∈ ?L1 ∩ ?L2 ⟹ x ∈ X ⟹ ¬ is_not_undefined π L1 ⟹ is_not_undefined π L2 ⟹ out[L2,map (λ(x, y). (x, the y)) π,x] = {}"
proof (rule ccontr)
fix π x assume "π ∈ ?L1 ∩ ?L2" and "x ∈ X" and "¬ is_not_undefined π L1" and "is_not_undefined π L2"
and "out[L2,map (λ(x, y). (x, the y)) π,x] ≠ {}"
let ?π = "map (λ(x, y). (x, the y)) π"
have "?π ∈ L2"
by (metis (mono_tags, lifting) ‹is_not_undefined π L2› bottom_id image_iff is_not_undefined.elims(2))
have "π ∈ ?L1"
using ‹π ∈ ?L1 ∩ ?L2› by auto
moreover have "π ∉ L1'a"
unfolding L1'a_def using ‹¬ is_not_undefined π L1› by auto
ultimately have "π ∈ L1'b"
unfolding ‹?L1 = L1'a ∪ L1'b› by blast
then obtain π' x' y' τ where "π = (map (λ(x,y) . (x,Some y)) π')@[(x',y')]@τ"
and "π' ∈ L1"
and "out[L1,π',x'] = {}"
and "x' ∈ X"
and "(y' = None ∨ y' ∈ Some ` Y)"
and "(∀ (x,y) ∈ set τ . x ∈ X ∧ (y = None ∨ y ∈ Some ` Y))"
unfolding L1'b_def
by blast
have "?π = (π'@[(x', the y')]) @ (map (λ(x, y). (x, the y)) τ)"
unfolding ‹π = (map (λ(x,y) . (x,Some y)) π')@[(x',y')]@τ›
using bottom_id by (induction π' arbitrary: x' y' τ; auto)
then have "π'@[(x', the y')] ∈ L2" and "π' ∈ L2"
using ‹?π ∈ L2›
by (metis assms(2) prefix_closure_no_member)+
then have "out[L2,π',x'] ≠ {}"
by fastforce
show False
using ‹?B› ‹π' ∈ L1› ‹π' ∈ L2› ‹x' ∈ X› ‹out[L2,π',x'] ≠ {}› ‹out[L1,π',x'] = {}›
by blast
qed
then show ?A
by blast
qed
then show ?thesis by meson
qed
also have "… = (L1 ≼[X,quasired Y] L2)"
unfolding quasired_type_1[OF assms, symmetric] quasi_reduction_def
by (meson assms(2) executable_inputs_in_alphabet outputs_executable)
finally show ?thesis
by meson
qed
subsection ‹Strong Reduction via Reduction and Undefinedness Outputs›
fun non_bottom_shortening :: "('x,'y option) word ⇒ ('x,'y option) word" where
"non_bottom_shortening π = filter (λ (x,y) . y ≠ None) π"
fun non_bottom_projection :: "('x,'y option) word ⇒ ('x,'y) word" where
"non_bottom_projection π = map (λ(x,y) . (x,the y)) (non_bottom_shortening π)"
lemma non_bottom_projection_split: "non_bottom_projection (π'@π'') = (non_bottom_projection π')@(non_bottom_projection π'')"
by (induction π' arbitrary: π''; auto)
lemma non_bottom_projection_id : "non_bottom_projection (map (λ(x,y) . (x,Some y)) π) = π"
by (induction π; auto)
fun undefinedness_completion :: "'x alphabet ⇒ ('x,'y) language ⇒ ('x, 'y option) language" where
"undefinedness_completion X L =
{π . non_bottom_projection π ∈ L ∧ (∀ π' x π'' . π = π' @ [(x,None)] @ π'' ⟶ x ∈ X ∧ out[L, non_bottom_projection π', x] = {})}"
lemma undefinedness_completion_is_language :
assumes "is_language X Y L"
shows "is_language X ({None} ∪ Some ` Y) (undefinedness_completion X L)"
proof -
let ?L = "undefinedness_completion X L"
have "[] ∈ L"
using language_contains_nil[OF assms] .
moreover have "non_bottom_projection [] = []"
by auto
ultimately have "[] ∈ ?L"
by simp
then have "?L ≠ {}"
by blast
moreover have "⋀ π . π ∈ ?L ⟹ (⋀ xy . xy ∈ set π ⟹ fst xy ∈ X ∧ snd xy ∈ ({None} ∪ Some ` Y))"
and "⋀ π . π ∈ ?L ⟹ (⋀ π' . prefix π' π ⟹ π' ∈ ?L)"
proof -
fix π assume "π ∈ ?L"
then have p1: "non_bottom_projection π ∈ L"
and p2: "⋀ π' x π'' . π = π' @ [(x,None)] @ π'' ⟹ x ∈ X ∧ out[L, non_bottom_projection π', x] = {}"
by auto
show "⋀ xy . xy ∈ set π ⟹ fst xy ∈ X ∧ snd xy ∈ ({None} ∪ Some ` Y)"
proof -
fix xy assume "xy ∈ set π"
then obtain π' x y π'' where "xy = (x,y)" and "π = π' @ [(x,y)] @ π''"
by (metis append_Cons append_Nil old.prod.exhaust split_list)
show "fst xy ∈ X ∧ snd xy ∈ ({None} ∪ Some ` Y)"
proof (cases "snd xy")
case None
then show ?thesis
unfolding ‹xy = (x,y)› snd_conv
using p2 ‹π = π' @ [(x,y)] @ π''›
by simp
next
case (Some y')
then have "y = Some y'"
unfolding ‹xy = (x,y)› by auto
have "(x,y') ∈ set (non_bottom_projection π)"
unfolding ‹π = π' @ [(x,y)] @ π''› ‹y = Some y'›
by auto
then show ?thesis
unfolding ‹xy = (x,y)› snd_conv ‹y = Some y'› fst_conv
using p1 assms
unfolding is_language.simps by fastforce
qed
qed
show "⋀ π' . prefix π' π ⟹ π' ∈ ?L"
proof -
fix π' assume "prefix π' π"
then obtain π'' where "π = π'@π''"
using prefixE by blast
have "non_bottom_projection π = (non_bottom_projection π')@(non_bottom_projection π'')"
unfolding ‹π = π'@π''›
using non_bottom_projection_split .
then have "non_bottom_projection π' ∈ L"
by (metis assms p1 prefix_closure_no_member)
moreover have "⋀ π''' x π'''' . π' = π''' @ [(x,None)] @ π'''' ⟹ x ∈ X ∧ out[L, non_bottom_projection π''', x] = {}"
using p2 unfolding ‹π = π'@π''›
by (metis append.assoc)
ultimately show "π' ∈ ?L"
by fastforce
qed
qed
ultimately show ?thesis
by (meson is_language.elims(3))
qed
lemma undefinedness_completion_inclusion :
assumes "π ∈ L"
shows "map (λ(x,y) . (x,Some y)) π ∈ undefinedness_completion X L"
proof -
let ?π = "map (λ(x,y) . (x,Some y)) π"
have "⋀ a . (a,None) ∉ set ?π"
by (induction π; auto)
then have "∀ π' x π'' . ?π = π' @ [(x,None)] @ π'' ⟶ x ∈ X ∧ out[L, non_bottom_projection π', x] = {}"
by (metis Cons_eq_appendI in_set_conv_decomp)
moreover have "non_bottom_projection ?π ∈ L"
using ‹π ∈ L› unfolding non_bottom_projection_id .
ultimately show ?thesis
by auto
qed
lemma undefinedness_completion_out_shortening :
assumes "is_language X Y L"
and "π ∈ undefinedness_completion X L"
and "x ∈ X"
shows "out[undefinedness_completion X L, π, x] = out[undefinedness_completion X L, non_bottom_shortening π, x]"
using assms(2,3) proof (induction "length π" arbitrary: π x rule: less_induct)
case less
let ?L = "undefinedness_completion X L"
show ?case proof (cases π rule: rev_cases)
case Nil
then show ?thesis by auto
next
case (snoc π' xy)
then obtain x' y' where "xy = (x',y')" by fastforce
have "x' ∈ X"
using snoc less.prems(1) unfolding ‹xy = (x',y')›
using undefinedness_completion_is_language[OF assms(1)]
by (metis fst_conv is_language.elims(2) last_in_set snoc_eq_iff_butlast)
have "π' ∈ ?L"
using snoc less.prems(1)
using undefinedness_completion_is_language[OF assms(1)]
using prefix_closure_no_member by blast
show ?thesis proof (cases y')
case None
then have "non_bottom_shortening π = non_bottom_shortening π'"
unfolding ‹xy = (x',y')› snoc by auto
then have "out[?L, non_bottom_shortening π, x] = out[?L, non_bottom_shortening π', x]"
by simp
also have "… = out[?L, π', x]"
using less.hyps[OF _ ‹π' ∈ ?L› ‹x ∈ X›] unfolding snoc
by (metis Suc_lessD length_append_singleton not_less_eq)
also have "… = out[?L, π, x]"
proof
show "out[?L, π', x] ⊆ out[?L, π, x]"
proof
fix y assume "y ∈ out[?L, π', x]"
then have "π'@[(x,y)] ∈ ?L"
by auto
then have p1: "non_bottom_projection (π'@[(x,y)]) ∈ L"
and p2: "⋀ γ' a γ'' . π'@[(x,y)] = γ' @ [(a,None)] @ γ'' ⟹ a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
by auto
have "non_bottom_projection (π@[(x,y)]) = non_bottom_projection (π'@[(x,y)])"
unfolding snoc ‹xy = (x',y')› None by auto
then have "non_bottom_projection (π@[(x,y)]) ∈ L"
using p1 by simp
moreover have "⋀ γ' a γ'' . π@[(x,y)] = γ' @ [(a,None)] @ γ'' ⟹ a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
proof -
fix γ' a γ'' assume "π@[(x,y)] = γ' @ [(a,None)] @ γ''"
then have "π'@[(x',None)]@[(x,y)] = γ' @ [(a,None)] @ γ''"
unfolding snoc ‹xy = (x',y')› None by auto
show "a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
proof (cases γ'' rule: rev_cases)
case Nil
then show ?thesis
using ‹π @ [(x, y)] = γ' @ [(a, None)] @ γ''› ‹non_bottom_shortening π = non_bottom_shortening π'› p2 by auto
next
case (snoc γ''' xy')
then show ?thesis
using ‹π @ [(x, y)] = γ' @ [(a, None)] @ γ''› less.prems(1) by force
qed
qed
ultimately show "y ∈ out[?L, π, x]"
by auto
qed
show "out[?L, π, x] ⊆ out[?L, π', x]"
proof
fix y assume "y ∈ out[?L, π, x]"
then have "π'@[(x',None)]@[(x,y)] ∈ ?L"
unfolding snoc ‹xy = (x',y')› None
by auto
then have p1: "non_bottom_projection (π'@[(x',None)]@[(x,y)]) ∈ L"
and p2: "⋀ γ' a γ'' . π'@[(x',None)]@[(x,y)] = γ' @ [(a,None)] @ γ'' ⟹ a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
by auto
have "non_bottom_projection (π'@[(x',None)]@[(x,y)]) = non_bottom_projection (π'@[(x,y)])"
by auto
then have "non_bottom_projection (π'@[(x,y)]) ∈ L"
using p1 by auto
moreover have "⋀ γ' a γ'' . π'@[(x,y)] = γ' @ [(a,None)] @ γ'' ⟹ a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
proof -
fix γ' a γ'' assume "π'@[(x,y)] = γ' @ [(a,None)] @ γ''"
show "a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
proof (cases γ'' rule: rev_cases)
case Nil
then show ?thesis
by (metis None ‹π' @ [(x, y)] = γ' @ [(a, None)] @ γ''› ‹non_bottom_shortening π = non_bottom_shortening π'› ‹xy = (x', y')› append.assoc append.right_neutral append1_eq_conv non_bottom_projection.simps p2 snoc)
next
case (snoc γ''' xy')
then show ?thesis
using ‹π' @ [(x, y)] = γ' @ [(a, None)] @ γ''› ‹π' ∈ undefinedness_completion X L› by force
qed
qed
ultimately show "y ∈ out[?L, π', x]"
by auto
qed
qed
finally show ?thesis
by blast
next
case (Some y'')
have "non_bottom_shortening π = (non_bottom_shortening π')@[(x',Some y'')]"
unfolding snoc ‹xy = (x',y')› Some by auto
then have "non_bottom_projection π = (non_bottom_projection π')@[(x',y'')]"
by auto
have "π' @ [(x', Some y'')] ∈ ?L"
using less.prems(1) unfolding snoc ‹xy = (x',y')› Some .
then have "Some y'' ∈ out[?L,π',x']"
by auto
moreover have "out[?L,π',x'] = out[?L,non_bottom_shortening π',x']"
using less.hyps[OF _ ‹π' ∈ ?L› ‹x' ∈ X›]
unfolding snoc ‹xy = (x',y')› Some
by (metis length_append_singleton lessI)
ultimately have "Some y'' ∈ out[?L,non_bottom_shortening π',x']"
by blast
show ?thesis
proof
show "out[?L,π,x] ⊆ out[?L,non_bottom_shortening π,x]"
proof
fix y assume "y ∈ out[?L,π,x]"
then have "π'@[(x',Some y'')]@[(x,y)] ∈ ?L"
unfolding snoc ‹xy = (x',y')› Some by auto
then have p1: "non_bottom_projection (π'@[(x',Some y'')]@[(x,y)]) ∈ L"
and p2: "⋀ γ' a γ'' . π'@[(x',Some y'')]@[(x,y)] = γ' @ [(a,None)] @ γ'' ⟹ a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
by auto
have "non_bottom_projection ((non_bottom_shortening π)@[(x,y)]) = non_bottom_projection (π'@[(x',Some y'')]@[(x,y)])"
unfolding ‹non_bottom_shortening π = (non_bottom_shortening π')@[(x',Some y'')]›
by auto
then have "non_bottom_projection ((non_bottom_shortening π)@[(x,y)]) ∈ L"
using p1 by simp
moreover have "⋀ γ' a γ'' . (non_bottom_shortening π)@[(x,y)] = γ' @ [(a,None)] @ γ'' ⟹ a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
proof -
fix γ' a γ'' assume "(non_bottom_shortening π)@[(x,y)] = γ' @ [(a,None)] @ γ''"
moreover have "(a, None) ∉ set (non_bottom_shortening π)"
by (induction π; auto)
moreover have "⋀ xs a ys b zs . xs@[a] = ys@[b]@zs ⟹ b ∉ set xs ⟹ zs = []"
by (metis append_Cons append_Nil butlast.simps(2) butlast_snoc in_set_butlast_appendI list.distinct(1) list.sel(1) list.set_sel(1))
ultimately have "γ'' = []"
by fastforce
then have "γ' = non_bottom_shortening π"
and "x = a"
and "y = None"
using ‹(non_bottom_shortening π)@[(x,y)] = γ' @ [(a,None)] @ γ''›
by auto
show "a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
using ‹x ∈ X› unfolding ‹x = a›
unfolding ‹γ' = non_bottom_shortening π›
by (metis (no_types, lifting) ‹non_bottom_projection (non_bottom_shortening π @ [(x, y)]) = non_bottom_projection (π' @ [(x', Some y'')] @ [(x, y)])› ‹x = a› ‹y = None› append.assoc append.right_neutral append_same_eq non_bottom_projection_split p2)
qed
ultimately show "y ∈ out[?L,non_bottom_shortening π,x]"
by auto
qed
show "out[?L,non_bottom_shortening π,x] ⊆ out[?L,π,x]"
proof
fix y assume "y ∈ out[?L,non_bottom_shortening π,x]"
then have "(non_bottom_shortening π')@[(x',Some y'')]@[(x,y)] ∈ ?L"
unfolding snoc ‹xy = (x',y')› Some by auto
then have p1: "non_bottom_projection ((non_bottom_shortening π')@[(x',Some y'')]@[(x,y)]) ∈ L"
and p2: "⋀ γ' a γ'' . (non_bottom_shortening π')@[(x',Some y'')]@[(x,y)] = γ' @ [(a,None)] @ γ'' ⟹ a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
by auto
have "non_bottom_projection ((non_bottom_shortening π')@[(x',Some y'')]@[(x,y)]) = non_bottom_projection (π@[(x,y)])"
unfolding snoc ‹xy = (x',y')› Some by auto
then have "non_bottom_projection (π@[(x,y)]) ∈ L"
using p1 by presburger
moreover have "⋀ γ' a γ'' . π@[(x,y)] = γ' @ [(a,None)] @ γ'' ⟹ a ∈ X ∧ out[L, non_bottom_projection γ', a] = {}"
proof
fix γ' a γ'' assume "π@[(x,y)] = γ' @ [(a,None)] @ γ''"
then have "(a,None) ∈ set (π@[(x,y)])"
by auto
then consider "(a,None) ∈ set π" | "(a,None) = (x,y)"
by auto
then show "a ∈ X"
by (metis assms(1) fst_conv is_language.elims(2) less.prems(1) less.prems(2) undefinedness_completion_is_language)
show "out[L,non_bottom_projection γ',a] = {}"
proof (cases γ'' rule: rev_cases)
case Nil
then have "π = γ'" and "x = a" and "y = None"
using ‹π@[(x,y)] = γ' @ [(a,None)] @ γ''› by auto
then show ?thesis
by (metis (no_types, opaque_lifting) ‹non_bottom_projection (non_bottom_shortening π' @ [(x', Some y'')] @ [(x, y)]) = non_bottom_projection (π @ [(x, y)])› ‹non_bottom_shortening π = non_bottom_shortening π' @ [(x', Some y'')]› append.assoc append_Cons append_Nil append_same_eq non_bottom_projection_split p2)
next
case (snoc γ''' xy')
then have "π = γ' @ [(a, None)] @ γ'''"
using ‹π@[(x,y)] = γ' @ [(a,None)] @ γ''› by auto
have "γ' @ [(a, None)] ∈ ?L"
using less.prems(1) unfolding ‹π = γ' @ [(a, None)] @ γ'''›
using undefinedness_completion_is_language[OF assms(1)]
by (metis append_assoc prefix_closure_no_member)
then show "out[L, non_bottom_projection γ', a] = {}"
by auto
qed
qed
ultimately show "y ∈ out[?L,π,x]"
by auto
qed
qed
qed
qed
qed
lemma undefinedness_completion_out_projection_not_empty :
assumes "is_language X Y L"
and "π ∈ undefinedness_completion X L"
and "x ∈ X"
and "out[L, non_bottom_projection π, x] ≠ {}"
shows "out[undefinedness_completion X L, non_bottom_shortening π, x] = Some ` out[L, non_bottom_projection π, x]"
proof
let ?L = "undefinedness_completion X L"
have "π@[(x,None)] ∉ ?L"
using assms(4) by auto
then have "None ∉ out[?L,π,x]"
by auto
then have "None ∉ out[?L,non_bottom_shortening π,x]"
using undefinedness_completion_out_shortening[OF assms(1,2,3)] by blast
then have "(non_bottom_shortening π)@[(x,None)] ∉ ?L"
by auto
show "out[?L, non_bottom_shortening π, x] ⊆ Some ` out[L, non_bottom_projection π, x]"
proof
fix y assume "y ∈ out[?L, non_bottom_shortening π, x]"
then have "(non_bottom_shortening π) @ [(x,y)] ∈ ?L" by auto
then have "y ≠ None"
using ‹(non_bottom_shortening π)@[(x,None)] ∉ ?L›
by meson
then obtain y' where "y = Some y'"
by auto
have "non_bottom_projection ((non_bottom_shortening π) @ [(x,y)]) = (non_bottom_projection π) @ [(x,y')]"
unfolding ‹y = Some y'›
by (induction π; auto)
then have "(non_bottom_projection π) @ [(x,y')] ∈ L"
using ‹(non_bottom_shortening π) @ [(x,y)] ∈ ?L› unfolding ‹y = Some y'›
by auto
then show "y ∈ Some ` out[L, non_bottom_projection π, x]"
unfolding ‹y = Some y'› by auto
qed
show "Some ` out[L,non_bottom_projection π,x] ⊆ out[?L,non_bottom_shortening π,x]"
proof
fix y assume "y ∈ Some ` out[L,non_bottom_projection π,x]"
then obtain y' where "y = Some y'" and "y' ∈ out[L,non_bottom_projection π,x]"
by auto
then have "(non_bottom_projection π) @ [(x,y')] ∈ L"
by auto
moreover have "non_bottom_projection ((non_bottom_shortening π) @ [(x,y)]) = (non_bottom_projection π) @ [(x,y')]"
unfolding ‹y = Some y'›
by (induction π; auto)
ultimately have "non_bottom_projection ((non_bottom_shortening π) @ [(x,y)]) ∈ L"
unfolding ‹y = Some y'›
by auto
moreover have "⋀ π' x' π'' . ((non_bottom_shortening π) @ [(x,y)]) = π' @ [(x',None)] @ π'' ⟹ x' ∈ X ∧ out[L, non_bottom_projection π', x'] = {}"
proof -
fix π' x' π'' assume "((non_bottom_shortening π) @ [(x,y)]) = π' @ [(x',None)] @ π''"
then have "(x',None) ∈ set (non_bottom_shortening π)"
by (metis ‹y = Some y'› append_Cons in_set_conv_decomp old.prod.inject option.distinct(1) rotate1.simps(2) set_ConsD set_rotate1)
then have False
by (induction π; auto)
then show "x' ∈ X ∧ out[L, non_bottom_projection π', x'] = {}"
by blast
qed
ultimately show "y ∈ out[?L,non_bottom_shortening π,x]"
by auto
qed
qed
lemma undefinedness_completion_out_projection_empty :
assumes "is_language X Y L"
and "π ∈ undefinedness_completion X L"
and "x ∈ X"
and "out[L, non_bottom_projection π, x] = {}"
shows "out[undefinedness_completion X L, non_bottom_shortening π, x] = {None}"
proof
let ?L = "undefinedness_completion X L"
have p1: "non_bottom_projection π ∈ L"
and p2: "⋀ π' x π'' . π = π' @ [(x,None)] @ π'' ⟹ x ∈ X ∧ out[L, non_bottom_projection π', x] = {}"
using assms(2) by auto
have "non_bottom_projection (π@[(x,None)]) ∈ L"
using p1 by auto
moreover have "⋀ π' x' π'' . π@[(x,None)] = π' @ [(x',None)] @ π'' ⟹ x' ∈ X ∧ out[L, non_bottom_projection π', x'] = {}"
proof -
fix π' x' π'' assume "π@[(x,None)] = π' @ [(x',None)] @ π''"
show "x' ∈ X ∧ out[L, non_bottom_projection π', x'] = {}"
proof (cases π'' rule: rev_cases)
case Nil
then show ?thesis
using ‹π @ [(x, None)] = π' @ [(x', None)] @ π''› assms(3) assms(4) by auto
next
case (snoc ys y)
then show ?thesis
using ‹π @ [(x, None)] = π' @ [(x', None)] @ π''› p2 by auto
qed
qed
ultimately have "π@[(x,None)] ∈ ?L"
by auto
then show "{None} ⊆ out[?L,non_bottom_shortening π,x]"
unfolding undefinedness_completion_out_shortening[OF assms(1,2,3), symmetric]
by auto
show "out[?L,non_bottom_shortening π,x] ⊆ {None}"
proof (rule ccontr)
assume "¬ out[?L,non_bottom_shortening π,x] ⊆ {None}"
then obtain y where "y ∈ out[?L,non_bottom_shortening π,x]" and "y ≠ None"
by blast
then obtain y' where "y = Some y'"
by auto
have "π@[(x,Some y')] ∈ ?L"
using ‹y ∈ out[?L,non_bottom_shortening π,x]›
unfolding ‹y = Some y'›
unfolding undefinedness_completion_out_shortening[OF assms(1,2,3), symmetric]
by auto
then have "(non_bottom_projection π)@[(x,y')] ∈ L"
by auto
then show False
using assms(4) by auto
qed
qed
theorem strongred_via_red :
assumes "is_language X Y L1"
and "is_language X Y L2"
shows "(L1 ≼[X,strongred Y] L2) ⟷ ((undefinedness_completion X L1) ≼[X, red ({None} ∪ Some ` Y)] (undefinedness_completion X L2))"
proof -
let ?L1 = "undefinedness_completion X L1"
let ?L2 = "undefinedness_completion X L2"
have "(L1 ≼[X,strongred Y] L2) = (∀ π ∈ L1 ∩ L2 . ∀ x ∈ X . (out[L1,π,x] = {} ∧ out[L2,π,x] = {}) ∨ (out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x]))"
(is "?A = ?B")
proof
show "?A ⟹ ?B"
unfolding strongred_type_1[OF assms, symmetric] strong_reduction_def quasi_reduction_def
by (metis outputs_executable)
show "?B ⟹ ?A"
unfolding strongred_type_1[OF assms, symmetric] strong_reduction_def quasi_reduction_def
by (metis assms(1) assms(2) executable_inputs_in_alphabet outputs_executable subset_empty)
qed
also have "… = (∀ π ∈ ?L1 ∩ ?L2 . ∀ x ∈ X . (out[L1,non_bottom_projection π,x] = {} ∧ out[L2,non_bottom_projection π,x] = {}) ∨ (out[L1,non_bottom_projection π,x] ≠ {} ∧ out[L1,non_bottom_projection π,x] ⊆ out[L2,non_bottom_projection π,x]))"
(is "?A = ?B")
proof
have "⋀ π x . ?A ⟹ π ∈ ?L1 ∩ ?L2 ⟹ x ∈ X ⟹ (out[L1,non_bottom_projection π,x] = {} ∧ out[L2,non_bottom_projection π,x] = {}) ∨ (out[L1,non_bottom_projection π,x] ≠ {} ∧ out[L1,non_bottom_projection π,x] ⊆ out[L2,non_bottom_projection π,x])"
proof -
fix π x assume "?A" and "π ∈ ?L1 ∩ ?L2" and "x ∈ X"
let ?π = "non_bottom_projection π"
have "?π ∈ L1"
and "?π ∈ L2"
using ‹π ∈ ?L1 ∩ ?L2› by auto
then show "(out[L1,?π,x] = {} ∧ out[L2,?π,x] = {}) ∨ (out[L1,?π,x] ≠ {} ∧ out[L1,?π,x] ⊆ out[L2,?π,x])"
using ‹?A› ‹x ∈ X› by blast
qed
then show "?A ⟹ ?B"
by blast
have "⋀ π x . ?B ⟹ π ∈ L1 ∩ L2 ⟹ x ∈ X ⟹ (out[L1,π,x] = {} ∧ out[L2,π,x] = {}) ∨ (out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x])"
proof -
fix π x assume "?B" and "π ∈ L1 ∩ L2" and "x ∈ X"
let ?π = "map (λ(x,y) . (x,Some y)) π"
have "?π ∈ ?L1" and "?π ∈ ?L2"
using ‹π ∈ L1 ∩ L2› undefinedness_completion_inclusion by blast+
then have "(out[L1,non_bottom_projection ?π,x] = {} ∧ out[L2,non_bottom_projection ?π,x] = {}) ∨ (out[L1,non_bottom_projection ?π,x] ≠ {} ∧ out[L1,non_bottom_projection ?π,x] ⊆ out[L2,non_bottom_projection ?π,x])"
using ‹?B› ‹x ∈ X› by blast
then show "(out[L1,π,x] = {} ∧ out[L2,π,x] = {}) ∨ (out[L1,π,x] ≠ {} ∧ out[L1,π,x] ⊆ out[L2,π,x])"
unfolding non_bottom_projection_id .
qed
then show "?B ⟹ ?A"
by blast
qed
also have "… = (∀ π ∈ ?L1 ∩ ?L2 . ∀ x ∈ X . (out[?L1,π,x] = {None} ∧ out[?L2,π,x] = {None}) ∨ (out[?L1,π,x] ≠ {None} ∧ out[?L1,π,x] ⊆ out[?L2,π,x]))"
proof -
have "⋀ π x . π ∈ ?L1 ∩ ?L2 ⟹ x ∈ X ⟹ (out[L1,non_bottom_projection π,x] = {} ∧ out[L2,non_bottom_projection π,x] = {}) = (out[?L1,π,x] = {None} ∧ out[?L2,π,x] = {None})"
by (metis IntD1 IntD2 None_notin_image_Some assms(1) assms(2) insertCI undefinedness_completion_out_projection_empty undefinedness_completion_out_projection_not_empty undefinedness_completion_out_shortening)
moreover have "⋀ π x . π ∈ ?L1 ∩ ?L2 ⟹ x ∈ X ⟹ (out[L1,non_bottom_projection π,x] ≠ {} ∧ out[L1,non_bottom_projection π,x] ⊆ out[L2,non_bottom_projection π,x]) = (out[?L1,π,x] ≠ {None} ∧ out[?L1,π,x] ⊆ out[?L2,π,x])"
proof -
fix π x assume "π ∈ ?L1 ∩ ?L2" and "x ∈ X"
then have "π ∈ ?L1" and "π ∈ ?L2" by auto
have "(out[L1,non_bottom_projection π,x] ≠ {}) = (out[?L1,π,x] ≠ {None})"
by (metis None_notin_image_Some ‹π ∈ undefinedness_completion X L1› ‹x ∈ X› assms(1) singletonI undefinedness_completion_out_projection_empty undefinedness_completion_out_projection_not_empty undefinedness_completion_out_shortening)
show "(out[L1,non_bottom_projection π,x] ≠ {} ∧ out[L1,non_bottom_projection π,x] ⊆ out[L2,non_bottom_projection π,x]) = (out[?L1,π,x] ≠ {None} ∧ out[?L1,π,x] ⊆ out[?L2,π,x])"
proof (cases "out[L1,non_bottom_projection π,x] ≠ {}")
case False
then show ?thesis using ‹(out[L1,non_bottom_projection π,x] ≠ {}) = (out[?L1,π,x] ≠ {None})› by blast
next
case True
have "out[undefinedness_completion X L1,π,x] = Some ` out[L1,non_bottom_projection π,x]"
using undefinedness_completion_out_projection_not_empty[OF assms(1) ‹π ∈ ?L1› ‹x ∈ X› True]
unfolding undefinedness_completion_out_shortening[OF assms(1) ‹π ∈ ?L1› ‹x ∈ X›,symmetric] .
show ?thesis proof (cases "out[L2,non_bottom_projection π,x] = {}")
case True
then show ?thesis
by (metis ‹(out[L1,non_bottom_projection π,x] ≠ {}) = (out[undefinedness_completion X L1,π,x] ≠ {None})› ‹π ∈ undefinedness_completion X L2› ‹out[undefinedness_completion X L1,π,x] = Some ` out[L1,non_bottom_projection π,x]› ‹x ∈ X› assms(2) image_is_empty subset_empty subset_singletonD undefinedness_completion_out_projection_empty undefinedness_completion_out_shortening)
next
case False
have "out[undefinedness_completion X L2,π,x] = Some ` out[L2,non_bottom_projection π,x]"
using undefinedness_completion_out_projection_not_empty[OF assms(2) ‹π ∈ ?L2› ‹x ∈ X› False]
unfolding undefinedness_completion_out_shortening[OF assms(2) ‹π ∈ ?L2› ‹x ∈ X›,symmetric] .
show ?thesis
unfolding ‹out[undefinedness_completion X L1,π,x] = Some ` out[L1,non_bottom_projection π,x]›
unfolding ‹out[undefinedness_completion X L2,π,x] = Some ` out[L2,non_bottom_projection π,x]›
by (metis ‹(out[L1,non_bottom_projection π,x] ≠ {}) = (out[undefinedness_completion X L1,π,x] ≠ {None})› ‹out[undefinedness_completion X L1,π,x] = Some ` out[L1,non_bottom_projection π,x]› subset_image_iff these_image_Some_eq)
qed
qed
qed
ultimately show ?thesis
by meson
qed
also have "… = (∀ π ∈ ?L1 ∩ ?L2 . ∀ x ∈ X . out[?L1,π,x] ⊆ out[?L2,π,x])"
(is "?A = ?B")
proof
show "?A ⟹ ?B"
by blast
show "?B ⟹ ?A"
by (metis IntD2 None_notin_image_Some assms(2) insert_subset undefinedness_completion_out_projection_empty undefinedness_completion_out_projection_not_empty undefinedness_completion_out_shortening)
qed
also have "… = (?L1 ≼[X, red ({None} ∪ Some ` Y)] ?L2)"
unfolding type_1_conforms.simps red.simps
using outputs_in_alphabet[OF undefinedness_completion_is_language[OF assms(2)]]
by force
finally show ?thesis .
qed
end