Mercurial Mercurial > hg > lexing / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Lexer.thy
changeset 216 ce3d07860a4a
parent 204 cd9e40280784
child 254 7c89d3f6923e 
--- 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 \<Rightarrow> rexp"
-where 
-  "ALTS [] = ZERO"
-| "ALTS [r] = r"
-| "ALTS (r # rs) = ALT r (ALTS rs)"
-
-fun SEQS :: "rexp list \<Rightarrow> 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) \<union> (L r2)"
 | "L (STAR r) = (L r)\<star>"
 
-lemma L_ALTS:
-  "L (ALTS rs) = (\<Union>r \<in> 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 \<Rightarrow> rexp"
-where
-  "delta r \<equiv> (if nullable r then ONE else ZERO)"
-
-lemma delta_simp:
-  shows "nullable r1 \<Longrightarrow> L (SEQ (delta r1) r2) = L r2"
-  and   "\<not>nullable r1 \<Longrightarrow> L (SEQ (delta r1) r2) = {}"
-unfolding delta_def
-by simp_all
-
-fun str_split :: "string \<Rightarrow> string \<Rightarrow> (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 \<Rightarrow> (string * string) list"
-where
-  "ssplit s = rev (str_split [] s)"  
-
-fun tsplit :: "string \<Rightarrow> (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 \<Rightarrow> rexp \<Rightarrow> 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) \<leftarrow> (ssplit s)])"
-| "D [] (STAR r) = STAR r"
-| "D (c#s) (STAR r) = ALTS (SEQ (D (c#s) r) (STAR r) # 
-      [SEQS ((map (\<lambda>c. delta (D [c] r)) s1) @ [D s2 (STAR r)]). (s1, s2) \<leftarrow> (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 \<leftarrow> 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 =
lexing