Theory Locale_Instances

section ‹Locale Instances›

theory Locale_Instances
  imports Hmax_Certificates Efficient_PDB
begin

text ‹Consistency witnesses for all locales of the development.  A locale whose
  assumptions are contradictory makes every theorem proved inside it vacuous;
  the interpretations below rule this out by exhibiting one concrete model for
  each of @{locale pdb_heuristic}, @{locale hmax_heuristic},
  @{locale efficient_pdb} and @{locale astar_run}.

  The witness is the smallest non-degenerate planning task: one variable
  @{text "0"}, initially false, required by the goal, and one action that adds
  it at cost 1.  The optimal plan is the single-action plan of cost 1, and we
  use the bound @{text "B = 1"}.  All interesting locale assumptions
  (the PDB distance conditions @{text d_goal}/@{text d_triangle}, the hmax
  table conditions, the A* expansion-closure condition) are discharged
  non-vacuously.

  The A* interpretation is additionally instantiated with the ∗‹interpreted›
  PDB certificate at the embedded variable type @{typ "nat + nat"} (gate names
  @{text "Inr (2*j+1)"}), i.e. the locales compose exactly as the paper's
  PDB-into-A* case study intends.  As a final sanity check the composition
  yields the concrete theorem @{text "optimal_plan demo_task [demo_act]"}.›

subsection ‹The demo task›

definition demo_act :: "nat action" where
  "demo_act = ⦇ pre = {}, add = {0}, del = {}, cost = 1 ⦈"

definition demo_task :: "nat strips_task" where
  "demo_task = ⦇ vars = {0}, acts = {demo_act}, init = {}, goal = {0} ⦈"

lemma demo_pow: "set [{}, {0::nat}] = Pow {0}"
  by (auto dest: subset_singletonD)

subsection ‹Interpretation of @{locale pdb_heuristic}›

interpretation demo_pdb: pdb_heuristic demo_task 1 "{0::nat}"
  "λsa. if 0 ∈ sa then 0 else 1" "[{}, {0}]" "[demo_act]" id
proof unfold_locales
  show "finite (vars demo_task)" by (simp add: demo_task_def)
  show "{0::nat} ⊆ vars demo_task" by (simp add: demo_task_def)
  show "set [{}, {0::nat}] = Pow {0}" by (rule demo_pow)
  show "distinct [{}, {0::nat}]" by simp
  show "∀a ∈ set [demo_act].
      pre a ⊆ vars demo_task ∧ add a ⊆ vars demo_task ∧ del a ⊆ vars demo_task"
    by (simp add: demo_act_def demo_task_def)
  show "∀a ∈ set [demo_act]. add a ∩ del a = {}"
    by (simp add: demo_act_def)
  show "⋀sa. sa ⊆ {0::nat} ⟹ goal demo_task ∩ {0} ⊆ sa ⟹
      (if 0 ∈ sa then 0 else 1) = (0::nat)"
    by (auto simp: demo_task_def)
  show "⋀sa a. sa ⊆ {0::nat} ⟹ a ∈ set [demo_act] ⟹ pre a ∩ {0} ⊆ sa ⟹
      (if 0 ∈ sa then 0 else 1)
        ≤ (if 0 ∈ (sa - del a) ∪ (add a ∩ {0}) then 0 else 1) + cost a"
    by (auto simp: demo_act_def)
  show "inj (id :: nat ⇒ nat)" by simp
qed

text ‹The interpreted facts are available, e.g. the validity of the PDB
  certificate for the demo table:›

lemma "hc_valid demo_task 1 [demo_act] demo_pdb.pdb_cert S"
  by (rule demo_pdb.pdb_hc_valid)

subsection ‹Interpretation of @{locale hmax_heuristic}›

text ‹The evaluated state is the initial state @{term "{} :: nat state"}; its
  hmax value is 1 (the single goal variable costs 1 to achieve), and the
  clipped max value of every variable is 1.›

interpretation demo_hmax: hmax_heuristic demo_task 1 "{} :: nat state" 1
  "λv. 1" "[0]" "[demo_act]" id
proof unfold_locales
  show "finite (vars demo_task)" by (simp add: demo_task_def)
  show "goal demo_task ⊆ vars demo_task" by (simp add: demo_task_def)
  show "{} ⊆ vars demo_task" by simp
  show "set [0] = vars demo_task" by (simp add: demo_task_def)
  show "distinct [0::nat]" by simp
  show "∀a ∈ set [demo_act].
      pre a ⊆ vars demo_task ∧ add a ⊆ vars demo_task ∧ del a ⊆ vars demo_task"
    by (simp add: demo_act_def demo_task_def)
  show "∀a ∈ set [demo_act]. add a ∩ del a = {}"
    by (simp add: demo_act_def)
  show "⋀v. v ∈ ({} :: nat state) ⟹ (1::nat) = 0" by simp
  show "goal demo_task ≠ {} ⟹ ∃v ∈ goal demo_task. (1::nat) = 1"
    by (simp add: demo_task_def)
  show "goal demo_task = {} ⟹ (1::nat) = 0" by (simp add: demo_task_def)
  show "⋀a v. a ∈ set [demo_act] ⟹ v ∈ add a ⟹ pre a ≠ {} ⟹
      ∃p ∈ pre a. (1::nat) ≤ 1 + cost a"
    by (simp add: demo_act_def)
  show "⋀a v. a ∈ set [demo_act] ⟹ v ∈ add a ⟹ pre a = {} ⟹
      (1::nat) ≤ cost a"
    by (simp add: demo_act_def)
  show "inj (id :: nat ⇒ nat)" by simp
qed

lemma "hc_valid demo_task 1 [demo_act] demo_hmax.hmax_cert {{}}"
  by (rule demo_hmax.hmax_hc_valid)

subsection ‹Interpretation of @{locale efficient_pdb}›

text ‹In the demo task every abstract state reaches the abstract goal, so the
  finiteness predicate is constantly true and the table coincides with the
  plain PDB table.›

interpretation demo_epdb: efficient_pdb demo_task 1 "{0::nat}"
  "λsa. if 0 ∈ sa then 0 else 1" "λsa. True" "[{}, {0}]" "[demo_act]" id
proof unfold_locales
  show "finite (vars demo_task)" by (simp add: demo_task_def)
  show "{0::nat} ⊆ vars demo_task" by (simp add: demo_task_def)
  show "set [{}, {0::nat}] = {sa. sa ⊆ {0} ∧ True}"
    using demo_pow by auto
  show "distinct [{}, {0::nat}]" by simp
  show "∀a ∈ set [demo_act].
      pre a ⊆ vars demo_task ∧ add a ⊆ vars demo_task ∧ del a ⊆ vars demo_task"
    by (simp add: demo_act_def demo_task_def)
  show "∀a ∈ set [demo_act]. add a ∩ del a = {}"
    by (simp add: demo_act_def)
  show "⋀sa. sa ⊆ {0::nat} ⟹ goal demo_task ∩ {0} ⊆ sa ⟹
      True ∧ (if 0 ∈ sa then 0 else 1) = (0::nat)"
    by (auto simp: demo_task_def)
  show "⋀sa a. sa ⊆ {0::nat} ⟹ a ∈ set [demo_act] ⟹ pre a ∩ {0} ⊆ sa ⟹
      True ⟹ True ∧ (if 0 ∈ sa then 0 else 1)
        ≤ (if 0 ∈ (sa - del a) ∪ (add a ∩ {0}) then 0 else 1) + cost a"
    by (auto simp: demo_act_def)
  show "inj (id :: nat ⇒ nat)" by simp
qed

lemma "hc_valid demo_task 1 [demo_act] demo_epdb.epdb_cert S"
  by (rule demo_epdb.epdb_hc_valid)

subsection ‹Interpretation of @{locale pdb_heuristic} at the embedded type›

text ‹For the A* interpretation the heuristic certificate must live at the
  extended variable type @{typ "nat + nat"} with the odd gate names
  @{text "Inr (2*j+1)"} that @{locale astar_run} reserves for the heuristic.›

lemma demo_taskE_simps:
  "vars (embed_task demo_task :: (nat + nat) strips_task) = {Inl 0}"
  "goal (embed_task demo_task :: (nat + nat) strips_task) = {Inl 0}"
  "init (embed_task demo_task :: (nat + nat) strips_task) = {}"
  "acts (embed_task demo_task :: (nat + nat) strips_task) = {embed_act demo_act}"
  by (simp_all add: embed_task_def demo_task_def)

lemma demo_actE_simps:
  "pre (embed_act demo_act :: (nat + nat) action) = {}"
  "add (embed_act demo_act :: (nat + nat) action) = {Inl 0}"
  "del (embed_act demo_act :: (nat + nat) action) = {}"
  "cost (embed_act demo_act :: (nat + nat) action) = 1"
  by (simp_all add: embed_act_def demo_act_def)

lemma demo_powE: "set [{}, {Inl 0} :: (nat + nat) state] = Pow {Inl 0}"
  by (auto dest: subset_singletonD)

interpretation demoE_pdb: pdb_heuristic
  "embed_task demo_task :: (nat + nat) strips_task" 1 "{Inl 0}"
  "λsa. if Inl 0 ∈ sa then 0 else 1" "[{}, {Inl 0}]" "[embed_act demo_act]"
  "λj. Inr (2 * j + 1)"
proof unfold_locales
  show "finite (vars (embed_task demo_task :: (nat + nat) strips_task))"
    by (simp add: demo_taskE_simps)
  show "{Inl 0} ⊆ vars (embed_task demo_task :: (nat + nat) strips_task)"
    by (simp add: demo_taskE_simps)
  show "set [{}, {Inl 0} :: (nat + nat) state] = Pow {Inl 0}"
    by (rule demo_powE)
  show "distinct [{}, {Inl 0} :: (nat + nat) state]" by simp
  show "∀a ∈ set [embed_act demo_act :: (nat + nat) action].
      pre a ⊆ vars (embed_task demo_task)
      ∧ add a ⊆ vars (embed_task demo_task)
      ∧ del a ⊆ vars (embed_task demo_task)"
    by (simp add: demo_actE_simps demo_taskE_simps)
  show "∀a ∈ set [embed_act demo_act :: (nat + nat) action]. add a ∩ del a = {}"
    by (simp add: demo_actE_simps)
  show "⋀sa. sa ⊆ {Inl 0} ⟹
      goal (embed_task demo_task :: (nat + nat) strips_task) ∩ {Inl 0} ⊆ sa ⟹
      (if Inl 0 ∈ sa then 0 else 1) = (0::nat)"
    by (auto simp: demo_taskE_simps)
  show "⋀sa a. sa ⊆ {Inl 0} ⟹ a ∈ set [embed_act demo_act :: (nat + nat) action] ⟹
      pre a ∩ {Inl 0} ⊆ sa ⟹
      (if Inl 0 ∈ sa then 0 else 1)
        ≤ (if Inl 0 ∈ (sa - del a) ∪ (add a ∩ {Inl 0}) then 0 else 1) + cost a"
    by (auto simp: demo_actE_simps)
  show "inj (λj. Inr (2 * j + 1) :: nat + nat)"
    by (auto simp: inj_def)
qed

subsection ‹Interpretation of @{locale astar_run}›

text ‹The A* snapshot after expanding the initial state: the closed list holds
  @{term "({}, 0)"}, the open list holds the goal state @{term "{0::nat}"}, and
  the heuristic certificate is the interpreted embedded PDB certificate.›

interpretation demo_astar: astar_run demo_task 1 "[({}, 0)]" "[{0::nat}]"
  demoE_pdb.pdb_cert "[embed_act demo_act]"
proof unfold_locales
  show "finite (vars demo_task)" by (simp add: demo_task_def)
  show "init demo_task ⊆ vars demo_task" by (simp add: demo_task_def)
  show "goal demo_task ⊆ vars demo_task" by (simp add: demo_task_def)
  show "finite (acts demo_task)" by (simp add: demo_task_def)
  show "∀a ∈ acts demo_task. add a ∩ del a = {}"
    by (simp add: demo_task_def demo_act_def)
  show "∀a ∈ acts demo_task.
      pre a ⊆ vars demo_task ∧ add a ⊆ vars demo_task ∧ del a ⊆ vars demo_task"
    by (simp add: demo_task_def demo_act_def)
  show "set [embed_act demo_act] = acts (embed_task demo_task)"
    by (simp add: embed_task_def demo_task_def)
  show "(1::nat) ≥ 1" by simp
  show "(init demo_task, 0) ∈ set [({}, 0)]" by (simp add: demo_task_def)
  show "∀(s, g) ∈ set [({}, 0)]. s ⊆ vars demo_task" by (simp add: demo_task_def)
  show "∀s ∈ set [{0::nat}]. s ⊆ vars demo_task" by (simp add: demo_task_def)
  show "∀(s, g) ∈ set [({}, 0::nat)]. is_goal_state demo_task s ⟶ g ≥ 1"
    by (simp add: is_goal_state_def demo_task_def)
  show "∀(s, g) ∈ set [({}, 0::nat)]. ∀a ∈ acts demo_task. applicable a s ⟶
      (is_goal_state demo_task s ∧ g ≥ 1)
    ∨ (∃g'. (successor a s, g') ∈ set [({}, 0)] ∧ g' ≤ g + cost a)
    ∨ (successor a s ∈ set [{0::nat}] ∧
       int (g + cost a) ≥ int 1 - int (hc_h demoE_pdb.pdb_cert (Inl ` successor a s)))"
  proof -
    have succ: "successor demo_act {} = {0}"
      by (simp add: successor_def demo_act_def)
    have h0: "hc_h demoE_pdb.pdb_cert {Inl (0::nat)} = 0"
      unfolding demoE_pdb.pdb_cert_def by simp
    have cost_a: "cost demo_act = 1"
      by (simp add: demo_act_def)
    have third: "successor demo_act {} ∈ set [{0::nat}] ∧
        int (0 + cost demo_act)
          ≥ int 1 - int (hc_h demoE_pdb.pdb_cert (Inl ` successor demo_act {}))"
      by (simp add: succ h0 cost_a)
    have inner: "∀a ∈ acts demo_task. applicable a {} ⟶
        (is_goal_state demo_task {} ∧ (0::nat) ≥ 1)
      ∨ (∃g'. (successor a {}, g') ∈ set [({}, 0)] ∧ g' ≤ 0 + cost a)
      ∨ (successor a {} ∈ set [{0::nat}] ∧
         int (0 + cost a) ≥ int 1 - int (hc_h demoE_pdb.pdb_cert (Inl ` successor a {})))"
    proof
      fix a assume "a ∈ acts demo_task"
      then have a_eq: "a = demo_act" by (simp add: demo_task_def)
      show "applicable a {} ⟶
          (is_goal_state demo_task {} ∧ (0::nat) ≥ 1)
        ∨ (∃g'. (successor a {}, g') ∈ set [({}, 0)] ∧ g' ≤ 0 + cost a)
        ∨ (successor a {} ∈ set [{0::nat}] ∧
           int (0 + cost a) ≥ int 1 - int (hc_h demoE_pdb.pdb_cert (Inl ` successor a {})))"
        unfolding a_eq using third by blast
    qed
    show ?thesis using inner by simp
  qed
  show "hc_valid (embed_task demo_task) 1 [embed_act demo_act] demoE_pdb.pdb_cert
      ((λs. Inl ` s) ` set [{0::nat}])"
    by (rule demoE_pdb.pdb_hc_valid)
  show "∀(r, cs, A) ∈ set (hc_gates demoE_pdb.pdb_cert).
      ∃j. r = Pos (ReifCert (Inr (2 * j + 1)))"
    using demoE_pdb.pdb_names by auto
  show "distinct (map (λ(r, cs, A). pvar_of_lit r) (hc_gates demoE_pdb.pdb_cert))"
    by (rule demoE_pdb.pdb_distinct)
  show "∀i < length (hc_gates demoE_pdb.pdb_cert).
      case hc_gates demoE_pdb.pdb_cert ! i of (r, cs, A) ⇒
        (∀x ∈ pvar_of_lit ` snd ` set cs.
          (∃v. x = StateVar v) ∨ (∃j. x = CostBit j)
          ∨ x ∈ pvar_of_lit ` fst ` set (take i (hc_gates demoE_pdb.pdb_cert)))"
    by (rule demoE_pdb.pdb_wf)
  show "∀s ∈ set [{0::nat}].
      hc_out demoE_pdb.pdb_cert (Inl ` s) ∈ fst ` set (hc_gates demoE_pdb.pdb_cert)"
    using demoE_pdb.pdb_out_in by simp
qed

subsection ‹End-to-end sanity check›

text ‹The composed interpretations yield a concrete, non-vacuous consequence:
  the single-action plan is optimal for the demo task.›

lemma demo_plan: "is_plan_for demo_task [demo_act]"
proof -
  have succ: "successor demo_act {} = {0}"
    by (simp add: successor_def demo_act_def)
  have p0: "path (acts demo_task) (successor demo_act {}) {0} []"
    unfolding succ by (rule path.path_nil)
  have appl: "applicable demo_act {}"
    by (simp add: applicable_def demo_act_def)
  have mem: "demo_act ∈ acts demo_task"
    by (simp add: demo_task_def)
  have "path (acts demo_task) {} {0} [demo_act]"
    by (rule path.path_cons[OF appl p0 mem])
  then show ?thesis
    unfolding is_plan_for_def is_goal_state_def
    by (intro exI[of _ "{0}"]) (simp add: demo_task_def)
qed

lemma demo_cost: "plan_cost [demo_act] = 1"
  by (simp add: plan_cost_def demo_act_def)

theorem demo_optimal: "optimal_plan demo_task [demo_act]"
  by (rule demo_astar.astar_optimal[OF demo_plan demo_cost])

text ‹And the lower bound directly: every plan for the demo task costs at
  least 1.›

theorem demo_lower_bound: "is_plan_for demo_task π ⟹ plan_cost π ≥ 1"
  by (rule demo_astar.astar_lower_bound)

end