By looking for the order.thy, I find the instance ```
instance "fun" :: (type, order) order proof
qed (auto simp add: le_fun_def intro: order.antisym)
```

. There is a straight idea whether fun could extend to linorder too.

Any help would be appreciated.

if could give idea to solve below lemma proving would be better

```
datatype 'a rexp =
is_Zero: Zero |
is_One: One |
Sym "'a Predicate.pred"|
Plus "('a rexp)" "('a rexp)" |
Times "('a rexp)" "('a rexp)" |
Star "('a rexp)"
instantiation rexp :: (order) "{order}"
begin
fun le_rexp :: "('a::order) rexp ⇒ ('a::order) rexp ⇒ bool"
where
"le_rexp Zero _ = True"
| "le_rexp _ Zero = False"
| "le_rexp One _ = True"
| "le_rexp _ One = False"
| "le_rexp (Sym a) (Sym b) = (Predicate.eval a ≤ Predicate.eval b)"
| "le_rexp (Sym _) _ = True"
| "le_rexp _ (Sym _) = False"
| "le_rexp (Star r) (Star s) = le_rexp r s"
| "le_rexp (Star _) _ = True"
| "le_rexp _ (Star _) = False"
| "le_rexp (Plus r r') (Plus s s') =
(if r = s then le_rexp r' s' else le_rexp r s)"
| "le_rexp (Plus _ _) _ = True"
| "le_rexp _ (Plus _ _) = False"
| "le_rexp (Times r r') (Times s s') =
(if r = s then le_rexp r' s' else le_rexp r s)"
term "Predicate.eval a"
definition less_eq_rexp where "r ≤ s ≡ le_rexp r s"
definition less_rexp where "r < s ≡ le_rexp r s ∧ r ≠ s"
lemma le_rexp_Zero: "le_rexp r Zero ⟹ r = Zero"
by (induction r) auto
lemma le_rexp_refl: "le_rexp r r"
by (induction r) auto
lemma le_rexp_antisym: "⟦le_rexp r s; le_rexp s r⟧ ⟹ r = s"
apply(induction r s rule: le_rexp.induct)
apply auto
using le_rexp_Zero apply auto[1]
by (simp add: pred.expand)
lemma le_rexp_trans: "⟦le_rexp r s; le_rexp s t⟧ ⟹ le_rexp r t"
proof (induction r s arbitrary: t rule: le_rexp.induct)
fix v t assume "le_rexp (Sym v) t" thus "le_rexp One t" by (cases t) auto
next
fix s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp One t" by (cases t) auto
next
fix s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp One t" by (cases t) auto
next
fix s t assume "le_rexp (Star s) t" thus "le_rexp One t" by (cases t) auto
next
fix v u t assume "le_rexp (Sym v) (Sym u)" "le_rexp (Sym u) t"
thus "le_rexp (Sym v) t" by (cases t) auto
next
fix v s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Sym v) t" by (cases t) auto
next
fix v s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Sym v) t" by (cases t) auto
next
fix v s t assume "le_rexp (Star s) t" thus "le_rexp (Sym v) t" by (cases t) auto
next
fix r s t
assume IH: "⋀t. le_rexp r s ⟹ le_rexp s t ⟹ le_rexp r t"
and "le_rexp (Star r) (Star s)" "le_rexp (Star s) t"
thus "le_rexp (Star r) t" by (cases t) auto
next
fix r s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto
next
fix r s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto
next
fix r1 r2 s1 s2 t
assume "⋀t. r1 = s1 ⟹ le_rexp r2 s2 ⟹ le_rexp s2 t ⟹ le_rexp r2 t"
"⋀t. r1 ≠ s1 ⟹ le_rexp r1 s1 ⟹ le_rexp s1 t ⟹ le_rexp r1 t"
"le_rexp (Plus r1 r2) (Plus s1 s2)" "le_rexp (Plus s1 s2) t"
thus "le_rexp (Plus r1 r2) t" by (cases t) (auto split: if_split_asm intro: le_rexp_antisym)
next
fix r1 r2 s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Plus r1 r2) t" by (cases t) auto
next
fix r1 r2 s1 s2 t
assume "⋀t. r1 = s1 ⟹ le_rexp r2 s2 ⟹ le_rexp s2 t ⟹ le_rexp r2 t"
"⋀t. r1 ≠ s1 ⟹ le_rexp r1 s1 ⟹ le_rexp s1 t ⟹ le_rexp r1 t"
"le_rexp (Times r1 r2) (Times s1 s2)" "le_rexp (Times s1 s2) t"
thus "le_rexp (Times r1 r2) t" by (cases t) (auto split: if_split_asm intro: le_rexp_antisym)
qed auto
instance proof
qed (auto simp add: less_eq_rexp_def less_rexp_def
intro: le_rexp_refl le_rexp_antisym le_rexp_trans)
end
instantiation rexp :: (linorder) "{linorder}"
begin
lemma le_rexp_total: "le_rexp (r :: 'a :: linorder rexp) s ∨ le_rexp s r"
apply (induction r s rule: le_rexp.induct)
apply auto
sorry
instance proof
qed (unfold less_eq_rexp_def less_rexp_def, rule le_rexp_total)
end
```

How to prove the rexp is an instantiation of linorder.

Can you explain to the intuition why you would always have `a <= b \/ b < a`

(in order to have `Sym a <= Sym b`

)?

because that seems far from obvious to me

My intuition is that if you take `a = (%x. even x)`

and `b = (%x. prime x)`

, you are going to have a hard timing finding whether a or b is larger…

but maybe I am missing something in your definition

I am trying to prove the predicate existing relationship of the linorder.

In such a case, I think a might be equal to b, according to the `predicate.eval`

I am not very clear about the relation between the order and linorder. Because like (<) in nat is an order, a < b then a < b or b < a will be always established.

you have a linorder on `'a`

, that does not say anything on having an order on a function

so the question should be recalled back to prove the linorder relation of predicate, whether I could understand in this way

No, the question is: what do you want to prove

and what you want to model

and how

in general, total orders on base elements does not mean anything on a function on those elements

even with lattices, you only get a partial order

okay, I want to implement a symbolic automaton, in which transition is the predicate, thus I include the predicate in the rexp(Sym). And I built on the basic of regular set in afp. When the type of character is nat, it belongs to the linear order. Currently, My theory could not handle such case, that's why I want to prove its linorder.

the original library is built on atom 'a, then linear order holds on

I see the predicate is a complete-lattices, but not linorder.

Wait let's go a step back before going onto the Isabelle part: what does it mean for an automata to have a total order?

or do you want to express the subset relationship on the recognized languages?

I use the method of derivative on regular expression

and it must be built on normal forms, and need some arbitrary total order on regular expressions

The relation \le can be some arbitrary total order on regular expressions. Our concrete definition (omitted) works as follows. Expressions with different constructors at the root are compared according to some arbitrary fixed total order of the constructors. Expressions with the same constructor at the root are compared according to the lexicographic order of the arguments. Atoms are assumed to be totally ordered. More precisely, \le is restricted to regular expressions over natural numbers. cite `Proof Pearl: Regular Expression Equivalence and Relation Algebra`

if you just need a total order, I think that you could ignore most of the Sym problem… something like `Sym a < Sym b`

iff `a 0 < b 0`

but I am not sure at the moment.

what you do not want is working on the function as a function to build an order

Sorry, not understand the final sentence, not very familiar with the function on order.

Why I need a total order or linear order lies on I could verify the bool value, but not for the nat value. So I guess the problem lies on the rexp doesn't support linear. If available, I could email you the project and see where is the problem on.

Last updated: Dec 07 2023 at 20:16 UTC