theory Status_Impl
imports
"Check-NT.Term_Order_Impl"
QTRS.Map_Choice
begin
type_synonym 'f status_impl = "(('f × nat) × nat list)list"
lift_definition (code_dt) status_of :: "'f status_impl ⇒ 'f status option" is
"λ s. if (∀ fidx ∈ set s. (∀ i ∈ set (snd fidx). i < snd (fst fidx)))
then Some (fun_of_map_fun (map_of s) (λ (f,n). [0 ..< n])) else None"
using map_of_SomeD by (fastforce split: option.splits)
lemma status_of_Some: "status_of s = Some σ
⟹ status σ = (fun_of_map_fun (map_of s) (λ (f,n). [0 ..< n]))"
using status_of.rep_eq[of s]
by (transfer, auto split: if_splits)
lemma status_of_default: assumes s: "status_of s = Some σ"
and f: "(f,n) ∉ fst ` set s"
shows "status σ (f,n) = [0 ..< n]"
proof -
from map_of_eq_None_iff[of s "(f,n)"] f have "map_of s (f,n) = None" by simp
thus ?thesis unfolding status_of_Some[OF s] by simp
qed
end