# Theory Code_Equations

theory Code_Equations
imports Equivalence_Relations Boolean_Expression_Checkers_AList_Mapping
```(*
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
```