CODEWITHSUNDEEP
classtypesisabelle
david streader
david streader

Reputation: 589

Can isabelle unfold definitions with explicit type?

I have defined directed sets but need to apply the definition to both "'a set" and "'a set set" in the same lemma. This seems to work fine. But both "apply (unfold directed_def)" and "apply(simp add: directed_def) only unfold the definition of directed with type "'a set" the definition of directed with type "'a set set" is not unfolded. (Example proof is striped of any value and just used to demonstrate the problem)

Is there any way to unfold definition instances that have distinct type?

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

Output at (* ** *)

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

Upvotes: 1

Views: 341

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

Inside the context of a type class like partial_order, the type variable 'a is fixed. It represents the instantiating type of the type class. Accordingly, the definition of directed is monomorphic inside the partial_order context. Your lemma, however, involves two different instances of the type class: 'a set and 'a. It therefore does not make sense to state it inside the type class context.

If you move it out of the partial_order context, both simp and unfold should act on both occurrences of directed.

Upvotes: 1

Related Questions