# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1549835637 0
# Node ID ee1caac29bb2bee7909368edab0c42a49cd70216
# Parent  6756b026c5febeaeada52408373217f447dd5850
updated to Isabelle 2018

diff -r 6756b026c5fe -r ee1caac29bb2 exps/both.scala
--- a/exps/both.scala	Fri Feb 08 12:47:35 2019 +0000
+++ b/exps/both.scala	Sun Feb 10 21:53:57 2019 +0000
@@ -580,14 +580,22 @@
 // Some Small Tests
 //==================
 
-/*
-println("simple tests:")
-println(blexing_simp((SYM.%), "abcd"))
-println(blexing_simp(((SYM.%) | ((SYM.% | NUM).%)), "12345"))
-println(blexing_simp((WHILE_REGS), "abcd"))
-println(blexing_simp((WHILE_REGS), "12345"))
-println(blexing_simp((WHILE_REGS), """write "Fib";"""))
-*/
+println("Small tests")
+
+val re1 = STAR("a" | "aa")
+println(astring(bders_simp("".toList, internalise(re1))))
+println(astring(bders_simp("a".toList, internalise(re1))))
+println(astring(bders_simp("aa".toList, internalise(re1))))
+println(astring(bders_simp("aaa".toList, internalise(re1))))
+println(astring(bders_simp("aaaaaa".toList, internalise(re1))))
+println(astring(bders_simp("aaaaaaaaa".toList, internalise(re1))))
+println(astring(bders_simp("aaaaaaaaaaaa".toList, internalise(re1))))
+println(astring(bders_simp("aaaaaaaaaaaaaaaaaaaaaaaaa".toList, internalise(re1))))
+println(astring(bders_simp("aaaaaabaaaabbbbbaaaaaaaaaaaaaaa".toList, internalise(re1))))
+
+
+
+
 
 
 // Bigger Tests
diff -r 6756b026c5fe -r ee1caac29bb2 thys/Positions.thy
--- a/thys/Positions.thy	Fri Feb 08 12:47:35 2019 +0000
+++ b/thys/Positions.thy	Sun Feb 10 21:53:57 2019 +0000
@@ -126,7 +126,7 @@
 
 
 
-section {* POSIX Ordering of Values According to Okui & Suzuki *}
+section {* POSIX Ordering of Values According to Okui \& Suzuki *}
 
 
 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
@@ -196,9 +196,9 @@
 using assms
 using PosOrd_irrefl PosOrd_trans by blast 
 
-text {*
+(*
   :\<sqsubseteq>val and :\<sqsubset>val are partial orders.
-*}
+*)
 
 lemma PosOrd_ordering:
   shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
diff -r 6756b026c5fe -r ee1caac29bb2 thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Fri Feb 08 12:47:35 2019 +0000
+++ b/thys/Sulzmann.thy	Sun Feb 10 21:53:57 2019 +0000
@@ -318,61 +318,5 @@
 qed
 
 
-lemma
-  "[a, a, a, a] \<in> (STAR(STAR(CHAR(a)))) \<rightarrow> 
-     (Stars [(Stars [Char a, Char a, Char a, Char a])])"
-  oops
-
-lemma
-  "([a,a] @ []) \<in> (STAR(STAR(CHAR(a)))) \<rightarrow> 
-     (Stars [(Stars [Char a, Char a])])"
-  apply(rule Posix.intros)
-  defer
-  apply (simp add: Posix_STAR2)
-  apply(simp)
-  apply(auto)[1]
-  apply(rule_tac s="[a] @ [a]" in subst)
-  apply(simp)
-  apply(rule Posix_STAR1)
-  apply(rule Posix_CHAR)
-  apply(rule_tac s="[a] @ []" in subst)
-  apply(simp)
-  apply(rule Posix_STAR1)
-       apply(rule Posix_CHAR)
-      apply(rule Posix_STAR2)
-     apply(simp)
-    apply(auto)
-  done
-
-
-lemma "lexer (STAR(STAR(CHAR(a)))) [a, a] = XXX"
-  apply(simp)
-  oops
-
-
-
-
-
-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"
-
-
-
-
-
-
-
-definition blexers where
- "blexer r s \<equiv> if bnullable (bders (intern r) s) then 
-                decode (bmkeps (bders (intern r) s)) r else None"
-
-unused_thms
-
-
-
 
 end
\ No newline at end of file
diff -r 6756b026c5fe -r ee1caac29bb2 thys/journal.pdf
Binary file thys/journal.pdf has changed