diff -r 645ce5697621 -r ce3d07860a4a thys/Lexer.thy --- a/thys/Lexer.thy Tue Feb 21 13:37:36 2017 +0000 +++ b/thys/Lexer.thy Sat Feb 25 21:16:46 2017 +0000 @@ -109,18 +109,6 @@ | ALT rexp rexp | STAR rexp -fun ALTS :: "rexp list \ rexp" -where - "ALTS [] = ZERO" -| "ALTS [r] = r" -| "ALTS (r # rs) = ALT r (ALTS rs)" - -fun SEQS :: "rexp list \ rexp" -where - "SEQS [] = ONE" -| "SEQS [r] = r" -| "SEQS (r # rs) = SEQ r (SEQS rs)" - section {* Semantics of Regular Expressions *} fun @@ -133,19 +121,6 @@ | "L (ALT r1 r2) = (L r1) \ (L r2)" | "L (STAR r) = (L r)\" -lemma L_ALTS: - "L (ALTS rs) = (\r \ set rs. L(r))" -by(induct rs rule: ALTS.induct)(simp_all) - -lemma L_SEQS: - "L (SEQS []) = {[]}" - "L (SEQS (r # rs)) = (L r) ;; (L (SEQS rs))" -apply(simp) -apply(case_tac rs) -apply(simp) -apply(simp) -done - section {* Nullable, Derivatives *} @@ -219,342 +194,6 @@ apply(simp_all) done - - -definition - delta :: "rexp \ rexp" -where - "delta r \ (if nullable r then ONE else ZERO)" - -lemma delta_simp: - shows "nullable r1 \ L (SEQ (delta r1) r2) = L r2" - and "\nullable r1 \ L (SEQ (delta r1) r2) = {}" -unfolding delta_def -by simp_all - -fun str_split :: "string \ string \ (string * string) list" -where - "str_split s1 [] = []" -| "str_split s1 [c] = [(s1, [c])]" -| "str_split s1 (c#s2) = (s1, c#s2) # str_split (s1 @ [c]) s2" - -fun ssplit :: "string \ (string * string) list" -where - "ssplit s = rev (str_split [] s)" - -fun tsplit :: "string \ (string * string) list" -where - "tsplit s = tl (str_split [] s)" - - -value "ssplit([])" -value "ssplit([a1])" -value "ssplit([a1, a2])" -value "ssplit([a1, a2, a3])" -value "ssplit([a1, a2, a3, a4])" - -value "tsplit([])" -value "tsplit([a1])" -value "tsplit([a1, a2])" -value "tsplit([a1, a2, a3])" -value "tsplit([a1, a2, a3, a4])" - -function - D :: "string \ rexp \ rexp" -where - "D s (ZERO) = ZERO" -| "D s (ONE) = (if s = [] then ONE else ZERO)" -| "D s (CHAR c) = (if s = [c] then ONE else - (if s = [] then (CHAR c) else ZERO))" -| "D s (ALT r1 r2) = ALT (D s r1) (D s r2)" -| "D s (SEQ r1 r2) = ALTS ((SEQ (D s r1) r2) # [SEQ (delta (D s1 r1)) (D s2 r2). (s1, s2) \ (ssplit s)])" -| "D [] (STAR r) = STAR r" -| "D (c#s) (STAR r) = ALTS (SEQ (D (c#s) r) (STAR r) # - [SEQS ((map (\c. delta (D [c] r)) s1) @ [D s2 (STAR r)]). (s1, s2) \ (tsplit (c#s))])" -sorry - -termination sorry - -thm D.simps -thm tl_def - -lemma D_Nil: - shows "D [] r = r" -apply(induct r) -apply(simp_all) -done - -lemma D_ALTS: - shows "D s (ALTS rs) = ALTS [D s r. r \ rs]" -apply(induct rs rule: ALTS.induct) -apply(simp_all) -done - -(* -lemma - "D [a] (SEQ E F) = ALT (SEQ (D [a] E) F) (SEQ (delta E) (D [a] F))" -apply(simp add: D_Nil) -done - -lemma - "D [a1, a2] (SEQ E F) = ALT (SEQ (D [a1, a2] E) F) - (ALT (SEQ (delta (D [a1] E)) (D [a2] F)) (SEQ (delta E) (D [a1, a2] F)))" -apply(simp add: D_Nil) -done -*) -(* -lemma D_Der1: - shows "L(D [c] r) = L(der c r)" -apply(induct r) -apply(simp) -apply(simp) -apply(simp) -prefer 2 -apply(simp) -apply(simp) -apply(auto)[1] -apply(simp add: D_Nil) -apply(simp add: delta_def) -apply(simp add: D_Nil) -apply(simp add: delta_def) -apply(simp add: D_Nil) -apply(simp add: delta_def) -apply(simp) -done - -lemma D_Der2: - shows "L(D [a1, a2] r) = L(der a2 (der a1 r))" -apply(induct r) -apply(simp) -apply(simp) -apply(simp) -prefer 2 -apply(simp) -apply(simp) -apply(auto)[1] -apply(simp add: delta_def) -apply(auto split: if_splits)[1] -apply(simp add: der_correctness Der_def D_Der1 D_Nil) -apply(simp add: der_correctness Der_def D_Der1 D_Nil) -apply (simp add: delta_def) -apply(simp add: der_correctness Der_def D_Der1 D_Nil) -apply (simp add: D_Der1 delta_def nullable_correctness) -apply (simp add: D_Der1 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Nil) -apply(simp add: der_correctness Der_def D_Der1 D_Nil) -apply (simp add: D_Der1 delta_def nullable_correctness) -apply(simp add: D_Der1 D_Nil delta_def) -apply(simp add: D_Der1 D_Nil delta_def nullable_correctness) -apply(simp add: D_Der1 D_Nil delta_def nullable_correctness) -apply(simp add: D_Der1 D_Nil delta_def nullable_correctness) -apply(simp add: D_Der1 D_Nil delta_def nullable_correctness) -apply(simp add: D_Der1 D_Nil delta_def nullable_correctness) -apply(simp add: D_Der1 D_Nil delta_def nullable_correctness) -apply(auto)[1] -apply(simp add: D_Der1 D_Nil delta_def nullable_correctness) -apply(simp add: D_Der1 D_Nil delta_def nullable_correctness) -apply(simp add: D_Der1 D_Nil delta_def nullable_correctness) -done - -lemma D_Der3: - shows "L(D [a1, a2, a3] r) = L(ders [a1, a2, a3] r)" -apply(induct r) -apply(simp) -apply(simp) -apply(simp) -prefer 2 -apply(simp) -apply(simp) -apply(auto)[1] -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -(* star case *) -apply(simp) -apply(auto)[1] -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply(simp add: Sequ_def) -apply(auto)[1] -defer -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -defer -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -defer -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness D_Der1) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -apply (simp add: D_Der2 delta_def nullable_correctness) -apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil) -defer -done - -lemma D_Ders: - shows "L (D (s1 @ s2) r) = L (D s2 (D s1 r))" -apply(induct r arbitrary: s1 s2) -apply(simp) -apply(simp) -apply(simp) -apply(auto)[1] -apply (metis Cons_eq_append_conv append_is_Nil_conv) -apply(simp) -apply(auto)[1] -apply(simp add: L_ALTS D_ALTS) -apply(auto)[1] -apply(simp add: L_ALTS) -oops - - -lemma D_cons: - shows "L (D (c # s) r) = L (D s (der c r))" -apply(induct r arbitrary: c s) -apply(simp) -apply(simp) -apply(simp) -apply(simp) -apply(auto)[1] -sorry - -lemma D_Zero: - shows "lang (D s Zero) = lang (derivs s Zero)" -by (induct s) (simp_all) - -lemma D_One: - shows "lang (D s One) = lang (derivs s One)" -by (induct s) (simp_all add: D_Zero[symmetric]) - -lemma D_Atom: - shows "lang (D s (Atom c)) = lang (derivs s (Atom c))" -by (induct s) (simp_all add: D_Zero[symmetric] D_One[symmetric]) - -lemma D_Plus: - shows "lang (D s (Plus r1 r2)) = lang (derivs s (Plus r1 r2))" -by (induct s arbitrary: r1 r2) (simp_all add: D_empty D_cons) - -lemma D_Times: - shows "lang (D s (Times r1 r2)) = lang (derivs s (Times r1 r2))" -apply(induct s arbitrary: r1 r2) -apply(simp_all add: D_empty D_cons) -apply(auto simp add: conc_def)[1] -apply(simp only: D_Plus[symmetric]) -apply(simp only: D.simps) -apply(simp) -*) - - section {* Values *} datatype val =