Theory Normal_Form_Code_Export

(*
    Author:   Salomon Sickert
    License:  BSD
*)

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 Un ψ2) M = (if (ψ1 Un ψ2)  set M then (flatten_pi_1_list ψ1 M) Wn (flatten_pi_1_list ψ2 M) else falsen)"
| "flatten_pi_1_list (ψ1 Wn ψ2) M = (flatten_pi_1_list ψ1 M) Wn (flatten_pi_1_list ψ2 M)"
| "flatten_pi_1_list (ψ1 Mn ψ2) M = (if (ψ1 Mn ψ2)  set M then (flatten_pi_1_list ψ1 M) Rn (flatten_pi_1_list ψ2 M) else falsen)"
| "flatten_pi_1_list (ψ1 Rn ψ2) M = (flatten_pi_1_list ψ1 M) Rn (flatten_pi_1_list ψ2 M)"
| "flatten_pi_1_list (ψ1 andn ψ2) M = (flatten_pi_1_list ψ1 M) andn (flatten_pi_1_list ψ2 M)"
| "flatten_pi_1_list (ψ1 orn ψ2) M = (flatten_pi_1_list ψ1 M) orn (flatten_pi_1_list ψ2 M)"
| "flatten_pi_1_list (Xn ψ) M = Xn (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 Un ψ2) N = (flatten_sigma_1_list ψ1 N) Un (flatten_sigma_1_list ψ2 N)"
| "flatten_sigma_1_list (ψ1 Wn ψ2) N = (if (ψ1 Wn ψ2)  set N then truen else (flatten_sigma_1_list ψ1 N) Un (flatten_sigma_1_list ψ2 N))"
| "flatten_sigma_1_list (ψ1 Mn ψ2) N = (flatten_sigma_1_list ψ1 N) Mn (flatten_sigma_1_list ψ2 N)"
| "flatten_sigma_1_list (ψ1 Rn ψ2) N = (if (ψ1 Rn ψ2)  set N then truen else (flatten_sigma_1_list ψ1 N) Mn (flatten_sigma_1_list ψ2 N))"
| "flatten_sigma_1_list (ψ1 andn ψ2) N = (flatten_sigma_1_list ψ1 N) andn (flatten_sigma_1_list ψ2 N)"
| "flatten_sigma_1_list (ψ1 orn ψ2) N = (flatten_sigma_1_list ψ1 N) orn (flatten_sigma_1_list ψ2 N)"
| "flatten_sigma_1_list (Xn ψ) N = Xn (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 (φ Un ψ) M = (flatten_sigma_2_list φ M) Un (flatten_sigma_2_list ψ M)"
| "flatten_sigma_2_list (φ Wn ψ) M = (flatten_sigma_2_list φ M) Un ((flatten_sigma_2_list ψ M) orn (Gn (flatten_pi_1_list φ M)))"
| "flatten_sigma_2_list (φ Mn ψ) M = (flatten_sigma_2_list φ M) Mn (flatten_sigma_2_list ψ M)"
| "flatten_sigma_2_list (φ Rn ψ) M = ((flatten_sigma_2_list φ M) orn (Gn (flatten_pi_1_list ψ M))) Mn (flatten_sigma_2_list ψ M)"
| "flatten_sigma_2_list (φ andn ψ) M = (flatten_sigma_2_list φ M) andn (flatten_sigma_2_list ψ M)"
| "flatten_sigma_2_list (φ orn ψ) M = (flatten_sigma_2_list φ M) orn (flatten_sigma_2_list ψ M)"
| "flatten_sigma_2_list (Xn φ) M = Xn (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 truen"

abbreviation "or_list  foldl Or_ltln falsen"

definition "normal_form_disjunct (φ :: String.literal ltln) M N 
   (flatten_sigma_2_list φ M)
      andn (and_list (map (λψ. Gn (Fn (flatten_sigma_1_list ψ N))) M) 
      andn (and_list (map (λψ. Fn (Gn (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 Gn (Fn ψ[N]Σ1)" and c3: "ψ  N. w n Fn (Gn ψ[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 Gn (Fn ψ[set ns]Σ1)" and c3: "ψ  set ns. w n Fn (Gn ψ[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