Theory af_Impl

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹af - Unfolding Functions - Optimized Code Equations›

theory af_Impl
  imports Main "../af" LTL_Impl
begin

text ‹Provide optimized code definitions for @{term "↑af"} and other functions, which use heuristics to reduce the formula size›

subsection ‹Helper Function›

fun remove_and_or
where
  "remove_and_or (z or y) = (case z of 
      (((z' and x') or y') and x) ⇒ if x = x' ∧ y = y' then ((z' and x') or y') else remove_and_or z or remove_and_or y 
     | _ ⇒ remove_and_or z or remove_and_or y)"
| "remove_and_or (x and y) = remove_and_or x and remove_and_or y"
| "remove_and_or x = x"

lemma remove_and_or_correct: 
  "S ⊨⇩P remove_and_or x ⟷ S ⊨⇩P x"
proof (induction x)
  case (LTLOr x y)
    thus ?case 
    proof (induction x) 
      case (LTLAnd x' y')
        thus ?case
          proof (induction x')
            case (LTLOr x'' y'')
              thus ?case
                by (induction x'') auto
          qed auto
    qed auto
qed auto

subsection ‹Optimized Equations›

fun af_letter_simp
where
  "af_letter_simp true ν = true"
| "af_letter_simp false ν = false"
| "af_letter_simp p(a) ν = (if a ∈ ν then true else false)"
| "af_letter_simp (np(a)) ν  = (if a ∉ ν then true else false)"
| "af_letter_simp (φ and ψ) ν = (case φ of
      true ⇒ af_letter_simp ψ ν
    | false ⇒ false
    | p(a) ⇒ if a ∈ ν then af_letter_simp ψ ν else false
    | np(a) ⇒ if a ∉ ν then af_letter_simp ψ ν else false
    | G φ' ⇒  
      (let 
        φ'' = af_letter_simp φ' ν; 
        ψ'' = af_letter_simp ψ ν 
       in
        (if φ'' = ψ'' then mk_and' (G φ') φ'' else mk_and id (mk_and' (G φ') φ'') ψ''))
    | _ ⇒ mk_and id (af_letter_simp φ ν) (af_letter_simp ψ ν))"
| "af_letter_simp (φ or ψ) ν = (case φ of
      true ⇒ true
    | false ⇒ af_letter_simp ψ ν
    | p(a) ⇒ if a ∈ ν then true else af_letter_simp ψ ν
    | np(a) ⇒ if a ∉ ν then true else af_letter_simp ψ ν
    | F φ' ⇒  
      (let 
        φ'' = af_letter_simp φ' ν; 
        ψ'' = af_letter_simp ψ ν 
       in
        (if φ'' = ψ'' then mk_or' (F φ') φ'' else mk_or id (mk_or' (F φ') φ'') ψ''))
    | _ ⇒ mk_or id (af_letter_simp φ ν) (af_letter_simp ψ ν))"
| "af_letter_simp (X φ) ν = φ"
| "af_letter_simp (G φ) ν = mk_and' (G φ) (af_letter_simp φ ν)"
| "af_letter_simp (F φ) ν = mk_or' (F φ) (af_letter_simp φ ν)"
| "af_letter_simp (φ U ψ) ν = mk_or' (mk_and' (φ U ψ) (af_letter_simp φ ν)) (af_letter_simp ψ ν)"

lemma af_letter_simp_correct:
  "S ⊨⇩P af_letter φ ν ⟷ S ⊨⇩P af_letter_simp φ ν"
proof (induction φ)
  case (LTLAnd φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_and_correct mk_and'_correct)
next
  case (LTLOr φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_or_correct mk_or'_correct)
qed (simp_all add: mk_and_correct mk_and'_correct mk_or_correct mk_or'_correct)

fun af_G_letter_simp
where
  "af_G_letter_simp true ν = true"
| "af_G_letter_simp false ν = false"
| "af_G_letter_simp p(a) ν = (if a ∈ ν then true else false)"
| "af_G_letter_simp (np(a)) ν  = (if a ∉ ν then true else false)"
| "af_G_letter_simp (φ and ψ) ν = (case φ of
      true ⇒ af_G_letter_simp ψ ν
    | false ⇒ false
    | p(a) ⇒ if a ∈ ν then af_G_letter_simp ψ ν else false
    | np(a) ⇒ if a ∉ ν then af_G_letter_simp ψ ν else false
    | _ ⇒ mk_and id (af_G_letter_simp φ ν) (af_G_letter_simp ψ ν))"
| "af_G_letter_simp (φ or ψ) ν = (case φ of
      true ⇒ true
    | false ⇒ af_G_letter_simp ψ ν
    | p(a) ⇒ if a ∈ ν then true else af_G_letter_simp ψ ν
    | np(a) ⇒ if a ∉ ν then true else af_G_letter_simp ψ ν
    | F φ' ⇒  
      (let 
        φ'' = af_G_letter_simp φ' ν; 
        ψ'' = af_G_letter_simp ψ ν 
       in
        (if φ'' = ψ'' then mk_or' (F φ') φ'' else mk_or id (mk_or' (F φ') φ'') ψ''))
    | _ ⇒ mk_or id (af_G_letter_simp φ ν) (af_G_letter_simp ψ ν))"
| "af_G_letter_simp (X φ) ν = φ"
| "af_G_letter_simp (G φ) ν = G φ"
| "af_G_letter_simp (F φ) ν = mk_or' (F φ) (af_G_letter_simp φ ν)"
| "af_G_letter_simp (φ U ψ) ν = mk_or' (mk_and' (φ U ψ) (af_G_letter_simp φ ν)) (af_G_letter_simp ψ ν)"

lemma af_G_letter_simp_correct:
  "S ⊨⇩P af_G_letter φ ν ⟷ S ⊨⇩P af_G_letter_simp φ ν"
proof (induction φ)
  case (LTLAnd φ ψ)
    thus ?case
      by (cases φ) (auto simp add: mk_and_correct)
next
  case (LTLOr φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_or_correct mk_or'_correct)
qed (simp_all add: mk_and_correct mk_and'_correct mk_or_correct mk_or'_correct)

fun step_simp
where
  "step_simp p(a) ν = (if a ∈ ν then true else false)"
| "step_simp (np(a)) ν  = (if a ∉ ν then true else false)"
| "step_simp (φ and ψ) ν = (mk_and id (step_simp φ ν) (step_simp ψ ν))"
| "step_simp (φ or ψ) ν = (mk_or id (step_simp φ ν) (step_simp ψ ν))"
| "step_simp (X φ) ν = remove_constants⇩P φ"
| "step_simp φ ν = φ"

lemma step_simp_correct:
  "S ⊨⇩P step φ ν ⟷ S ⊨⇩P step_simp φ ν"
proof (induction φ)
  case (LTLAnd φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_and_correct mk_and'_correct) 
next
  case (LTLOr φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_or_correct mk_or'_correct)
qed (simp_all add: mk_and_correct mk_and'_correct mk_or_correct mk_or'_correct remove_constants_correct[symmetric]) 

fun Unf_simp
where
  "Unf_simp (φ and ψ) = (case φ of
      true ⇒ Unf_simp ψ
    | false ⇒ false
    | G φ' ⇒  
      (let 
        φ'' = Unf_simp φ'; ψ'' = Unf_simp ψ
       in
        (if φ'' = ψ'' then mk_and' (G φ') φ'' else mk_and id (mk_and' (G φ') φ'') ψ''))
    | _ ⇒ mk_and id (Unf_simp φ) (Unf_simp ψ))"
| "Unf_simp (φ or ψ) = (case φ of
      true ⇒ true
    | false ⇒ Unf_simp ψ
    | F φ' ⇒  
      (let 
        φ'' = Unf_simp φ'; ψ'' = Unf_simp ψ
       in
        (if φ'' = ψ'' then mk_or' (F φ') φ'' else mk_or id (mk_or' (F φ') φ'') ψ''))
    | _ ⇒ mk_or id (Unf_simp φ) (Unf_simp ψ))"
| "Unf_simp (G φ) = mk_and' (G φ) (Unf_simp φ)"
| "Unf_simp (F φ) = mk_or' (F φ) (Unf_simp φ)"
| "Unf_simp (φ U ψ) = mk_or' (mk_and' (φ U ψ) (Unf_simp φ)) (Unf_simp ψ)"
| "Unf_simp φ = φ"

lemma Unf_simp_correct:
  "S ⊨⇩P Unf φ ⟷ S ⊨⇩P Unf_simp φ"
proof (induction φ)
  case (LTLAnd φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_and_correct mk_and'_correct)
next
  case (LTLOr φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_or_correct mk_or'_correct)
qed (simp_all add: mk_and_correct mk_and'_correct mk_or_correct mk_or'_correct)

fun Unf⇩G_simp
where
  "Unf⇩G_simp (φ and ψ) = mk_and id (Unf⇩G_simp φ) (Unf⇩G_simp ψ)"
| "Unf⇩G_simp (φ or ψ) = (case φ of
      true ⇒ true
    | false ⇒ Unf⇩G_simp ψ
    | F φ' ⇒  
      (let 
        φ'' = Unf⇩G_simp φ'; ψ'' = Unf⇩G_simp ψ
       in
        (if φ'' = ψ'' then mk_or' (F φ') φ'' else mk_or id (mk_or' (F φ') φ'') ψ''))
    | _ ⇒ mk_or id (Unf⇩G_simp φ) (Unf⇩G_simp ψ))"
| "Unf⇩G_simp (F φ) = mk_or' (F φ) (Unf⇩G_simp φ)"
| "Unf⇩G_simp (φ U ψ) = mk_or' (mk_and' (φ U ψ) (Unf⇩G_simp φ)) (Unf⇩G_simp ψ)"
| "Unf⇩G_simp φ = φ"

lemma Unf⇩G_simp_correct:
  "S ⊨⇩P Unf⇩G φ ⟷ S ⊨⇩P Unf⇩G_simp φ"
proof (induction φ)
  case (LTLAnd φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_and_correct mk_and'_correct)
next
  case (LTLOr φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_or_correct mk_or'_correct)
qed (simp_all add: mk_and_correct mk_and'_correct mk_or_correct mk_or'_correct)

fun af_letter_opt_simp
where
  "af_letter_opt_simp true ν = true"
| "af_letter_opt_simp false ν = false"
| "af_letter_opt_simp p(a) ν = (if a ∈ ν then true else false)"
| "af_letter_opt_simp (np(a)) ν  = (if a ∉ ν then true else false)"
| "af_letter_opt_simp (φ and ψ) ν = (case φ of
      true ⇒ af_letter_opt_simp ψ ν
    | false ⇒ false
    | p(a) ⇒ if a ∈ ν then af_letter_opt_simp ψ ν else false
    | np(a) ⇒ if a ∉ ν then af_letter_opt_simp ψ ν else false
    | G φ' ⇒  
      (let 
        φ'' = Unf_simp φ'; 
        ψ'' = af_letter_opt_simp ψ ν 
       in
        (if φ'' = ψ'' then mk_and' (G φ') φ'' else mk_and id (mk_and' (G φ') φ'') ψ''))
    | _ ⇒ mk_and id (af_letter_opt_simp φ ν) (af_letter_opt_simp ψ ν))"
| "af_letter_opt_simp (φ or ψ) ν = (case φ of
      true ⇒ true
    | false ⇒ af_letter_opt_simp ψ ν
    | p(a) ⇒ if a ∈ ν then true else af_letter_opt_simp ψ ν
    | np(a) ⇒ if a ∉ ν then true else af_letter_opt_simp ψ ν
    | F φ' ⇒  
      (let 
        φ'' = Unf_simp φ'; 
        ψ'' = af_letter_opt_simp ψ ν 
       in
        (if φ'' = ψ'' then mk_or' (F φ') φ'' else mk_or id (mk_or' (F φ') φ'') ψ''))
    | _ ⇒ mk_or id (af_letter_opt_simp φ ν) (af_letter_opt_simp ψ ν))"
| "af_letter_opt_simp (X φ) ν = Unf_simp φ"
| "af_letter_opt_simp (G φ) ν = mk_and' (G φ) (Unf_simp φ)"
| "af_letter_opt_simp (F φ) ν = mk_or' (F φ) (Unf_simp φ)"
| "af_letter_opt_simp (φ U ψ) ν = mk_or' (mk_and' (φ U ψ) (Unf_simp φ)) (Unf_simp ψ)"

lemma af_letter_opt_simp_correct:
  "S ⊨⇩P af_letter_opt φ ν ⟷ S ⊨⇩P af_letter_opt_simp φ ν"
proof (induction φ)
  case (LTLAnd φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_and_correct mk_and'_correct) 
next
  case (LTLOr φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_or_correct mk_or'_correct)
qed (simp_all add: mk_and_correct mk_and'_correct mk_or_correct mk_or'_correct Unf_simp_correct) 

fun af_G_letter_opt_simp
where
  "af_G_letter_opt_simp true ν = true"
| "af_G_letter_opt_simp false ν = false"
| "af_G_letter_opt_simp p(a) ν = (if a ∈ ν then true else false)"
| "af_G_letter_opt_simp (np(a)) ν  = (if a ∉ ν then true else false)"
| "af_G_letter_opt_simp (φ and ψ) ν = (case φ of
      true ⇒ af_G_letter_opt_simp ψ ν
    | false ⇒ false
    | p(a) ⇒ if a ∈ ν then af_G_letter_opt_simp ψ ν else false
    | np(a) ⇒ if a ∉ ν then af_G_letter_opt_simp ψ ν else false
    | _ ⇒ mk_and id (af_G_letter_opt_simp φ ν) (af_G_letter_opt_simp ψ ν))"
| "af_G_letter_opt_simp (φ or ψ) ν = (case φ of
      true ⇒ true
    | false ⇒ af_G_letter_opt_simp ψ ν
    | p(a) ⇒ if a ∈ ν then true else af_G_letter_opt_simp ψ ν
    | np(a) ⇒ if a ∉ ν then true else af_G_letter_opt_simp ψ ν
    | F φ' ⇒  
      (let 
        φ'' = Unf⇩G_simp φ'; 
        ψ'' = af_G_letter_opt_simp ψ ν 
       in
        (if φ'' = ψ'' then mk_or' (F φ') φ'' else mk_or id (mk_or' (F φ') φ'') ψ''))
    | _ ⇒ mk_or id (af_G_letter_opt_simp φ ν) (af_G_letter_opt_simp ψ ν))"
| "af_G_letter_opt_simp (X φ) ν = Unf⇩G_simp φ"
| "af_G_letter_opt_simp (G φ) ν = G φ"
| "af_G_letter_opt_simp (F φ) ν = mk_or' (F φ) (Unf⇩G_simp φ)"
| "af_G_letter_opt_simp (φ U ψ) ν = mk_or' (mk_and' (φ U ψ) (Unf⇩G_simp φ)) (Unf⇩G_simp ψ)"

lemma af_G_letter_opt_simp_correct:
  "S ⊨⇩P af_G_letter_opt φ ν ⟷ S ⊨⇩P af_G_letter_opt_simp φ ν"
proof (induction φ)
  case (LTLAnd φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_and_correct mk_and'_correct) 
next
  case (LTLOr φ ψ)
    thus ?case
      by (cases φ) (auto simp add: Let_def mk_or_correct mk_or'_correct)
qed (simp_all add: mk_and_correct mk_and'_correct mk_or_correct mk_or'_correct Unf⇩G_simp_correct) 

subsection ‹Register Code Equations›
 
lemma [code]: 
  "↑af (Abs φ) ν = Abs (remove_and_or (af_letter_simp φ ν))"
  unfolding af_abs.f_abs.abs_eq af_letter_abs_def ltl_prop_equiv_quotient.abs_eq_iff ltl_prop_equiv_def
  using af_letter_simp_correct remove_and_or_correct by blast

lemma [code]:
  "↑af⇩G (Abs φ) ν = Abs (remove_and_or (af_G_letter_simp φ ν))"
  unfolding af_G_abs.f_abs.abs_eq af_G_letter_abs_def ltl_prop_equiv_quotient.abs_eq_iff ltl_prop_equiv_def
  using af_G_letter_simp_correct remove_and_or_correct by blast

lemma [code]: 
  "↑step (Abs φ) ν = Abs (step_simp φ ν)"
  unfolding step_abs.abs_eq ltl_prop_equiv_quotient.abs_eq_iff ltl_prop_equiv_def
  using step_simp_correct by blast

lemma [code]: 
  "↑Unf (Abs φ) = Abs (remove_and_or (Unf_simp φ))"
  unfolding Unf_abs.abs_eq ltl_prop_equiv_quotient.abs_eq_iff ltl_prop_equiv_def
  using Unf_simp_correct remove_and_or_correct by blast

lemma [code]: 
  "↑Unf⇩G (Abs φ) = Abs (remove_and_or (Unf⇩G_simp φ))"
  unfolding Unf⇩G_abs.abs_eq ltl_prop_equiv_quotient.abs_eq_iff ltl_prop_equiv_def
  using Unf⇩G_simp_correct remove_and_or_correct by blast

lemma [code]: 
  "↑af⇩𝔘 (Abs φ) ν = Abs (remove_and_or (af_letter_opt_simp φ ν))"
  unfolding af_abs_opt.f_abs.abs_eq af_letter_abs_opt_def ltl_prop_equiv_quotient.abs_eq_iff ltl_prop_equiv_def
  using af_letter_opt_simp_correct remove_and_or_correct by blast

lemma [code]:
  "↑af⇩G⇩𝔘 (Abs φ) ν = Abs (remove_and_or (af_G_letter_opt_simp φ ν))"
  unfolding af_G_abs_opt.f_abs.abs_eq af_G_letter_abs_opt_def ltl_prop_equiv_quotient.abs_eq_iff ltl_prop_equiv_def
  using af_G_letter_opt_simp_correct remove_and_or_correct by blast

end