diff -r d688a01b8f89 -r 1a4e5b94293b thys/Simplifying.thy --- 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) \ ONE" | (NONE_ONE) "fst (simp r1) \ ONE" "fst (simp r2) = ONE" - | (NONE_NONE) "fst (simp r1) \ ONE" "fst (simp r2) \ ONE" by auto + | (NONE_NONE) "fst (simp r1) \ ONE" "fst (simp r2) \ ONE" + by auto then show "s \ SEQ r1 r2 \ snd (simp (SEQ r1 r2)) v" proof(cases) case (ONE_ONE) @@ -183,14 +188,18 @@ then show "s \ SEQ r1 r2 \ snd (simp (SEQ r1 r2)) v" using NONE_ONE by simp next case (NONE_NONE) - with as have "s \ SEQ (fst (simp r1)) (fst (simp r2)) \ v" by simp + from as have 00: "fst (simp r1) \ ZERO" "fst (simp r2) \ 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 \ SEQ (fst (simp r1)) (fst (simp r2)) \ v" by simp then obtain s1 s2 v1 v2 where eqs: "s = s1 @ s2" "v = Seq v1 v2" "s1 \ (fst (simp r1)) \ v1" "s2 \ (fst (simp r2)) \ v2" "\ (\s\<^sub>3 s\<^sub>4. s\<^sub>3 \ [] \ s\<^sub>3 @ s\<^sub>4 = s2 \ s1 @ s\<^sub>3 \ L r1 \ s\<^sub>4 \ L r2)" by (erule_tac Posix_elims(5)) (auto simp add: L_fst_simp[symmetric]) then have "s1 \ r1 \ (snd (simp r1) v1)" "s2 \ r2 \ (snd (simp r2) v2)" using IH1 IH2 by auto - then show "s \ SEQ r1 r2 \ snd (simp (SEQ r1 r2)) v" using eqs NONE_NONE + then show "s \ SEQ r1 r2 \ 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 \ {r2})" -| "simp2_SEQ r1 ONE seen = (r1, seen \ {r1})" -| "simp2_SEQ r1 r2 seen = (SEQ r1 r2, seen \ {SEQ r1 r2})" - - - - -fun - simp2 :: "rexp \ rexp set \ 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 \ seen) then (ZERO, seen) - else simp2_SEQ r1s r2s seen)" -| "simp2 r seen = (if r \ seen then (ZERO, seen) else (r, seen \ {r}))" - - -lemma simp2_ALT[simp]: - shows "L (fst (simp2_ALT r1 r2 seen)) = L r1 \ 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 \ snd (simp2_SEQ r1 r2 rs)" - apply(induct r1 r2 rs rule: simp2_SEQ.induct) - apply(auto) - done - -lemma test3: - shows "rs \ 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 "\(L ` snd (simp2 r rs)) \ L(r) \ (\ (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 "(\r' \ rs. L r') \ L r" - shows "L(fst (simp2 r rs)) \ 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 \ 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)) \ L x1 \ 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