How do I code algebraic cpos as an Isabelle locale

Question

I am trying to prove the known fact that there is a standard way to build an algebriac_cpo from a partial_order. My problem is I keep getting the error

Type unification failed: No type arity set :: partial_order

and I can not understand what this means.

I think I have tracked down my problem to the definition of cpo. The definition works and I have proven various results for it but the working interpretation of a partial_order fails with cpo.

   theory LocaleProblem imports  "HOL-Lattice.Bounds" 
begin
definition directed:: "'a::partial_order set ⇒ bool" where
 " directed a  ≡ 
    ¬a={} ∧ ( ∀ a1 a2. a1∈a∧ a2∈a ⟶ (∃ ub . (is_Sup {a1,a2} ub))) " 
class cpo = partial_order +
  fixes bot :: "'a::partial_order" ("⊥")
  assumes bottom: " ∀ x::'a. ⊥ ⊑ x "  
  assumes dlub:  "directed (d::'a::partial_order set)  ⟶ (∃ lub . is_Inf  d lub) "

print_locale cpo 

interpretation "idl" : partial_order
   "(⊆)::( ('b set) ⇒ ('b set) ⇒ bool) " 
  by (unfold_locales , auto) (* works *)

interpretation "idl" : cpo
   "(⊆)::( ('b set) ⇒ ('b set) ⇒ bool) " 
   "{}" (* gives error 
Type unification failed: No type arity set :: partial_order

Failed to meet type constraint:

Term:  (⊆) :: 'b set ⇒ 'b set ⇒ bool
Type:  ??'a ⇒ ??'a ⇒ bool *)

Any help much appreciated. david

You offered two solutions. Following the work of Hennessy in Algebraic Theory of Processes" I am trying to prove (where I(A) are the Ideal which are sets) "If a is_a partial_order then I(A) is an algebraic_cpo" I will then want to apply the result to a number of semantics, give as sets. Dose your comment mean that the second solution is not a good idea?

Initially I had a proven lemma that started

lemma directed_ran: "directed (d::('a::partial_order×'b::partial_order) set) ⟹   directed (Range d)"
proof (unfold directed_def)

With the First solution started well:

context partial_order begin (* type 'a  is now a partial_order *)   
definition
  is_Sup :: "'a set ⇒ 'a ⇒ bool" where
  "is_Sup A sup = ((∀x ∈ A. x ⊑ sup) ∧ (∀z. (∀x ∈ A. x ⊑ z) ⟶ sup ⊑ z))"

definition directed:: "'a  set ⇒ bool" where
 " directed a  ≡ 
    ¬a={} ∧ ( ∀ a1 a2. a1∈a∧ a2∈a ⟶ (∃ ub . (is_Sup {a1,a2} ub))) " 

lemma directed_ran: "directed (d::('c::partial_order×'b::partial_order) set) ⟹   directed (Range d)"
proof - assume a:"directed d" 
  from a local.directed_def[of "d"]  (* Fail with message below *)

  show "directed (Range d)"

Alas the working lemma now fails: I rewrote proof (unfold local.directed_def) so I explored and found that although the fact local.directed_def exists is can not be unified

Failed to meet type constraint:

Term:  d :: ('c × 'b) set
Type:  'a set

I changed the type successfully in the lemma statement but now can find no way to unfold the definition in the proof. Is there some way to do this?

Second solution again starts well:

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

but next step fails

instance proof 
  fix d show "directed d ⟶ (∃lub. is_Sup d (lub::'a set))"
  proof assume "directed d " with directed_def[of "d"]  show "∃lub. is_Sup d lub" 
      by (metis Sup_least Sup_upper is_SupI setpoDef)
  qed
next   
  from class.cpo_axioms_def[of "bot"]  show  "∀x . ⊥  ⊑ x " (* Fails *)
qed
end

the first subgoal is proven but show "∀x . ⊥ ⊑ x " although cut an paste from the subgaol in the output does not match the subgoal. Normally at this point is need to add type constraints. But I cannot find any that work. Do you know what is going wrong? Do you know if I can force the Output to reveal the type information in the sugoal.

Andreas Lochbihler Andreas Lochbihler · Accepted Answer · 2020-01-24T06:36:49

The interpretation command acts on the locale that a type class definition implicitly declares. In particular, it does not register the type constructor as an instance of the type class. That's what the command instantiation is good for. Therefore, in the second interpretation, Isabelle complains about set not having been registered as a instance of partial_order.

Since directed only needs the ordering for one type instance (namely 'a), I recommend to move the definition of directed into the locale context of the partial_order type class and remove the sort constraint on 'a:

context partial_order begin
definition directed:: "'a set ⇒ bool" where 
  "directed a ≡ ¬a={} ∧ ( ∀ a1 a2. a1∈a∧ a2∈a ⟶ (∃ ub . (is_Sup {a1,a2} ub))) " 
end

(This only works if is_Sup is also defined in the locale context. If not, I recommend to replace the is_Sup condition with a1 <= ub and a2 <= ub.)

Then, you don't need to constrain 'a in the cpo type class definition, either:

class cpo = partial_order +
  fixes bot :: "'a" ("⊥")
  assumes bottom: " ∀ x::'a. ⊥ ⊑ x "  
  assumes dlub:  "directed (d::'a set)  ⟶ (∃ lub . is_Inf  d lub)"

And consequently, your interpretation should not fail due to sort constraints.

Alternatively, you could declare set as an instance of partial_order instead of interpreting the type class. The advantage is that you can then also use constants and theorems that need partial_order as a sort constraint, i.e., that have not been defined or proven inside the locale context of partial_order. The disadvantage is that you'd have to define the type class operation inside the instantiation block. So you can't just say that the subset relation should be used; this has to be a new constant. Depending on what you intend to do with the instantiation, this might not matter or be very annoying.

How do I code algebraic cpos as an Isabelle locale

1 Answers