--- a/thys/Simplifying.thy Mon Sep 10 21:41:54 2018 +0100
+++ b/thys/Simplifying.thy Sun Sep 30 12:02:04 2018 +0100
@@ -32,16 +32,20 @@
| "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)"
| "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"
-(* where is ZERO *)
+
fun simp_SEQ where
"simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"
| "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"
+| "simp_SEQ (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ZERO, undefined)"
+| "simp_SEQ (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (ZERO, undefined)"
| "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"
lemma simp_SEQ_simps[simp]:
"simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2))
else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2))
- else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))"
+ else (if (fst p1 = ZERO) then (ZERO, undefined)
+ else (if (fst p2 = ZERO) then (ZERO, undefined)
+ else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))))"
by (induct p1 p2 rule: simp_SEQ.induct) (auto)
lemma simp_ALT_simps[simp]:
@@ -141,7 +145,8 @@
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
+ | (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)
@@ -183,14 +188,18 @@
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
+ from as have 00: "fst (simp r1) \<noteq> ZERO" "fst (simp r2) \<noteq> ZERO"
+ apply(auto)
+ apply(smt Posix_elims(1) fst_conv)
+ by (smt NONE_NONE(2) Posix_elims(1) fstI)
+ with NONE_NONE 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
+ then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using eqs NONE_NONE 00
by(auto intro: Posix_SEQ)
qed
qed (simp_all)
@@ -230,142 +239,4 @@
qed
qed
-(*
-fun simp2_ALT where
- "simp2_ALT ZERO r2 seen = (r2, seen)"
-| "simp2_ALT r1 ZERO seen = (r1, seen)"
-| "simp2_ALT r1 r2 seen = (ALT r1 r2, seen)"
-
-fun simp2_SEQ where
- "simp2_SEQ ZERO r2 seen = (ZERO, seen)"
-| "simp2_SEQ r1 ZERO seen = (ZERO, seen)"
-| "simp2_SEQ ONE r2 seen = (r2, seen \<union> {r2})"
-| "simp2_SEQ r1 ONE seen = (r1, seen \<union> {r1})"
-| "simp2_SEQ r1 r2 seen = (SEQ r1 r2, seen \<union> {SEQ r1 r2})"
-
-
-
-
-fun
- simp2 :: "rexp \<Rightarrow> rexp set \<Rightarrow> rexp * rexp set"
-where
- "simp2 (ALT r1 r2) seen =
- (let (r1s, seen1) = simp2 r1 seen in
- let (r2s, seen2) = simp2 r2 seen1
- in simp2_ALT r1s r2s seen2)"
-| "simp2 (SEQ r1 r2) seen =
- (let (r1s, _) = simp2 r1 {} in
- let (r2s, _) = simp2 r2 {}
- in if (SEQ r1s r2s \<in> seen) then (ZERO, seen)
- else simp2_SEQ r1s r2s seen)"
-| "simp2 r seen = (if r \<in> seen then (ZERO, seen) else (r, seen \<union> {r}))"
-
-
-lemma simp2_ALT[simp]:
- shows "L (fst (simp2_ALT r1 r2 seen)) = L r1 \<union> L r2"
- apply(induct r1 r2 seen rule: simp2_ALT.induct)
- apply(simp_all)
- done
-
-lemma test1:
- shows "snd (simp2_ALT r1 r2 rs) = rs"
- apply(induct r1 r2 rs rule: simp2_ALT.induct)
- apply(auto)
- done
-
-lemma test2:
- shows "rs \<subseteq> snd (simp2_SEQ r1 r2 rs)"
- apply(induct r1 r2 rs rule: simp2_SEQ.induct)
- apply(auto)
- done
-
-lemma test3:
- shows "rs \<subseteq> snd (simp2 r rs)"
- apply(induct r rs rule: simp2.induct)
- apply(auto split: prod.split)
- apply (metis set_mp test1)
- by (meson set_mp test2)
-
-lemma test3a:
- shows "\<Union>(L ` snd (simp2 r rs)) \<subseteq> L(r) \<union> (\<Union> (L ` rs))"
- apply(induct r rs rule: simp2.induct)
- apply(auto split: prod.split simp add: Sequ_def)
- apply (smt UN_iff Un_iff set_mp test1)
-
-
-lemma test:
- assumes "(\<Union>r' \<in> rs. L r') \<subseteq> L r"
- shows "L(fst (simp2 r rs)) \<subseteq> L(r)"
- using assms
- apply(induct r arbitrary: rs)
- apply(simp only: simp2.simps)
- apply(simp)
- apply(simp only: simp2.simps)
- apply(simp)
- apply(simp only: simp2.simps)
- apply(simp)
- prefer 3
- apply(simp only: simp2.simps)
- apply(simp)
- prefer 2
- apply(simp only: simp2.simps)
- apply(simp)
- apply(subst prod.split)
- apply(rule allI)+
- apply(rule impI)
- apply(subst prod.split)
- apply(rule allI)+
- apply(rule impI)
- apply(simp)
- apply(drule_tac x="rs" in meta_spec)
- apply(simp)
- apply(drule_tac x="x2" in meta_spec)
- apply(simp)
- apply(auto)[1]
- apply(subgoal_tac "rs \<subseteq> x2a")
- prefer 2
- apply (metis order_trans prod.sel(2) test3)
-
-
- apply(rule antisym)
- prefer 2
- apply(simp)
- apply(rule conjI)
- apply(drule meta_mp)
- prefer 2
- apply(simp)
- apply(auto)[1]
- apply(auto)[1]
-
- thm prod.split
- apply(auto split: prod.split)[1]
- apply(drule_tac x="rs" in meta_spec)
- apply(drule_tac x="rs" in meta_spec)
- apply(simp)
- apply(rule_tac x="SEQ x1 x1a" in bexI)
- apply(simp add: Sequ_def)
-
- apply(auto)[1]
- apply(simp)
- apply(subgoal_tac "L (fst (simp2_SEQ x1 x1a rs)) \<subseteq> L x1 \<union> L x1a")
- apply(frule_tac x="{}" in meta_spec)
- apply(rotate_tac 1)
- apply(frule_tac x="{}" in meta_spec)
- apply(simp)
-
-
- apply(rule_tac x="SEQ x1 x1a" in bexI)
- apply(simp add: Sequ_def)
- apply(auto)[1]
- apply(simp)
- using L.simps(2) apply blast
- prefer 3
- apply(simp only: simp2.simps)
- apply(simp)
- using L.simps(3) apply blast
- prefer 2
- apply(simp add: Sequ_def)
- apply(auto)[1]
- oops
-*)
end
\ No newline at end of file