--- a/thys/SpecExt.thy Sun Oct 08 14:21:24 2017 +0100
+++ b/thys/SpecExt.thy Tue Oct 10 10:40:44 2017 +0100
@@ -1173,9 +1173,12 @@
\<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (v # vs)"
| Posix_NMTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n; n \<le> m\<rbrakk>
\<Longrightarrow> [] \<in> NMTIMES r n m \<rightarrow> Stars vs"
-| Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v \<noteq> []; n \<le> m;
- \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r n m))\<rbrakk>
- \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)"
+| Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n; n \<le> m;
+ \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))\<rbrakk>
+ \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r n m \<rightarrow> Stars (v # vs)"
+| Posix_NMTIMES3: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < m;
+ \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))\<rbrakk>
+ \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r 0 m \<rightarrow> Stars (v # vs)"
inductive_cases Posix_elims:
"s \<in> ZERO \<rightarrow> v"
@@ -1220,9 +1223,14 @@
apply(rule_tac x="Suc x" in bexI)
apply(auto simp add: Sequ_def)[2]
apply(simp)
- apply(simp)
- by (simp add: Star.step Star_Pow)
-
+ apply(simp)
+ apply(clarify)
+ apply(rule_tac x="Suc x" in bexI)
+ apply(auto simp add: Sequ_def)[2]
+ apply(simp)
+ apply(simp add: Star.step Star_Pow)
+done
+
text {*
Our Posix definition determines a unique value.
*}
@@ -1396,12 +1404,59 @@
ultimately show "Stars (v # vs) = v2" by auto
next
case (Posix_NMTIMES1 s1 r v s2 n m vs v2)
- then show "Stars (v # vs) = v2"
- sorry
+ have "(s1 @ s2) \<in> NMTIMES r n m \<rightarrow> v2"
+ "s1 \<in> r \<rightarrow> v" "s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> Stars vs" "flat v \<noteq> []"
+ "0 < n" "n \<le> m"
+ "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))" by fact+
+ then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'"
+ "s2 \<in> (NMTIMES r (n - 1) (m - 1)) \<rightarrow> (Stars vs')"
+ apply(cases) apply (auto simp add: append_eq_append_conv2)
+ using Posix1(1) Posix1(2) apply blast
+ apply(case_tac n)
+ apply(simp)
+ apply(simp)
+ apply(case_tac m)
+ apply(simp)
+ apply(simp)
+ apply(drule_tac x="va" in meta_spec)
+ apply(drule_tac x="vs" in meta_spec)
+ apply(simp)
+ apply(drule meta_mp)
+ apply (smt L.simps(10) Posix1(1) Posix1(2) Posix_NMTIMES1.hyps(4) UN_E append.right_neutral
+ append_eq_append_conv2 diff_Suc_1 val.inject(5))
+ apply (metis L.simps(10) Posix1(1) UN_E append_Nil2 append_self_conv2)
+ by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append.right_neutral append_Nil)
+ moreover
+ have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+ "\<And>v2. s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+ ultimately show "Stars (v # vs) = v2" by auto
next
case (Posix_NMTIMES2 vs r n m v2)
then show "Stars vs = v2"
- sorry
+ apply(erule_tac Posix_elims)
+ apply(simp)
+ apply(rule List_eq_zipI)
+ apply(auto)
+ apply (meson in_set_zipE)
+ apply (simp add: Posix1(2))
+ apply(erule_tac Posix_elims)
+ apply(auto)
+ apply (simp add: Posix1(2))+
+ done
+next
+ case (Posix_NMTIMES3 s1 r v s2 m vs v2)
+ have "(s1 @ s2) \<in> NMTIMES r 0 m \<rightarrow> v2"
+ "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" "0 < m"
+ "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1 )))" by fact+
+ then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (UPNTIMES r (m - 1)) \<rightarrow> (Stars vs')"
+ apply(cases) apply (auto simp add: append_eq_append_conv2)
+ using Posix1(2) apply blast
+ apply (smt L.simps(7) Posix1(1) UN_E append_eq_append_conv2)
+ by (metis One_nat_def Posix1(1) Posix_NMTIMES3.hyps(7) append.right_neutral append_Nil)
+ moreover
+ have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+ "\<And>v2. s2 \<in> UPNTIMES r (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+ ultimately show "Stars (v # vs) = v2" by auto
qed
@@ -1441,9 +1496,52 @@
apply(simp)
apply(rule Prf.intros)
apply(simp)
+ apply(simp)
+ (* NTIMES *)
+ prefer 4
+ apply(simp)
+ apply(case_tac n)
apply(simp)
+ apply(simp)
+ apply(clarify)
+ apply(rotate_tac 5)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(subst append.simps(2)[symmetric])
+ apply(rule Prf.intros)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 4
+ apply(simp)
+ apply (metis Prf.intros(8) length_removeAll_less less_irrefl_nat removeAll.simps(1) self_append_conv2)
(* NMTIMES *)
- sorry
-
+ apply(simp)
+ apply (metis Prf.intros(11) append_Nil empty_iff list.set(1))
+ apply(simp)
+ apply(clarify)
+ apply(rotate_tac 6)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(subst append.simps(2)[symmetric])
+ apply(rule Prf.intros)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(rule Prf.intros)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(clarify)
+ apply(rotate_tac 6)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(rule Prf.intros)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+done
end
\ No newline at end of file