--- a/thys/SpecExt.thy Sat Oct 07 22:16:16 2017 +0100
+++ b/thys/SpecExt.thy Sun Oct 08 14:21:24 2017 +0100
@@ -272,7 +272,10 @@
| "der c (STAR r) = SEQ (der c r) (STAR r)"
| "der c (UPNTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (UPNTIMES r (n - 1)))"
| "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))"
-| "der c (FROMNTIMES r n) = SEQ (der c r) (FROMNTIMES r (n - 1))"
+| "der c (FROMNTIMES r n) =
+ (if n = 0
+ then SEQ (der c r) (STAR r)
+ else SEQ (der c r) (FROMNTIMES r (n - 1)))"
| "der c (NMTIMES r n m) =
(if m < n then ZERO
else (if n = 0 then (if m = 0 then ZERO else
@@ -314,6 +317,8 @@
apply(simp)
(* FROMNTIMES *)
apply(simp add: nullable_correctness del: Der_UNION)
+ apply(rule conjI)
+prefer 2
apply(subst Sequ_Union_in)
apply(subst Der_Pow_Sequ[symmetric])
apply(subst Pow.simps[symmetric])
@@ -322,12 +327,10 @@
apply(subst Pow_Sequ_Un2)
apply(simp)
apply(simp)
-apply(auto simp add: Sequ_def Der_def)[1]
-apply(rule_tac x="Suc xa" in exI)
-apply(auto simp add: Sequ_def)[1]
-apply(drule Pow_decomp)
-apply(auto)[1]
- apply (metis append_Cons)
+ apply(auto simp add: Sequ_def Der_def)[1]
+ apply(auto simp add: Sequ_def split: if_splits)[1]
+ using Star_Pow apply fastforce
+ using Pow_Star apply blast
(* NMTIMES *)
apply(simp add: nullable_correctness del: Der_UNION)
apply(rule impI)
@@ -1165,6 +1168,9 @@
| Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n;
\<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 (FROMNTIMES r (n - 1)))\<rbrakk>
\<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> Stars (v # vs)"
+| Posix_FROMNTIMES3: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
+ \<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 (STAR r))\<rbrakk>
+ \<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;
@@ -1205,6 +1211,7 @@
apply(rule_tac x="Suc x" in bexI)
apply(simp add: Sequ_def)
apply(auto)[3]
+ defer
apply(simp)
apply fastforce
apply(simp)
@@ -1213,7 +1220,8 @@
apply(rule_tac x="Suc x" in bexI)
apply(auto simp add: Sequ_def)[2]
apply(simp)
-done
+ apply(simp)
+ by (simp add: Star.step Star_Pow)
text {*
Our Posix definition determines a unique value.
@@ -1343,22 +1351,21 @@
next
case (Posix_FROMNTIMES1 s1 r v s2 n vs v2)
have "(s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> v2"
- "s1 \<in> r \<rightarrow> v" "s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []"
+ "s1 \<in> r \<rightarrow> v" "s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" "0 < n"
"\<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 (FROMNTIMES r (n - 1 )))" by fact+
then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs')"
apply(cases) apply (auto simp add: append_eq_append_conv2)
using Posix1(1) Posix1(2) apply blast
- apply(drule_tac x="v" in meta_spec)
- apply(drule_tac x="vs" in meta_spec)
- apply(simp)
- apply(drule meta_mp)
apply(case_tac n)
apply(simp)
- apply(rule conjI)
- apply (smt L.simps(9) One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps Suc_mono Suc_pred UN_E append.right_neutral append_Nil lessI less_antisym list.size(3) nat.simps(3) neq0_conv not_less_eq val.inject(5))
- apply(rule List_eq_zipI)
- apply(auto)[1]
- sorry
+ 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 (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil diff_Suc_1 local.Posix_FROMNTIMES1(4) val.inject(5))
+ apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil)
+ by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) self_append_conv self_append_conv2)
moreover
have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
"\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1370,9 +1377,24 @@
apply(auto)
apply(rule List_eq_zipI)
apply(auto)
- apply(meson in_set_zipE)
- by (simp add: Posix1(2))
+ apply(meson in_set_zipE)
+ apply (simp add: Posix1(2))
+ using Posix1(2) by blast
next
+ case (Posix_FROMNTIMES3 s1 r v s2 vs v2)
+ have "(s1 @ s2) \<in> FROMNTIMES r 0 \<rightarrow> v2"
+ "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []"
+ "\<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 (STAR r))" by fact+
+ then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')"
+ apply(cases) apply (auto simp add: append_eq_append_conv2)
+ using Posix1(2) apply fastforce
+ using Posix1(1) apply fastforce
+ by (metis Posix1(1) Posix_FROMNTIMES3.hyps(6) append.right_neutral append_Nil)
+ moreover
+ have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+ "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+ 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
@@ -1397,55 +1419,31 @@
defer
apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2]
apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq)
- prefer 4
- apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[1]
- apply(subst append.simps(2)[symmetric])
- apply(rule Prf.intros)
- apply(auto)
- prefer 4
- apply (metis Prf.intros(8) append_Nil empty_iff list.set(1))
- apply(erule Posix_elims)
- apply(auto)
- apply(rule_tac t="v # vsa" and s = "[v] @ vsa" in subst)
- apply(simp)
- apply(rule Prf.intros)
- apply(simp)
- apply(auto)[1]
- apply(auto simp add: Sequ_def intro: Prf.intros elim: Prf_elims)[1]
- apply(simp)
- apply(rotate_tac 4)
- apply(erule Prf_elims)
- apply(auto)
- apply(case_tac n)
- apply(simp)
-
+ apply(simp)
+ apply(clarify)
+ apply(case_tac n)
+ apply(simp)
+ apply(simp)
+ apply(erule Prf_elims)
+ apply(simp)
apply(subst append.simps(2)[symmetric])
- apply(rule Prf.intros)
- apply(auto)
- apply(rule Prf.intros(10))
- apply(auto)
- apply (metis Prf.intros(11) append_Nil empty_iff list.set(1))
- apply(rotate_tac 6)
- apply(erule Prf_elims)
- apply(simp)
- apply(subst append.simps(2)[symmetric])
- apply(rule Prf.intros)
- apply(auto)
- apply(rule_tac t="v # vsa" and s = "(v # vsa) @ []" in subst)
- apply(simp)
- apply(simp add: Prf.intros(12))
- done
+ apply(rule Prf.intros)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(rule Prf.intros)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(clarify)
+ apply(erule Prf_elims)
+ apply(simp)
+ apply(rule Prf.intros)
+ apply(simp)
+ apply(simp)
+ (* NMTIMES *)
+ sorry
-lemma FROMNTIMES_0:
- assumes "s \<in> FROMNTIMES r 0 \<rightarrow> v"
- shows "s = [] \<and> v = Stars []"
- using assms
- apply(erule_tac Posix_elims)
- apply(auto)
- done
-
-lemma FROMNTIMES_der_0:
- shows "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)"
-by(simp)
end
\ No newline at end of file