Hongjian Jiang (Jul 31 2023 at 17:58): Hongjian Jiang (Jul 31 2023 at 17:58):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.
Hongjian Jiang (Jul 31 2023 at 19:16):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.
Mathias Fleury (Jul 31 2023 at 19:35):Can you explain to the intuition why you would always have a <= b \/ b < a (in order to have Sym a <= Sym b)?
Mathias Fleury (Jul 31 2023 at 19:36):because that seems far from obvious to me
Mathias Fleury (Jul 31 2023 at 19:38):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…
Mathias Fleury (Jul 31 2023 at 19:39):but maybe I am missing something in your definition
Hongjian Jiang (Jul 31 2023 at 19:49):I am trying to prove the predicate existing relationship of the linorder.
Hongjian Jiang (Jul 31 2023 at 19:50):In such a case, I think a might be equal to b, according to the predicate.eval
Hongjian Jiang (Jul 31 2023 at 19:52):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.
Mathias Fleury (Jul 31 2023 at 19:57):you have a linorder on 'a, that does not say anything on having an order on a function
Hongjian Jiang (Jul 31 2023 at 20:01):so the question should be recalled back to prove the linorder relation of predicate, whether I could understand in this way
Mathias Fleury (Jul 31 2023 at 20:02):No, the question is: what do you want to prove
Mathias Fleury (Jul 31 2023 at 20:02):and what you want to model
Mathias Fleury (Jul 31 2023 at 20:02):and how
Mathias Fleury (Jul 31 2023 at 20:05):in general, total orders on base elements does not mean anything on a function on those elements
Mathias Fleury (Jul 31 2023 at 20:05):even with lattices, you only get a partial order
Hongjian Jiang (Jul 31 2023 at 20:07):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.
Hongjian Jiang (Jul 31 2023 at 20:08):the original library is built on atom 'a, then linear order holds on
Hongjian Jiang (Jul 31 2023 at 20:09):I see the predicate is a complete-lattices, but not linorder.
Mathias Fleury (Jul 31 2023 at 20:14):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?
Mathias Fleury (Jul 31 2023 at 20:16):or do you want to express the subset relationship on the recognized languages?
Hongjian Jiang (Jul 31 2023 at 20:16):I use the method of derivative on regular expression
Hongjian Jiang (Jul 31 2023 at 20:18):and it must be built on normal forms, and need some arbitrary total order on regular expressions
Hongjian Jiang (Jul 31 2023 at 20:20):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
Mathias Fleury (Jul 31 2023 at 20:27):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
Mathias Fleury (Jul 31 2023 at 20:28):but I am not sure at the moment.
Mathias Fleury (Jul 31 2023 at 20:28):what you do not want is working on the function as a function to build an order
Hongjian Jiang (Jul 31 2023 at 20:33):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: Apr 27 2024 at 20:14 UTC