--- a/thys/Simplifying.thy Mon May 16 15:20:23 2016 +0100
+++ b/thys/Simplifying.thy Tue May 17 03:47:33 2016 +0100
@@ -82,29 +82,118 @@
assumes "s \<in> (fst (simp r)) \<rightarrow> v"
shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"
using assms
-apply(induct r arbitrary: s v rule: simp.induct)
-apply(simp_all)
-apply(auto)[1]
-using Posix_elims(1) apply blast
-apply (simp add: Posix_ALT1)
-apply (metis L.simps(1) L_fst_simp Posix_ALT2 empty_iff)
-apply (smt F_ALT.simps(1) F_ALT.simps(2) L_fst_simp Posix_ALT1 Posix_ALT2 Posix_elims(4))
-apply(auto)[1]
-apply (metis (no_types, lifting) Nil_is_append_conv Posix_SEQ Posix_elims(2))
-apply(subst append_Nil2[symmetric])
-apply(rule Posix_SEQ)
-apply(simp)
-using Posix_ONE apply blast
-apply blast
-apply(subst append_Nil[symmetric])
-apply(rule Posix_SEQ)
-using Posix_ONE apply blast
-apply blast
-apply(auto)[1]
-apply (metis L.simps(2) L_fst_simp ex_in_conv insert_iff)
-apply(erule Posix_elims)
-apply(auto)
-using L_fst_simp Posix_SEQ by auto
+proof(induct r arbitrary: s v rule: rexp.induct)
+ case (ALT r1 r2 s v)
+ have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact
+ have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact
+ have as: "s \<in> fst (simp (ALT r1 r2)) \<rightarrow> v" by fact
+ consider (ZERO_ZERO) "fst (simp r1) = ZERO" "fst (simp r2) = ZERO"
+ | (ZERO_NZERO) "fst (simp r1) = ZERO" "fst (simp r2) \<noteq> ZERO"
+ | (NZERO_ZERO) "fst (simp r1) \<noteq> ZERO" "fst (simp r2) = ZERO"
+ | (NZERO_NZERO) "fst (simp r1) \<noteq> ZERO" "fst (simp r2) \<noteq> ZERO" by auto
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v"
+ proof(cases)
+ case (ZERO_ZERO)
+ with as have "s \<in> ZERO \<rightarrow> v" by simp
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" by (rule Posix_elims(1))
+ next
+ case (ZERO_NZERO)
+ with as have "s \<in> fst (simp r2) \<rightarrow> v" by simp
+ with IH2 have "s \<in> r2 \<rightarrow> snd (simp r2) v" by simp
+ moreover
+ from ZERO_NZERO have "fst (simp r1) = ZERO" by simp
+ then have "L (fst (simp r1)) = {}" by simp
+ then have "L r1 = {}" using L_fst_simp by simp
+ then have "s \<notin> L r1" by simp
+ ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right (snd (simp r2) v)" by (rule Posix_ALT2)
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v"
+ using ZERO_NZERO by simp
+ next
+ case (NZERO_ZERO)
+ with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp
+ with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp
+ then have "s \<in> ALT r1 r2 \<rightarrow> Left (snd (simp r1) v)" by (rule Posix_ALT1)
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_ZERO by simp
+ next
+ case (NZERO_NZERO)
+ with as have "s \<in> ALT (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp
+ then consider (Left) v1 where "v = Left v1" "s \<in> (fst (simp r1)) \<rightarrow> v1"
+ | (Right) v2 where "v = Right v2" "s \<in> (fst (simp r2)) \<rightarrow> v2" "s \<notin> L (fst (simp r1))"
+ by (erule_tac Posix_elims(4))
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v"
+ proof(cases)
+ case (Left)
+ then have "v = Left v1" "s \<in> r1 \<rightarrow> (snd (simp r1) v1)" using IH1 by simp_all
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_NZERO
+ by (simp_all add: Posix_ALT1)
+ next
+ case (Right)
+ then have "v = Right v2" "s \<in> r2 \<rightarrow> (snd (simp r2) v2)" "s \<notin> L r1" using IH2 L_fst_simp by simp_all
+ then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_NZERO
+ by (simp_all add: Posix_ALT2)
+ qed
+ qed
+next
+ case (SEQ r1 r2 s v)
+ have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact
+ have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact
+ have as: "s \<in> fst (simp (SEQ r1 r2)) \<rightarrow> v" by fact
+ consider (ONE_ONE) "fst (simp r1) = ONE" "fst (simp r2) = ONE"
+ | (ONE_NONE) "fst (simp r1) = ONE" "fst (simp r2) \<noteq> ONE"
+ | (NONE_ONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) = ONE"
+ | (NONE_NONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) \<noteq> ONE" by auto
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v"
+ proof(cases)
+ case (ONE_ONE)
+ with as have b: "s \<in> ONE \<rightarrow> v" by simp
+ from b have "s \<in> r1 \<rightarrow> snd (simp r1) v" using IH1 ONE_ONE by simp
+ moreover
+ from b have c: "s = []" "v = Void" using Posix_elims(2) by auto
+ moreover
+ have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE)
+ then have "[] \<in> fst (simp r2) \<rightarrow> Void" using ONE_ONE by simp
+ then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp
+ ultimately have "([] @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) Void)"
+ using Posix_SEQ by blast
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using c ONE_ONE by simp
+ next
+ case (ONE_NONE)
+ with as have b: "s \<in> fst (simp r2) \<rightarrow> v" by simp
+ from b have "s \<in> r2 \<rightarrow> snd (simp r2) v" using IH2 ONE_NONE by simp
+ moreover
+ have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE)
+ then have "[] \<in> fst (simp r1) \<rightarrow> Void" using ONE_NONE by simp
+ then have "[] \<in> r1 \<rightarrow> snd (simp r1) Void" using IH1 by simp
+ moreover
+ from ONE_NONE(1) have "L (fst (simp r1)) = {[]}" by simp
+ then have "L r1 = {[]}" by (simp add: L_fst_simp[symmetric])
+ ultimately have "([] @ s) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) v)"
+ by(rule_tac Posix_SEQ) auto
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using ONE_NONE by simp
+ next
+ case (NONE_ONE)
+ with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp
+ with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp
+ moreover
+ have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE)
+ then have "[] \<in> fst (simp r2) \<rightarrow> Void" using NONE_ONE by simp
+ then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp
+ ultimately have "(s @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) v) (snd (simp r2) Void)"
+ by(rule_tac Posix_SEQ) auto
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using NONE_ONE by simp
+ next
+ case (NONE_NONE)
+ with as have "s \<in> SEQ (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp
+ then obtain s1 s2 v1 v2 where eqs: "s = s1 @ s2" "v = Seq v1 v2"
+ "s1 \<in> (fst (simp r1)) \<rightarrow> v1" "s2 \<in> (fst (simp r2)) \<rightarrow> v2"
+ "\<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 r1 \<and> s\<^sub>4 \<in> L r2)"
+ by (erule_tac Posix_elims(5)) (auto simp add: L_fst_simp[symmetric])
+ then have "s1 \<in> r1 \<rightarrow> (snd (simp r1) v1)" "s2 \<in> r2 \<rightarrow> (snd (simp r2) v2)"
+ using IH1 IH2 by auto
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using eqs NONE_NONE
+ by(auto intro: Posix_SEQ)
+ qed
+qed (simp_all)
lemma slexer_correctness: