Theory WS1S_Nameful

section ‹Nameful WS1S Formulas›

(*<*)
theory WS1S_Nameful
imports WS1S_Formula
begin
(*>*)

declare [[coercion "of_char :: char ⇒ nat", coercion_enabled]]

definition is_upper :: "char ⇒ bool" where [simp]: "is_upper c = (c ∈ {65..90 :: nat})"
definition is_lower :: "char ⇒ bool" where [simp]: "is_lower c = (c ∈ {97..122 :: nat})"

(*nonempty string starting with lower case*)
typedef fo = "{s. s ≠ [] ∧ is_lower (hd s)}" by (auto intro!: exI[of _ "''x''"])
(*nonempty string starting with upper case*)
typedef so = "{s. s ≠ [] ∧ is_upper (hd s)}" by (auto intro!: exI[of _ "''X''"])

datatype ws1s =
    T | F | Or ws1s ws1s | And ws1s ws1s | Not ws1s
  | Ex1 fo ws1s | Ex2 so ws1s | All1 fo ws1s | All2 so ws1s
  | Lt fo fo
  | In fo so
  | Eq_Const fo nat
  | Eq_Presb so nat
  | Eq_FO fo fo
  | Eq_FO_Offset fo fo nat
  | Eq_SO so so
  | Eq_SO_Inc so so
  | Eq_Max fo so
  | Eq_Min fo so
  | Empty so
  | Singleton so
  | Subset so so
  | Disjoint so so
  | Eq_Union so so so
  | Eq_Inter so so so
  | Eq_Diff so so so

(*standard WS1S semantics, finiteness captured by the type fset*)
primrec satisfies :: "(fo ⇒ nat) ⇒ (so ⇒ nat fset) ⇒ ws1s ⇒ bool" where
  "satisfies I1 I2 T = True"
| "satisfies I1 I2 F = False"
| "satisfies I1 I2 (Or φ ψ) = (satisfies I1 I2 φ ∨ satisfies I1 I2 ψ)"
| "satisfies I1 I2 (And φ ψ) = (satisfies I1 I2 φ ∧ satisfies I1 I2 ψ)"
| "satisfies I1 I2 (Not φ) = (¬ satisfies I1 I2 φ)"
| "satisfies I1 I2 (Ex1 x φ) = (∃n. satisfies (I1(x := n)) I2 φ)"
| "satisfies I1 I2 (Ex2 X φ) = (∃N. satisfies I1 (I2(X := N)) φ)"
| "satisfies I1 I2 (All1 x φ) = (∀n. satisfies (I1(x := n)) I2 φ)"
| "satisfies I1 I2 (All2 X φ) = (∀N. satisfies I1 (I2(X := N)) φ)"

| "satisfies I1 I2 (Lt x y) = (I1 x < I1 y)"
| "satisfies I1 I2 (In x X) = (I1 x |∈| I2 X)"
| "satisfies I1 I2 (Eq_Const x n) = (I1 x = n)"
| "satisfies I1 I2 (Eq_Presb X n) = ((∑x ∈ fset (I2 X). 2 ^ x) = n)"
| "satisfies I1 I2 (Eq_FO x y) = (I1 x = I1 y)"
| "satisfies I1 I2 (Eq_FO_Offset x y n) = (I1 x = I1 y + n)"
| "satisfies I1 I2 (Eq_SO X Y) = (I2 X = I2 Y)"
| "satisfies I1 I2 (Eq_SO_Inc X Y) = (I2 X = Suc |`| I2 Y)"
| "satisfies I1 I2 (Eq_Max x X) = (let Z = I2 X in Z ≠ {||} ∧ I1 x = fMax Z)"
| "satisfies I1 I2 (Eq_Min x X) = (let Z = I2 X in Z ≠ {||} ∧ I1 x = fMin Z)"
| "satisfies I1 I2 (Empty X) = (I2 X = {||})"
| "satisfies I1 I2 (Singleton X) = (∃x. I2 X = {|x|})"
| "satisfies I1 I2 (Subset X Y) = (I2 X |⊆| I2 Y)"
| "satisfies I1 I2 (Disjoint X Y) = (I2 X |∩| I2 Y = {||})"
| "satisfies I1 I2 (Eq_Union X Y Z) = (I2 X = I2 Y |∪| I2 Z)"
| "satisfies I1 I2 (Eq_Inter X Y Z) = (I2 X = I2 Y |∩| I2 Z)"
| "satisfies I1 I2 (Eq_Diff X Y Z) = (I2 X = I2 Y |-| I2 Z)"

primrec fos where
  "fos T = []"
| "fos F = []"
| "fos (Or φ ψ) = List.union (fos φ) (fos ψ)"
| "fos (And φ ψ) = List.union (fos φ) (fos ψ)"
| "fos (Not φ) = fos φ"
| "fos (Ex1 x φ) = List.remove1 x (fos φ)"
| "fos (Ex2 X φ) = fos φ"
| "fos (All1 x φ) = List.remove1 x (fos φ)"
| "fos (All2 X φ) = fos φ"
| "fos (Lt x y) = remdups [x, y]"
| "fos (In x X) = [x]"
| "fos (Eq_Const x n) = [x]"
| "fos (Eq_Presb X n) = []"
| "fos (Eq_FO x y) = remdups [x, y]"
| "fos (Eq_FO_Offset x y n) = remdups [x, y]"
| "fos (Eq_SO X Y) = []"
| "fos (Eq_SO_Inc X Y) = []"
| "fos (Eq_Max x X) = [x]"
| "fos (Eq_Min x X) = [x]"
| "fos (Empty X) = []"
| "fos (Singleton X) = []"
| "fos (Subset X Y) = []"
| "fos (Disjoint X Y) = []"
| "fos (Eq_Union X Y Z) = []"
| "fos (Eq_Inter X Y Z) = []"
| "fos (Eq_Diff X Y Z) = []"

primrec sos where
  "sos T = []"
| "sos F = []"
| "sos (Or φ ψ) = List.union (sos φ) (sos ψ)"
| "sos (And φ ψ) = List.union (sos φ) (sos ψ)"
| "sos (Not φ) = sos φ"
| "sos (Ex1 x φ) = sos φ"
| "sos (Ex2 X φ) = List.remove1 X (sos φ)"
| "sos (All1 x φ) = sos φ"
| "sos (All2 X φ) = List.remove1 X (sos φ)"
| "sos (Lt x y) = []"
| "sos (In x X) = [X]"
| "sos (Eq_Const x n) = []"
| "sos (Eq_Presb X n) = [X]"
| "sos (Eq_FO x y) = []"
| "sos (Eq_FO_Offset x y n) = []"
| "sos (Eq_SO X Y) = remdups [X, Y]"
| "sos (Eq_SO_Inc X Y) = remdups [X, Y]"
| "sos (Eq_Max x X) = [X]"
| "sos (Eq_Min x X) = [X]"
| "sos (Empty X) = [X]"
| "sos (Singleton X) = [X]"
| "sos (Subset X Y) = remdups [X, Y]"
| "sos (Disjoint X Y) = remdups [X, Y]"
| "sos (Eq_Union X Y Z) = remdups [X, Y, Z]"
| "sos (Eq_Inter X Y Z) = remdups [X, Y, Z]"
| "sos (Eq_Diff X Y Z) = remdups [X, Y, Z]"

lemma distinct_fos[simp]: "distinct (fos φ)" by (induct φ) auto
lemma distinct_sos[simp]: "distinct (sos φ)" by (induct φ) auto

primrec ε where
  "ε bs1 bs2 T = FBool True"
| "ε bs1 bs2 F = FBool False"
| "ε bs1 bs2 (Or φ ψ) = FOr (ε bs1 bs2 φ) (ε bs1 bs2 ψ)"
| "ε bs1 bs2 (And φ ψ) = FAnd (ε bs1 bs2 φ) (ε bs1 bs2 ψ)"
| "ε bs1 bs2 (Not φ) = FNot (ε bs1 bs2 φ)"
| "ε bs1 bs2 (Ex1 x φ) = FEx FO (ε (x # bs1) bs2 φ)"
| "ε bs1 bs2 (Ex2 X φ) = FEx SO (ε bs1 (X # bs2) φ)"
| "ε bs1 bs2 (All1 x φ) = FAll FO (ε (x # bs1) bs2 φ)"
| "ε bs1 bs2 (All2 X φ) = FAll SO (ε bs1 (X # bs2) φ)"
| "ε bs1 bs2 (Lt x y) = FBase (Less None (index bs1 x) (index bs1 y))"
| "ε bs1 bs2 (In x X) = FBase (WS1S_Formula.In False (index bs1 x) (index bs2 X))"
| "ε bs1 bs2 (Eq_Const x n) = FBase (WS1S_Formula.Eq_Const None (index bs1 x) n)"
| "ε bs1 bs2 (Eq_Presb X n) = FBase (WS1S_Formula.Eq_Presb None (index bs2 X) n)"
| "ε bs1 bs2 (Eq_FO x y) = FBase (WS1S_Formula.Eq_FO False (index bs1 x) (index bs1 y))"
| "ε bs1 bs2 (Eq_FO_Offset x y n) = FBase (WS1S_Formula.Plus_FO None (index bs1 x) (index bs1 y) n)"
| "ε bs1 bs2 (Eq_SO X Y) = FBase (WS1S_Formula.Eq_SO (index bs2 X) (index bs2 Y))"
| "ε bs1 bs2 (Eq_SO_Inc X Y) = FBase (WS1S_Formula.Suc_SO False False (index bs2 X) (index bs2 Y))"
| "ε bs1 bs2 (Eq_Max x X) = FBase (WS1S_Formula.Eq_Max False (index bs1 x) (index bs2 X))"
| "ε bs1 bs2 (Eq_Min x X) = FBase (WS1S_Formula.Eq_Min False (index bs1 x) (index bs2 X))"
| "ε bs1 bs2 (Empty X) = FBase (WS1S_Formula.Empty (index bs2 X))"
| "ε bs1 bs2 (Singleton X) = FBase (WS1S_Formula.Singleton (index bs2 X))"
| "ε bs1 bs2 (Subset X Y) = FBase (WS1S_Formula.Subset (index bs2 X) (index bs2 Y))"
| "ε bs1 bs2 (Disjoint X Y) = FBase (WS1S_Formula.Disjoint (index bs2 X) (index bs2 Y))"
| "ε bs1 bs2 (Eq_Union X Y Z) = FBase (WS1S_Formula.Eq_Union (index bs2 X) (index bs2 Y) (index bs2 Z))"
| "ε bs1 bs2 (Eq_Inter X Y Z) = FBase (WS1S_Formula.Eq_Inter (index bs2 X) (index bs2 Y) (index bs2 Z))"
| "ε bs1 bs2 (Eq_Diff X Y Z) = FBase (WS1S_Formula.Eq_Diff(index bs2 X) (index bs2 Y) (index bs2 Z))"

lift_definition mk_I ::
  "(fo ⇒ nat) ⇒ (so ⇒ nat fset) ⇒ fo list ⇒ so list ⇒ interp" is
  "λI1 I2 fs ss. let I1s = map (λx. {|I1 x|}) fs; I2s = map I2 ss in (MSB (I1s @ I2s), I1s, I2s)"
  by (auto simp: Let_def)

definition dec_I1 :: "interp ⇒ fo list ⇒ fo ⇒ nat" where "dec_I1 𝔄 fs x = fMin (index fs x⇗𝔄⇖FO)"
definition dec_I2 :: "interp ⇒ so list ⇒ so ⇒ nat fset" where "dec_I2 𝔄 ss X = index ss X⇗𝔄⇖SO"

lemma nvars_mk_I[simp]: "#V (mk_I I1 I2 fs ss) = Abs_idx (length fs, length ss)"
  by transfer (auto simp: Let_def)

lemma assigns_mk_I_FO[simp]:
  "m⇗mk_I I1 I2 bs1 bs2⇖FO = (if m < length bs1 then {|I1 (bs1 ! m)|} else {||})"
  by transfer (auto simp: Let_def)

lemma assigns_mk_I_SO[simp]:
  "m⇗mk_I I1 I2 bs1 bs2⇖SO = (if m < length bs2 then I2 (bs2 ! m) else {||})"
  by transfer (auto simp: Let_def)

lemma satisfies_cong:
  "⟦∀x ∈ set (fos φ). I1 x = J1 x; ∀X ∈ set (sos φ). I2 X = J2 X⟧ ⟹
  satisfies I1 I2 φ ⟷ satisfies J1 J2 φ"
proof (induct φ arbitrary: I1 I2 J1 J2)
  case (Or φ ψ) from Or.hyps[of I1 J1 I2 J2] Or.prems show ?case by auto
next
  case (And φ ψ) from And.hyps[of I1 J1 I2 J2] And.prems show ?case by auto
next
  case (Ex1 x φ) with Ex1.hyps[of "I1(x := y)" "J1(x := y)" I2 J2 for y, cong] show ?case by auto
next
  case (Ex2 X φ) with Ex2.hyps[of I1 J1 "I2(X := Y)" "J2(X := Y)" for Y, cong] show ?case by auto
next
  case (All1 x φ) with All1.hyps[of "I1(x := y)" "J1(x := y)" I2 J2 for y, cong] show ?case by auto
next
  case (All2 X φ) with All2.hyps[of I1 J1 "I2(X := Y)" "J2(X := Y)" for Y, cong] show ?case by auto
qed simp_all

lemma dec_I_mk_I_satisfies_cong:
  "⟦set (fos φ) ⊆ set bs1; set (sos φ) ⊆ set bs2; 𝔄 = mk_I I1 I2 bs1 bs2⟧ ⟹
  satisfies (dec_I1 𝔄 bs1) (dec_I2 𝔄 bs2) φ ⟷ satisfies I1 I2 φ"
  by (rule satisfies_cong) (auto simp: dec_I1_def dec_I2_def)

definition "ok_I 𝔄 fs = (∀x ∈ set fs. index fs x⇗𝔄⇖FO ≠ {||})"

lemma ok_I_mk_I[simp]: "ok_I (mk_I I1 I2 bs1 bs2) bs1"
  unfolding ok_I_def by transfer (auto simp: Let_def)

lemma in_FV_εD[dest]: "⟦v ∈ FV (ε bs1 bs2 φ) FO;
  set (fos φ) ⊆ set bs1; set (sos φ) ⊆ set bs2⟧ ⟹
  (∃y ∈ set bs1. v = index bs1 y)"
proof (induct φ arbitrary: bs1 bs2 v)
  case (Ex1 x φ) from Ex1.hyps[of "Suc v" "x # bs1" bs2] Ex1.prems show ?case
    by (auto simp: Diff_subset_conv split: if_splits)
next
  case (Ex2 X φ) from Ex2.hyps[of v bs1 "X # bs2"] Ex2.prems show ?case
    by (auto simp: Diff_subset_conv split: if_splits)
next
  case (All1 x φ) from All1.hyps[of "Suc v" "x # bs1" bs2] All1.prems show ?case
    by (auto simp: Diff_subset_conv split: if_splits)
next
  case (All2 X φ) from All2.hyps[of v bs1 "X # bs2"] All2.prems show ?case
    by (auto simp: Diff_subset_conv split: if_splits)
qed (auto split: if_splits)

lemma dec_I1_Extend_FO[simp]:
  "dec_I1 (Extend FO 0 𝔄 P) (x # bs1) = (dec_I1 𝔄 bs1)(x := fMin P)"
  by (auto simp: dec_I1_def)

lemma dec_I1_Extend_SO[simp]: "dec_I1 (Extend SO i 𝔄 P) bs1 = dec_I1 𝔄 bs1"
  by (auto simp: dec_I1_def)

lemma dec_I2_Extend_FO[simp]: "dec_I2 (Extend FO i 𝔄 P) bs2 = dec_I2 𝔄 bs2"
  by (auto simp: dec_I2_def)

lemma dec_I2_Extend_SO[simp]:
  "dec_I2 (Extend SO 0 𝔄 P) (X # bs2) = (dec_I2 𝔄 bs2)(X := P)"
  by (auto simp: dec_I2_def fun_eq_iff)

lemma sat_ε: "⟦set (fos φ) ⊆ set bs1; set (sos φ) ⊆ set bs2; ok_I 𝔄 bs1⟧ ⟹
  WS1S.sat 𝔄 (ε bs1 bs2 φ) ⟷
  satisfies (dec_I1 𝔄 bs1) (dec_I2 𝔄 bs2) φ"
proof (induct φ arbitrary: 𝔄 bs1 bs2)
  case (Or φ ψ) from Or.hyps[of bs1 bs2 𝔄] Or.prems show ?case
    unfolding WS1S.sat_def
    by (auto simp: restrict_def ok_I_def split: order.splits)
next
  case (And φ ψ) from And.hyps[of bs1 bs2 𝔄] And.prems show ?case
    unfolding WS1S.sat_def
    by (auto simp: restrict_def ok_I_def split: order.splits)
next
  case (Not φ) from Not.hyps[of bs1 bs2 𝔄] Not.prems show ?case
    unfolding WS1S.sat_def
    by (auto simp: restrict_def ok_I_def split: order.splits)
next
  case (Ex1 x φ)
  { fix P :: "nat fset" assume "P ≠ {||}"
    with Ex1.prems have "WS1S.sat (Extend FO 0 𝔄 P) (ε (x # bs1) bs2 φ) ⟷
      satisfies (dec_I1 (Extend FO 0 𝔄 P) (x # bs1)) (dec_I2 (Extend FO 0 𝔄 P) bs2) φ"
      by (intro Ex1.hyps) (auto simp: ok_I_def)
  } note IH = this
  show ?case
  proof
    assume "WS1S.sat 𝔄 (ε bs1 bs2 (Ex1 x φ))"
    then obtain P where "P ≠ {||}" "WS1S.sat (Extend FO 0 𝔄 P) (ε (x # bs1) bs2 φ)"
      unfolding WS1S.sat_def by (auto simp: restrict_def split: order.splits)
    then have "satisfies (dec_I1 (Extend FO 0 𝔄 P) (x # bs1)) (dec_I2 (Extend FO 0 𝔄 P) bs2) φ"
      by (auto simp: IH)
    then show "satisfies (dec_I1 𝔄 bs1) (dec_I2 𝔄 bs2) (Ex1 x φ)" by auto
  next
    assume "satisfies (dec_I1 𝔄 bs1) (dec_I2 𝔄 bs2) (Ex1 x φ)"
    then obtain n where "satisfies (dec_I1 (Extend FO 0 𝔄 {|n|}) (x # bs1))
      (dec_I2 (Extend FO 0 𝔄 {|n|}) bs2) φ" by auto
    then have "WS1S.sat (Extend FO 0 𝔄 {|n|}) (ε (x # bs1) bs2 φ)"
      by (auto simp: IH)
    then show "WS1S.sat 𝔄 (ε bs1 bs2 (Ex1 x φ))" unfolding WS1S.sat_def
      by (auto simp: restrict_def split: order.splits)
  qed
next
  case (Ex2 X φ)
  { fix P :: "nat fset"
    from Ex2.prems have "WS1S.sat (Extend SO 0 𝔄 P) (ε bs1 (X # bs2) φ) ⟷
      satisfies (dec_I1 (Extend SO 0 𝔄 P) bs1) (dec_I2 (Extend SO 0 𝔄 P) (X # bs2)) φ"
      by (intro Ex2.hyps) (auto simp: ok_I_def)
  } note IH = this
  show ?case
  proof -
    have "WS1S.sat 𝔄 (ε bs1 bs2 (Ex2 X φ)) ⟷
      (∃P. WS1S.sat (Extend SO 0 𝔄 P) (ε bs1 (X # bs2) φ))"
      unfolding WS1S.sat_def by (auto simp: restrict_def split: order.splits)
    also have "… ⟷ (∃P. satisfies (dec_I1 (Extend SO 0 𝔄 P) bs1)
      (dec_I2 (Extend SO 0 𝔄 P) (X # bs2)) φ)" by (auto simp: IH)
    also have "… ⟷ satisfies (dec_I1 𝔄 bs1) (dec_I2 𝔄 bs2) (Ex2 X φ)" by simp
    finally show ?thesis .
  qed
next
  case (All1 x φ)
  { fix P :: "nat fset" assume "P ≠ {||}"
    with All1.prems have "WS1S.sat (Extend FO 0 𝔄 P) (ε (x # bs1) bs2 φ) ⟷
      satisfies (dec_I1 (Extend FO 0 𝔄 P) (x # bs1)) (dec_I2 (Extend FO 0 𝔄 P) bs2) φ"
      by (intro All1.hyps) (auto simp: ok_I_def)
  } note IH = this
  show ?case
  proof
    assume L: "WS1S.sat 𝔄 (ε bs1 bs2 (All1 x φ))"
    { fix n :: "nat"
      from L have "WS1S.sat (Extend FO 0 𝔄 {|n|}) (ε (x # bs1) bs2 φ)"
        unfolding WS1S.sat_def by (auto simp: restrict_def split: order.splits)
      then have "satisfies (dec_I1 (Extend FO 0 𝔄 {|n|}) (x # bs1))
        (dec_I2 (Extend FO 0 𝔄 {|n|}) bs2) φ" by (auto simp: IH)
    }
    then show "satisfies (dec_I1 𝔄 bs1) (dec_I2 𝔄 bs2) (All1 x φ)" by simp
  next
    assume R: "satisfies (dec_I1 𝔄 bs1) (dec_I2 𝔄 bs2) (All1 x φ)"
    { fix P :: "nat fset" assume "P ≠ {||}"
      with R have "satisfies (dec_I1 (Extend FO 0 𝔄 P) (x # bs1))
        (dec_I2 (Extend FO 0 𝔄 P) bs2) φ" by auto
      with ‹P ≠ {||}› have "WS1S.sat (Extend FO 0 𝔄 P) (ε (x # bs1) bs2 φ)"
        by (auto simp: IH)
    }
    with All1.prems in_FV_εD[of _ "x # bs1" bs2 φ]
      show "WS1S.sat 𝔄 (ε bs1 bs2 (All1 x φ))" unfolding WS1S.sat_def
      by (auto 0 3 simp: restrict_def ok_I_def split: if_splits order.splits)
  qed
next
  case (All2 X φ)
  { fix P :: "nat fset"
    from All2.prems have "WS1S.sat (Extend SO 0 𝔄 P) (ε bs1 (X # bs2) φ) ⟷
      satisfies (dec_I1 (Extend SO 0 𝔄 P) bs1) (dec_I2 (Extend SO 0 𝔄 P) (X # bs2)) φ"
      by (intro All2.hyps) (auto simp: ok_I_def)
  } note IH = this
  show ?case
  proof -
    have "WS1S.sat 𝔄 (ε bs1 bs2 (All2 X φ)) ⟷
      (∀P. WS1S.sat (Extend SO 0 𝔄 P) (ε bs1 (X # bs2) φ))"
      unfolding WS1S.sat_def by (auto simp: restrict_def split: order.splits)
    also have "… ⟷ (∀P. satisfies (dec_I1 (Extend SO 0 𝔄 P) bs1)
      (dec_I2 (Extend SO 0 𝔄 P) (X # bs2)) φ)" by (auto simp: IH)
    also have "… ⟷ satisfies (dec_I1 𝔄 bs1) (dec_I2 𝔄 bs2) (All2 X φ)" by simp
    finally show ?thesis .
  qed
qed (auto simp: WS1S.sat_def Let_def dec_I1_def dec_I2_def ok_I_def
  restrict_def split: if_splits order.splits)

definition "eqv φ ψ =
  (let fs = List.union (fos φ) (fos ψ); ss = List.union (sos φ) (sos ψ)
  in check_eqv (Abs_idx (length fs, length ss)) (ε fs ss φ) (ε fs ss ψ))"

lemma eqv_sound: "eqv φ ψ ⟹ satisfies I1 I2 φ ⟷ satisfies I1 I2 ψ"
  unfolding eqv_def Let_def
  by (drule check_eqv_sound[rotated, of _ _ _
    "mk_I I1 I2 (List.union (fos φ) (fos ψ)) (List.union (sos φ) (sos ψ))"])
    (auto simp: sat_ε dec_I_mk_I_satisfies_cong)

definition "Thm φ = eqv φ T"

lemma "Thm Φ ⟹ satisfies I1 I2 Φ"
  unfolding Thm_def by (drule eqv_sound[of _ _ I1 I2]) simp

setup_lifting type_definition_fo
setup_lifting type_definition_so

instantiation fo :: equal
begin
  lift_definition equal_fo :: "fo ⇒ fo ⇒ bool" is "(=)" .
  instance by (standard, transfer) simp
end

instantiation so :: equal
begin
  lift_definition equal_so :: "so ⇒ so ⇒ bool" is "(=)" .
  instance by (standard, transfer) simp
end

(*<*)
end
(*>*)