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