--- a/src/HOL/HOLCF/Library/List_Cpo.thy Sun Jan 05 18:10:34 2025 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy Sun Jan 05 21:17:36 2025 +0100
@@ -16,21 +16,19 @@
definition
"xs \<sqsubseteq> ys \<longleftrightarrow> list_all2 (\<sqsubseteq>) xs ys"
-instance proof
- fix xs :: "'a list"
- from below_refl show "xs \<sqsubseteq> xs"
+instance
+proof
+ fix xs ys zs :: "'a list"
+ show "xs \<sqsubseteq> xs"
+ using below_refl
unfolding below_list_def
by (rule list_all2_refl)
-next
- fix xs ys zs :: "'a list"
- assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> zs"
- with below_trans show "xs \<sqsubseteq> zs"
+ show "xs \<sqsubseteq> ys \<Longrightarrow> ys \<sqsubseteq> zs \<Longrightarrow> xs \<sqsubseteq> zs"
+ using below_trans
unfolding below_list_def
by (rule list_all2_trans)
-next
- fix xs ys zs :: "'a list"
- assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> xs"
- with below_antisym show "xs = ys"
+ show "xs \<sqsubseteq> ys \<Longrightarrow> ys \<sqsubseteq> xs \<Longrightarrow> xs = ys"
+ using below_antisym
unfolding below_list_def
by (rule list_all2_antisym)
qed