73 by (auto split: prod.split option.split)

    73 by (auto split: prod.split option.split)

    74 

    74 

    75 

    75 

    76 lemma L_fst_simp:

    76 lemma L_fst_simp:

    77   shows "L(r) = L(fst (simp r))"

    77   shows "L(r) = L(fst (simp r))"

    79 by (induct r) (auto)

    78 by (induct r) (auto)

    80 

    79 

    81 lemma Posix_simp:

    80 lemma Posix_simp:

    82   assumes "s \<in> (fst (simp r)) \<rightarrow> v" 

    81   assumes "s \<in> (fst (simp r)) \<rightarrow> v" 

    83   shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"

    82   shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"