problems with leamma proving · General

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)

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"

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 = {[]}"

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"

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.

Stream: General

Topic: problems with leamma proving

Hongjian Jiang (Mar 02 2023 at 11:07):