Theory LTL_Impl

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

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