## Stream: Beginner Questions

### Topic: Wellorder instance of char

#### 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"
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 ..
``````

#### Manuel Eberl (Jul 18 2021 at 16:58):

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)
``````

#### Robert Soeldner (Jul 18 2021 at 17:41):

Thank you for this. Impressive how fast you found the proof :)

Last updated: Sep 25 2021 at 08:21 UTC