Theory WS1S_Presburger_Equivalence

section ‹Comparing WS1S Formulas with Presburger Formulas›

(*<*)
theory WS1S_Presburger_Equivalence
imports Presburger_Formula WS1S_Formula
begin
(*>*)

lift_definition letter_eq :: "idx ⇒ nat ⇒ bool list × bool list ⇒ bool list ⇒ bool" is
  "λ(m1,m2) n (bs1, bs2) bs. m1 = 0 ∧ m2 = n ∧ bs1 = [] ∧ bs2 = bs" .

lemma letter_eq[dest]:
  "letter_eq idx n a b ⟹ (a ∈ set (WS1S_Prelim.σ idx)) = (b ∈ set (Presburger_Formula.σ n))"
  by transfer (force simp: Presburger_Formula.σ_def set_n_lists image_iff)

global_interpretation WS1S_Presb: DAs
  "WS1S_Prelim.σ idx"
  "(λφ. norm (RESTRICT φ) :: (ws1s, order) aformula)"
  "(λa φ. norm (deriv lderiv0 (a :: atom) φ))"
  "(WS1S.final idx)"
  "(λφ :: formula. ws1s_wf idx φ ∧ ws1s_lformula φ)"
  "λφ. Formula.lang WS1S_Prelim.nvars
     WS1S_Prelim.Extend WS1S_Prelim.CONS WS1S_Prelim.Length WS1S_Prelim.size_atom
     WS1S_Formula.satisfies0 idx φ"
  "(λφ :: formula. ws1s_wf idx φ ∧ ws1s_lformula φ)"
  "λφ. Formula.language WS1S_Prelim.assigns
     WS1S_Prelim.nvars WS1S_Prelim.Extend WS1S_Prelim.CONS
     WS1S_Prelim.Length WS1S_Prelim.size_atom restrict WS1S_Formula.FV0
     WS1S_Formula.satisfies0 idx φ"
  "(Presburger_Formula.σ n)"
  "(λφ. Presburger_Formula.norm (Presburger_Formula.RESTRICT φ))"
  "(λa φ. Presburger_Formula.norm (Presburger_Formula.deriv Presburger_Formula.lderiv0 a φ))"
  "(Presburger_Formula.final n)"
  "(λφ. presb_wf n φ ∧ presb_lformula φ)"
  "(λφ. Formula.lang Presburger_Formula.nvars
            Presburger_Formula.Extend Presburger_Formula.CONS Presburger_Formula.Length
            Presburger_Formula.size_atom (⊨0) n φ)"
  "(λφ. presb_wf n φ ∧ presb_lformula φ)"
  "(λφ. Formula.language Presburger_Formula.assigns
            Presburger_Formula.nvars Presburger_Formula.Extend Presburger_Formula.CONS
            Presburger_Formula.Length Presburger_Formula.size_atom (λ_ _. True)
            Presburger_Formula.FV0 (⊨0)
            n φ)"
  "letter_eq idx n"
  defines check_eqv = "λidx n. DAs.check_eqv
    (σ idx) (λφ. norm (RESTRICT φ) :: (ws1s, order) aformula)
    (λa φ. norm (deriv (lderiv0 :: _ ⇒ _ ⇒ formula) (a :: atom) φ))
    (final idx) (λφ :: formula. ws1s_wf idx φ ∧ ws1s_lformula φ)
    (Presburger_Formula.σ n) (λφ. Presburger_Formula.norm (Presburger_Formula.RESTRICT φ))
    (λa φ. Presburger_Formula.norm (Presburger_Formula.deriv Presburger_Formula.lderiv0 a φ))
    (Presburger_Formula.final n) (λφ. presb_wf n φ ∧ presb_lformula φ) (letter_eq idx n)"
  by unfold_locales auto

(*Workaround for code generation*)
lemma check_eqv_code[code]: "check_eqv idx n r s ⟷
  ((ws1s_wf idx r ∧ ws1s_lformula r) ∧ (presb_wf n s ∧ presb_lformula s) ∧
  (case rtrancl_while (λ(p, q). final idx p = Presburger_Formula.final n q)
  (λ(p, q).
    map (λ(a, b). (norm (deriv lderiv0 a p),
      Presburger_Formula.norm (Presburger_Formula.deriv Presburger_Formula.lderiv0 b q)))
     [(x, y)←List.product (σ idx) (Presburger_Formula.σ n). letter_eq idx n x y])
    (norm (RESTRICT r), Presburger_Formula.norm (Presburger_Formula.RESTRICT s)) of
    None ⇒ False
  | Some ([], x) ⇒ True
  | Some (a # list, x) ⇒ False))"
  unfolding check_eqv_def WS1S_Presb.check_eqv_def ..

method_setup check_equiv = ‹
  let
    fun tac ctxt =
      let
        val conv = @{computation_check terms: Trueprop
          "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" Suc
          "plus :: nat ⇒ _" "minus :: nat ⇒ _"
          "times :: nat ⇒ _" "divide :: nat ⇒ _" "modulo :: nat ⇒ _"
          "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
          check_eqv datatypes: idx "(presb, unit) aformula" "((nat, nat) atomic, WS1S_Prelim.order) aformula"
          "nat × nat" "nat option" "bool option" "int list" integer} ctxt
      in
        CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
        resolve_tac ctxt [TrueI]
      end
  in
    Scan.succeed (SIMPLE_METHOD' o tac)
  end
›

(*<*)
end
(*>*)