Theory Finite_IDL_Solver_Interface

section ‹An Interface for Solvers for a Subset of Finite Integer Difference Logic›

theory Finite_IDL_Solver_Interface
  imports Main
begin

text ‹We require a solver for (a subset of) integer-difference-logic (IDL). We basically just need
  comparisons of variables against constants, and difference of two variables.

  Note that all variables can be assumed to be finitely bounded, so we only need a solver for 
  finite IDL search problems.
  Moreover, it suffices to consider inputs where only those variables are put in comparison that 
  share the same sort
  (the second parameter of a variable),
  and the bounds are completely determined by the sorts.›

type_synonym ('v,'s)fidl_input = "(('v × 's) × int) list × (('v × 's) × 'v × 's) list list" 

definition fidl_input :: "('v,'s)fidl_input ⇒ bool" where 
  "fidl_input = (λ (bnds, diffs).
     distinct (map fst bnds) ∧ (∀ v w u. (v,w) ∈ set (concat diffs) ⟶ u ∈ {v,w} ⟶ u ∈ fst ` set bnds) 
     ∧ (∀ v w. (v,w) ∈ set (concat diffs) ⟶ snd v = snd w) 
     ∧ (∀ v w. (v,w) ∈ set (concat diffs) ⟶ v ≠ w) 
     ∧ (∀ v w b1 b2. (v,b1) ∈ set bnds ⟶ (w,b2) ∈ set bnds ⟶ snd v = snd w ⟶ b1 = b2) 
     ∧ (∀ v b. (v,b) ∈ set bnds ⟶ b ≥ 0))" 

definition fidl_solvable :: "('v,'s)fidl_input ⇒ bool" where
  "fidl_solvable = (λ (bnds, diffs). (∃α :: 'v × 's ⇒ int.
    (∀ (v,b) ∈ set bnds. 0 ≤ α v ∧ α v ≤ b) ∧
    (∀ c ∈ set diffs. ∃ (v,w) ∈ set c. α v ≠ α w)))" 

definition finite_idl_solver where  "finite_idl_solver solver = (∀ input.
   fidl_input input ⟶ solver input = fidl_solvable input)"

definition dummy_fidl_solver where 
  "dummy_fidl_solver input = fidl_solvable input" 

lemma dummy_fidl_solver: "finite_idl_solver dummy_fidl_solver" 
  unfolding dummy_fidl_solver_def finite_idl_solver_def by simp

lemma dummy_fidl_solver_code[code]: "dummy_fidl_solver input = Code.abort (STR ''dummy fidl solver'') (λ _. dummy_fidl_solver input)" 
  by simp

end