# Theory LTL_Impl

theory LTL_Impl
imports LTL_FGXU Boolean_Expression_Checkers_AList_Mapping
```(*
Author:      Salomon Sickert
*)

section ‹LTL Code Equations›

theory LTL_Impl
imports Main
"../LTL_FGXU"
Boolean_Expression_Checkers.Boolean_Expression_Checkers
Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping
begin

subsection ‹Subformulae›

fun G_list :: "'a ltl ⇒'a ltl list"
where
"G_list (φ and ψ) = List.union (G_list φ) (G_list ψ)"
| "G_list (φ or ψ) = List.union (G_list φ) (G_list ψ)"
| "G_list (F φ) = G_list φ"
| "G_list (G φ) = List.insert (G φ) (G_list φ)"
| "G_list (X φ) = G_list φ"
| "G_list (φ U ψ) = List.union (G_list φ) (G_list ψ)"
| "G_list φ = []"

lemma G_eq_G_list:
"❙G φ = set (G_list φ)"
by (induction φ) auto

lemma G_list_distinct:
"distinct (G_list φ)"
by (induction φ) auto

subsection ‹Propositional Equivalence›

fun ifex_of_ltl :: "'a ltl ⇒ 'a ltl ifex"
where
"ifex_of_ltl true = Trueif"
| "ifex_of_ltl false = Falseif"
| "ifex_of_ltl (φ and ψ) = normif Mapping.empty (ifex_of_ltl φ) (ifex_of_ltl ψ) Falseif"
| "ifex_of_ltl (φ or ψ) = 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 = (⊨⇩P) {x. s x} 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)"
by (unfold reduced_bdt_checkers_def; insert val_ifex reduced_ifex; blast)

lemma [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 [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

subsection ‹Remove Constants›

fun remove_constants⇩P :: "'a ltl ⇒ 'a ltl"
where
"remove_constants⇩P (φ and ψ) = (
case (remove_constants⇩P φ) of
false ⇒ false
| true ⇒ remove_constants⇩P ψ
| φ' ⇒ (case remove_constants⇩P ψ of
false ⇒ false
| true ⇒ φ'
| ψ' ⇒ φ' and ψ'))"
| "remove_constants⇩P (φ or ψ) = (
case (remove_constants⇩P φ) of
true ⇒ true
| false ⇒ remove_constants⇩P ψ
| φ' ⇒ (case remove_constants⇩P ψ of
true ⇒ true
| false ⇒ φ'
| ψ' ⇒ φ' or ψ'))"
| "remove_constants⇩P φ = φ"

lemma remove_constants_correct:
"S ⊨⇩P φ ⟷ S ⊨⇩P remove_constants⇩P φ"
by (induction φ arbitrary: S) (auto split: ltl.split)

subsection ‹And/Or Constructors›

fun in_and
where
"in_and x (y and z) = (in_and x y ∨ in_and x z)"
| "in_and x y = (x = y)"

fun in_or
where
"in_or x (y or z) = (in_or x y ∨ in_or x z)"
| "in_or x y = (x = y)"

lemma in_entailment:
"in_and x y ⟹ S ⊨⇩P y ⟹ S ⊨⇩P x"
"in_or x y ⟹ S ⊨⇩P x ⟹ S ⊨⇩P y"
by (induction y) auto

definition mk_and
where
"mk_and f x y = (case f x of false ⇒ false | true ⇒ f y
| x' ⇒ (case f y of false ⇒ false | true ⇒ x'
| y' ⇒ if in_and x' y' then y' else if in_and y' x' then x' else x' and y'))"

definition mk_and'
where
"mk_and' x y ≡ case y of false ⇒ false | true ⇒ x | _ ⇒ x and y"

definition mk_or
where
"mk_or f x y = (case f x of true ⇒ true | false ⇒ f y
| x' ⇒ (case f y of true ⇒ true | false ⇒ x'
| y' ⇒ if in_or x' y' then y' else if in_or y' x' then x' else x' or y'))"

definition mk_or'
where
"mk_or' x y ≡ case y of true ⇒ true | false ⇒ x | _ ⇒ x or y"

lemma mk_and_correct:
"S ⊨⇩P mk_and f x y ⟷ S ⊨⇩P f x and f y"
proof -
have X: "⋀x' y'. S ⊨⇩P (if in_and x' y' then y' else if in_and y' x' then x' else x' and y')
⟷ S ⊨⇩P x' and y'"
using in_entailment by auto
show ?thesis
unfolding mk_and_def ltl.split X by (cases "f x"; cases "f y"; simp)
qed

lemma mk_and'_correct:
"S ⊨⇩P mk_and' x y ⟷ S ⊨⇩P x and y"
unfolding mk_and'_def by (cases y; simp)

lemma mk_or_correct:
"S ⊨⇩P mk_or f x y ⟷ S ⊨⇩P f x or f y"
proof -
have X: "⋀x' y'. S ⊨⇩P (if in_or x' y' then y' else if in_or y' x' then x' else x' or y')
⟷ S ⊨⇩P x' or y'"
using in_entailment by auto
show ?thesis
unfolding mk_or_def ltl.split X by (cases "f x"; cases "f y"; simp)
qed

lemma mk_or'_correct:
"S ⊨⇩P mk_or' x y ⟷ S ⊨⇩P x or y"
unfolding mk_or'_def by (cases y; simp)

end
```