
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) \<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




