Theory Preliminaries

theory Preliminaries
  imports MDL
begin

section ‹Formulas and Satisfiability›

declare [[typedef_overloaded]]

context
begin

qualified datatype ('a, 't :: timestamp) formula = Bool bool | Atom 'a | Neg "('a, 't) formula" |
  Bin "bool ⇒ bool ⇒ bool" "('a, 't) formula" "('a, 't) formula" |
  Prev "'t ℐ" "('a, 't) formula" | Next "'t ℐ" "('a, 't) formula" |
  Since "('a, 't) formula" "'t ℐ" "('a, 't) formula" |
  Until "('a, 't) formula" "'t ℐ" "('a, 't) formula" |
  MatchP "'t ℐ" "('a, 't) regex" | MatchF "'t ℐ" "('a, 't) regex"
  and ('a, 't) regex = Test "('a, 't) formula" | Wild |
  Plus "('a, 't) regex" "('a, 't) regex" | Times "('a, 't) regex" "('a, 't) regex" |
  Star "('a, 't) regex"

end

fun mdl2mdl :: "('a, 't :: timestamp) Preliminaries.formula ⇒ ('a, 't) formula"
  and embed :: "('a, 't) Preliminaries.regex ⇒ ('a, 't) regex" where
  "mdl2mdl (Preliminaries.Bool b) = Bool b"
| "mdl2mdl (Preliminaries.Atom a) = Atom a"
| "mdl2mdl (Preliminaries.Neg phi) = Neg (mdl2mdl phi)"
| "mdl2mdl (Preliminaries.Bin f phi psi) = Bin f (mdl2mdl phi) (mdl2mdl psi)"
| "mdl2mdl (Preliminaries.Prev I phi) = Prev I (mdl2mdl phi)"
| "mdl2mdl (Preliminaries.Next I phi) = Next I (mdl2mdl phi)"
| "mdl2mdl (Preliminaries.Since phi I psi) = Since (mdl2mdl phi) I (mdl2mdl psi)"
| "mdl2mdl (Preliminaries.Until phi I psi) = Until (mdl2mdl phi) I (mdl2mdl psi)"
| "mdl2mdl (Preliminaries.MatchP I r) = MatchP I (Times (embed r) (Symbol (Bool True)))"
| "mdl2mdl (Preliminaries.MatchF I r) = MatchF I (Times (embed r) (Symbol (Bool True)))"
| "embed (Preliminaries.Test phi) = Lookahead (mdl2mdl phi)"
| "embed Preliminaries.Wild = Symbol (Bool True)"
| "embed (Preliminaries.Plus r s) = Plus (embed r) (embed s)"
| "embed (Preliminaries.Times r s) = Times (embed r) (embed s)"
| "embed (Preliminaries.Star r) = Star (embed r)"

lemma mdl2mdl_wf:
  fixes phi :: "('a, 't :: timestamp) Preliminaries.formula"
  shows "wf_fmla (mdl2mdl phi)"
  by (induction phi rule: mdl2mdl_embed.induct(1)[where ?Q="λr. wf_regex (Times (embed r) (Symbol (Bool True))) ∧ (∀phi ∈ atms (embed r). wf_fmla phi)"]) auto

fun embed' :: "(('a, 't :: timestamp) formula ⇒ ('a, 't) Preliminaries.formula) ⇒ ('a, 't) regex ⇒ ('a, 't) Preliminaries.regex" where
  "embed' f (Lookahead phi) = Preliminaries.Test (f phi)"
| "embed' f (Symbol phi) = Preliminaries.Times (Preliminaries.Test (f phi)) Preliminaries.Wild"
| "embed' f (Plus r s) = Preliminaries.Plus (embed' f r) (embed' f s)"
| "embed' f (Times r s) = Preliminaries.Times (embed' f r) (embed' f s)"
| "embed' f (Star r) = Preliminaries.Star (embed' f r)"

lemma embed'_cong[fundef_cong]: "(⋀phi. phi ∈ atms r ⟹ f phi = f' phi) ⟹ embed' f r = embed' f' r"
  by (induction r) auto

fun mdl2mdl' :: "('a, 't :: timestamp) formula ⇒ ('a, 't) Preliminaries.formula" where
  "mdl2mdl' (Bool b) = Preliminaries.Bool b"
| "mdl2mdl' (Atom a) = Preliminaries.Atom a"
| "mdl2mdl' (Neg phi) = Preliminaries.Neg (mdl2mdl' phi)"
| "mdl2mdl' (Bin f phi psi) = Preliminaries.Bin f (mdl2mdl' phi) (mdl2mdl' psi)"
| "mdl2mdl' (Prev I phi) = Preliminaries.Prev I (mdl2mdl' phi)"
| "mdl2mdl' (Next I phi) = Preliminaries.Next I (mdl2mdl' phi)"
| "mdl2mdl' (Since phi I psi) = Preliminaries.Since (mdl2mdl' phi) I (mdl2mdl' psi)"
| "mdl2mdl' (Until phi I psi) = Preliminaries.Until (mdl2mdl' phi) I (mdl2mdl' psi)"
| "mdl2mdl' (MatchP I r) = Preliminaries.MatchP I (embed' mdl2mdl' (rderive r))"
| "mdl2mdl' (MatchF I r) = Preliminaries.MatchF I (embed' mdl2mdl' (rderive r))"

context MDL
begin

fun rvsat :: "('a, 't) Preliminaries.formula ⇒ nat ⇒ bool"
  and rvmatch :: "('a, 't) Preliminaries.regex ⇒ (nat × nat) set" where
  "rvsat (Preliminaries.Bool b) i = b"
| "rvsat (Preliminaries.Atom a) i = (a ∈ Γ σ i)"
| "rvsat (Preliminaries.Neg φ) i = (¬ rvsat φ i)"
| "rvsat (Preliminaries.Bin f φ ψ) i = (f (rvsat φ i) (rvsat ψ i))"
| "rvsat (Preliminaries.Prev I φ) i = (case i of 0 ⇒ False | Suc j ⇒ mem (τ σ j) (τ σ i) I ∧ rvsat φ j)"
| "rvsat (Preliminaries.Next I φ) i = (mem (τ σ i) (τ σ (Suc i)) I ∧ rvsat φ (Suc i))"
| "rvsat (Preliminaries.Since φ I ψ) i = (∃j≤i. mem (τ σ j) (τ σ i) I ∧ rvsat ψ j ∧ (∀k ∈ {j<..i}. rvsat φ k))"
| "rvsat (Preliminaries.Until φ I ψ) i = (∃j≥i. mem (τ σ i) (τ σ j) I ∧ rvsat ψ j ∧ (∀k ∈ {i..<j}. rvsat φ k))"
| "rvsat (Preliminaries.MatchP I r) i = (∃j≤i. mem (τ σ j) (τ σ i) I ∧ (j, i) ∈ rvmatch r)"
| "rvsat (Preliminaries.MatchF I r) i = (∃j≥i. mem (τ σ i) (τ σ j) I ∧ (i, j) ∈ rvmatch r)"
| "rvmatch (Preliminaries.Test φ) = {(i, i) | i. rvsat φ i}"
| "rvmatch Preliminaries.Wild = {(i, i + 1) | i. True}"
| "rvmatch (Preliminaries.Plus r s) = rvmatch r ∪ rvmatch s"
| "rvmatch (Preliminaries.Times r s) = rvmatch r O rvmatch s"
| "rvmatch (Preliminaries.Star r) = rtrancl (rvmatch r)"

lemma mdl2mdl_equivalent:
  fixes phi :: "('a, 't :: timestamp) Preliminaries.formula"
  shows "⋀i. sat (mdl2mdl phi) i ⟷ rvsat phi i"
  by (induction phi rule: mdl2mdl_embed.induct(1)[where ?Q="λr. match (embed r) = rvmatch r"]) (auto split: nat.splits)

lemma mdlstar2mdl:
  fixes phi :: "('a, 't :: timestamp) Preliminaries.formula"
  shows "wf_fmla (mdl2mdl phi)" "⋀i. sat (mdl2mdl phi) i ⟷ rvsat phi i"
  apply (rule mdl2mdl_wf)
  apply (rule mdl2mdl_equivalent)
  done

lemma rvmatch_embed':
  assumes "⋀phi i. phi ∈ atms r ⟹ rvsat (mdl2mdl' phi) i ⟷ sat phi i"
  shows "rvmatch (embed' mdl2mdl' r) = match r"
  using assms
  by (induction r) auto

lemma mdl2mdlstar:
  fixes phi :: "('a, 't :: timestamp) formula"
  assumes "wf_fmla phi"
  shows "⋀i. rvsat (mdl2mdl' phi) i ⟷ sat phi i"
  using assms
  apply (induction phi rule: mdl2mdl'.induct)
                apply (auto split: nat.splits)[8]
  subgoal for I r i
    by auto (metis atms_rderive match_rderive rvmatch_embed' wf_fmla.simps(1))+
  subgoal for I r i
    by auto (metis atms_rderive match_rderive rvmatch_embed' wf_fmla.simps(1))+
  done

end

end