--- a/thys/LexerExt.thy Sat Oct 07 22:16:16 2017 +0100
+++ b/thys/LexerExt.thy Sun Oct 08 14:21:24 2017 +0100
@@ -170,7 +170,6 @@
apply(simp add: Prf_injval_flat)
apply(simp)
apply(simp)
- using Prf.intros(10) Prf_injval_flat apply auto
done
@@ -190,15 +189,6 @@
apply(auto)
done
-lemma test:
- assumes "s \<in> der c (FROMNTIMES r 0) \<rightarrow> v"
- shows "XXX"
-using assms
- apply(simp)
- apply(erule Posix_elims)
- apply(drule FROMNTIMES_0)
- apply(auto)
-oops
lemma Posix_injval:
assumes "s \<in> (der c r) \<rightarrow> v"
@@ -454,18 +444,15 @@
"v = Seq v1 (Stars vs)" "s = s1 @ s2"
"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs)" "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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r (n - 1)))"
- | (null) v1 where
- "v = Seq v1 (Stars [])"
- "s \<in> der c r \<rightarrow> v1" "[] \<in> (FROMNTIMES r 0) \<rightarrow> (Stars [])" "n = 0"
+ | (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 *)
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(case_tac "n = 0")
- apply(simp)
- apply(drule FROMNTIMES_0)
- apply(simp)
- using FROMNTIMES_0 Posix_mkeps apply force
apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
apply(clarify)
apply(drule_tac x="v1" in meta_spec)
@@ -473,13 +460,22 @@
apply(drule_tac x="s1" in meta_spec)
apply(drule_tac x="s2" in meta_spec)
apply(simp add: der_correctness Der_def)
- apply(case_tac "n = 0")
- apply(simp)
- apply(simp)
- apply(rotate_tac 4)
+ apply(rotate_tac 5)
apply(erule Posix_elims)
apply(auto)[2]
- done
+ 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> (FROMNTIMES r n) \<rightarrow> injval (FROMNTIMES r n) c v"
proof (cases)
case cons
@@ -508,27 +504,27 @@
then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp)
next
case null
- have "s \<in> der c r \<rightarrow> v1" by fact
- then have "(c # s) \<in> r \<rightarrow> injval r c v1" using IH by simp
- moreover
- have "[] \<in> (FROMNTIMES r 0) \<rightarrow> Stars []" by fact
- moreover
- have "(c # s) \<in> r \<rightarrow> injval r c v1" by fact
- then have "flat (injval r c v1) = (c # s)" by (rule Posix1)
+ 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> STAR r \<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 (STAR r))" 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 (STAR r))"
+ by (simp add: der_correctness Der_def)
ultimately
- have "((c # s) @ []) \<in> FROMNTIMES r 1 \<rightarrow> Stars [injval r c v1]"
- apply (rule_tac Posix.intros)
- apply(simp_all)
+ have "((c # s1) @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (injval r c v1 # vs)"
+ apply (rule_tac Posix.intros) back
+ apply(simp_all)
done
then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null
apply(simp)
- apply(erule Posix_elims)
- apply(auto)
- apply(rotate_tac 6)
- apply(drule FROMNTIMES_0)
- apply(simp)
- sorry
+ done
qed
next
case (NMTIMES x1 x2 m s v)
--- a/thys/PositionsExt.thy Sat Oct 07 22:16:16 2017 +0100
+++ b/thys/PositionsExt.thy Sun Oct 08 14:21:24 2017 +0100
@@ -889,7 +889,55 @@
then show "Stars (v # vs) :\<sqsubseteq>val v3"
unfolding PosOrd_ex_eq_def using cond2
by (simp add: PosOrd_shorterI)
- qed
+ qed
+next
+ case (Posix_FROMNTIMES3 s1 r v s2 vs v3)
+ have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<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 (STAR r) 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 (STAR r))" by fact
+ have cond2: "flat v \<noteq> []" by fact
+ have "v3 \<in> LV (FROMNTIMES r 0) (s1 @ s2)" by fact
+ then consider
+ (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
+ "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
+ "flat (Stars (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)
+ done
+ then show "Stars (v # vs) :\<sqsubseteq>val v3"
+ proof (cases)
+ case (NonEmpty v3a vs3)
+ have "flat (Stars (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))
+ 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 (STAR r) 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_NMTIMES2 vs r n m v2)
then show "Stars vs :\<sqsubseteq>val v2" sorry
--- 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