# HG changeset patch
# User wenzelm
# Date 1734019026 -3600
# Node ID a065d8bcfd3df9da9ea43915bf03f62ed2526bcf
# Parent  b6df830451782e6ab8c53ed639450e36017581a8
clarified class/locale reasoning: avoid side-stepping constraints;

diff -r b6df83045178 -r a065d8bcfd3d src/HOL/HOLCF/Algebraic.thy
--- a/src/HOL/HOLCF/Algebraic.thy	Thu Dec 12 15:45:29 2024 +0100
+++ b/src/HOL/HOLCF/Algebraic.thy	Thu Dec 12 16:57:06 2024 +0100
@@ -24,7 +24,7 @@
 
 instance fin_defl :: (bifinite) po
 using type_definition_fin_defl below_fin_defl_def
-by (rule typedef_po)
+by (rule typedef_po_class)
 
 lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
 using Rep_fin_defl by simp
diff -r b6df83045178 -r a065d8bcfd3d src/HOL/HOLCF/Cpodef.thy
--- a/src/HOL/HOLCF/Cpodef.thy	Thu Dec 12 15:45:29 2024 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy	Thu Dec 12 16:57:06 2024 +0100
@@ -16,21 +16,20 @@
   if the ordering is defined in the standard way.
 \<close>
 
-setup \<open>Sign.add_const_constraint (\<^const_name>\<open>below\<close>, NONE)\<close>
-
-theorem typedef_po:
-  fixes Abs :: "'a::po \<Rightarrow> 'b::type"
+theorem (in below) typedef_class_po:
+  fixes Abs :: "'b::po \<Rightarrow> 'a"
   assumes type: "type_definition Rep Abs A"
     and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-  shows "OFCLASS('b, po_class)"
-  apply (intro_classes, unfold below)
+  shows "class.po below"
+  apply (rule class.po.intro)
+  apply (unfold below)
     apply (rule below_refl)
    apply (erule (1) below_trans)
   apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
   apply (erule (1) below_antisym)
   done
 
-setup \<open>Sign.add_const_constraint (\<^const_name>\<open>below\<close>, SOME \<^typ>\<open>'a::below \<Rightarrow> 'a::below \<Rightarrow> bool\<close>)\<close>
+lemmas typedef_po_class = below.typedef_class_po [THEN po.intro_of_class]
 
 
 subsection \<open>Proving a subtype is finite\<close>
diff -r b6df83045178 -r a065d8bcfd3d src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Thu Dec 12 15:45:29 2024 +0100
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Thu Dec 12 16:57:06 2024 +0100
@@ -183,7 +183,7 @@
     val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
     val thy = lthy
       |> Class.prove_instantiation_exit
-          (fn ctxt => resolve_tac ctxt [@{thm typedef_po} OF [type_definition, below_def]] 1)
+          (fn ctxt => resolve_tac ctxt [@{thm typedef_po_class} OF [type_definition, below_def]] 1)
   in ((info, below_def), thy) end
 
 fun prepare_cpodef
diff -r b6df83045178 -r a065d8bcfd3d src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Thu Dec 12 15:45:29 2024 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Thu Dec 12 16:57:06 2024 +0100
@@ -252,7 +252,7 @@
 
 instance compact_basis :: (pcpo) po
 using type_definition_compact_basis compact_le_def
-by (rule typedef_po)
+by (rule typedef_po_class)
 
 definition
   approximants :: "'a::pcpo \<Rightarrow> 'a compact_basis set" where