# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1384511344 0
# Node ID 6518475020fc669b56f2efea585903b922a6c519
# Parent  9f0631804555e6cbe0c0a8c1a5aa6ac930d102eb
added

diff -r 9f0631804555 -r 6518475020fc progs/Matcher2.thy
--- a/progs/Matcher2.thy	Thu Nov 14 20:15:06 2013 +0000
+++ b/progs/Matcher2.thy	Fri Nov 15 10:29:04 2013 +0000
@@ -155,9 +155,8 @@
 by pat_completeness auto
 
 termination der 
-apply(relation "measure (\<lambda>(c, r). M r)")
-apply(simp_all)
-done
+by (relation "measure (\<lambda>(c, r). M r)") (simp_all)
+
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -240,39 +239,25 @@
 unfolding Der_def 
 by(auto simp add: Cons_eq_append_conv Seq_def)
 
-
 lemma Der_UNION [simp]: 
   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
 by (auto simp add: Der_def)
 
-lemma test:
+lemma Suc_Union:
   "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))"
 by (metis UN_insert atMost_Suc)
 
-lemma yy:
+lemma Suc_reduce_Union:
   "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"
 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)
 
-lemma uu:
-  "(Suc n) + m = Suc (n + m)"
-by simp
 
 lemma der_correctness:
   shows "L (der c r) = Der c (L r)"
-apply(induct rule: der.induct) 
-apply(simp_all add: nullable_correctness)[12]
-apply(simp only: L.simps der.simps)
-apply(simp only: Der_UNION)
-apply(simp del: pow.simps Der_pow)
-apply(simp only: atLeast0AtMost)
-apply(simp only: test)
-apply(simp only: L.simps der.simps)
-apply(simp only: Der_UNION)
-apply(simp only: yy add_Suc)
-apply(simp only: seq_Union)
-apply(simp only: Der_UNION)
-apply(simp only: pow.simps)
-done
+by (induct rule: der.induct) 
+   (simp_all add: nullable_correctness 
+    Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
+
 
 lemma matcher_correctness:
   shows "matcher r s \<longleftrightarrow> s \<in> L r"