Can I construct a while structure algebraically using class and locale?

Question

I am constructing program statements from algebraic structures, rather than using definitions or functions.That is to set their properties in Isabelle using locale or class commands.
Now I need to construct a while statement.

I know I can define it in command of functions, or I can define it using kleene algebra. But, as I said before, I just want to describe the nature of a class or locale.
So I wrote this code:

consts skip  :: "'a" ("II")
type_synonym 'a proc = "'a "

class sequen = 
  fixes seq :: "'a proc ⇒'a proc  ⇒'a proc " (infixl ";;" 60)
  assumes seq_assoc : "(x ;; y) ;; z = x ;; (y ;; z)"
      and seq_skip_left : "II ;; x = x"
      and seq_skip_right : "x ;; II = x" 

definition ifprog :: " 'a proc  ⇒ bool ⇒ 'a proc  ⇒ 'a proc "  ("(_ ◃ _ ▹ _)" [52,0,53] 52)
  where "x ◃ bexp ▹ y ≡ (THE z::'a proc . (bexp = True ⟶ z = x) ∧ (bexp = False ⟶ z = y))"

locale while_unfold =
  sequen seq 
  for seq :: "'a proc ⇒'a proc  ⇒'a proc " +
  fixes while ::"bool ⇒ 'a proc ⇒ 'a proc" ("while _ do _ od")
  assumes while_ltera : "while bexp do P od =  (P ;; (while bexp do P od)) ◃ bexp ▹ II"

If that were possible, I wouldn't be asking questions here, I've got a problem :
Type unification failed: Variable 'a::type not of sort sequen

And then, these details are:

Type unification failed: Variable 'a::type not of sort sequen

Type error in application: incompatible operand type

Operator: (;;) :: ??'a ⇒ ??'a ⇒ ??'a
Operand: P :: 'a

How can I avoid this problem, or can this descriptive method be used to construct statements that have an iterative function, such as while.

Answer 1

I have not looked at the content of the class/locale, but the error message seems to be self-explanatory: type unification failed due to an incompatible sort constraint for the type variable 'a. Unless you rely on type inference, the sort constraint needs to be provided explicitly:

consts skip  :: "'a" ("II")
type_synonym 'a proc = "'a "

class sequen = 
  fixes seq :: "'a proc ⇒'a proc  ⇒'a proc " (infixl ";;" 60)
  assumes seq_assoc : "(x ;; y) ;; z = x ;; (y ;; z)"
      and seq_skip_left : "II ;; x = x"
      and seq_skip_right : "x ;; II = x" 

(*sequen_class.seq has the type 
"'a::sequen ⇒ 'a::sequen ⇒ 'a::sequen",
 which includes the sort constraint sequen for the type variable 'a:*)
declare [[show_sorts]]
term sequen_class.seq

definition ifprog :: " 'a proc  ⇒ bool ⇒ 'a proc  ⇒ 'a proc "  ("(_ ◃ _ ▹ _)" [52,0,53] 52)
  where "x ◃ bexp ▹ y ≡ (THE z::'a proc . (bexp = True ⟶ z = x) ∧ (bexp = False ⟶ z = y))"

(*note the sort constraint*)
locale while_unfold =
  sequen seq 
  for seq :: "'a::sequen proc ⇒'a proc  ⇒'a proc " +
  fixes while ::"bool ⇒ 'a proc ⇒ 'a proc" ("while _ do _ od")
  assumes while_ltera : "while bexp do P od =  (P ;; (while bexp do P od)) ◃ bexp ▹ II"

(*alternatively, consider using a class instead of a locale, although,
most certainly, the best choice depends on your application*)
class while_unfold' =
  sequen +
  fixes while ::"bool ⇒ 'a proc ⇒ 'a proc" ("while _ do _ od")
  assumes while_ltera : "while bexp do P od =  (P ;; (while bexp do P od)) ◃ bexp ▹ II"

For more information about classes and sort constraints see sections 3.3.6 and 5.8 in the Isabelle/Isar Reference Manual. You can also take a look at section 2 in the The Isabelle/Isar Implementation.

---

Isabelle version: Isabelle2020