302 unused_thms

   302 lemma Posix_flex:

   303   assumes "s2 \<in> (ders s1 r) \<rightarrow> v"

   304   shows "(s1 @ s2) \<in> r \<rightarrow> flex r id s1 v"

   305   using assms

   306   apply(induct s1 arbitrary: r v s2)

   307   apply(simp)

   308   apply(simp)  

   309   apply(drule_tac x="der a r" in meta_spec)

   310   apply(drule_tac x="v" in meta_spec)

   311   apply(drule_tac x="s2" in meta_spec)

   312   apply(simp)

   313   using  Posix_injval

   314   apply(drule_tac Posix_injval)

   315   apply(subst (asm) (5) flex_fun_apply)

   316   apply(simp)

   317   done

   318 

   319 lemma injval_inj:

   320   assumes "\<Turnstile> a : (der c r)" "\<Turnstile> v : (der c r)" "injval r c a = injval r c v" 

   321   shows "a = v"

   322   using  assms

   323   apply(induct r arbitrary: a c v)

   324        apply(auto)

   325   using Prf_elims(1) apply blast

   326   using Prf_elims(1) apply blast

   327      apply(case_tac "c = x")

   328       apply(auto)

   329   using Prf_elims(4) apply auto[1]

   330   using Prf_elims(1) apply blast

   331     prefer 2

   332   apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) val.distinct(25) val.inject(3) val.inject(4))

   333   apply(case_tac "nullable r1")

   334     apply(auto)

   335     apply(erule Prf_elims)

   336      apply(erule Prf_elims)

   337      apply(erule Prf_elims)

   338       apply(erule Prf_elims)

   339       apply(auto)

   340      apply (metis Prf_injval_flat list.distinct(1) mkeps_flat)

   341   apply(erule Prf_elims)

   342      apply(erule Prf_elims)

   343   apply(auto)

   344   using Prf_injval_flat mkeps_flat apply fastforce

   345   apply(erule Prf_elims)

   346      apply(erule Prf_elims)

   347    apply(auto)

   348   apply(erule Prf_elims)

   349      apply(erule Prf_elims)

   350   apply(auto)

   351    apply (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5))

   352   by (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5))

   353   

   354   

   355 

   356 lemma uu:

   357   assumes "(c # s) \<in> r \<rightarrow> injval r c v" "\<Turnstile> v : (der c r)"

   358   shows "s \<in> der c r \<rightarrow> v"

   359   using assms

   360   apply -

   361   apply(subgoal_tac "lexer r (c # s) = Some (injval r c v)")

   362   prefer 2

   363   using lexer_correctness(1) apply blast

   364   apply(simp add: )

   365   apply(case_tac  "lexer (der c r) s")

   366    apply(simp)

   367   apply(simp)

   368   apply(case_tac "s \<in> der c r \<rightarrow> a")

   369    prefer 2

   370    apply (simp add: lexer_correctness(1))

   371   apply(subgoal_tac "\<Turnstile> a : (der c r)")

   372    prefer 2

   373   using Posix_Prf apply blast

   374   using injval_inj by blast

   375   

   376 

   377 lemma Posix_flex2:

   378   assumes "(s1 @ s2) \<in> r \<rightarrow> flex r id s1 v" "\<Turnstile> v : ders s1 r"

   379   shows "s2 \<in> (ders s1 r) \<rightarrow> v"

   380   using assms

   381   apply(induct s1 arbitrary: r v s2 rule: rev_induct)

   382   apply(simp)

   383   apply(simp)  

   384   apply(drule_tac x="r" in meta_spec)

   385   apply(drule_tac x="injval (ders xs r) x v" in meta_spec)

   386   apply(drule_tac x="x#s2" in meta_spec)

   387   apply(simp add: flex_append ders_append)

   388   using Prf_injval uu by blast

   389 

   390 lemma Posix_flex3:

   391   assumes "s1 \<in> r \<rightarrow> flex r id s1 v" "\<Turnstile> v : ders s1 r"

   392   shows "[] \<in> (ders s1 r) \<rightarrow> v"

   393   using assms

   394   by (simp add: Posix_flex2)

   395 

   396 lemma flex_injval:

   397   shows "flex (der a r) (injval r a) s v = injval r a (flex (der a r) id s v)"

   398   by (simp add: flex_fun_apply)

   399   

   400 

   401