# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1538305324 -3600
# Node ID 1a4e5b94293b46714141fb4c57f3e6204d8cfd08
# Parent  d688a01b8f890cfecc4c42a4bbbedfea86786a08
updated

diff -r d688a01b8f89 -r 1a4e5b94293b progs/scala/re-basic.scala
--- a/progs/scala/re-basic.scala	Mon Sep 10 21:41:54 2018 +0100
+++ b/progs/scala/re-basic.scala	Sun Sep 30 12:02:04 2018 +0100
@@ -230,3 +230,13 @@
 
 filelines.foreach({ case (s: String, i: Int) => process(s, i) })
 
+
+
+// test: ("a" | "aa")*
+val EVIL3 = STAR(ALT(CHAR('a'), SEQ(CHAR('a'), CHAR('a'))))
+
+for (i <- 1 to 29 by 1) {
+  println(i + " " + "%.5f".format(time_needed(2, matcher(EVIL3, "a" * i))) + 
+	  " size: " + size(ders(("a" * i).toList, EVIL3)))
+}
+
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
diff -r d688a01b8f89 -r 1a4e5b94293b thys/Spec.thy
--- a/thys/Spec.thy	Mon Sep 10 21:41:54 2018 +0100
+++ b/thys/Spec.thy	Sun Sep 30 12:02:04 2018 +0100
@@ -163,6 +163,7 @@
 
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
+  apply(induct r)
 by (induct r) (auto simp add: Sequ_def) 
 
 lemma der_correctness:
diff -r d688a01b8f89 -r 1a4e5b94293b thys/SpecExt.thy
--- a/thys/SpecExt.thy	Mon Sep 10 21:41:54 2018 +0100
+++ b/thys/SpecExt.thy	Sun Sep 30 12:02:04 2018 +0100
@@ -505,7 +505,10 @@
 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [];
     length vs > n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : NMTIMES r n m"
 
-  
+
+ 
+
+
 inductive_cases Prf_elims:
   "\<Turnstile> v : ZERO"
   "\<Turnstile> v : SEQ r1 r2"
@@ -764,7 +767,34 @@
   shows "L(r) = {flat v | v. \<Turnstile> v : r}"
 using L_flat_Prf1 L_flat_Prf2 by blast
 
+thm Prf.intros
+thm Prf.cases
 
+lemma
+  assumes "\<Turnstile> v : (STAR r)" 
+  shows "\<Turnstile> v : (FROMNTIMES r 0)"
+  using assms
+  apply(erule_tac Prf.cases)
+             apply(simp_all)
+  apply(case_tac vs)
+   apply(auto)
+  apply(subst append_Nil[symmetric])
+   apply(rule Prf.intros)
+     apply(auto)
+  apply(simp add: Prf.intros)
+  done
+
+lemma
+  assumes "\<Turnstile> v : (FROMNTIMES r 0)" 
+  shows "\<Turnstile> v : (STAR r)"
+  using assms
+  apply(erule_tac Prf.cases)
+             apply(simp_all)
+   apply(rule Prf.intros)
+   apply(simp)
+  apply(rule Prf.intros)
+   apply(simp)
+  done
 
 section {* Sets of Lexical Values *}
 
diff -r d688a01b8f89 -r 1a4e5b94293b thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Mon Sep 10 21:41:54 2018 +0100
+++ b/thys/Sulzmann.thy	Sun Sep 30 12:02:04 2018 +0100
@@ -312,9 +312,19 @@
   }
   then show "blexer r s = lexer r s"
     unfolding blexer_def lexer_flex
-    by(auto simp add: bnullable_correctness[symmetric])
+    apply(subst bnullable_correctness[symmetric])
+    apply(simp)
+    done
 qed
 
+fun simp where
+  "simp (AALT bs a AZERO) = fuse bs (simp a)"
+| "simp (AALT bs AZERO a) = fuse bs (simp a)"
+| "simp (ASEQ bs a AZERO) = AZERO"
+| "simp (ASEQ bs AZERO a) = AZERO"
+| "simp a = a"
+
+
 unused_thms
   
 end
\ No newline at end of file