--- a/thys/LexerExt.thy Sun Oct 08 14:21:24 2017 +0100
+++ b/thys/LexerExt.thy Tue Oct 10 10:40:44 2017 +0100
@@ -447,8 +447,7 @@
| (null) v1 vs s1 s2 where
"v = Seq v1 (Stars vs)" "s = s1 @ s2" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"
"s1 \<in> der c r \<rightarrow> v1" "n = 0"
- "\<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 (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"
- (* here *)
+ "\<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 (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"
apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
prefer 2
apply(erule Posix_elims)
@@ -527,11 +526,100 @@
done
qed
next
- case (NMTIMES x1 x2 m s v)
- then show ?case sorry
+ case (NMTIMES r n m s v)
+ have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+ have "s \<in> der c (NMTIMES r n m) \<rightarrow> v" by fact
+ then consider
+ (cons) v1 vs s1 s2 where
+ "v = Seq v1 (Stars vs)" "s = s1 @ s2"
+ "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NMTIMES r (n - 1) (m - 1)) \<rightarrow> (Stars vs)" "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 (der c r) \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))"
+ | (null) v1 vs s1 s2 where
+ "v = Seq v1 (Stars vs)" "s = s1 @ s2" "s2 \<in> (UPNTIMES r (m - 1)) \<rightarrow> (Stars vs)"
+ "s1 \<in> der c r \<rightarrow> v1" "n = 0" "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 (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))"
+ apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
+ prefer 2
+ apply(erule Posix_elims)
+ apply(simp)
+ apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+ apply(clarify)
+ apply(drule_tac x="v1" in meta_spec)
+ apply(drule_tac x="vss" in meta_spec)
+ apply(drule_tac x="s1" in meta_spec)
+ apply(drule_tac x="s2" in meta_spec)
+ apply(simp add: der_correctness Der_def)
+ apply(rotate_tac 5)
+ apply(erule Posix_elims)
+ apply(auto)[2]
+ apply(erule Posix_elims)
+ apply(simp)
+ apply blast
+
+ apply(erule Posix_elims)
+ apply(auto)
+ apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
+ apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+ apply(clarify)
+ apply simp
+ apply(rotate_tac 6)
+ apply(erule Posix_elims)
+ apply(auto)[2]
+ done
+ then show "(c # s) \<in> (NMTIMES r n m) \<rightarrow> injval (NMTIMES r n m) c v"
+ proof (cases)
+ case cons
+ have "s1 \<in> der c r \<rightarrow> v1" by fact
+ then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ moreover
+ have "s2 \<in> (NMTIMES r (n - 1) (m - 1)) \<rightarrow> Stars vs" by fact
+ moreover
+ have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
+ then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+ then have "flat (injval r c v1) \<noteq> []" by simp
+ moreover
+ have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))" by fact
+ then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))"
+ by (simp add: der_correctness Der_def)
+ ultimately
+ have "((c # s1) @ s2) \<in> NMTIMES r n m \<rightarrow> Stars (injval r c v1 # vs)"
+ apply (rule_tac Posix.intros)
+ apply(simp_all)
+ apply(case_tac n)
+ apply(simp)
+ using Posix_elims(1) NMTIMES.prems apply auto[1]
+ using cons(5) apply blast
+ apply(simp)
+ apply(rule cons)
+ done
+ then show "(c # s) \<in> NMTIMES r n m \<rightarrow> injval (NMTIMES r n m) c v" using cons by(simp)
+ next
+ case null
+ have "s1 \<in> der c r \<rightarrow> v1" by fact
+ then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+ moreover
+ have "s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs" by fact
+ moreover
+ have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
+ then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
+ then have "flat (injval r c v1) \<noteq> []" by simp
+ moreover
+ moreover
+ have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))" by fact
+ then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))"
+ by (simp add: der_correctness Der_def)
+ ultimately
+ have "((c # s1) @ s2) \<in> NMTIMES r 0 m \<rightarrow> Stars (injval r c v1 # vs)"
+ apply (rule_tac Posix.intros) back
+ apply(simp_all)
+ apply(rule null)
+ done
+ then show "(c # s) \<in> NMTIMES r n m \<rightarrow> injval (NMTIMES r n m) c v" using null
+ apply(simp)
+ done
+ qed
qed
-
section {* Lexer Correctness *}
lemma lexer_correct_None:
--- a/thys/PositionsExt.thy Sun Oct 08 14:21:24 2017 +0100
+++ b/thys/PositionsExt.thy Tue Oct 10 10:40:44 2017 +0100
@@ -940,10 +940,123 @@
qed
next
case (Posix_NMTIMES2 vs r n m v2)
- then show "Stars vs :\<sqsubseteq>val v2" sorry
+ then show "Stars vs :\<sqsubseteq>val v2"
+ apply(auto simp add: LV_def)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(rule PosOrd_eq_Stars_zipI)
+ apply(auto)
+ apply (meson in_set_zipE)
+ by (metis Posix1(2) flats_empty)
next
- case (Posix_NMTIMES1 s1 r v s2 n m vs v2)
- then show "Stars (v # vs) :\<sqsubseteq>val v2" sorry
+ case (Posix_NMTIMES1 s1 r v s2 n m vs v3)
+ have "s1 \<in> r \<rightarrow> v" "s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> Stars vs" by fact+
+ then have as1: "s1 = flat v" "s2 = flats vs" by (auto dest: Posix1(2))
+ have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
+ have IH2: "\<And>v3. v3 \<in> LV (NMTIMES r (n - 1) (m - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+ have cond: "\<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
+ have cond2: "flat v \<noteq> []" by fact
+ have "v3 \<in> LV (NMTIMES r n m) (s1 @ s2)" by fact
+ then consider
+ (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
+ "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : NMTIMES r (n - 1) (m - 1)"
+ "flats (v3a # vs3) = s1 @ s2"
+ | (Empty) "v3 = Stars []"
+ unfolding LV_def
+ apply(auto)
+ apply(erule Prf.cases)
+ apply(auto)
+ apply(case_tac n)
+ apply(auto intro: Prf.intros)
+ apply(case_tac vs1)
+ apply(auto intro: Prf.intros)
+ apply (simp add: as1(1) cond2 flats_empty)
+ apply (simp add: Prf.intros(11))
+ apply(case_tac n)
+ apply(simp)
+ using Posix_NMTIMES1.hyps(6) apply blast
+ apply(simp)
+ apply(case_tac vs)
+ apply(auto)
+ by (simp add: Prf.intros(12))
+ then show "Stars (v # vs) :\<sqsubseteq>val v3"
+ proof (cases)
+ case (NonEmpty v3a vs3)
+ have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) .
+ with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
+ unfolding prefix_list_def
+ by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7) flat_Stars)
+ then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
+ by (simp add: sprefix_list_def append_eq_conv_conj)
+ then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)"
+ using PosOrd_spreI as1(1) NonEmpty(4) by blast
+ then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (NMTIMES r (n - 1) (m - 1)) s2)"
+ using NonEmpty(2,3) by (auto simp add: LV_def)
+ then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
+ then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)"
+ unfolding PosOrd_ex_eq_def by auto
+ then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
+ unfolding PosOrd_ex_eq_def
+ using PosOrd_StarsI PosOrd_StarsI2 by auto
+ then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
+ next
+ case Empty
+ have "v3 = Stars []" by fact
+ then show "Stars (v # vs) :\<sqsubseteq>val v3"
+ unfolding PosOrd_ex_eq_def using cond2
+ by (simp add: PosOrd_shorterI)
+ qed
+next
+ case (Posix_NMTIMES3 s1 r v s2 m vs v3)
+ have "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs" by fact+
+ then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
+ have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
+ have IH2: "\<And>v3. v3 \<in> LV (UPNTIMES r (m - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+ have cond: "\<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
+ have cond2: "flat v \<noteq> []" by fact
+ have "v3 \<in> LV (NMTIMES r 0 m) (s1 @ s2)" by fact
+ then consider
+ (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
+ "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : UPNTIMES r (m - 1)"
+ "flats (v3a # vs3) = s1 @ s2"
+ | (Empty) "v3 = Stars []"
+ unfolding LV_def
+ apply(auto)
+ apply(erule Prf.cases)
+ apply(auto)
+ apply(case_tac vs)
+ apply(auto intro: Prf.intros)
+ by (simp add: Prf.intros(7) as1(1) cond2)
+ then show "Stars (v # vs) :\<sqsubseteq>val v3"
+ proof (cases)
+ case (NonEmpty v3a vs3)
+ have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) .
+ with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
+ unfolding prefix_list_def
+ apply(simp)
+ apply(simp add: append_eq_append_conv2)
+ apply(auto)
+ by (metis L_flat_Prf1 One_nat_def cond flat_Stars)
+ then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
+ by (simp add: sprefix_list_def append_eq_conv_conj)
+ then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)"
+ using PosOrd_spreI as1(1) NonEmpty(4) by blast
+ then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (UPNTIMES r (m - 1)) s2)"
+ using NonEmpty(2,3) by (auto simp add: LV_def)
+ then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
+ then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)"
+ unfolding PosOrd_ex_eq_def by auto
+ then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
+ unfolding PosOrd_ex_eq_def
+ using PosOrd_StarsI PosOrd_StarsI2 by auto
+ then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
+ next
+ case Empty
+ have "v3 = Stars []" by fact
+ then show "Stars (v # vs) :\<sqsubseteq>val v3"
+ unfolding PosOrd_ex_eq_def using cond2
+ by (simp add: PosOrd_shorterI)
+ qed
qed
--- a/thys/ROOT Sun Oct 08 14:21:24 2017 +0100
+++ b/thys/ROOT Tue Oct 10 10:40:44 2017 +0100
@@ -1,11 +1,13 @@
session "Lex" = HOL +
theories [document = false]
"Spec"
+ "SpecExt"
"Lexer"
"LexerExt"
"Simplifying"
(*"Sulzmann"*)
"Positions"
+ "PositionsExt"
"Exercises"
session Paper in "Paper" = Lex +
--- 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