1150 L5: "nullable(r1) \<longrightarrow> s2 \<in> L(der c r2) \<longrightarrow> PC32 s2 (SEQ (der c r1) r2) (der c r2) \<longrightarrow> PC42 [] (c#s2) r1 r2" and |
1150 L5: "nullable(r1) \<longrightarrow> s2 \<in> L(der c r2) \<longrightarrow> PC32 s2 (SEQ (der c r1) r2) (der c r2) \<longrightarrow> PC42 [] (c#s2) r1 r2" and |
1151 L6: "s0 \<in> L(der c r0) \<longrightarrow> s \<in> L(STAR r0) \<longrightarrow> PC42 s0 s (der c r0) (STAR r0) \<longrightarrow> PC42 (c#s0) s r0 (STAR r0)" and |
1151 L6: "s0 \<in> L(der c r0) \<longrightarrow> s \<in> L(STAR r0) \<longrightarrow> PC42 s0 s (der c r0) (STAR r0) \<longrightarrow> PC42 (c#s0) s r0 (STAR r0)" and |
1152 L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC32 s' r r'" and |
1152 L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC32 s' r r'" and |
1153 L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow> x \<noteq> [] \<longrightarrow> \<not>PC42 s s' r r'" |
1153 L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow> x \<noteq> [] \<longrightarrow> \<not>PC42 s s' r r'" |
1154 apply(auto simp add: PC32_def PC42_def)[1] |
1154 apply(auto simp add: PC32_def PC42_def)[1] |
|
1155 apply(simp add: Sequ_def) |
|
1156 apply (metis nullable_correctness) |
|
1157 apply(auto simp add: PC32_def PC42_def Sequ_def)[1] |
|
1158 apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1] |
|
1159 apply(simp add: Cons_eq_append_conv) |
|
1160 apply(auto)[1] |
|
1161 defer |
|
1162 apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1] |
|
1163 apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def nullable_correctness)[1] |
|
1164 apply (metis append_Cons append_assoc hd_Cons_tl list.discI list.inject) |
|
1165 apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1] |
|
1166 apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1] |
|
1167 apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1] |
1155 oops |
1168 oops |
1156 |
1169 |
1157 definition |
1170 definition |
1158 PC33 :: "string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool" |
1171 PC33 :: "string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool" |
1159 where |
1172 where |
1661 apply(simp) |
1674 apply(simp) |
1662 apply(auto) |
1675 apply(auto) |
1663 apply(drule_tac x="Seq (projval r1 c v) vb" in spec) |
1676 apply(drule_tac x="Seq (projval r1 c v) vb" in spec) |
1664 apply(drule mp) |
1677 apply(drule mp) |
1665 apply(simp) |
1678 apply(simp) |
|
1679 |
1666 apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2) |
1680 apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2) |
1667 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1") |
1681 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1") |
1668 apply (metis NPrf_imp_Prf Prf.intros(1)) |
1682 apply (metis NPrf_imp_Prf Prf.intros(1)) |
1669 apply(rule NPrf_imp_Prf) |
1683 apply(rule NPrf_imp_Prf) |
1670 apply(rule v3_proj) |
1684 apply(rule v3_proj) |