Theory Test_Suite_Generator_Code_Export
section ‹Code Export›
text ‹This theory exports various functions developed in this library.›
theory Test_Suite_Generator_Code_Export
imports "EquivalenceTesting/H_Method_Implementations"
"EquivalenceTesting/HSI_Method_Implementations"
"EquivalenceTesting/W_Method_Implementations"
"EquivalenceTesting/Wp_Method_Implementations"
"EquivalenceTesting/SPY_Method_Implementations"
"EquivalenceTesting/SPYH_Method_Implementations"
"EquivalenceTesting/Partial_S_Method_Implementations"
"AdaptiveStateCounting/Test_Suite_Calculation_Refined"
"Prime_Transformation"
"Prefix_Tree_Refined"
"EquivalenceTesting/Test_Suite_Representations_Refined"
"HOL-Library.List_Lexorder"
"HOL-Library.Code_Target_Nat"
"HOL-Library.Code_Target_Int"
"Native_Word.Uint64"
FSM_Code_Datatype
begin
subsection ‹Reduction Testing›
definition generate_reduction_test_suite_naive :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ String.literal + (uint64×uint64) list list" where
"generate_reduction_test_suite_naive M m = (case (calculate_test_suite_naive_as_io_sequences_with_assumption_check M (nat_of_integer m)) of
Inl err ⇒ Inl err |
Inr ts ⇒ Inr (sorted_list_of_set ts))"
definition generate_reduction_test_suite_greedy :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ String.literal + (uint64×uint64) list list" where
"generate_reduction_test_suite_greedy M m = (case (calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m)) of
Inl err ⇒ Inl err |
Inr ts ⇒ Inr (sorted_list_of_set ts))"
subsubsection ‹Fault Detection Capabilities of the Test Harness›
text ‹The test harness for reduction testing (see https://bitbucket.org/RobertSachtleben/an-approach-for-the-verification-and-synthesis-of-complete)
applies a test suite to a system under test (SUT) by repeatedly applying each IO-sequence
(test case) in the test suite input by input to the SUT until either the test case has been
fully applied or the first output is observed that does not correspond to the outputs in the
IO-sequence and then checks whether the observed IO-sequence (consisting of a prefix of the
test case possibly followed by an IO-pair consisting of the next input in the test case and an
output that is not the next output in the test case) is prefix of some test case in the test
suite. If such a prefix exists, then the application passes, else it fails and the overall
application is aborted, reporting a failure.
The following lemma shows that the SUT (whose behaviour corresponds to an FSM @{text "M'"})
conforms to the specification (here FSM @{text "M"}) if and only if the above application
procedure does not fail. As the following lemma uses quantification over all possible
responses of the SUT to each test case, a further testability hypothesis is required to
transfer this result to the actual test application process, which by necessity can only
perform a finite number of applications: we assume that some value @{text "k"} exists such
that by applying each test case @{text "k"} times, all responses of the SUT to it can be
observed.›
lemma reduction_test_harness_soundness :
fixes M :: "(uint64,uint64,uint64) fsm"
assumes "observable M'"
and "FSM.inputs M' = FSM.inputs M"
and "completely_specified M'"
and "size M' ≤ nat_of_integer m"
and "generate_reduction_test_suite_greedy M m = Inr ts"
shows "(L M' ⊆ L M) ⟷ (list_all (λ io . ¬ (∃ ioPre x y y' ioSuf . io = ioPre@[(x,y)]@ioSuf ∧ ioPre@[(x,y')] ∈ L M' ∧ ¬(∃ ioSuf' . ioPre@[(x,y')]@ioSuf' ∈ list.set ts))) ts)"
proof -
obtain tss where "calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m) = Inr tss"
using assms(5) unfolding generate_reduction_test_suite_greedy_def
by (metis Inr_Inl_False old.sum.exhaust old.sum.simps(5))
have "FSM.inputs M ≠ {}"
and "observable M"
and "completely_specified M"
using ‹calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m) = Inr tss›
unfolding calculate_test_suite_greedy_as_io_sequences_with_assumption_check_def
by (meson Inl_Inr_False)+
then have "tss = (test_suite_to_io_maximal M (calculate_test_suite_greedy M (nat_of_integer m)))"
using ‹calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m) = Inr tss›
unfolding calculate_test_suite_greedy_as_io_sequences_with_assumption_check_def
by (metis sum.inject(2))
have "⋀q. q ∈ FSM.states M ⟹ ∃d∈list.set (maximal_repetition_sets_from_separators_list_greedy M). q ∈ fst d"
unfolding maximal_repetition_sets_from_separators_list_greedy_def Let_def
using greedy_pairwise_r_distinguishable_state_sets_from_separators_cover[of _ M]
by simp
moreover have "⋀d. d ∈ list.set (maximal_repetition_sets_from_separators_list_greedy M) ⟹ fst d ⊆ FSM.states M ∧ (snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)"
and "⋀ d q1 q2. d ∈ list.set (maximal_repetition_sets_from_separators_list_greedy M) ⟹ q1∈fst d ⟹ q2∈fst d ⟹ q1 ≠ q2 ⟹ (q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
proof
fix d assume "d ∈ list.set (maximal_repetition_sets_from_separators_list_greedy M)"
then have "fst d ∈ list.set (greedy_pairwise_r_distinguishable_state_sets_from_separators M)"
and "(snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)"
unfolding maximal_repetition_sets_from_separators_list_greedy_def Let_def by force+
then have "fst d ∈ pairwise_r_distinguishable_state_sets_from_separators M"
using greedy_pairwise_r_distinguishable_state_sets_from_separators_soundness by blast
then show "fst d ⊆ FSM.states M" and "(snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)"
and "⋀ q1 q2 . q1∈fst d ⟹ q2∈fst d ⟹ q1 ≠ q2 ⟹ (q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
using ‹(snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)›
unfolding pairwise_r_distinguishable_state_sets_from_separators_def
by force+
qed
ultimately have "implies_completeness (calculate_test_suite_greedy M (nat_of_integer m)) M (nat_of_integer m)"
and "is_finite_test_suite (calculate_test_suite_greedy M (nat_of_integer m))"
using calculate_test_suite_for_repetition_sets_sufficient_and_finite[OF ‹observable M› ‹completely_specified M› ‹FSM.inputs M ≠ {}›]
unfolding calculate_test_suite_greedy_def
by simp+
then have "finite tss"
using test_suite_to_io_maximal_finite[OF _ _ ‹observable M›]
unfolding ‹tss = (test_suite_to_io_maximal M (calculate_test_suite_greedy M (nat_of_integer m)))›
by blast
have "list.set ts = test_suite_to_io_maximal M (calculate_test_suite_greedy M (nat_of_integer m))"
and "ts = sorted_list_of_set tss"
using sorted_list_of_set(1)[OF ‹finite tss›]
using assms(5)
unfolding ‹tss = (test_suite_to_io_maximal M (calculate_test_suite_greedy M (nat_of_integer m)))›
‹calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m) = Inr tss›
generate_reduction_test_suite_greedy_def
by simp+
then have "(L M' ⊆ L M) = pass_io_set_maximal M' (list.set ts)"
using calculate_test_suite_greedy_as_io_sequences_with_assumption_check_completeness[OF assms(1,2,3,4)]
‹calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m) = Inr tss›
‹tss = test_suite_to_io_maximal M (calculate_test_suite_greedy M (nat_of_integer m))›
by simp
moreover have "pass_io_set_maximal M' (list.set ts)
= (list_all (λ io . ¬ (∃ ioPre x y y' ioSuf . io = ioPre@[(x,y)]@ioSuf ∧ ioPre@[(x,y')] ∈ L M' ∧ ¬(∃ ioSuf' . ioPre@[(x,y')]@ioSuf' ∈ list.set ts))) ts)"
proof -
have "⋀ P . list_all P (sorted_list_of_set tss) = (∀ x ∈ tss . P x)"
by (simp add: ‹finite tss› list_all_iff)
then have scheme: "⋀ P . list_all P ts = (∀ x ∈ (list.set ts) . P x)"
unfolding ‹ts = sorted_list_of_set tss› sorted_list_of_set(1)[OF ‹finite tss›]
by simp
show ?thesis
using scheme[of "(λ io . ¬ (∃ ioPre x y y' ioSuf . io = ioPre@[(x,y)]@ioSuf ∧ ioPre@[(x,y')] ∈ L M' ∧ ¬(∃ ioSuf' . ioPre@[(x,y')]@ioSuf' ∈ list.set ts)))"]
unfolding pass_io_set_maximal_def
by fastforce
qed
ultimately show ?thesis
by simp
qed
subsection ‹Equivalence Testing›
subsubsection ‹Test Strategy Application and Transformation›
fun apply_method_to_prime :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64,uint64,uint64) fsm ⇒ nat ⇒ (uint64×uint64) prefix_tree) ⇒ (uint64×uint64) prefix_tree" where
"apply_method_to_prime M additionalStates isAlreadyPrime f = (let
M' = (if isAlreadyPrime then M else to_prime_uint64 M);
m = size_r M' + (nat_of_integer additionalStates)
in f M' m)"
lemma apply_method_to_prime_completeness :
fixes M2 :: "('a,uint64,uint64) fsm"
assumes "⋀ M1 m (M2 :: ('a,uint64,uint64) fsm) .
observable M1 ⟹
observable M2 ⟹
minimal M1 ⟹
minimal M2 ⟹
size_r M1 ≤ m ⟹
size M2 ≤ m ⟹
FSM.inputs M2 = FSM.inputs M1 ⟹
FSM.outputs M2 = FSM.outputs M1 ⟹
(L M1 = L M2) ⟷ ((L M1 ∩ set (f M1 m)) = (L M2 ∩ set (f M1 m)))"
and "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ ((L M1 ∩ set (apply_method_to_prime M1 additionalStates isAlreadyPrime f)) = (L M2 ∩ set (apply_method_to_prime M1 additionalStates isAlreadyPrime f)))"
proof -
define M' where "M' = (if isAlreadyPrime then M1 else to_prime_uint64 M1)"
have "observable M'" and "minimal M'" and "L M1 = L M'" and "FSM.inputs M' = FSM.inputs M1" and "FSM.outputs M' = FSM.outputs M1"
unfolding M'_def using to_prime_uint64_props[OF assms(8)] assms(7)
by (metis (full_types))+
then have "FSM.inputs M2 = FSM.inputs M'" and "FSM.outputs M2 = FSM.outputs M'"
using assms(5,6) by auto
have "size_r M' = size_r (to_prime M1)"
by (metis (no_types) ‹L M1 = L M'› ‹minimal M'› ‹observable M'› minimal_equivalence_size_r to_prime_props(1) to_prime_props(2) to_prime_props(3))
then have "size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
by simp
show ?thesis
using assms(1)[OF ‹observable M'› assms(2) ‹minimal M'› assms(3) ‹size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)› assms(4) ‹FSM.inputs M2 = FSM.inputs M'› ‹FSM.outputs M2 = FSM.outputs M'›]
unfolding apply_method_to_prime.simps Let_def ‹size_r M' = size_r (to_prime M1)›[symmetric] M'_def ‹L M1 = L M'› .
qed
fun apply_to_prime_and_return_io_lists :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64,uint64,uint64) fsm ⇒ nat ⇒ (uint64×uint64) prefix_tree) ⇒ ((uint64×uint64)×bool) list list" where
"apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime f = (let M' = (if isAlreadyPrime then M else to_prime_uint64 M) in
sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M' (FSM.initial M') (apply_method_to_prime M additionalStates isAlreadyPrime f)))"
lemma apply_to_prime_and_return_io_lists_completeness :
fixes M2 :: "('a,uint64,uint64) fsm"
assumes "⋀ M1 m (M2 :: ('a,uint64,uint64) fsm) .
observable M1 ⟹
observable M2 ⟹
minimal M1 ⟹
minimal M2 ⟹
size_r M1 ≤ m ⟹
size M2 ≤ m ⟹
FSM.inputs M2 = FSM.inputs M1 ⟹
FSM.outputs M2 = FSM.outputs M1 ⟹
((L M1 = L M2) ⟷ ((L M1 ∩ set (f M1 m)) = (L M2 ∩ set (f M1 m))))
∧ finite_tree (f M1 m)"
and "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (apply_to_prime_and_return_io_lists M1 additionalStates isAlreadyPrime f)"
proof -
define M' where "M' = (if isAlreadyPrime then M1 else to_prime_uint64 M1)"
have "observable M'" and "minimal M'" and "L M1 = L M'" and "FSM.inputs M' = FSM.inputs M1" and "FSM.outputs M' = FSM.outputs M1"
unfolding M'_def using to_prime_uint64_props[OF assms(8)] assms(7)
by (metis (full_types))+
then have "FSM.inputs M2 = FSM.inputs M'" and "FSM.outputs M2 = FSM.outputs M'"
using assms(5,6) by auto
have "L M' = L (to_prime M1)"
using to_prime_props(1) M'_def
using ‹L M1 = L M'› by blast
have "size_r M' = size_r (to_prime M1)"
using minimal_equivalence_size_r[OF ‹minimal M'› _ ‹observable M'› _ ‹L M' = L (to_prime M1)›]
using assms(7) to_prime_props(2,3)
unfolding M'_def
by blast
then have "size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
by simp
have *:"(L M1 = L M2) ⟷ ((L M1 ∩ set (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))) = (L M2 ∩ set (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))))"
and **:"finite_tree (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))"
using assms(1)[OF ‹observable M'› assms(2) ‹minimal M'› assms(3) ‹size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)› assms(4) ‹FSM.inputs M2 = FSM.inputs M'› ‹FSM.outputs M2 = FSM.outputs M'›]
unfolding ‹L M1 = L M'› by blast+
show ?thesis
unfolding *
using passes_test_cases_from_io_tree[OF ‹observable M'› assms(2) fsm_initial[of M'] fsm_initial[of M2] ** ]
unfolding ‹size_r M' = size_r (to_prime M1)›[symmetric]
unfolding apply_to_prime_and_return_io_lists.simps apply_method_to_prime.simps Let_def ‹L M1 = L M'›
unfolding M'_def by blast
qed
fun apply_to_prime_and_return_input_lists :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64,uint64,uint64) fsm ⇒ nat ⇒ (uint64×uint64) prefix_tree) ⇒ uint64 list list" where
"apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime f = test_suite_to_input_sequences (apply_method_to_prime M additionalStates isAlreadyPrime f)"
lemma apply_to_prime_and_return_input_lists_completeness :
fixes M2 :: "('a,uint64,uint64) fsm"
assumes "⋀ M1 m (M2 :: ('a,uint64,uint64) fsm) .
observable M1 ⟹
observable M2 ⟹
minimal M1 ⟹
minimal M2 ⟹
size_r M1 ≤ m ⟹
size M2 ≤ m ⟹
FSM.inputs M2 = FSM.inputs M1 ⟹
FSM.outputs M2 = FSM.outputs M1 ⟹
((L M1 = L M2) ⟷ ((L M1 ∩ set (f M1 m)) = (L M2 ∩ set (f M1 m))))
∧ finite_tree (f M1 m)"
and "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (apply_to_prime_and_return_input_lists M1 additionalStates isAlreadyPrime f). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
proof -
define M' where "M' = (if isAlreadyPrime then M1 else to_prime_uint64 M1)"
have "observable M'" and "minimal M'" and "L M1 = L M'" and "FSM.inputs M' = FSM.inputs M1" and "FSM.outputs M' = FSM.outputs M1"
unfolding M'_def using to_prime_uint64_props[OF assms(8)] assms(7)
by (metis (full_types))+
then have "FSM.inputs M2 = FSM.inputs M'" and "FSM.outputs M2 = FSM.outputs M'"
using assms(5,6) by auto
have "L M' = L (to_prime M1)"
using to_prime_props(1) M'_def ‹L M1 = L M'› by metis
have "size_r M' = size_r (to_prime M1)"
using minimal_equivalence_size_r[OF ‹minimal M'› _ ‹observable M'› _ ‹L M' = L (to_prime M1)›]
using assms(7) to_prime_props(2,3)
unfolding M'_def
by blast
then have "size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
by simp
have *:"(L M1 = L M2) = ((L M1 ∩ set (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))) = (L M2 ∩ set (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))))"
and **:"finite_tree (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))"
using assms(1)[OF ‹observable M'› assms(2) ‹minimal M'› assms(3) ‹size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)› assms(4) ‹FSM.inputs M2 = FSM.inputs M'› ‹FSM.outputs M2 = FSM.outputs M'›]
unfolding ‹L M1 = L M'› by blast+
show ?thesis
using test_suite_to_input_sequences_pass_alt_def[OF ** *]
unfolding ‹size_r M' = size_r (to_prime M1)›[symmetric]
unfolding apply_to_prime_and_return_input_lists.simps apply_method_to_prime.simps Let_def M'_def .
qed
subsubsection ‹W-Method›
definition w_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"w_method_via_h_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime w_method_via_h_framework"
lemma w_method_via_h_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (w_method_via_h_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=w_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using w_method_via_h_framework_completeness_and_finiteness
unfolding w_method_via_h_framework_ts_def
by metis
definition w_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"w_method_via_h_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime w_method_via_h_framework"
lemma w_method_via_h_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (w_method_via_h_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=w_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using w_method_via_h_framework_completeness_and_finiteness
unfolding w_method_via_h_framework_input_def[symmetric]
by (metis (no_types, lifting))
definition w_method_via_h_framework_2_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"w_method_via_h_framework_2_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime w_method_via_h_framework_2"
lemma w_method_via_h_framework_2_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (w_method_via_h_framework_2_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=w_method_via_h_framework_2 and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using w_method_via_h_framework_2_completeness_and_finiteness
unfolding w_method_via_h_framework_2_ts_def
by metis
definition w_method_via_h_framework_2_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"w_method_via_h_framework_2_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime w_method_via_h_framework_2"
lemma w_method_via_h_framework_2_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (w_method_via_h_framework_2_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=w_method_via_h_framework_2 and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using w_method_via_h_framework_2_completeness_and_finiteness
unfolding w_method_via_h_framework_2_input_def[symmetric]
by (metis (no_types, lifting))
definition w_method_via_spy_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"w_method_via_spy_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime w_method_via_spy_framework"
lemma w_method_via_spy_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (w_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=w_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using w_method_via_spy_framework_completeness_and_finiteness
unfolding w_method_via_spy_framework_ts_def
by metis
definition w_method_via_spy_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"w_method_via_spy_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime w_method_via_spy_framework"
lemma w_method_via_spy_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (w_method_via_spy_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=w_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using w_method_via_spy_framework_completeness_and_finiteness
unfolding w_method_via_spy_framework_input_def[symmetric]
by (metis (no_types, lifting))
definition w_method_via_pair_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"w_method_via_pair_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime w_method_via_pair_framework"
lemma w_method_via_pair_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (w_method_via_pair_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=w_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using w_method_via_pair_framework_completeness_and_finiteness
unfolding w_method_via_pair_framework_ts_def
by metis
definition w_method_via_pair_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"w_method_via_pair_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime w_method_via_pair_framework"
lemma w_method_via_pair_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (w_method_via_pair_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=w_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using w_method_via_pair_framework_completeness_and_finiteness
unfolding w_method_via_pair_framework_input_def[symmetric]
by (metis (no_types, lifting))
subsubsection ‹Wp-Method›
definition wp_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"wp_method_via_h_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime wp_method_via_h_framework"
lemma wp_method_via_h_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_h_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=wp_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using wp_method_via_h_framework_completeness_and_finiteness
unfolding wp_method_via_h_framework_ts_def
by metis
definition wp_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"wp_method_via_h_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime wp_method_via_h_framework"
lemma wp_method_via_h_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (wp_method_via_h_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=wp_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using wp_method_via_h_framework_completeness_and_finiteness
unfolding wp_method_via_h_framework_input_def[symmetric]
by (metis (no_types, lifting))
definition wp_method_via_spy_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"wp_method_via_spy_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime wp_method_via_spy_framework"
lemma wp_method_via_spy_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=wp_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using wp_method_via_spy_framework_completeness_and_finiteness
unfolding wp_method_via_spy_framework_ts_def
by metis
definition wp_method_via_spy_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"wp_method_via_spy_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime wp_method_via_spy_framework"
lemma wp_method_via_spy_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (wp_method_via_spy_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=wp_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using wp_method_via_spy_framework_completeness_and_finiteness
unfolding wp_method_via_spy_framework_input_def[symmetric]
by (metis (no_types, lifting))
subsubsection ‹HSI-Method›
definition hsi_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"hsi_method_via_h_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime hsi_method_via_h_framework"
lemma hsi_method_via_h_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (hsi_method_via_h_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=hsi_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using hsi_method_via_h_framework_completeness_and_finiteness
unfolding hsi_method_via_h_framework_ts_def
by metis
definition hsi_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"hsi_method_via_h_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime hsi_method_via_h_framework"
lemma hsi_method_via_h_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (hsi_method_via_h_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=hsi_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using hsi_method_via_h_framework_completeness_and_finiteness
unfolding hsi_method_via_h_framework_input_def[symmetric]
by (metis (no_types, lifting))
definition hsi_method_via_spy_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"hsi_method_via_spy_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime hsi_method_via_spy_framework"
lemma hsi_method_via_spy_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (hsi_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=hsi_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using hsi_method_via_spy_framework_completeness_and_finiteness
unfolding hsi_method_via_spy_framework_ts_def
by metis
definition hsi_method_via_spy_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"hsi_method_via_spy_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime hsi_method_via_spy_framework"
lemma hsi_method_via_spy_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (hsi_method_via_spy_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=hsi_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using hsi_method_via_spy_framework_completeness_and_finiteness
unfolding hsi_method_via_spy_framework_input_def[symmetric]
by (metis (no_types, lifting))
definition hsi_method_via_pair_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"hsi_method_via_pair_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime hsi_method_via_pair_framework"
lemma hsi_method_via_pair_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (hsi_method_via_pair_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=hsi_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using hsi_method_via_pair_framework_completeness_and_finiteness
unfolding hsi_method_via_pair_framework_ts_def
by metis
definition hsi_method_via_pair_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"hsi_method_via_pair_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime hsi_method_via_pair_framework"
lemma hsi_method_via_pair_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (hsi_method_via_pair_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=hsi_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using hsi_method_via_pair_framework_completeness_and_finiteness
unfolding hsi_method_via_pair_framework_input_def[symmetric]
by (metis (no_types, lifting))
subsubsection ‹H-Method›
definition h_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"h_method_via_h_framework_ts M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_h_framework M m c b)"
lemma h_method_via_h_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (h_method_via_h_framework_ts M1 additionalStates isAlreadyPrime c b)"
using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . h_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using h_method_via_h_framework_completeness_and_finiteness
unfolding h_method_via_h_framework_ts_def
by metis
definition h_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ uint64 list list" where
"h_method_via_h_framework_input M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_h_framework M m c b)"
lemma h_method_via_h_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (h_method_via_h_framework_input M1 additionalStates isAlreadyPrime c b). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . h_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using h_method_via_h_framework_completeness_and_finiteness
unfolding h_method_via_h_framework_input_def[symmetric]
by (metis (no_types, lifting))
definition h_method_via_pair_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"h_method_via_pair_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime h_method_via_pair_framework"
lemma h_method_via_pair_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (h_method_via_pair_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=h_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using h_method_via_pair_framework_completeness_and_finiteness
unfolding h_method_via_pair_framework_ts_def
by metis
definition h_method_via_pair_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"h_method_via_pair_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime h_method_via_pair_framework"
lemma h_method_via_pair_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (h_method_via_pair_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=h_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using h_method_via_pair_framework_completeness_and_finiteness
unfolding h_method_via_pair_framework_input_def[symmetric]
by (metis (no_types, lifting))
definition h_method_via_pair_framework_2_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"h_method_via_pair_framework_2_ts M additionalStates isAlreadyPrime c = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_pair_framework_2 M m c)"
lemma h_method_via_pair_framework_2_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (h_method_via_pair_framework_2_ts M1 additionalStates isAlreadyPrime c)"
using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . h_method_via_pair_framework_2 M m c)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using h_method_via_pair_framework_2_completeness_and_finiteness
unfolding h_method_via_pair_framework_2_ts_def
by metis
definition h_method_via_pair_framework_2_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ uint64 list list" where
"h_method_via_pair_framework_2_input M additionalStates isAlreadyPrime c = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_pair_framework_2 M m c)"
lemma h_method_via_pair_framework_2_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (h_method_via_pair_framework_2_input M1 additionalStates isAlreadyPrime c). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . h_method_via_pair_framework_2 M m c)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using h_method_via_pair_framework_2_completeness_and_finiteness
unfolding h_method_via_pair_framework_2_input_def[symmetric]
by (metis (no_types, lifting))
definition h_method_via_pair_framework_3_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"h_method_via_pair_framework_3_ts M additionalStates isAlreadyPrime c1 c2 = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_pair_framework_3 M m c1 c2)"
lemma h_method_via_pair_framework_3_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (h_method_via_pair_framework_3_ts M1 additionalStates isAlreadyPrime c1 c2)"
using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . h_method_via_pair_framework_3 M m c1 c2)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using h_method_via_pair_framework_3_completeness_and_finiteness
unfolding h_method_via_pair_framework_3_ts_def
by metis
definition h_method_via_pair_framework_3_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ uint64 list list" where
"h_method_via_pair_framework_3_input M additionalStates isAlreadyPrime c1 c2 = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_pair_framework_3 M m c1 c2)"
lemma h_method_via_pair_framework_3_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (h_method_via_pair_framework_3_input M1 additionalStates isAlreadyPrime c1 c2). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . h_method_via_pair_framework_3 M m c1 c2)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using h_method_via_pair_framework_3_completeness_and_finiteness
unfolding h_method_via_pair_framework_3_input_def[symmetric]
by (metis (no_types, lifting))
subsubsection ‹SPY-Method›
definition spy_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"spy_method_via_h_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime spy_method_via_h_framework"
lemma spy_method_via_h_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (spy_method_via_h_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=spy_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using spy_method_via_h_framework_completeness_and_finiteness
unfolding spy_method_via_h_framework_ts_def
by metis
definition spy_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"spy_method_via_h_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime spy_method_via_h_framework"
lemma spy_method_via_h_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (spy_method_via_h_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=spy_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using spy_method_via_h_framework_completeness_and_finiteness
unfolding spy_method_via_h_framework_input_def[symmetric]
by (metis (no_types, lifting))
definition spy_method_via_spy_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"spy_method_via_spy_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime spy_method_via_spy_framework"
lemma spy_method_via_spy_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (spy_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)"
using apply_to_prime_and_return_io_lists_completeness[where f=spy_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using spy_method_via_spy_framework_completeness_and_finiteness
unfolding spy_method_via_spy_framework_ts_def
by metis
definition spy_method_via_spy_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
"spy_method_via_spy_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime spy_method_via_spy_framework"
lemma spy_method_via_spy_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (spy_method_via_spy_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f=spy_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using spy_method_via_spy_framework_completeness_and_finiteness
unfolding spy_method_via_spy_framework_input_def[symmetric]
by (metis (no_types, lifting))
subsubsection ‹SPYH-Method›
definition spyh_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"spyh_method_via_h_framework_ts M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . spyh_method_via_h_framework M m c b)"
lemma spyh_method_via_h_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (spyh_method_via_h_framework_ts M1 additionalStates isAlreadyPrime c b)"
using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . spyh_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using spyh_method_via_h_framework_completeness_and_finiteness
unfolding spyh_method_via_h_framework_ts_def
by metis
definition spyh_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ uint64 list list" where
"spyh_method_via_h_framework_input M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . spyh_method_via_h_framework M m c b)"
lemma spyh_method_via_h_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (spyh_method_via_h_framework_input M1 additionalStates isAlreadyPrime c b). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . spyh_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using spyh_method_via_h_framework_completeness_and_finiteness
unfolding spyh_method_via_h_framework_input_def[symmetric]
by (metis (no_types, lifting))
definition spyh_method_via_spy_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"spyh_method_via_spy_framework_ts M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . spyh_method_via_spy_framework M m c b)"
lemma spyh_method_via_spy_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (spyh_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime c b)"
using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . spyh_method_via_spy_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using spyh_method_via_spy_framework_completeness_and_finiteness
unfolding spyh_method_via_spy_framework_ts_def
by metis
definition spyh_method_via_spy_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ uint64 list list" where
"spyh_method_via_spy_framework_input M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . spyh_method_via_spy_framework M m c b)"
lemma spyh_method_via_spy_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (spyh_method_via_spy_framework_input M1 additionalStates isAlreadyPrime c b). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . spyh_method_via_spy_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using spyh_method_via_spy_framework_completeness_and_finiteness
unfolding spyh_method_via_spy_framework_input_def[symmetric]
by (metis (no_types, lifting))
subsubsection ‹Partial S-Method›
definition partial_s_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
"partial_s_method_via_h_framework_ts M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . partial_s_method_via_h_framework M m c b)"
lemma partial_s_method_via_h_framework_ts_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (partial_s_method_via_h_framework_ts M1 additionalStates isAlreadyPrime c b)"
using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . partial_s_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using partial_s_method_via_h_framework_completeness_and_finiteness
unfolding partial_s_method_via_h_framework_ts_def
by metis
definition partial_s_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ uint64 list list" where
"partial_s_method_via_h_framework_input M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . partial_s_method_via_h_framework M m c b)"
lemma partial_s_method_via_h_framework_input_completeness :
assumes "observable M2"
and "minimal M2"
and "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
and "FSM.inputs M2 = FSM.inputs M1"
and "FSM.outputs M2 = FSM.outputs M1"
and "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
and "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (partial_s_method_via_h_framework_input M1 additionalStates isAlreadyPrime c b). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . partial_s_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
using partial_s_method_via_h_framework_completeness_and_finiteness
unfolding partial_s_method_via_h_framework_input_def[symmetric]
by (metis (no_types, lifting))
subsection ‹New Instances›
lemma finiteness_fset_UNIV : "finite (UNIV :: 'a fset set) = finite (UNIV :: 'a set)"
proof
define f :: "'a ⇒ ('a) fset" where f_def: "f = (λ q . {| q |})"
have "inj f"
proof
fix x y assume "x ∈ (UNIV :: 'a set)" and "y ∈ UNIV" and "f x = f y"
then show "x = y" unfolding f_def by (transfer; auto)
qed
show "finite (UNIV :: 'a fset set) ⟹ finite (UNIV :: 'a set)"
proof (rule ccontr)
assume "finite (UNIV :: 'a fset set)" and "¬ finite (UNIV :: 'a set)"
then have "¬ finite (f ` UNIV)"
using ‹inj f›
using finite_imageD by blast
then have "¬ finite (UNIV :: 'a fset set)"
by (meson infinite_iff_countable_subset top_greatest)
then show False
using ‹finite (UNIV :: 'a fset set)› by auto
qed
show "finite (UNIV :: 'a set) ⟹ finite (UNIV :: 'a fset set)"
proof -
assume "finite (UNIV :: 'a set)"
then have "finite (UNIV :: 'a set set)"
by (simp add: Finite_Set.finite_set)
moreover have "fset ` (UNIV :: 'a fset set) ⊆ (UNIV :: 'a set set)"
by auto
moreover have "inj fset"
by (meson fset_inject injI)
ultimately show ?thesis by (metis inj_on_finite)
qed
qed
instantiation fset :: (finite_UNIV) finite_UNIV begin
definition "finite_UNIV = Phantom('a fset) (of_phantom (finite_UNIV :: 'a finite_UNIV))"
instance by(intro_classes)(simp add: finite_UNIV_fset_def finite_UNIV finiteness_fset_UNIV)
end
derive (eq) ceq fset
derive (no) cenum fset
derive (no) ccompare fset
derive (dlist) set_impl fset
instantiation fset :: (type) cproper_interval begin
definition cproper_interval_fset :: "(('a) fset) proper_interval"
where "cproper_interval_fset _ _ = undefined"
instance by(intro_classes)(simp add: ID_None ccompare_fset_def)
end
lemma card_fPow: "card (Pow (fset A)) = 2 ^ card (fset A)"
using card_Pow[of "fset A"]
by simp
lemma finite_sets_finite_univ :
assumes "finite (UNIV :: 'a set)"
shows "finite (xs :: 'a set)"
by (metis Diff_UNIV Diff_infinite_finite assms finite_Diff)
lemma card_UNIV_fset: "CARD('a fset) = (if CARD('a) = 0 then 0 else 2 ^ CARD('a))"
apply (simp add: card_eq_0_iff)
proof
have "inj fset"
by (meson fset_inject injI)
have "card (UNIV :: 'a fset set) = card (fset ` (UNIV :: 'a fset set))"
by (simp add: ‹inj fset› card_image)
show "finite (UNIV :: 'a set) ⟶ CARD('a fset) = 2 ^ CARD('a)"
proof
assume "finite (UNIV :: 'a set)"
then have "CARD('a set) = 2 ^ CARD('a)"
by (metis Pow_UNIV card_Pow)
have "finite (UNIV :: 'a set set)"
using ‹finite (UNIV :: 'a set)›
by (simp add: Finite_Set.finite_set)
have "finite (UNIV :: 'a fset set)"
using ‹finite (UNIV :: 'a set)› finiteness_fset_UNIV by auto
have "⋀ xs :: 'a set . finite xs"
using finite_sets_finite_univ[OF ‹finite (UNIV :: 'a set)›] .
then have "(UNIV :: 'a set set) = fset ` (UNIV :: 'a fset set)"
by (metis UNIV_I UNIV_eq_I fset_to_fset image_iff)
have "CARD('a fset) ≤ CARD('a set)"
unfolding ‹card (UNIV :: 'a fset set) = card (fset ` (UNIV :: 'a fset set))›
by (metis ‹finite (UNIV :: 'a set set)› card_mono subset_UNIV)
moreover have "CARD('a fset) ≥ CARD('a set)"
unfolding ‹(UNIV :: 'a set set) = fset ` (UNIV :: 'a fset set)›
using ‹CARD('a::type fset) = card (range fset)› by linarith
ultimately have "CARD('a fset) = CARD('a set)"
by linarith
then show "CARD('a fset) = (2::nat) ^ CARD('a)"
by (simp add: ‹CARD('a::type set) = (2::nat) ^ CARD('a::type)›)
qed
show "infinite (UNIV :: 'a set) ⟶ infinite (UNIV :: 'a fset set)"
by (simp add: finiteness_fset_UNIV)
qed
instantiation fset :: (card_UNIV) card_UNIV begin
definition "card_UNIV = Phantom('a fset)
(let c = of_phantom (card_UNIV :: 'a card_UNIV) in if c = 0 then 0 else 2 ^ c)"
instance by intro_classes (simp add: card_UNIV_fset_def card_UNIV_fset card_UNIV)
end
derive (choose) mapping_impl fset
lemma uint64_range : "range nat_of_uint64 = {..<2 ^ 64}"
proof
show "{..<2 ^ 64} ⊆ range nat_of_uint64"
using uint64_nat_bij
by (metis lessThan_iff range_eqI subsetI)
have "⋀ x . nat_of_uint64 x < 2^64"
apply transfer using take_bit_nat_eq_self
by (metis uint64.size_eq_length unsigned_less)
then show "range nat_of_uint64 ⊆ {..<2 ^ 64}"
by auto
qed
lemma card_UNIV_uint64: "CARD(uint64) = 2^64"
proof -
have "inj nat_of_uint64"
apply transfer
by simp
then have "bij_betw nat_of_uint64 (UNIV :: uint64 set) {..<2^64}"
using uint64_range
unfolding bij_betw_def by blast
then show ?thesis
by (simp add: bij_betw_same_card)
qed
lemma nat_of_uint64_bij_betw : "bij_betw nat_of_uint64 (UNIV :: uint64 set) {..<2 ^ 64}"
unfolding bij_betw_def
using uint64_range
by transfer (auto)
lemma uint64_UNIV : "(UNIV :: uint64 set) = uint64_of_nat ` {..<2 ^ 64}"
using nat_of_uint64_bij_betw
by (metis UNIV_I UNIV_eq_I bij_betw_def card_UNIV_uint64 imageI image_eqI inj_on_contraD lessThan_iff rangeI uint64_nat_bij uint64_range)
lemma uint64_of_nat_bij_betw : "bij_betw uint64_of_nat {..<2 ^ 64} (UNIV :: uint64 set)"
unfolding bij_betw_def
proof
show "inj_on uint64_of_nat {..<2 ^ 64}"
using nat_of_uint64_bij_betw uint64_nat_bij
by (metis inj_on_inverseI lessThan_iff)
show "uint64_of_nat ` {..<2 ^ 64} = UNIV"
using uint64_UNIV by blast
qed
lemma uint64_finite : "finite (UNIV :: uint64 set)"
unfolding uint64_UNIV
by simp
instantiation uint64 :: finite_UNIV begin
definition "finite_UNIV = Phantom(uint64) True"
instance apply intro_classes
by (simp add: finite_UNIV_uint64_def uint64_finite)
end
instantiation uint64 :: card_UNIV begin
definition "card_UNIV = Phantom(uint64) (2^64)"
instance
by intro_classes (simp add: card_UNIV_uint64_def card_UNIV_uint64 card_UNIV)
end
instantiation uint64 :: compare
begin
definition compare_uint64 :: "uint64 ⇒ uint64 ⇒ order" where
"compare_uint64 x y = (case (x < y, x = y) of (True,_) ⇒ Lt | (False,True) ⇒ Eq | (False,False) ⇒ Gt)"
instance
apply intro_classes
proof
show "⋀x y::uint64. invert_order (compare x y) = compare y x"
proof -
fix x y::uint64 show "invert_order (compare x y) = compare y x"
proof (cases "x = y")
case True
then show ?thesis unfolding compare_uint64_def by auto
next
case False
then show ?thesis proof (cases "x < y")
case True
then show ?thesis unfolding compare_uint64_def using False
using order_less_not_sym by fastforce
next
case False
then show ?thesis unfolding compare_uint64_def using ‹x ≠ y›
using linorder_less_linear by fastforce
qed
qed
qed
show "⋀x y::uint64. compare x y = Eq ⟹ x = y"
unfolding compare_uint64_def
by (metis (mono_tags) case_prod_conv old.bool.simps(3) old.bool.simps(4) order.distinct(1) order.distinct(3))
show "⋀x y z::uint64. compare x y = Lt ⟹ compare y z = Lt ⟹ compare x z = Lt"
unfolding compare_uint64_def
by (metis (full_types, lifting) case_prod_conv old.bool.simps(3) old.bool.simps(4) order.distinct(5) order_less_trans)
qed
end
instantiation uint64 :: ccompare
begin
definition ccompare_uint64 :: "(uint64 ⇒ uint64 ⇒ order) option" where
"ccompare_uint64 = Some compare"
instance by (intro_classes; simp add: ccompare_uint64_def comparator_compare)
end
derive (eq) ceq uint64
derive (no) cenum uint64
derive (rbt) set_impl uint64
derive (rbt) mapping_impl uint64
instantiation uint64 :: proper_interval begin
fun proper_interval_uint64 :: "uint64 proper_interval"
where
"proper_interval_uint64 None None = True" |
"proper_interval_uint64 None (Some y) = (y > 0)"|
"proper_interval_uint64 (Some x) None = (x ≠ uint64_of_nat (2^64-1))" |
"proper_interval_uint64 (Some x) (Some y) = (x < y ∧ x+1 < y)"
instance apply intro_classes
proof -
show "proper_interval None (None :: uint64 option) = True" by auto
show "⋀y. proper_interval None (Some (y::uint64)) = (∃z. z < y)"
unfolding proper_interval_uint64.simps
apply transfer
using word_gt_a_gt_0 by auto
have "⋀ x . (x ≠ uint64_of_nat (2^64-1)) = (nat_of_uint64 x ≠ 2^64-1)"
proof
fix x
show "(x ≠ uint64_of_nat (2^64-1)) ⟹ (nat_of_uint64 x ≠ 2^64-1)"
apply transfer
by (metis Word.of_nat_unat ucast_id)
show "nat_of_uint64 x ≠ 2 ^ 64 - 1 ⟹ x ≠ uint64_of_nat (2 ^ 64 - 1)"
by (meson diff_less pos2 uint64_nat_bij zero_less_one zero_less_power)
qed
then show "⋀x. proper_interval (Some (x::uint64)) None = (∃z. x < z)"
unfolding proper_interval_uint64.simps
apply transfer
by (metis uint64.size_eq_length unat_minus_one_word word_le_less_eq word_le_not_less word_order.extremum)
show "⋀x y. proper_interval (Some x) (Some (y::uint64)) = (∃z>x. z < y)"
unfolding proper_interval_uint64.simps
apply transfer
using inc_le less_is_non_zero_p1 word_overflow
by fastforce
qed
end
instantiation uint64 :: cproper_interval begin
definition "cproper_interval = (proper_interval :: uint64 proper_interval)"
instance
apply intro_classes
apply (simp add: cproper_interval_uint64_def ord_defs ccompare_uint64_def ID_Some proper_interval_class.axioms uint64_finite)
proof
fix x y :: uint64
show "proper_interval None (None :: uint64 option) = True"
by auto
have "(∃z. lt_of_comp compare z y) = (∃z. z < y)"
unfolding compare_uint64_def lt_of_comp_def
by (metis bool.case_eq_if case_prod_conv order.simps(7) order.simps(8) order.simps(9))
then show "proper_interval None (Some y) = (∃z. lt_of_comp compare z y)"
using proper_interval_simps(2) by blast
have "(∃z. lt_of_comp compare x z) = (∃z. x < z)"
unfolding compare_uint64_def lt_of_comp_def
by (metis bool.case_eq_if case_prod_conv order.simps(7) order.simps(8) order.simps(9))
then show "proper_interval (Some x) None = (∃z. lt_of_comp compare x z)"
using proper_interval_simps(3) by blast
have "(∃z. lt_of_comp compare x z ∧ lt_of_comp compare z y) ⟹ (∃z>x. z < y)"
unfolding compare_uint64_def lt_of_comp_def
by (metis bool.case_eq_if case_prod_conv order.simps(7) order.simps(9))
moreover have "(∃z>x. z < y) ⟹ (∃z. lt_of_comp compare x z ∧ lt_of_comp compare z y)"
unfolding compare_uint64_def lt_of_comp_def
unfolding proper_interval_simps(4)[symmetric]
using compare_uint64_def
by (metis (mono_tags, lifting) ‹⋀y x. (∃z>x. z < y) = proper_interval (Some x) (Some y)› case_prod_conv old.bool.simps(3) order.simps(8))
ultimately show "proper_interval (Some x) (Some y) = (∃z. lt_of_comp compare x z ∧ lt_of_comp compare z y)"
using proper_interval_simps(4) by blast
qed
end
subsection ‹Exports›
fun fsm_from_list_uint64 :: "uint64 ⇒ (uint64 × uint64 × uint64 × uint64) list ⇒ (uint64, uint64, uint64) fsm"
where "fsm_from_list_uint64 q ts = fsm_from_list q ts"
fun fsm_from_list_integer :: "integer ⇒ (integer × integer × integer × integer) list ⇒ (integer, integer, integer) fsm"
where "fsm_from_list_integer q ts = fsm_from_list q ts"
export_code Inl
fsm_from_list
fsm_from_list_uint64
fsm_from_list_integer
size
to_prime
make_observable
rename_states
index_states
restrict_to_reachable_states
integer_of_nat
generate_reduction_test_suite_naive
generate_reduction_test_suite_greedy
w_method_via_h_framework_ts
w_method_via_h_framework_input
w_method_via_h_framework_2_ts
w_method_via_h_framework_2_input
w_method_via_spy_framework_ts
w_method_via_spy_framework_input
w_method_via_pair_framework_ts
w_method_via_pair_framework_input
wp_method_via_h_framework_ts
wp_method_via_h_framework_input
wp_method_via_spy_framework_ts
wp_method_via_spy_framework_input
hsi_method_via_h_framework_ts
hsi_method_via_h_framework_input
hsi_method_via_spy_framework_ts
hsi_method_via_spy_framework_input
hsi_method_via_pair_framework_ts
hsi_method_via_pair_framework_input
h_method_via_h_framework_ts
h_method_via_h_framework_input
h_method_via_pair_framework_ts
h_method_via_pair_framework_input
h_method_via_pair_framework_2_ts
h_method_via_pair_framework_2_input
h_method_via_pair_framework_3_ts
h_method_via_pair_framework_3_input
spy_method_via_h_framework_ts
spy_method_via_h_framework_input
spy_method_via_spy_framework_ts
spy_method_via_spy_framework_input
spyh_method_via_h_framework_ts
spyh_method_via_h_framework_input
spyh_method_via_spy_framework_ts
spyh_method_via_spy_framework_input
partial_s_method_via_h_framework_ts
partial_s_method_via_h_framework_input
in Haskell module_name GeneratedCode file_prefix haskell_export
export_code Inl
fsm_from_list
fsm_from_list_uint64
fsm_from_list_integer
size
to_prime
make_observable
rename_states
index_states
restrict_to_reachable_states
integer_of_nat
generate_reduction_test_suite_naive
generate_reduction_test_suite_greedy
w_method_via_h_framework_ts
w_method_via_h_framework_input
w_method_via_h_framework_2_ts
w_method_via_h_framework_2_input
w_method_via_spy_framework_ts
w_method_via_spy_framework_input
w_method_via_pair_framework_ts
w_method_via_pair_framework_input
wp_method_via_h_framework_ts
wp_method_via_h_framework_input
wp_method_via_spy_framework_ts
wp_method_via_spy_framework_input
hsi_method_via_h_framework_ts
hsi_method_via_h_framework_input
hsi_method_via_spy_framework_ts
hsi_method_via_spy_framework_input
hsi_method_via_pair_framework_ts
hsi_method_via_pair_framework_input
h_method_via_h_framework_ts
h_method_via_h_framework_input
h_method_via_pair_framework_ts
h_method_via_pair_framework_input
h_method_via_pair_framework_2_ts
h_method_via_pair_framework_2_input
h_method_via_pair_framework_3_ts
h_method_via_pair_framework_3_input
spy_method_via_h_framework_ts
spy_method_via_h_framework_input
spy_method_via_spy_framework_ts
spy_method_via_spy_framework_input
spyh_method_via_h_framework_ts
spyh_method_via_h_framework_input
spyh_method_via_spy_framework_ts
spyh_method_via_spy_framework_input
partial_s_method_via_h_framework_ts
partial_s_method_via_h_framework_input
in Scala module_name GeneratedCode file_prefix scala_export (case_insensitive)
export_code Inl
fsm_from_list
fsm_from_list_uint64
fsm_from_list_integer
size
to_prime
make_observable
rename_states
index_states
restrict_to_reachable_states
integer_of_nat
generate_reduction_test_suite_naive
generate_reduction_test_suite_greedy
w_method_via_h_framework_ts
w_method_via_h_framework_input
w_method_via_h_framework_2_ts
w_method_via_h_framework_2_input
w_method_via_spy_framework_ts
w_method_via_spy_framework_input
w_method_via_pair_framework_ts
w_method_via_pair_framework_input
wp_method_via_h_framework_ts
wp_method_via_h_framework_input
wp_method_via_spy_framework_ts
wp_method_via_spy_framework_input
hsi_method_via_h_framework_ts
hsi_method_via_h_framework_input
hsi_method_via_spy_framework_ts
hsi_method_via_spy_framework_input
hsi_method_via_pair_framework_ts
hsi_method_via_pair_framework_input
h_method_via_h_framework_ts
h_method_via_h_framework_input
h_method_via_pair_framework_ts
h_method_via_pair_framework_input
h_method_via_pair_framework_2_ts
h_method_via_pair_framework_2_input
h_method_via_pair_framework_3_ts
h_method_via_pair_framework_3_input
spy_method_via_h_framework_ts
spy_method_via_h_framework_input
spy_method_via_spy_framework_ts
spy_method_via_spy_framework_input
spyh_method_via_h_framework_ts
spyh_method_via_h_framework_input
spyh_method_via_spy_framework_ts
spyh_method_via_spy_framework_input
partial_s_method_via_h_framework_ts
partial_s_method_via_h_framework_input
in SML module_name GeneratedCode file_prefix sml_export
export_code Inl
fsm_from_list
fsm_from_list_uint64
fsm_from_list_integer
size
to_prime
make_observable
rename_states
index_states
restrict_to_reachable_states
integer_of_nat
generate_reduction_test_suite_naive
generate_reduction_test_suite_greedy
w_method_via_h_framework_ts
w_method_via_h_framework_input
w_method_via_h_framework_2_ts
w_method_via_h_framework_2_input
w_method_via_spy_framework_ts
w_method_via_spy_framework_input
w_method_via_pair_framework_ts
w_method_via_pair_framework_input
wp_method_via_h_framework_ts
wp_method_via_h_framework_input
wp_method_via_spy_framework_ts
wp_method_via_spy_framework_input
hsi_method_via_h_framework_ts
hsi_method_via_h_framework_input
hsi_method_via_spy_framework_ts
hsi_method_via_spy_framework_input
hsi_method_via_pair_framework_ts
hsi_method_via_pair_framework_input
h_method_via_h_framework_ts
h_method_via_h_framework_input
h_method_via_pair_framework_ts
h_method_via_pair_framework_input
h_method_via_pair_framework_2_ts
h_method_via_pair_framework_2_input
h_method_via_pair_framework_3_ts
h_method_via_pair_framework_3_input
spy_method_via_h_framework_ts
spy_method_via_h_framework_input
spy_method_via_spy_framework_ts
spy_method_via_spy_framework_input
spyh_method_via_h_framework_ts
spyh_method_via_h_framework_input
spyh_method_via_spy_framework_ts
spyh_method_via_spy_framework_input
partial_s_method_via_h_framework_ts
partial_s_method_via_h_framework_input
in OCaml module_name GeneratedCode file_prefix ocaml_export
end