Theory BoolProgs_LTL_Conv

theory BoolProgs_LTL_Conv
imports
  BoolProgs_Extras
  "HOL-Library.Mapping"
  LTL.LTL
begin

fun b2l :: "bexp ⇒ nat ltlc" where
  "b2l TT = true⇩c"
| "b2l FF = false⇩c"
| "b2l (bexp.V v) = prop⇩c(v)"
| "b2l (bexp.Not e) = not⇩c (b2l e)"
| "b2l (And e1 e2) = b2l e1 and⇩c b2l e2"
| "b2l (Or e1 e2) = b2l e1 or⇩c b2l e2"

datatype
  propc = CProp String.literal | FProp "String.literal * integer"

fun ltl_conv :: "const_map ⇒ fun_map ⇒ propc ltlc ⇒ (nat ltlc + String.literal)"
where
  "ltl_conv _ _ True_ltlc = Inl True_ltlc"
| "ltl_conv _ _ False_ltlc = Inl False_ltlc"
| "ltl_conv C _ (Prop_ltlc (CProp s)) = (case Mapping.lookup C s of
                                              Some c ⇒ Inl (b2l c)
                                             | None ⇒ Inr (STR ''Unknown constant: '' + s))"
| "ltl_conv _ M (Prop_ltlc (FProp (s, argm))) = (case Mapping.lookup M s of
                                                    Some f ⇒ (Inl ∘ b2l ∘ f ∘ nat_of_integer) argm
                                                  | None ⇒ Inr (STR ''Unknown function: '' + s))"
| "ltl_conv C M (Not_ltlc x) = (case ltl_conv C M x of Inl l ⇒ Inl (Not_ltlc l) | Inr s ⇒ Inr s)"
| "ltl_conv C M (Next_ltlc x) = (case ltl_conv C M x of Inl l ⇒ Inl (Next_ltlc l) | Inr s ⇒ Inr s)"
| "ltl_conv C M (Final_ltlc x) = (case ltl_conv C M x of Inl l ⇒ Inl (Final_ltlc l) | Inr s ⇒ Inr s)"
| "ltl_conv C M (Global_ltlc x) = (case ltl_conv C M x of Inl l ⇒ Inl (Global_ltlc l) | Inr s ⇒ Inr s)"
| "ltl_conv C M (And_ltlc x y) = (case ltl_conv C M x of 
                                    Inr s ⇒ Inr s
                                  | Inl l ⇒ (case ltl_conv C M y of Inl r ⇒ Inl (And_ltlc l r) | Inr s ⇒ Inr s))"
| "ltl_conv C M (Or_ltlc x y) = (case ltl_conv C M x of 
                                    Inr s ⇒ Inr s
                                  | Inl l ⇒ (case ltl_conv C M y of Inl r ⇒ Inl (Or_ltlc l r) | Inr s ⇒ Inr s))"
| "ltl_conv C M (Implies_ltlc x y) = (case ltl_conv C M x of 
                                    Inr s ⇒ Inr s
                                  | Inl l ⇒ (case ltl_conv C M y of Inl r ⇒ Inl (Implies_ltlc l r) | Inr s ⇒ Inr s))"
| "ltl_conv C M (Until_ltlc x y) = (case ltl_conv C M x of 
                                    Inr s ⇒ Inr s
                                  | Inl l ⇒ (case ltl_conv C M y of Inl r ⇒ Inl (Until_ltlc l r) | Inr s ⇒ Inr s))"
| "ltl_conv C M (Release_ltlc x y) = (case ltl_conv C M x of 
                                    Inr s ⇒ Inr s
                                  | Inl l ⇒ (case ltl_conv C M y of Inl r ⇒ Inl (Release_ltlc l r) | Inr s ⇒ Inr s))"

end