Theory WS1S_Alt_Formula

section ‹Concrete Atomic WS1S Formulas (Singleton Semantics for FO Variables)›

(*<*)
theory WS1S_Alt_Formula
imports
  Abstract_Formula
  WS1S_Prelim
begin
(*>*)

datatype (FOV0: 'fo, SOV0: 'so) atomic =
  Fo 'fo |
  Z 'fo |
  Less 'fo 'fo |
  In 'fo 'so

derive linorder atomic

type_synonym fo = nat
type_synonym so = nat
type_synonym ws1s = "(fo, so) atomic"
type_synonym formula = "(ws1s, order) aformula"

primrec wf0 where
  "wf0 idx (Fo m) = LESS FO m idx"
| "wf0 idx (Z m) = LESS FO m idx"
| "wf0 idx (Less m1 m2) = (LESS FO m1 idx ∧ LESS FO m2 idx)"
| "wf0 idx (In m M) = (LESS FO m idx ∧ LESS SO M idx)"

inductive lformula0 where
  "lformula0 (Fo m)"
| "lformula0 (Z m)"
| "lformula0 (Less m1 m2)"
| "lformula0 (In m M)"

code_pred lformula0 .

declare lformula0.intros[simp]

inductive_cases lformula0E[elim]: "lformula0 a"

abbreviation "FV0 ≡ case_order FOV0 SOV0"

fun find0 where
  "find0 FO i (Fo m) = (i = m)"
| "find0 FO i (Z m) = (i = m)"
| "find0 FO i (Less m1 m2) = (i = m1 ∨ i = m2)"
| "find0 FO i (In m _) = (i = m)"
| "find0 SO i (In _ M) = (i = M)"
| "find0 _ _ _ = False"

abbreviation "decr0 ord k ≡ map_atomic (case_order (dec k) id ord) (case_order id (dec k) ord)"

primrec satisfies0 where
  "satisfies0 𝔄 (Fo m) = (∃x. m⇗𝔄⇖FO = {|x|})"
| "satisfies0 𝔄 (Z m) = (m⇗𝔄⇖FO = {||})"
| "satisfies0 𝔄 (Less m1 m2) =
   (let P1 = m1⇗𝔄⇖FO; P2 = m2⇗𝔄⇖FO in if ¬(∃x. P1 = {|x|}) ∨ ¬(∃x. P2 = {|x|})
   then False
   else fthe_elem P1 < fthe_elem P2)"
| "satisfies0 𝔄 (In m M) =
   (let P = m⇗𝔄⇖FO in if ¬(∃x. P = {|x|}) then False else fMin P |∈| M⇗𝔄⇖SO)"

fun lderiv0 where
  "lderiv0 (bs1, bs2) (Fo m) = (if bs1 ! m then FBase (Z m) else FBase (Fo m))"
| "lderiv0 (bs1, bs2) (Z m) = (if bs1 ! m then FBool False else FBase (Z m))"
| "lderiv0 (bs1, bs2) (Less m1 m2) = (case (bs1 ! m1, bs1 ! m2) of
    (False, False) ⇒ FBase (Less m1 m2)
  | (True, False) ⇒ FAnd (FBase (Z m1)) (FBase (Fo m2))
  | _ ⇒ FBool False)"
| "lderiv0 (bs1, bs2) (In m M) = (case (bs1 ! m, bs2 ! M) of
    (False, _) ⇒ FBase (In m M)
  | (True, True) ⇒ FBase (Z m)
  | _ ⇒ FBool False)"

primrec rev where
  "rev (Fo m) = Fo m"
| "rev (Z m) = Z m"
| "rev (Less m1 m2) = Less m2 m1"
| "rev (In m M) = In m M"

abbreviation "rderiv0 v ≡ map_aformula rev id o lderiv0 v o rev"

primrec nullable0 where
  "nullable0 (Fo m) = False"
| "nullable0 (Z m) = True"
| "nullable0 (Less m1 m2) = False"
| "nullable0 (In m M) = False"

lemma fimage_Suc_fsubset0[simp]: "Suc |`| A |⊆| {|0|} ⟷ A = {||}"
  by blast

lemma fsubset_singleton_iff: "A |⊆| {|x|} ⟷ A = {||} ∨ A = {|x|}"
  by blast

definition "restrict ord P = (case ord of FO ⇒ ∃x. P = {|x|} | SO ⇒ True)"
definition "Restrict ord i = (case ord of FO ⇒ FBase (Fo i) | SO ⇒ FBool True)"

declare [[goals_limit = 50]]


global_interpretation WS1S_Alt: Formula SUC LESS assigns nvars Extend CONS SNOC Length
  extend size_atom zero σ eval downshift upshift finsert cut len restrict Restrict
  lformula0 FV0 find0 wf0 decr0 satisfies0 nullable0 lderiv0 rderiv0 undefined
  defines norm = "Formula_Operations.norm find0 decr0"
  and nFOr = "Formula_Operations.nFOr :: formula ⇒ _"
  and nFAnd = "Formula_Operations.nFAnd :: formula ⇒ _"
  and nFNot = "Formula_Operations.nFNot find0 decr0 :: formula ⇒ _"
  and nFEx = "Formula_Operations.nFEx find0 decr0"
  and nFAll = "Formula_Operations.nFAll find0 decr0"
  and decr = "Formula_Operations.decr decr0 :: _ ⇒ _ ⇒ formula ⇒ _"
  and find = "Formula_Operations.find find0 :: _ ⇒ _ ⇒ formula ⇒ _"
  and FV = "Formula_Operations.FV FV0"
  and RESTR = "Formula_Operations.RESTR Restrict :: _ ⇒ formula"
  and RESTRICT = "Formula_Operations.RESTRICT Restrict FV0"
  and deriv = "λd0 (a :: atom) (φ :: formula). Formula_Operations.deriv extend d0 a φ"
  and nullable = "λφ :: formula. Formula_Operations.nullable nullable0 φ"
  and fut_default = "Formula.fut_default extend zero rderiv0"
  and fut = "Formula.fut extend zero find0 decr0 rderiv0"
  and finalize = "Formula.finalize SUC extend zero find0 decr0 rderiv0"
  and final = "Formula.final SUC extend zero find0 decr0
     nullable0 rderiv0 :: idx ⇒ formula ⇒ _"
  and ws1s_wf = "Formula_Operations.wf SUC (wf0 :: idx ⇒ ws1s ⇒ _)"
  and ws1s_lformula = "Formula_Operations.lformula lformula0 :: formula ⇒ _"
  and check_eqv = "λidx. DAs.check_eqv
    (σ idx) (λφ. norm (RESTRICT φ) :: (ws1s, order) aformula)
    (λa φ. norm (deriv (lderiv0 :: _ ⇒ _ ⇒ formula) (a :: atom) φ))
    (final idx) (λφ :: formula. ws1s_wf idx φ ∧ ws1s_lformula φ)
    (σ idx) (λφ. norm (RESTRICT φ) :: (ws1s, order) aformula)
    (λa φ. norm (deriv (lderiv0 :: _ ⇒ _ ⇒ formula) (a :: atom) φ))
    (final idx) (λφ :: formula. ws1s_wf idx φ ∧ ws1s_lformula φ) (=)"
  and bounded_check_eqv = "λidx. DAs.check_eqv
    (σ idx) (λφ. norm (RESTRICT φ) :: (ws1s, order) aformula)
    (λa φ. norm (deriv (lderiv0 :: _ ⇒ _ ⇒ formula) (a :: atom) φ))
    nullable (λφ :: formula. ws1s_wf idx φ ∧ ws1s_lformula φ)
    (σ idx) (λφ. norm (RESTRICT φ) :: (ws1s, order) aformula)
    (λa φ. norm (deriv (lderiv0 :: _ ⇒ _ ⇒ formula) (a :: atom) φ))
    nullable (λφ :: formula. ws1s_wf idx φ ∧ ws1s_lformula φ) (=)"
  and automaton = "DA.automaton
    (λa φ. norm (deriv lderiv0 (a :: atom) φ :: formula))"
proof
  fix k idx and a :: ws1s and l assume "wf0 (SUC k idx) a" "LESS k l (SUC k idx)" "¬ find0 k l a"
  then show "wf0 idx (decr0 k l a)"
    by (induct a) (unfold wf0.simps atomic.map find0.simps,
     (transfer, force simp: dec_def split: if_splits order.splits)+) ― ‹slow›
next
  fix k and a :: ws1s and l assume "lformula0 a"
  then show "lformula0 (decr0 k l a)" by (induct a) auto
next
  fix i k and a :: ws1s and 𝔄 :: interp and P assume *: "¬ find0 k i a" "LESS k i (SUC k (#V 𝔄))"
    and disj: "lformula0 a ∨ len P ≤ Length 𝔄"
  from disj show "satisfies0 (Extend k i 𝔄 P) a = satisfies0 𝔄 (decr0 k i a)"
  proof
    assume "lformula0 a"
    then show ?thesis using *
      by (induct a)
        (auto simp: dec_def split: if_splits order.split option.splits bool.splits) ― ‹slow›
  next
    assume "len P ≤ Length 𝔄"
    with * show ?thesis
    proof (induct a)
      case Fo then show ?case by (cases k) (auto simp: dec_def)
    next
      case Z then show ?case by (cases k) (auto simp: dec_def)
    next
      case Less then show ?case by (cases k) (auto simp: dec_def)
    next
      case In then show ?case by (cases k) (auto simp: dec_def)
    qed
  qed
next
  fix idx and a :: ws1s and x assume "lformula0 a" "wf0 idx a"
  then show "Formula_Operations.wf SUC wf0 idx (lderiv0 x a)"
    by (induct a rule: lderiv0.induct)
      (auto simp: Formula_Operations.wf.simps Let_def split: bool.splits order.splits)
next
  fix a :: ws1s and x assume "lformula0 a"
  then show "Formula_Operations.lformula lformula0 (lderiv0 x a)"
    by (induct a rule: lderiv0.induct)
      (auto simp: Formula_Operations.lformula.simps split: bool.splits)
next
  fix idx and a :: ws1s and x assume "wf0 idx a"
  then show "Formula_Operations.wf SUC wf0 idx (rderiv0 x a)"
    by (induct a rule: lderiv0.induct)
      (auto simp: Formula_Operations.wf.simps Let_def sorted_append
        split: bool.splits order.splits nat.splits)
next
  fix 𝔄 :: interp and a :: ws1s
  assume "Length 𝔄 = 0"
  then show "nullable0 a = satisfies0 𝔄 a"
    by (induct a, unfold wf0.simps nullable0.simps satisfies0.simps Let_def)
      (transfer, (auto 0 3 dest: MSB_greater split: prod.splits if_splits option.splits bool.splits nat.splits) [])+  ― ‹slow›
next
   note Formula_Operations.satisfies_gen.simps[simp] Let_def[simp] upshift_def[simp]
   fix x :: atom and a :: ws1s and 𝔄 :: interp
   assume "lformula0 a" "wf0 (#V 𝔄) a" "#V 𝔄 = size_atom x"
   then show "Formula_Operations.satisfies Extend Length satisfies0 𝔄 (lderiv0 x a) =
     satisfies0 (CONS x 𝔄) a"
   proof (induct a)
   qed (auto split: prod.splits bool.splits)
next
   note Formula_Operations.satisfies_gen.simps[simp] Let_def[simp] upshift_def[simp]
   fix x :: atom and a :: ws1s and 𝔄 :: interp
   assume "lformula0 a" "wf0 (#V 𝔄) a" "#V 𝔄 = size_atom x"
   then show "Formula_Operations.satisfies_bounded Extend Length len satisfies0 𝔄 (lderiv0 x a) =
     satisfies0 (CONS x 𝔄) a"
     by (induct a) (auto split: prod.splits bool.splits)
next
   note Formula_Operations.satisfies_gen.simps[simp] Let_def[simp]
   fix x :: atom and a :: ws1s and 𝔄 :: interp
   assume "wf0 (#V 𝔄) a" "#V 𝔄 = size_atom x"
   then show "Formula_Operations.satisfies_bounded Extend Length len satisfies0 𝔄 (rderiv0 x a) =
     satisfies0 (SNOC x 𝔄) a"
   proof (induct a)
     case Less then show ?case
       apply (auto 2 0 split: prod.splits option.splits bool.splits)
       apply (auto simp add: fsubset_singleton_iff)
       apply (metis assigns_less_Length finsertCI less_not_sym)
       apply force
       apply (metis assigns_less_Length finsertCI less_not_sym)
       apply force
       done
   next
     case In then show ?case by (force split: prod.splits)
   qed (auto split: prod.splits)
next
   fix a :: ws1s and 𝔄 𝔅 :: interp
   assume "wf0 (#V 𝔅) a" "#V 𝔄 = #V 𝔅" "(⋀m k. LESS k m (#V 𝔅) ⟹ m⇗𝔄⇖k = m⇗𝔅⇖k)" "lformula0 a"
   then show "satisfies0 𝔄 a ⟷ satisfies0 𝔅 a" by (induct a) auto
next
   fix a :: ws1s
   assume "lformula0 a"
   moreover
   define d where "d = Formula_Operations.deriv extend lderiv0"
   define Φ :: "_ ⇒ (ws1s, order) aformula set"
     where "Φ a =
       (case a of
         Fo m ⇒ {FBase (Fo m), FBase (Z m), FBool False}
       | Z m ⇒ {FBase (Z m), FBool False}
       | Less m1 m2 ⇒ {FBase (Less m1 m2),
          FAnd (FBase (Z m1)) (FBase (Fo m2)),
          FAnd (FBase (Z m1)) (FBase (Z m2)),
          FAnd (FBase (Z m1)) (FBool False),
          FAnd (FBool False) (FBase (Fo m2)),
          FAnd (FBool False) (FBase (Z m2)),
          FAnd (FBool False) (FBool False),
         FBool False}
       | In i I ⇒ {FBase (In i I),  FBase (Z i), FBool False})" for a
   { fix xs
     note Formula_Operations.fold_deriv_FBool[simp] Formula_Operations.deriv.simps[simp] Φ_def[simp]
     from ‹lformula0 a› have "FBase a ∈ Φ a" by (cases a) auto
     moreover have "⋀x φ. φ ∈ Φ a ⟹ d x φ ∈ Φ a"
       by (auto simp: d_def split: atomic.splits list.splits bool.splits if_splits option.splits)
     then have "⋀φ. φ ∈ Φ a ⟹ fold d xs φ ∈ Φ a" by (induct xs) auto
     ultimately have "fold d xs (FBase a) ∈ Φ a" by blast
   }
   moreover have "finite (Φ a)" using ‹lformula0 a› unfolding Φ_def by (auto split: atomic.splits)
   ultimately show "finite {fold d xs (FBase a) | xs. True}" by (blast intro: finite_subset)
next
   fix a :: ws1s
   define d where "d = Formula_Operations.deriv extend rderiv0"
   define Φ :: "_ ⇒ (ws1s, order) aformula set"
     where "Φ a =
       (case a of
         Fo m ⇒ {FBase (Fo m), FBase (Z m), FBool False}
       | Z m ⇒ {FBase (Z m), FBool False}
       | Less m1 m2 ⇒ {FBase (Less m1 m2),
          FAnd (FBase (Z m2)) (FBase (Fo m1)) ,
          FAnd (FBase (Z m2)) (FBase (Z m1)),
          FAnd (FBase (Z m2)) (FBool False),
          FAnd (FBool False) (FBase (Fo m1)),
          FAnd (FBool False) (FBase (Z m1)),
          FAnd (FBool False) (FBool False),
         FBool False}
       | In i I ⇒ {FBase (In i I),  FBase (Z i), FBool False})" for a
   { fix xs
     note Formula_Operations.fold_deriv_FBool[simp] Formula_Operations.deriv.simps[simp] Φ_def[simp]
     then have "FBase a ∈ Φ a" by (auto split: atomic.splits option.splits)
     moreover have "⋀x φ. φ ∈ Φ a ⟹ d x φ ∈ Φ a"
       by (auto simp add: d_def Let_def not_le gr0_conv_Suc
         split: atomic.splits list.splits bool.splits if_splits option.splits nat.splits)
     then have "⋀φ. φ ∈ Φ a ⟹ fold d xs φ ∈ Φ a"
       by (induct xs) auto
     ultimately have "fold d xs (FBase a) ∈ Φ a" by blast
   }
   moreover have "finite (Φ a)" unfolding Φ_def using [[simproc add: finite_Collect]]
     by (auto split: atomic.splits)
   ultimately show "finite {fold d xs (FBase a) | xs. True}" by (blast intro: finite_subset)
next
  fix k l and a :: ws1s
  show "find0 k l a ⟷ l ∈ FV0 k a" by (induct a rule: find0.induct) auto
next
  fix a :: ws1s and k :: order
  show "finite (FV0 k a)" by (cases k) (induct a, auto)+
next
  fix idx a k v
  assume "wf0 idx a" "v ∈ FV0 k a"
  then show "LESS k v idx" by (cases k) (induct a, auto)+
next
  fix idx k i
  assume "LESS k i idx"
  then show "Formula_Operations.wf SUC wf0 idx (Restrict k i)"
     unfolding Restrict_def by (cases k) (auto simp: Formula_Operations.wf.simps)
next
  fix k and i :: nat
  show "Formula_Operations.lformula lformula0 (Restrict k i)"
    unfolding Restrict_def by (cases k) (auto simp: Formula_Operations.lformula.simps)
next
  fix i 𝔄 k P r
  assume "i⇗𝔄⇖k = P"
  then show "restrict k P ⟷
    Formula_Operations.satisfies_gen Extend Length satisfies0 r 𝔄 (Restrict k i)"
    unfolding restrict_def Restrict_def
    by (cases k) (auto simp: Formula_Operations.satisfies_gen.simps)
qed (auto simp: Extend_commute_unsafe downshift_def upshift_def fimage_iff Suc_le_eq len_def
  dec_def eval_def cut_def len_downshift_helper CONS_inj dest!: CONS_surj
  dest: fMax_ge fMax_ffilter_less fMax_boundedD fsubset_fsingletonD
  split: order.splits if_splits)

(*Workaround for code generation*)
lemma check_eqv_code[code]: "check_eqv idx r s =
  ((ws1s_wf idx r ∧ ws1s_lformula r) ∧ (ws1s_wf idx s ∧ ws1s_lformula s) ∧
  (case rtrancl_while (λ(p, q). final idx p = final idx q)
    (λ(p, q). map (λa. (norm (deriv lderiv0 a p), norm (deriv lderiv0 a q))) (σ idx))
    (norm (RESTRICT r), norm (RESTRICT s)) of
    None ⇒ False
  | Some ([], x) ⇒ True
  | Some (a # list, x) ⇒ False))"
  unfolding check_eqv_def WS1S_Alt.check_eqv_def WS1S_Alt.step_alt ..

definition while where [code del, code_abbrev]: "while idx φ = while_default (fut_default idx φ)"
declare while_default_code[of "fut_default idx φ" for idx φ, folded while_def, code]

lemma check_eqv_sound: 
  "⟦#V 𝔄 = idx; check_eqv idx φ ψ⟧ ⟹ (WS1S_Alt.sat 𝔄 φ ⟷ WS1S_Alt.sat 𝔄 ψ)"
  unfolding check_eqv_def by (rule WS1S_Alt.check_eqv_soundness)

lemma bounded_check_eqv_sound:
  "⟦#V 𝔄 = idx; bounded_check_eqv idx φ ψ⟧ ⟹ (WS1S_Alt.satb 𝔄 φ ⟷ WS1S_Alt.satb 𝔄 ψ)"
  unfolding bounded_check_eqv_def by (rule WS1S_Alt.bounded_check_eqv_soundness)

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: formula "int list" integer idx
          "nat × nat" "nat option" "bool option"} 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