Theory Presburger_Formula

section ‹Concrete Atomic Presburger Formulas›

(*<*)
theory Presburger_Formula
imports
  Abstract_Formula
  "HOL-Library.Code_Target_Int"
  "List-Index.List_Index"
begin
(*>*)

declare [[coercion "of_bool :: bool  nat"]]
declare [[coercion int]]
declare [[coercion_map map]]
declare [[coercion_enabled]]

fun len :: "nat  nat" where ― ‹FIXME yet another logarithm›
  "len 0 = 0"
| "len (Suc 0) = 1"
| "len n = Suc (len (n div 2))"

lemma len_eq0_iff: "len n = 0  n = 0"
  by (induct n rule: len.induct) auto

lemma len_mult2[simp]: "len (2 * x) = (if x = 0 then 0 else Suc (len x))"
proof (induct x rule: len.induct)
  show "len (2 * Suc 0) = (if Suc 0 = 0 then 0 else Suc (len (Suc 0)))" by (simp add: numeral_eq_Suc)
qed auto

lemma len_mult2'[simp]: "len (x * 2) = (if x = 0 then 0 else Suc (len x))"
  using len_mult2 [of x] by (simp add: ac_simps)

lemma len_Suc_mult2[simp]: "len (Suc (2 * x)) = Suc (len x)"
proof (induct x rule: len.induct)
  show "len (Suc (2 * Suc 0)) = Suc (len (Suc 0))"
    by (metis div_less One_nat_def div2_Suc_Suc len.simps(3) lessI mult.right_neutral numeral_2_eq_2)
qed auto

lemma len_le_iff: "len x  l  x < 2 ^ l"
proof (induct x arbitrary: l rule: len.induct)
  fix l show "(len (Suc 0)  l) = (Suc 0 < 2 ^ l)"
  proof (cases l)
    case Suc then show ?thesis using le_less by fastforce
  qed simp
next
  fix v l assume "l. (len (Suc (Suc v) div 2)  l) = (Suc (Suc v) div 2 < 2 ^ l)"
  then show "(len (Suc (Suc v))  l) = (Suc (Suc v) < 2 ^ l)"
    by (cases l) (simp_all, linarith)
qed simp

lemma len_pow2[simp]: "len (2 ^ x) = Suc x"
  by (induct x) auto

lemma len_div2[simp]: "len (x div 2) = len x - 1"
  by (induct x rule: len.induct) auto

lemma less_pow2_len[simp]: "x < 2 ^ len x"
  by (induct x rule: len.induct) auto

lemma len_alt: "len x = (LEAST i. x < 2 ^ i)"
proof (rule antisym)
  show "len x  (LEAST i. x < 2 ^ i)"
    unfolding len_le_iff by (rule LeastI) (rule less_pow2_len)
qed (auto intro: Least_le)

lemma len_mono[simp]: "x  y  len x  len y"
  unfolding len_le_iff using less_pow2_len[of y] by linarith

lemma len_div_pow2[simp]: "len (x div 2 ^ m) = len x - m"
  by (induct m arbitrary: x) (auto simp: div_mult2_eq)

lemma len_mult_pow2[simp]: "len (x * 2 ^ m) = (if x = 0 then 0 else len x + m)"
  by (induct m arbitrary: x) (auto simp: div_mult2_eq mult.assoc[symmetric] mult.commute[of _ 2])

lemma map_index'_Suc[simp]: "map_index' (Suc i) f xs = map_index' i (λi. f (Suc i)) xs"
  by (induct xs arbitrary: i) auto


abbreviation (input) "zero n  replicate n False"
abbreviation (input) "SUC  λ_::unit. Suc"
definition "test_bit m n  (m :: nat) div 2 ^ n mod 2 = 1"
lemma test_bit_eq_iff: test_bit = bit
  by (simp add: fun_eq_iff test_bit_def bit_iff_odd_drop_bit mod_2_eq_odd flip: drop_bit_eq_div)
definition "downshift m  (m :: nat) div 2"
definition "upshift m  (m :: nat) * 2"
lemma set_bit_def: "set_bit n m  m + (if ¬ test_bit m n then 2 ^ n else (0 :: nat))"
  apply (rule eq_reflection)
  apply (rule bit_eqI)
  apply (subst disjunctive_add)
   apply (auto simp add: bit_simps test_bit_eq_iff)
  done
definition "cut_bits n m  (m :: nat) mod 2 ^ n"

typedef interp = "{(n :: nat, xs :: nat list). x  set xs. len x  n}"
  by (force intro: exI[of _ "[]"])

setup_lifting type_definition_interp
type_synonym atom = "bool list"
type_synonym "value" = "nat"
datatype presb = Eq (tm: "int list") (const: int) (offset: "int")
derive linorder list
derive linorder presb
type_synonym formula = "(presb, unit) aformula"

lift_definition assigns :: "nat  interp  unit  value" ("___" [900, 999, 999] 999) is
  "λn (_, I) _. if n < length I then I ! n else 0" .

lift_definition nvars :: "interp  nat" ("#V _" [1000] 900) is
  "λ(_, I). length I" .

lift_definition Length :: "interp  nat" is "λ(n, _). n" .

lift_definition Extend :: "unit  nat  interp  value  interp" is
  "λ_ i (n, I) m. (max n (len m), insert_nth i m I)"
  by (force simp: max_def dest: in_set_takeD in_set_dropD)

lift_definition CONS :: "atom  interp  interp" is
  "λbs (n, I). (Suc n, map_index (λi n. 2 * n + (if bs ! i then 1 else 0)) I)"
  by (auto simp: set_zip)

lift_definition SNOC :: "atom  interp  interp" is
  "λbs (n, I). (Suc n, map_index (λi m. m + (if bs ! i then 2 ^ n else 0)) I)"
  by (auto simp: all_set_conv_all_nth len_le_iff)

definition extend :: "unit  bool  atom  atom" where
  "extend _ b bs  b # bs"

abbreviation (input) size_atom :: "atom  nat" where
  "size_atom  length"

definition FV0 :: "unit  presb  nat set" where
  "FV0 _ fm = (case fm of Eq is _ _  {n. n < length is  is!n  0})"

lemma FV0_code[code]:
  "FV0 x (Eq is i off) = Option.these (set (map_index (λi x. if x = 0 then None else Some i) is))"
  unfolding FV0_def by (force simp: Option.these_def image_iff)

primrec wf0 :: "nat  presb  bool" where
  "wf0 idx (Eq is _ _) = (length is = idx)"

fun find0 where
  "find0 (_::unit) n (Eq is _ _) = (is ! n  0)"

primrec decr0 where
  "decr0 (_::unit) k (Eq is i d) = Eq (take k is @ drop (Suc k) is) i d"

definition scalar_product :: "nat list  int list  int" where
  "scalar_product ns is =
     sum_list (map_index (λi b. (if i < length ns then ns ! i else 0) * b) is)"

lift_definition eval_tm :: "interp  int list  int" is
  "λ(_, I). scalar_product I" .

primrec satisfies0 where
  "satisfies0 I (Eq is i d) = (eval_tm I is = i - (2 ^ Length I) * d)"

inductive lformula0 where
  "lformula0 (Eq is i 0)"

code_pred lformula0 .

fun lderiv0 :: "bool list  presb  formula" where
  "lderiv0 bs (Eq is i d) = (if d  0 then undefined else
  (let v = i - scalar_product bs is
   in if v mod 2 = 0 then FBase (Eq is (v div 2) 0) else FBool False))"

fun rderiv0 :: "bool list  presb  formula" where
  "rderiv0 bs (Eq is i d) =
  (let
     l = - sum_list [i. i  is, i < 0];
     h = - sum_list [i. i  is, i > 0];
     d' = scalar_product bs is + 2 * d
   in if d'  {min h i .. max l i} then FBase (Eq is i d') else FBool False)"

primrec nullable0 where
  "nullable0 (Eq is i off) = (i = off)"

definition σ :: "nat  atom list" where
  "σ n = List.n_lists n [True, False]"

named_theorems Presb_simps

lemma nvars_Extend[Presb_simps]: "#V (Extend () i 𝔄 P) = Suc (#V 𝔄)"
  by (transfer, auto)

lemma Length_Extend[Presb_simps]: "Length (Extend () i 𝔄 P) = max (Length 𝔄) (len P)"
  by (transfer, auto)

lemma Length0_inj[Presb_simps]: "Length 𝔄 = 0  Length 𝔅 = 0  #V 𝔄 = #V 𝔅  𝔄 = 𝔅"
  by transfer (auto intro: nth_equalityI simp: all_set_conv_all_nth len_eq0_iff)

lemma ex_Length0[Presb_simps]: "𝔄. Length 𝔄 = 0  #V 𝔄 = idx"
  by (transfer fixing: idx) (auto intro: exI[of _ "replicate idx 0"])

lemma Extend_commute_safe[Presb_simps]: "j  i; i < Suc (#V 𝔄) 
  Extend k j (Extend k i 𝔄 P) Q = Extend k (Suc i) (Extend k j 𝔄 Q) P"
  by transfer (auto simp add: min_def take_Cons take_drop le_imp_diff_is_add split: nat.splits)

lemma Extend_commute_unsafe[Presb_simps]:
  "k  k'  Extend k j (Extend k' i 𝔄 P) Q = Extend k' i (Extend k j 𝔄 Q) P"
  by transfer auto

lemma assigns_Extend[Presb_simps]: "i < Suc (#V 𝔄) 
  mExtend k i 𝔄 Pk' = (if k = k' then if m = i then P else dec i m𝔄k else m𝔄k')"
  by transfer (auto simp: nth_append dec_def min_def)

lemma assigns_SNOC_zero[Presb_simps]: "m < #V 𝔄  mSNOC (zero (#V 𝔄)) 𝔄k = m𝔄k"
  by transfer auto

lemma Length_CONS[Presb_simps]: "Length (CONS x 𝔄) = Suc (Length 𝔄)"
  by transfer auto

lemma Length_SNOC[Presb_simps]: "Length (SNOC x 𝔄) = Suc (Length 𝔄)"
  by transfer auto

lemma nvars_CONS[Presb_simps]: "#V (CONS x 𝔄) = #V 𝔄"
  by transfer auto

lemma nvars_SNOC[Presb_simps]: "#V (SNOC x 𝔄) = #V 𝔄"
  by transfer auto

lemma Extend_CONS[Presb_simps]: "#V 𝔄 = length x 
  Extend k 0 (CONS x 𝔄) P = CONS (extend k (test_bit P 0) x) (Extend k 0 𝔄 (downshift P))"
  by transfer (auto simp: extend_def downshift_def test_bit_def, presburger+)

lemma Extend_SNOC[Presb_simps]: "#V 𝔄 = length x; len P  Length (SNOC x 𝔄) 
  Extend k 0 (SNOC x 𝔄) P =
    SNOC (extend k (test_bit P (Length 𝔄)) x) (Extend k 0 𝔄 (cut_bits (Length 𝔄) P))"
  apply transfer
  apply (auto simp: cut_bits_def extend_def test_bit_def nth_Cons' max_absorb1 len_le_iff
    split: if_splits cong del: if_weak_cong)
   apply (metis add.commute div_mult_mod_eq less_mult_imp_div_less mod_less mult_numeral_1 numeral_1_eq_Suc_0)
  apply (metis div_eq_0_iff less_mult_imp_div_less mod2_eq_if mod_less power_not_zero zero_neq_numeral)
  done

lemma odd_neq_even:
  "Suc (2 * x) = 2 * y  False"
  "2 * y = Suc (2 * x)  False"
  by presburger+

lemma CONS_inj[Presb_simps]: "size x = #V 𝔄  size y = #V 𝔄  #V 𝔄 = #V 𝔅 
  CONS x 𝔄 = CONS y 𝔅  (x = y  𝔄 = 𝔅)"
  by transfer (auto simp: list_eq_iff_nth_eq odd_neq_even split: if_splits)

lemma mod_2_Suc_iff:
  "x mod 2 = Suc 0  x = Suc (2 * (x div 2))"
  by presburger+

lemma CONS_surj[Presb_simps]: "Length 𝔄  0 
  x 𝔅. 𝔄 = CONS x 𝔅  #V 𝔅 = #V 𝔄  size x = #V 𝔄"
  by transfer
    (auto simp: gr0_conv_Suc list_eq_iff_nth_eq len_le_iff split: if_splits
    intro!: exI[of _ "map (λn. n mod 2  0) _"] exI[of _ "map (λn. n div 2) _"];
    auto simp: mod_2_Suc_iff)

lemma [Presb_simps]: 
  "length (extend k b x) = Suc (length x)"
  "downshift (upshift P) = P"
  "downshift (set_bit 0 P) = downshift P"
  "test_bit (set_bit n P) n"
  "¬ test_bit (upshift P) 0"
  "len P  p  ¬ test_bit P p"
  "len (cut_bits n P)  n"
  "len P  n  cut_bits n P = P"
  "len (upshift P) = (case len P of 0  0 | Suc n  Suc (Suc n))"
  "len (downshift P) = (case len P of 0  0 | Suc n  n)"
  by (auto simp: extend_def set_bit_def cut_bits_def upshift_def downshift_def test_bit_def
    len_le_iff len_eq0_iff div_add_self2 split: nat.split)

lemma Suc0_div_pow2_eq: "Suc 0 div 2 ^ i = (if i = 0 then 1 else 0)"
  by (induct i) (auto simp: div_mult2_eq)

lemma set_unset_bit_preserves_len:
  assumes "x div 2 ^ m = 2 * q" "m < len x"
  shows "x + 2 ^ m < 2 ^ len x"
using assms proof (induct m arbitrary: x)
  case 0 then show ?case
    by (auto simp: div_mult2_eq len_Suc_mult2[symmetric]
      simp del: len_Suc_mult2 power_Suc split: if_splits)
next
  case (Suc m)
  with Suc(1)[of "x div 2"] show ?case by (cases "len x") (auto simp: div_mult2_eq)
qed

lemma len_set_bit[Presb_simps]: "len (set_bit m P) = max (Suc m) (len P)"
proof (rule antisym)
  show "len (set_bit m P)  max (Suc m) (len P)"
    by (auto simp: set_bit_def test_bit_def max_def Suc_le_eq not_less len_le_iff
      set_unset_bit_preserves_len simp del: One_nat_def)
next
  have "P < 2 ^ len (P + 2 ^ m)" by (rule order.strict_trans2[OF less_pow2_len]) auto
  moreover have "m < len (P + 2 ^ m)" by (rule order.strict_trans2[OF _ len_mono[of "2 ^ m"]]) auto
  ultimately show "max (Suc m) (len P)  len (set_bit m P)"
    by (auto simp: set_bit_def test_bit_def max_def Suc_le_eq not_less len_le_iff)
qed

lemma mod_pow2_div_pow2:
  fixes p m n :: nat
  shows "m < n  p mod 2 ^ n div 2 ^ m = p div 2 ^ m mod 2 ^ (n - m)"
  by (induct m arbitrary: p n) (auto simp: div_mult2_eq mod_mult2_eq Suc_less_eq2)

lemma irrelevant_set_bit[simp]:
  fixes p m n :: nat
  assumes "n  m"
  shows "(p + 2 ^ m) mod 2 ^ n = p mod 2 ^ n"
proof -
  from assms obtain q :: nat where "2 ^ m = q * 2 ^ n"
    by (metis le_add_diff_inverse mult.commute power_add)
  then show ?thesis by simp
qed

lemma mod_lemma: " (0::nat) < c; r < b   b * (q mod c) + r < b * c"
  by (metis add_gr_0 div_le_mono div_mult_self1_is_m less_imp_add_positive mod_less_divisor not_less split_div)

lemma relevant_set_bit[simp]:
  fixes p m n :: nat
  assumes "m < n" "p div 2 ^ m = 2 * q"
  shows "(p + 2 ^ m) mod 2 ^ n = p mod 2 ^ n + 2 ^ m"
proof -
  have "p mod 2 ^ n + 2 ^ m < 2 ^ n"
  using assms proof (induct m arbitrary: p n)
    case 0 then show ?case
      by (auto simp: gr0_conv_Suc)
         (metis One_nat_def Suc_eq_plus1 lessI mod_lemma numeral_2_eq_2 zero_less_numeral zero_less_power)
  next
    case (Suc m)
    from Suc(1)[of "n - 1" "p div 2"] Suc(2,3) show ?case
      by (auto simp: div_mult2_eq mod_mult2_eq Suc_less_eq2)
  qed
  with m < n show ?thesis by (subst mod_add_eq [symmetric]) auto
qed

lemma cut_bits_set_bit[Presb_simps]: "cut_bits n (set_bit m p) =
  (if n  m then cut_bits n p else set_bit m (cut_bits n p))"
  unfolding cut_bits_def set_bit_def test_bit_def
  by (auto simp: not_le mod_pow2_div_pow2 mod_mod_cancel simp del: One_nat_def)

lemma wf0_decr0[Presb_simps]:
  "wf0 (Suc idx) a  l < Suc idx  ¬ find0 k l a  wf0 idx (decr0 k l a)"
  by (induct a) auto

lemma lformula0_decr0[Presb_simps]: "lformula0 a  lformula0 (decr0 k l a)"
  by (induct a) (auto elim: lformula0.cases intro: lformula0.intros)

abbreviation sat0_syn (infix "⊨0" 65) where
 "sat0_syn  satisfies0"
abbreviation sat_syn (infix "" 65) where
 "sat_syn  Formula_Operations.satisfies Extend Length satisfies0"
abbreviation sat_bounded_syn (infix "b" 65) where
 "sat_bounded_syn  Formula_Operations.satisfies_bounded Extend Length len satisfies0"

lemma scalar_product_Nil[simp]: "scalar_product [] xs = 0"
  by (induct xs) (auto simp: scalar_product_def)

lemma scalar_product_Nil2[simp]: "scalar_product xs [] = 0"
  by (induct xs) (auto simp: scalar_product_def)

lemma scalar_product_Cons[simp]:
  "scalar_product xs (y # ys) = (case xs of x # xs  x * y + scalar_product xs ys | []  0)"
  by (cases xs) (simp, auto simp: scalar_product_def cong del: if_weak_cong)

lemma scalar_product_append[simp]: "scalar_product ns (xs @ ys) =
  scalar_product (take (length xs) ns) xs + scalar_product (drop (length xs) ns) ys"
  by (induct xs arbitrary: ns) (auto split: list.splits)

lemma scalar_product_trim: "scalar_product ns xs = scalar_product (take (length xs) ns) xs"
  by (induct xs arbitrary: ns) (auto split: list.splits)

lemma Extend_satisfies0_decr0[Presb_simps]:
  assumes "¬ find0 k i a" "i < Suc (#V 𝔄)" "lformula0 a  len P  Length 𝔄"
  shows "Extend k i 𝔄 P ⊨0 a = 𝔄 ⊨0 decr0 k i a"
proof -
   { fix "is" :: "int list"
     assume "is ! i = 0"
     with assms(1,2) have "eval_tm (Extend k i 𝔄 P) is = eval_tm 𝔄 (take i is @ drop (Suc i) is)"
       by (cases a, transfer)
         (force intro: trans[OF scalar_product_trim] simp: min_def
         arg_cong2[OF refl id_take_nth_drop, of i _ scalar_product "take i xs @ _" for i x xs])
  } note * = this
  from assms show ?thesis
    by (cases a) (auto dest!: * simp: Length_Extend max_def elim: lformula0.cases)
qed

lemma scalar_product_eq0: "cset ns. c = 0  scalar_product ns is = 0"
proof (induct "is" arbitrary: "ns")
  case Cons
  then show ?case by (cases ns) (auto simp: scalar_product_def cong del: if_weak_cong)
qed (simp add: scalar_product_def)

lemma nullable0_satisfies0[Presb_simps]: "Length 𝔄 = 0  nullable0 a = 𝔄 ⊨0 a"
proof (induct a)
  case Eq then show ?case unfolding nullable0.simps satisfies0.simps
    by transfer (auto simp: len_eq0_iff scalar_product_eq0)
qed

lemma satisfies0_cong: "wf0 (#V 𝔅) a  #V 𝔄 = #V 𝔅  lformula0 a 
  (m k. m < #V 𝔅  m𝔄k = m𝔅k)  𝔄 ⊨0 a = 𝔅 ⊨0 a"
proof (induct a)
  case Eq then show ?case unfolding satisfies0.simps
    by transfer (auto simp: scalar_product_def
      intro!: arg_cong[of _ _ sum_list] map_index_cong elim!: lformula0.cases)
qed

lemma wf_lderiv0[Presb_simps]:
  "wf0 idx a  lformula0 a  Formula_Operations.wf (λ_. Suc) wf0 idx (lderiv0 x a)"
  by (induct a) (auto elim: lformula0.cases simp: Formula_Operations.wf.simps Let_def)

lemma lformula_lderiv0[Presb_simps]:
  "lformula0 a  Formula_Operations.lformula lformula0 (lderiv0 x a)"
  by (induct a)
    (auto elim: lformula0.cases intro: lformula0.intros simp: Let_def Formula_Operations.lformula.simps)

lemma wf_rderiv0[Presb_simps]:
  "wf0 idx a  Formula_Operations.wf (λ_. Suc) wf0 idx (rderiv0 x a)"
  by (induct a) (auto elim: lformula0.cases simp: Formula_Operations.wf.simps Let_def)

lemma find0_FV0[Presb_simps]: "wf0 idx a; l < idx  find0 k l a = (l  FV0 k a)"
  by (induct a) (auto simp: FV0_def)

lemma FV0_less[Presb_simps]: "wf0 idx a  v  FV0 k a  v < idx"
  by (induct a) (auto simp: FV0_def)

lemma finite_FV0[Presb_simps]: "finite (FV0 k a)"
  by (induct a) (auto simp: FV0_def)

lemma finite_lderiv0[Presb_simps]:
  assumes "lformula0 a"
  shows "finite {φ. xs. φ = fold (Formula_Operations.deriv extend lderiv0) xs (FBase a)}"
proof -
  define d where "d = Formula_Operations.deriv extend lderiv0"
  define l where "l is = sum_list [i. i  is, i < 0]" for "is" :: "int list"
  define h where "h is = sum_list [i. i  is, i > 0]" for "is" :: "int list"
  define Φ where "Φ a = (case a of
    Eq is n z  {FBase (Eq is i 0) | i . i  {min (- h is) n .. max (- l is) n}} 
      {FBool False :: formula})" 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 (auto simp: elim!: lformula0.cases)
    moreover have "x φ. φ  Φ a  d x φ  Φ a"
    proof (induct a, unfold Φ_def presb.case, elim UnE CollectE insertE emptyE exE conjE)
      fix "is" :: "int list" and bs :: "bool list" and i n :: int and φ :: formula
      assume "i  {min (- h is) n..max (- l is) n}" "φ = FBase (presb.Eq is i 0)"
      moreover have "scalar_product bs is  h is"
      proof (induct "is" arbitrary: bs)
        case (Cons x xs)
        from Cons[of "tl bs"] show ?case by (cases bs) (auto simp: h_def)
      qed (auto simp: h_def scalar_product_def)
      moreover have "l is  scalar_product bs is"
      proof (induct "is" arbitrary: bs)
        case (Cons x xs)
        from Cons[of "tl bs"] show ?case by (cases bs) (auto simp: l_def)
      qed (auto simp: l_def scalar_product_def)
      ultimately show "d bs φ 
        {FBase (presb.Eq is i 0) |i. i  {min (- h is) n..max (- l is) n}}  {FBool False}"
        by (auto simp: d_def Let_def)
    qed (auto simp: d_def)
    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 by (auto split: presb.splits)
   ultimately show "?thesis" unfolding d_def by (blast intro: finite_subset)
qed

lemma finite_rderiv0[Presb_simps]:
  "finite {φ. xs. φ = fold (Formula_Operations.deriv extend rderiv0) xs (FBase a)}"
proof -
  define d where "d = Formula_Operations.deriv extend rderiv0"
  define l where "l is = sum_list [i. i  is, i < 0]"for "is" :: "int list"
  define h where "h is = sum_list [i. i  is, i > 0]"for "is" :: "int list"
  define Φ where "Φ a = (case a of
    Eq is n z  {FBase (Eq is n i) | i . i  {min (- h is) (min n z) .. max (- l is) (max n z)}} 
      {FBool False :: formula})" for a
  { fix xs
    note Formula_Operations.fold_deriv_FBool[simp] Formula_Operations.deriv.simps[simp] Φ_def[simp]
    have "FBase a  Φ a" by (auto split: presb.splits)
    moreover have "x φ. φ  Φ a  d x φ  Φ a"
    proof (induct a, unfold Φ_def presb.case, elim UnE CollectE insertE emptyE exE conjE)
      fix "is" :: "int list" and bs :: "bool list" and i n m :: int and φ :: formula
      assume "i  {min (- h is) (min n m)..max (- l is) (max n m)}" "φ = FBase (presb.Eq is n i)"
      moreover have "scalar_product bs is  h is"
      proof (induct "is" arbitrary: bs)
        case (Cons x xs)
        from Cons[of "tl bs"] show ?case by (cases bs) (auto simp: h_def)
      qed (auto simp: h_def scalar_product_def)
      moreover have "l is  scalar_product bs is"
      proof (induct "is" arbitrary: bs)
        case (Cons x xs)
        from Cons[of "tl bs"] show ?case by (cases bs) (auto simp: l_def)
      qed (auto simp: l_def scalar_product_def)
      ultimately show "d bs φ 
        {FBase (presb.Eq is n i) |i. i  {min (- h is) (min n m)..max (- l is) (max n m)}}  {FBool False}"
        by (auto 0 1 simp: d_def Let_def h_def l_def)
    qed (auto simp: d_def)
    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 by (auto split: presb.splits)
   ultimately show "?thesis" unfolding d_def by (blast intro: finite_subset)
qed

lemma scalar_product_CONS: "length xs = length (bs :: bool list) 
  scalar_product (map_index (λi n. 2 * n + bs ! i) xs) is =
  scalar_product bs is + 2 * scalar_product xs is"
  by (induct "is" arbitrary: bs xs) (auto split: list.splits simp: algebra_simps)

lemma eval_tm_CONS[simp]:
  "length is  #V 𝔄; #V 𝔄 = length x 
   eval_tm (CONS x 𝔄) is = scalar_product x is + 2 * eval_tm 𝔄 is"
  by transfer (auto simp: scalar_product_CONS[symmetric]
    intro!: arg_cong2[of _ _ _ _ scalar_product] nth_equalityI)

lemma satisfies_lderiv0[Presb_simps]:
  "wf0 (#V 𝔄) a; #V 𝔄 = length x; lformula0 a  𝔄  lderiv0 x a  CONS x 𝔄 ⊨0 a"
  by (auto simp: Let_def Formula_Operations.satisfies_gen.simps
    split: if_splits elim!: lformula0.cases)

lemma satisfies_bounded_lderiv0[Presb_simps]:
  "wf0 (#V 𝔄) a; #V 𝔄 = length x; lformula0 a  𝔄 b lderiv0 x a  CONS x 𝔄 ⊨0 a"
  by (auto simp: Let_def Formula_Operations.satisfies_gen.simps
    split: if_splits elim!: lformula0.cases)

lemma scalar_product_SNOC: "length xs = length (bs :: bool list)  
  scalar_product (map_index (λi m. m + 2 ^ a * bs ! i) xs) is =
  scalar_product xs is + 2 ^ a * scalar_product bs is"
  by (induct "is" arbitrary: bs xs) (auto split: list.splits simp: algebra_simps)

lemma eval_tm_SNOC[simp]:
  "length is  #V 𝔄; #V 𝔄 = length x 
   eval_tm (SNOC x 𝔄) is = eval_tm 𝔄 is + 2 ^ Length 𝔄 * scalar_product x is"
  by transfer (auto simp: scalar_product_SNOC[symmetric]
    intro!: arg_cong2[of _ _ _ _ scalar_product] nth_equalityI)

lemma Length_eq0_eval_tm_eq0[simp]: "Length 𝔄 = 0  eval_tm 𝔄 is = 0"
  by transfer (auto simp: len_eq0_iff scalar_product_eq0)

lemma less_pow2: "x < 2 ^ a  int x < 2 ^ a"
  by (metis of_nat_less_iff of_nat_numeral of_nat_power [symmetric])

lemma scalar_product_upper_bound: "xset b. len x  a 
  scalar_product b is  (2 ^ a - 1) * sum_list [i. i  is, i > 0]"
proof (induct "is" arbitrary: b)
  case (Cons i "is")
  then have "scalar_product (tl b) is  (2 ^ a - 1) * sum_list [i. i  is, i > 0]"
    by (auto simp: in_set_tlD)
  with Cons(2) show ?case
    by (auto 0 3 split: list.splits simp: len_le_iff mult_le_0_iff
      distrib_left add.commute[of _ "(2 ^ a - 1) * i"] less_pow2
      intro: add_mono elim: order_trans[OF add_mono[OF order_refl]])
qed simp

lemma scalar_product_lower_bound: "xset b. len x  a 
  scalar_product b is  (2 ^ a - 1) * sum_list [i. i  is, i < 0]"
proof (induct "is" arbitrary: b)
  case (Cons i "is")
  then have "scalar_product (tl b) is  (2 ^ a - 1) * sum_list [i. i  is, i < 0]"
    by (auto simp: in_set_tlD)
  with Cons(2) show ?case
    by (auto 0 3 split: list.splits simp: len_le_iff mult_le_0_iff
      distrib_left add.commute[of _ "(2 ^ a - 1) * i"] less_pow2
      intro: add_mono elim: order_trans[OF add_mono[OF order_refl]] order_trans)
qed simp

lemma eval_tm_upper_bound: "eval_tm 𝔄 is  (2 ^ Length 𝔄 - 1) * sum_list [i. i  is, i > 0]"
  by transfer (auto simp: scalar_product_upper_bound)

lemma eval_tm_lower_bound: "eval_tm 𝔄 is  (2 ^ Length 𝔄 - 1) * sum_list [i. i  is, i < 0]"
  by transfer (auto simp: scalar_product_lower_bound)

lemma satisfies_bounded_rderiv0[Presb_simps]:
  "wf0 (#V 𝔄) a; #V 𝔄 = length x  𝔄 b rderiv0 x a  SNOC x 𝔄 ⊨0 a"
proof (induct a)
  case (Eq "is" n d)
  let ?l = "Length 𝔄"
  define d' where "d' = scalar_product x is + 2 * d"
  define l where "l = sum_list  [i. i  is, i < 0]"
  define h where "h = sum_list  [i. i  is, i > 0]"
  from Eq show ?case
  unfolding wf0.simps satisfies0.simps rderiv0.simps Let_def
  proof (split if_splits, simp only: Formula_Operations.satisfies_gen.simps satisfies0.simps
    Length_SNOC eval_tm_SNOC simp_thms(13) de_Morgan_conj not_le
    min_less_iff_conj max_less_iff_conj d'_def[symmetric] h_def[symmetric] l_def[symmetric], safe)
    assume "eval_tm 𝔄 is + 2 ^ ?l * scalar_product x is = n - 2 ^ Suc ?l * d"
    with eval_tm_upper_bound[of 𝔄 "is"] eval_tm_lower_bound[of 𝔄 "is"] have
      *: "n + h  2 ^ ?l * (h + d')" "2 ^ ?l * (l + d')  n + l"
      by (auto simp: algebra_simps h_def l_def d'_def)
    assume **: "d'  {min (- h) n..max (- l) n}"
    { assume "0  n + h"
      from order_trans[OF this *(1)] have "0  h + d'"
        unfolding zero_le_mult_iff using zero_less_power[of 2] by presburger
    }
    moreover
    { assume "n + h < 0"
      with *(1) have "n  d'" by (auto dest: order_trans[OF _ mult_right_mono_neg[of 1]])
    }
    moreover
    { assume "n + l < 0"
      from le_less_trans[OF *(2) this] have "l + d' < 0" unfolding mult_less_0_iff by auto
    }
    moreover
    { assume "0  n + l"
      then have "0  l + d'" using ** calculation(1-2) by force
      with *(2) have "d'  n" by (force dest: order_trans[OF mult_right_mono[of 1], rotated])
    }
    ultimately have "min (- h) n  d'" "d'  max (- l) n" by (auto simp: min_def max_def)
    with ** show False by auto
  qed (auto simp: algebra_simps d'_def)
qed

declare [[goals_limit = 100]]

global_interpretation Presb: Formula
  where SUC = SUC and LESS = "λ_. (<)" and Length = Length
  and assigns = assigns and nvars = nvars and Extend = Extend and CONS = CONS and SNOC = SNOC
  and extend = extend and size = size_atom and zero = zero and alphabet = σ and eval = test_bit
  and downshift = downshift and upshift = upshift and add = set_bit and cut = cut_bits and len = len
  and restrict = "λ_ _. True" and Restrict = "λ_ _. FBool True" and lformula0 = lformula0
  and FV0 = FV0 and find0 = find0 and wf0 = wf0 and decr0 = decr0 and satisfies0 = satisfies0
  and nullable0 = nullable0 and lderiv0 = lderiv0 and rderiv0 = rderiv0
  and TYPEVARS = 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 (λ_ _. FBool True) :: _  formula"
  and RESTRICT = "Formula_Operations.RESTRICT (λ_ _. FBool True) 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 :: nat  formula  _"
  and presb_wf = "Formula_Operations.wf SUC (wf0 :: nat  presb  _)"
  and presb_lformula = "Formula_Operations.lformula (lformula0 :: presb  _) :: formula  _"
  and check_eqv = "λidx. DAs.check_eqv
    (σ idx) (λφ. norm (RESTRICT φ) :: formula)
    (λa φ. norm (deriv (lderiv0 :: _  _  formula) (a :: atom) φ))
    (final idx) (λφ :: formula. presb_wf idx φ  presb_lformula φ)
    (σ idx) (λφ. norm (RESTRICT φ) :: formula)
    (λa φ. norm (deriv (lderiv0 :: _  _  formula) (a :: atom) φ))
    (final idx) (λφ :: formula. presb_wf idx φ  presb_lformula φ)
    (=)"
  and bounded_check_eqv = "λidx. DAs.check_eqv
    (σ idx) (λφ. norm (RESTRICT φ) :: formula)
    (λa φ. norm (deriv (lderiv0 :: _  _  formula) (a :: atom) φ))
    nullable (λφ :: formula. presb_wf idx φ  presb_lformula φ)
    (σ idx) (λφ. norm (RESTRICT φ) :: formula)
    (λa φ. norm (deriv (lderiv0 :: _  _  formula) (a :: atom) φ))
    nullable (λφ :: formula. presb_wf idx φ  presb_lformula φ)
    (=)"
  and automaton = "DA.automaton
    (λa φ. norm (deriv lderiv0 (a :: atom) φ :: formula))"
  apply standard apply (auto simp: Presb_simps σ_def set_n_lists distinct_n_lists
    Formula_Operations.lformula.simps Formula_Operations.satisfies_gen.simps Formula_Operations.wf.simps
    dest: satisfies0_cong split: presb.splits if_splits)
  apply (simp add: downshift_def)
  done

(*Workaround for code generation*)
lemma check_eqv_code[code]: "check_eqv idx r s =
  ((presb_wf idx r  presb_lformula r)  (presb_wf idx s  presb_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 Presb.check_eqv_def Presb.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 φ ψ  (Presb.sat 𝔄 φ  Presb.sat 𝔄 ψ)"
  unfolding check_eqv_def by (rule Presb.check_eqv_soundness)

lemma bounded_check_eqv_sound:
  "#V 𝔄 = idx; bounded_check_eqv idx φ ψ  (Presb.satb 𝔄 φ  Presb.satb 𝔄 ψ)"
  unfolding bounded_check_eqv_def by (rule Presb.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 bool} 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