theory Strange
imports Main
begin

  locale partial_order =
  fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes le_refl: "le x x"
  and le_antisym: "le x y \<and> le y x \<longrightarrow> x = y"
  and le_trans: "le x y \<and> le y z \<longrightarrow> le x z"

  locale sup_semilattice =
  fixes I :: 'a and sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes sup_unit_left: "sup I x = x"
  and sup_unit_right: "sup x I = x"
  and sup_commute: "sup x y = sup y x"
  and sup_assoc: "sup x (sup y z) = sup (sup x y) z"
  and sup_idem: "sup x x = x"
  begin
    definition le where "le x y = (sup x y = y)"
    lemma le_refl: "le x x" using le_def sup_idem by blast
    lemma le_antisym: "\<lbrakk> le x y; le y x \<rbrakk> \<Longrightarrow> x = y" using le_def sup_commute by auto
    lemma le_trans: "\<lbrakk> le x y; le y z \<rbrakk> \<Longrightarrow> le x z" using le_def sup_assoc by metis

    lemma le_po: "partial_order le"
    proof
      fix x y z
      show "le x x" using le_refl by auto
      show "le x y \<and> le y x \<longrightarrow> x = y" using le_antisym by auto
      show "le x y \<and> le y z \<longrightarrow> le x z" using le_trans by blast
    qed

    interpretation partial_order le using le_po by auto
  end

  sublocale sup_semilattice \<subseteq> partial_order
  proof
    fix x y z
    show "le x x" using le_refl by auto  (* Fails!  Nitpick gives a counterexample. *)
    show "le x y \<and> le y x \<longrightarrow> x = y" using le_antisym by auto
    show "le x y \<and> le y z \<longrightarrow> le x z" using le_trans by blast
  qed

end