1    

     2 theory Bounds

     3   imports "Lexer" 

     4 begin

     5 

     6 definition Size :: "rexp \<Rightarrow> nat"

     7 where "Size r == Max {size (ders s r) | s. True }"

     8 

     9 fun bar :: "rexp \<Rightarrow> string \<Rightarrow> rexp" where

    10   "bar r [] = r"

    11 | "bar r (c # s) = ALT (ders (c # s) r) (bar r s)"

    12 

    13 lemma size_ALT:

    14   "size (ders s (ALT r1 r2)) = Suc (size (ders s r1) + size (ders s r2))"

    15 apply(induct s arbitrary: r1 r2)

    16 apply(simp_all)

    17 done

    18 

    19 lemma size_bar_ALT:

    20   "size (bar (ALT r1 r2) s) = Suc (size (bar r1 s) + size (bar r2 s))"

    21 apply(induct s)

    22 apply(simp)

    23 apply(simp add: size_ALT)

    24 done

    25 

    26 lemma size_SEQ:

    27   "size (ders s (SEQ r1 r2)) \<le> Suc (size (ders s r1)) + size r2 + size (bar (SEQ r1 r2) s)"

    28 apply(induct s arbitrary: r1 r2)

    29 apply(simp_all)

    30 done

    31 

    32 (*

    33 lemma size_bar_SEQ:

    34   "size (bar (SEQ r1 r2) s) \<le> Suc (size (bar r1 s) + size (bar r2 s))"

    35 apply(induct s)

    36 apply(simp)

    37 apply(auto simp add: size_SEQ size_ALT)

    38 apply(rule le_trans)

    39 apply(rule size_SEQ)

    40 done

    41 *)

    42 

    43 lemma size_STAR:

    44   "size (ders s (STAR r)) \<le> Suc (size (bar r s)) + size (STAR r)"

    45 apply(induct s arbitrary: r)

    46 apply(simp)

    47 apply(simp)

    48 apply(rule le_trans)

    49 apply(rule size_SEQ)

    50 apply(simp)

    51 oops

    52 

    53 lemma Size_ALT:

    54   "Size (ALT r1 r2) \<le> Suc (Size r1 + Size r2)"

    55 unfolding Size_def

    56 apply(auto)

    57 apply(simp add: size_ALT)

    58 apply(subgoal_tac "Max {n. \<exists>s. n = Suc (size (ders s r1) + size (ders s r2))} \<ge>

    59   Suc (Max {n. \<exists>s. n = size (ders s r1) + size (ders s r2)})")

    60 prefer 2

    61 oops

    62 

    63 

    64 

    65 end