Может ли Изабель раскрыть определения с явным типом?

Question

Я определил направленные множества, но мне нужно применить определение к «множеству» и «множеству» в одной и той же лемме. Кажется, это работает нормально. Но и «apply (развернуть направленный_деф)», и «применить (симпд: направленный_деф) раскрывают только определение направленного с типом« набор », определение направленного с типом« набор »не развернуто. (Пример доказательства имеет любое значение и используется только для демонстрации проблемы)

Есть ли способ развернуть экземпляры определений различного типа?

theory Scratch imports  "HOL-Lattice.Bounds" 
begin
instantiation  set:: (type)  partial_order
begin
definition setpoDef: "a⊑(b:: 'a set) = subset_eq a  b"
instance proof 
   fix x::"'a set"     show " x ⊑ x" by (auto simp: setpoDef) 
  fix x y z::"'a set" show  "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z" by (auto simp: setpoDef)
  fix x y::"'a set" show "x ⊑ y ⟹ y ⊑ x ⟹ x = y"   by (auto simp: setpoDef)
qed     
end
context partial_order begin 
definition directed:: "'a  set ⇒ bool" where
 " directed D  ≡ 
    ¬D={} ∧ ( ∀ a1 a2. a1∈D∧ a2∈D ⟶ (∃ ub∈D . (a1⊑ ub ∧ a2⊑ ub))) " (* page 120 *)

lemma " ((directed:: 'a set set ⇒ bool) D)   ⟹ directed (⋃ D)"
  apply (simp add:  directed_def ) (* ** *)
  apply(unfold  directed_def )   
end
end

Вывод в (* ** *)

(directed D ⟹ (∃x∈D. x ≠ {}) ∧ (∀a1 a2. (∃X∈D. a1 ∈ X) ∧ (∃X∈D. a2 ∈ X) ⟶ (∃y∈D. ∃ub∈y. a1 ⊑ ub ∧ a2 ⊑ ub))

Answer 1

Внутри класса типа, такого как partial_order, переменная типа 'a является фиксированной. Он представляет инстанцирующий тип класса type. Соответственно, определение directed является мономорфным c в контексте partial_order. Ваша лемма, однако, включает в себя два разных экземпляра класса типов: 'a set и 'a. Поэтому не имеет смысла указывать его внутри контекста класса типов.

Если вы переместите его из контекста partial_order, то simp и unfold должны действовать в обоих случаях directed .