# HG changeset patch
# User fahad
# Date 1424954542 0
# Node ID f182c125980e9e8345757f30d3507b107db7cf42
# Parent  d86d685273ceba29999e1240effaea959b0043f8# Parent  45274393f28ce6884a0e0488f727289cc0a5918b
merged

diff -r d86d685273ce -r f182c125980e thys/Re1.thy
--- a/thys/Re1.thy	Thu Feb 26 12:41:55 2015 +0000
+++ b/thys/Re1.thy	Thu Feb 26 12:42:22 2015 +0000
@@ -42,6 +42,7 @@
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
+<<<<<<< local
 fun
  nullable :: "rexp \<Rightarrow> bool"
 where
@@ -50,12 +51,19 @@
 | "nullable (CHAR c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
+=======
+value "L(CHAR c)"
+value "L(SEQ(CHAR c)(CHAR b))"
+>>>>>>> other
 
+<<<<<<< local
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 apply (induct r) 
 apply(auto simp add: Sequ_def) 
 done
+=======
+>>>>>>> other
 
 section {* Values *}
 
@@ -116,7 +124,13 @@
 apply(auto intro: Prf.intros)
 done
 
+<<<<<<< local
+=======
+value "flat(Seq(Char c)(Char b))"
+value "flat(Right(Void))"
+>>>>>>> other
 
+<<<<<<< local
 
 lemma mkeps_flat:
   assumes "nullable(r)" shows "flat (mkeps r) = []"
@@ -129,6 +143,17 @@
   The value mkeps returns is always the correct POSIX
   value.
 *}
+=======
+fun flats :: "val \<Rightarrow> string list"
+where
+  "flats(Void) = [[]]"
+| "flats(Char c) = [[c]]"
+| "flats(Left v) = flats(v)"
+| "flats(Right v) = flats(v)"
+| "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
+>>>>>>> other
+
+value "flats(Seq(Char c)(Char b))"
 
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
@@ -150,7 +175,7 @@
 apply(auto)
 done
 
-definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
+definition definition prefix :: :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
 where
   "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"