Theory Dynamic

theory Dynamic
  imports Main
begin

locale dynval =
  fixes
    uninitialized :: 'dyn and
    is_true :: "'dyn ⇒ bool" and
    is_false :: "'dyn ⇒ bool"
  assumes
    not_true_and_false: "¬ (is_true d ∧ is_false d)"
begin

lemma false_not_true: "is_false d ⟹ ¬ is_true d"
  using not_true_and_false by blast

lemma true_not_false: "is_true d ⟹ ¬ is_false d"
  using not_true_and_false by blast

lemma is_true_and_is_false_implies_False: "is_true d ⟹ is_false d ⟹ False"
  using true_not_false false_not_true by simp

end

end