Theory Code_Equations

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Code lemmas for abstract definitions›

theory Code_Equations
imports
  LTL Equivalence_Relations
  Boolean_Expression_Checkers.Boolean_Expression_Checkers
  Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping
begin

subsection ‹Propositional Equivalence›

fun ifex_of_ltl :: "'a ltln ⇒ 'a ltln ifex"
where
  "ifex_of_ltl true⇩n = Trueif"
| "ifex_of_ltl false⇩n = Falseif"
| "ifex_of_ltl (φ and⇩n ψ) = normif Mapping.empty (ifex_of_ltl φ) (ifex_of_ltl ψ) Falseif"
| "ifex_of_ltl (φ or⇩n ψ) = normif Mapping.empty (ifex_of_ltl φ) Trueif (ifex_of_ltl ψ)"
| "ifex_of_ltl φ = IF φ Trueif Falseif"

lemma val_ifex:
  "val_ifex (ifex_of_ltl b) s = {x. s x} ⊨⇩P b"
  by (induction b) (simp add: agree_Nil val_normif)+

lemma reduced_ifex:
  "reduced (ifex_of_ltl b) {}"
  by (induction b) (simp; metis keys_empty reduced_normif)+

lemma ifex_of_ltl_reduced_bdt_checker:
  "reduced_bdt_checkers ifex_of_ltl (λy s. {x. s x} ⊨⇩P y)"
  unfolding reduced_bdt_checkers_def
  using val_ifex reduced_ifex by blast

lemma ltl_prop_equiv_impl[code]:
  "(φ ∼⇩P ψ) = equiv_test ifex_of_ltl φ ψ"
  by (simp add: ltl_prop_equiv_def reduced_bdt_checkers.equiv_test[OF ifex_of_ltl_reduced_bdt_checker]; fastforce)

lemma ltl_prop_implies_impl[code]:
  "(φ ⟶⇩P ψ) = impl_test ifex_of_ltl φ ψ"
  by (simp add: ltl_prop_implies_def reduced_bdt_checkers.impl_test[OF ifex_of_ltl_reduced_bdt_checker]; force)

― ‹Check code export›
export_code "(∼⇩P)" "(⟶⇩P)" checking

end