Email Gateway (Mar 02 2023 at 13:23): Email Gateway (Mar 02 2023 at 13:23):From: Hongjian Jiang <jianghongjian87@gmail.com>
In my project, I try to prove such a lemma:∀q. (∃x∈trans2LTS r v.
single_LTS_reachable_by_path q x) ⟶ q ∈ sem_reg r v ⟹ x ∈ star (trans2LTS r v)
⟹ single_LTS_reachable_by_path q x ⟹ q ∈ star (sem_reg r v)
This is the definition of star:
inductive_set star :: "'v list set ⇒ 'v list set"
for r :: "'v list set" where
zero[intro!]:"[] ∈ star r"|
step[intro!]:"x ∈ r ∧ y ∈ star r ⟹ x @ y ∈ star r"
The definition of semantic :
datatype ('v)regexp = ESet | LChr 'v| Concat "'v regexp" "'v regexp"|
Alter "('v) regexp" "('v) regexp"| Dot|
Star "'v regexp" |(* Plus "('v) regexp" |*) Ques "('v)
regexp" | ε
primrec sem_reg :: "('v) regexp => 'v set⇒ 'v list set" where
"sem_reg ESet v = {[]}"| (Empty Set)
"sem_reg (Dot) vset = (λx .[x]) ` vset" |
"sem_reg (Concat r1 r2) v ={q@p| q p. q ∈ sem_reg r1 v ∧ p ∈ sem_reg r2 v}"|
"sem_reg (LChr a) v = {[a]}"|
"sem_reg (Alter v1 v2) a = (sem_reg v1 a) ∪ (sem_reg v2 a)"|
"sem_reg (Star a) v = star (sem_reg a v)"|
"sem_reg (Ques v) a = {[]} ∪ (sem_reg v a)"|
"sem_reg ε v = {[]}"
The definition of LTS:
fun concat_transition ::"(('v regexp × 'v set × 'v regexp) set * 'v regexp *
'v regexp) list set \<Rightarrow> (('v regexp × 'v set × 'v regexp) set * 'v
regexp * 'v regexp) list set \<Rightarrow> (('v regexp × 'v set × 'v regexp)
set * 'v regexp * 'v regexp) list set" where
"concat_transition lset1 lset2 = {x@y| x y. x\<in> lset1 \<and> y\<in>lset2}"
primrec trans2LTS :: "'v regexp ⇒ 'v set ⇒ (('v regexp × 'v set × 'v regexp)
set * 'v regexp * 'v regexp) list set" where
"trans2LTS (LChr v) alp_set= {[({(LChr v, {v}, \<epsilon>)}, LChr v,
\<epsilon>)]}"|
"trans2LTS (ESet) alp_set= {[({(ESet, {} ,\<epsilon>)},ESet,
\<epsilon>)]}"|
"trans2LTS (\<epsilon>) alp_set = {[({},\<epsilon>,\<epsilon>)]}"|
"trans2LTS (Dot) alp_set = {[({(Dot, alp_set, \<epsilon>)},Dot,
\<epsilon>)]}"|
"trans2LTS (Alter r1 r2) alp_set = trans2LTS r1 alp_set \<union>
trans2LTS r2 alp_set"|
"trans2LTS (Concat r1 r2) alp_set = concat_transition (trans2LTS r1
alp_set) (trans2LTS r2 alp_set)" |
"trans2LTS (Star r) alp_set = star (trans2LTS r alp_set)" |
"trans2LTS (Ques r) alp_set = {[({(Ques r, {}, \<epsilon>)},Ques r,
\<epsilon>)]} \<union> trans2LTS r alp_set"
And the definition of single_LTS_reahchable:
type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"
primrec single_LTS_reachable_by_path :: "'a list ⇒ (('q,'a) LTS * 'q * 'q)
list ⇒ bool " where
"single_LTS_reachable_by_path w []= (w = [])"|
"single_LTS_reachable_by_path w (x# xs) = (∃p q. (w = p @ q ∧ LTS_is_reachable
(fst x) (fst (snd x)) p (snd (snd x)) ∧ single_LTS_reachable_by_path q xs))"
Basically, I try to use star induction help to prove this but failed. An
auxiliary lemma help to prove I think is on the single_LTS_reahchable, like
some function on x, then get the result of the function on w. But I am new
Isabeller and couldn't think about any idea to prove it. Hope anyone could
help me solve it, thx a lot.
Last updated: Apr 24 2024 at 16:18 UTC