--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Bounds.thy	Thu Jun 09 12:31:02 2016 +0100
@@ -0,0 +1,65 @@
+   
+theory Bounds
+  imports "Lexer" 
+begin
+
+definition Size :: "rexp \<Rightarrow> nat"
+where "Size r == Max {size (ders s r) | s. True }"
+
+fun bar :: "rexp \<Rightarrow> string \<Rightarrow> rexp" where
+  "bar r [] = r"
+| "bar r (c # s) = ALT (ders (c # s) r) (bar r s)"
+
+lemma size_ALT:
+  "size (ders s (ALT r1 r2)) = Suc (size (ders s r1) + size (ders s r2))"
+apply(induct s arbitrary: r1 r2)
+apply(simp_all)
+done
+
+lemma size_bar_ALT:
+  "size (bar (ALT r1 r2) s) = Suc (size (bar r1 s) + size (bar r2 s))"
+apply(induct s)
+apply(simp)
+apply(simp add: size_ALT)
+done
+
+lemma size_SEQ:
+  "size (ders s (SEQ r1 r2)) \<le> Suc (size (ders s r1)) + size r2 + size (bar (SEQ r1 r2) s)"
+apply(induct s arbitrary: r1 r2)
+apply(simp_all)
+done
+
+(*
+lemma size_bar_SEQ:
+  "size (bar (SEQ r1 r2) s) \<le> Suc (size (bar r1 s) + size (bar r2 s))"
+apply(induct s)
+apply(simp)
+apply(auto simp add: size_SEQ size_ALT)
+apply(rule le_trans)
+apply(rule size_SEQ)
+done
+*)
+
+lemma size_STAR:
+  "size (ders s (STAR r)) \<le> Suc (size (bar r s)) + size (STAR r)"
+apply(induct s arbitrary: r)
+apply(simp)
+apply(simp)
+apply(rule le_trans)
+apply(rule size_SEQ)
+apply(simp)
+oops
+
+lemma Size_ALT:
+  "Size (ALT r1 r2) \<le> Suc (Size r1 + Size r2)"
+unfolding Size_def
+apply(auto)
+apply(simp add: size_ALT)
+apply(subgoal_tac "Max {n. \<exists>s. n = Suc (size (ders s r1) + size (ders s r2))} \<ge>
+  Suc (Max {n. \<exists>s. n = size (ders s r1) + size (ders s r2)})")
+prefer 2
+oops
+
+
+
+end
\ No newline at end of file