Theory Normal_Form_Code_Export
section ‹Code Export›
theory Normal_Form_Code_Export imports
LTL.Code_Equations
LTL.Rewriting
LTL.Disjunctive_Normal_Form
HOL.String
Normal_Form
begin
fun flatten_pi_1_list :: "String.literal ltln ⇒ String.literal ltln list ⇒ String.literal ltln"
where
"flatten_pi_1_list (ψ⇩1 U⇩n ψ⇩2) M = (if (ψ⇩1 U⇩n ψ⇩2) ∈ set M then (flatten_pi_1_list ψ⇩1 M) W⇩n (flatten_pi_1_list ψ⇩2 M) else false⇩n)"
| "flatten_pi_1_list (ψ⇩1 W⇩n ψ⇩2) M = (flatten_pi_1_list ψ⇩1 M) W⇩n (flatten_pi_1_list ψ⇩2 M)"
| "flatten_pi_1_list (ψ⇩1 M⇩n ψ⇩2) M = (if (ψ⇩1 M⇩n ψ⇩2) ∈ set M then (flatten_pi_1_list ψ⇩1 M) R⇩n (flatten_pi_1_list ψ⇩2 M) else false⇩n)"
| "flatten_pi_1_list (ψ⇩1 R⇩n ψ⇩2) M = (flatten_pi_1_list ψ⇩1 M) R⇩n (flatten_pi_1_list ψ⇩2 M)"
| "flatten_pi_1_list (ψ⇩1 and⇩n ψ⇩2) M = (flatten_pi_1_list ψ⇩1 M) and⇩n (flatten_pi_1_list ψ⇩2 M)"
| "flatten_pi_1_list (ψ⇩1 or⇩n ψ⇩2) M = (flatten_pi_1_list ψ⇩1 M) or⇩n (flatten_pi_1_list ψ⇩2 M)"
| "flatten_pi_1_list (X⇩n ψ) M = X⇩n (flatten_pi_1_list ψ M)"
| "flatten_pi_1_list φ _ = φ"
fun flatten_sigma_1_list :: "String.literal ltln ⇒ String.literal ltln list ⇒ String.literal ltln"
where
"flatten_sigma_1_list (ψ⇩1 U⇩n ψ⇩2) N = (flatten_sigma_1_list ψ⇩1 N) U⇩n (flatten_sigma_1_list ψ⇩2 N)"
| "flatten_sigma_1_list (ψ⇩1 W⇩n ψ⇩2) N = (if (ψ⇩1 W⇩n ψ⇩2) ∈ set N then true⇩n else (flatten_sigma_1_list ψ⇩1 N) U⇩n (flatten_sigma_1_list ψ⇩2 N))"
| "flatten_sigma_1_list (ψ⇩1 M⇩n ψ⇩2) N = (flatten_sigma_1_list ψ⇩1 N) M⇩n (flatten_sigma_1_list ψ⇩2 N)"
| "flatten_sigma_1_list (ψ⇩1 R⇩n ψ⇩2) N = (if (ψ⇩1 R⇩n ψ⇩2) ∈ set N then true⇩n else (flatten_sigma_1_list ψ⇩1 N) M⇩n (flatten_sigma_1_list ψ⇩2 N))"
| "flatten_sigma_1_list (ψ⇩1 and⇩n ψ⇩2) N = (flatten_sigma_1_list ψ⇩1 N) and⇩n (flatten_sigma_1_list ψ⇩2 N)"
| "flatten_sigma_1_list (ψ⇩1 or⇩n ψ⇩2) N = (flatten_sigma_1_list ψ⇩1 N) or⇩n (flatten_sigma_1_list ψ⇩2 N)"
| "flatten_sigma_1_list (X⇩n ψ) N = X⇩n (flatten_sigma_1_list ψ N)"
| "flatten_sigma_1_list φ _ = φ"
fun flatten_sigma_2_list :: "String.literal ltln ⇒ String.literal ltln list ⇒ String.literal ltln"
where
"flatten_sigma_2_list (φ U⇩n ψ) M = (flatten_sigma_2_list φ M) U⇩n (flatten_sigma_2_list ψ M)"
| "flatten_sigma_2_list (φ W⇩n ψ) M = (flatten_sigma_2_list φ M) U⇩n ((flatten_sigma_2_list ψ M) or⇩n (G⇩n (flatten_pi_1_list φ M)))"
| "flatten_sigma_2_list (φ M⇩n ψ) M = (flatten_sigma_2_list φ M) M⇩n (flatten_sigma_2_list ψ M)"
| "flatten_sigma_2_list (φ R⇩n ψ) M = ((flatten_sigma_2_list φ M) or⇩n (G⇩n (flatten_pi_1_list ψ M))) M⇩n (flatten_sigma_2_list ψ M)"
| "flatten_sigma_2_list (φ and⇩n ψ) M = (flatten_sigma_2_list φ M) and⇩n (flatten_sigma_2_list ψ M)"
| "flatten_sigma_2_list (φ or⇩n ψ) M = (flatten_sigma_2_list φ M) or⇩n (flatten_sigma_2_list ψ M)"
| "flatten_sigma_2_list (X⇩n φ) M = X⇩n (flatten_sigma_2_list φ M)"
| "flatten_sigma_2_list φ _ = φ"
lemma flatten_code_equations[simp]:
"φ[set M]⇩Π⇩1 = flatten_pi_1_list φ M"
"φ[set M]⇩Σ⇩1 = flatten_sigma_1_list φ M"
"φ[set M]⇩Σ⇩2 = flatten_sigma_2_list φ M"
by (induction φ) auto
abbreviation "and_list ≡ foldl And_ltln true⇩n"
abbreviation "or_list ≡ foldl Or_ltln false⇩n"
definition "normal_form_disjunct (φ :: String.literal ltln) M N
≡ (flatten_sigma_2_list φ M)
and⇩n (and_list (map (λψ. G⇩n (F⇩n (flatten_sigma_1_list ψ N))) M)
and⇩n (and_list (map (λψ. F⇩n (G⇩n (flatten_pi_1_list ψ M))) N)))"
definition "normal_form (φ :: String.literal ltln)
≡ or_list (map (λ(M, N). normal_form_disjunct φ M N) (advice_sets φ))"
lemma and_list_semantic: "w ⊨⇩n and_list xs ⟷ (∀x ∈ set xs. w ⊨⇩n x)"
by (induction xs rule: rev_induct) auto
lemma or_list_semantic: "w ⊨⇩n or_list xs ⟷ (∃x ∈ set xs. w ⊨⇩n x)"
by (induction xs rule: rev_induct) auto
theorem normal_form_correct:
"w ⊨⇩n φ ⟷ w ⊨⇩n normal_form φ"
proof
assume "w ⊨⇩n φ"
then obtain M N where "M ⊆ subformulas⇩μ φ" and "N ⊆ subformulas⇩ν φ"
and c1: "w ⊨⇩n φ[M]⇩Σ⇩2" and c2: "∀ψ ∈ M. w ⊨⇩n G⇩n (F⇩n ψ[N]⇩Σ⇩1)" and c3: "∀ψ ∈ N. w ⊨⇩n F⇩n (G⇩n ψ[M]⇩Π⇩1)"
using normal_form_with_flatten_sigma_2 by metis
then obtain ms ns where "M = set ms" and "N = set ns" and ms_ns_in: "(ms, ns) ∈ set (advice_sets φ)"
by (meson advice_sets_subformulas)
then have "w ⊨⇩n normal_form_disjunct φ ms ns"
using c1 c2 c3 by (simp add: and_list_semantic normal_form_disjunct_def)
then show "w ⊨⇩n normal_form φ"
using normal_form_def or_list_semantic ms_ns_in by fastforce
next
assume "w ⊨⇩n normal_form φ"
then obtain ms ns where "(ms, ns) ∈ set (advice_sets φ)"
and "w ⊨⇩n normal_form_disjunct φ ms ns"
unfolding normal_form_def or_list_semantic by force
then have "set ms ⊆ subformulas⇩μ φ" and "set ns ⊆ subformulas⇩ν φ"
and c1: "w ⊨⇩n φ[set ms]⇩Σ⇩2" and c2: "∀ψ ∈ set ms. w ⊨⇩n G⇩n (F⇩n ψ[set ns]⇩Σ⇩1)" and c3: "∀ψ ∈ set ns. w ⊨⇩n F⇩n (G⇩n ψ[set ms]⇩Π⇩1)"
using advice_sets_element_subfrmlsn
by (auto simp: and_list_semantic normal_form_disjunct_def) blast
then show "w ⊨⇩n φ"
using normal_form_with_flatten_sigma_2 by metis
qed
definition "normal_form_with_simplifier (φ :: String.literal ltln)
≡ min_dnf (simplify Slow (normal_form (simplify Slow φ)))"
lemma ltl_semantics_min_dnf:
"w ⊨⇩n φ ⟷ (∃C ∈ min_dnf φ. ∀ψ. ψ |∈| C ⟶ w ⊨⇩n ψ)" (is "?lhs ⟷ ?rhs")
proof
let ?M = "{ψ. w ⊨⇩n ψ}"
assume ?lhs
hence "?M ⊨⇩P φ"
using ltl_models_equiv_prop_entailment by blast
then obtain M' where "fset M' ⊆ ?M" and "M' ∈ min_dnf φ"
using min_dnf_iff_prop_assignment_subset by blast
thus ?rhs
by (meson in_mono mem_Collect_eq)
next
let ?M = "{ψ. w ⊨⇩n ψ}"
assume ?rhs
then obtain M' where "fset M' ⊆ ?M" and "M' ∈ min_dnf φ"
by auto
hence "?M ⊨⇩P φ"
using min_dnf_iff_prop_assignment_subset by blast
thus ?lhs
using ltl_models_equiv_prop_entailment by blast
qed
theorem
"w ⊨⇩n φ ⟷ (∃C ∈ (normal_form_with_simplifier φ). ∀ψ. ψ |∈| C ⟶ w ⊨⇩n ψ)" (is "?lhs ⟷ ?rhs")
unfolding normal_form_with_simplifier_def ltl_semantics_min_dnf[symmetric]
using normal_form_correct by simp
text ‹In order to export the code run \texttt{isabelle build -D [PATH] -e}.›
export_code normal_form in SML
export_code normal_form_with_simplifier in SML
end