Robert Soeldner (Jul 18 2021 at 11:15): Robert Soeldner (Jul 18 2021 at 11:15):I'm stuck at proving the wellorder properties for char. The current goal is
proof (prove)
goal (1 subgoal):
1. ⋀(P::char ⇒ bool) a::char. (⋀x::char. (⋀y::char. of_char y < of_char x ⟹ P y) ⟹ P x) ⟹ P a
I would assume this should be pretty straightforward since there exist a wellorder instance for nat?
Alexander Taepper (Jul 18 2021 at 16:27):I played around a bit and came up with this instantiation proof:
lemma wellorder_char:
"class.wellorder (λc d. of_char c ≤ (of_char d :: nat)) (λc d. of_char c < (of_char d :: nat))"
proof (standard, auto)
fix P a
assume step: "(⋀y. (of_char y :: nat) < (of_char x :: nat) ⟹ P y) ⟹ P x" for x :: char
define n where "n = (of_char a :: nat)"
have "⋀q. (of_char q :: nat) ≤ n ⟹ P q"
proof (induction n rule: less_induct)
case (less x)
then show ?case
by (metis step nat_less_le)
qed
then show "P a"
by (simp add: n_def)
qed
I assume it can be simplified, but hope this helps :)
Manuel Eberl (Jul 18 2021 at 16:33):proof (standard, auto)? I see you like to live dangerously. :smiling_devil:
Manuel Eberl (Jul 18 2021 at 16:55):Note that if you want a linorder instance for char, you should import HOL-Library.Char_ord.
Manuel Eberl (Jul 18 2021 at 16:56):As for wellorder, here's a more general solution that works for any finite types:
class finite_linorder = finite + linorder
begin
subclass wellorder
proof
fix P :: "'a ⇒ bool" and x :: 'a
assume IH: "⋀x. (⋀y. y < x ⟹ P y) ⟹ P x"
define xs where "xs = sorted_list_of_set (UNIV :: 'a set)"
define f where "f = (λi. xs ! i)"
define n where "n = card (UNIV :: 'a set)"
have xs: "set xs = UNIV" "sorted xs" "distinct xs" and n: "length xs = n"
unfolding xs_def using finite[of UNIV] by (simp_all add: n_def)
have range_f: "∃j<n. f j = y" for y
using xs unfolding f_def by (metis UNIV_I in_set_conv_nth n)
from xs have less_iff: "f i < f j ⟷ i < j" if "i < n" "j < n" for i j
using that n unfolding f_def
by (metis linorder_class.not_le local.antisym_conv1 local.not_less local.sorted_nth_mono
nth_eq_iff_index_eq order_class.less_le)
from range_f obtain i where "i < n" "f i = x"
by blast
moreover have "P (f i)" if "i < n"
using that by (induction i rule: less_induct) (use IH range_f less_iff in metis)
ultimately show "P x"
by blast
qed
end
instance char :: finite_linorder ..
Or, alternative solution without the extra type class:
lemma finite_linorder_is_wellorder:
assumes "SORT_CONSTRAINT('a :: {finite, linorder})"
shows "OFCLASS('a, wellorder_class)"
proof
fix P :: "'a ⇒ bool" and x :: 'a
assume IH: "⋀x. (⋀y. y < x ⟹ P y) ⟹ P x"
define xs where "xs = sorted_list_of_set (UNIV :: 'a set)"
define f where "f = (λi. xs ! i)"
define n where "n = card (UNIV :: 'a set)"
have xs: "set xs = UNIV" "sorted xs" "distinct xs" and n: "length xs = n"
unfolding xs_def using finite[of UNIV] by (simp_all add: n_def)
have range_f: "∃j<n. f j = y" for y
using xs unfolding f_def by (metis UNIV_I in_set_conv_nth n)
from xs have less_iff: "f i < f j ⟷ i < j" if "i < n" "j < n" for i j
using that n unfolding f_def
by (metis not_less sorted_nth_mono nth_eq_iff_index_eq less_le)
from range_f obtain i where "i < n" "f i = x"
by blast
moreover have "P (f i)" if "i < n"
using that by (induction i rule: less_induct) (use IH range_f less_iff in metis)
ultimately show "P x"
by blast
qed
instance char :: wellorder
by (rule finite_linorder_is_wellorder)
Thank you for this. Impressive how fast you found the proof :)
Last updated: Apr 26 2024 at 04:17 UTC