Mercurial Mercurial > hg > afl-material / 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.
progs/Matcher2.thy
changeset 397 cf3ca219c727
parent 385 7f8516ff408d
child 455 1dbf84ade62c 
--- a/progs/Matcher2.thy	Tue Jan 12 02:49:26 2016 +0000
+++ b/progs/Matcher2.thy	Mon Feb 22 22:09:31 2016 +0000
@@ -1,4 +1,4 @@
-ytheory Matcher2
+theory Matcher2
   imports "Main" 
 begin
 
@@ -26,19 +26,6 @@
 | NTIMES rexp nat
 | NMTIMES rexp nat nat
 
-fun M :: "rexp \<Rightarrow> nat"
-where
-  "M (NULL) = 0"
-| "M (EMPTY) = 0"
-| "M (CHAR char) = 0"
-| "M (SEQ r1 r2) = Suc ((M r1) + (M r2))"
-| "M (ALT r1 r2) = Suc ((M r1) + (M r2))"
-| "M (STAR r) = Suc (M r)"
-| "M (NOT r) = Suc (M r)"
-| "M (PLUS r) = Suc (M r)"
-| "M (OPT r) = Suc (M r)"
-| "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
-| "M (NMTIMES r n m) = Suc (M r) * 2 * (Suc m - Suc n)"
 
 section {* Sequential Composition of Sets *}
 
@@ -183,6 +170,21 @@
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 
+fun M :: "rexp \<Rightarrow> nat"
+where
+  "M (NULL) = 0"
+| "M (EMPTY) = 0"
+| "M (CHAR char) = 0"
+| "M (SEQ r1 r2) = Suc ((M r1) + (M r2))"
+| "M (ALT r1 r2) = Suc ((M r1) + (M r2))"
+| "M (STAR r) = Suc (M r)"
+| "M (NOT r) = Suc (M r)"
+| "M (PLUS r) = Suc (M r)"
+| "M (OPT r) = Suc (M r)"
+| "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
+| "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"
+
+
 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
   "der c (NULL) = NULL"
@@ -197,23 +199,59 @@
 | "der c (NTIMES r 0) = NULL"
 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
 | "der c (NMTIMES r n m) = 
-     (if m < n then NULL else 
-     (if m = 0 then NULL else
-     (der c (SEQ r (NMTIMES r (n - 1) (m - 1))))))"
-(*
+        (if m < n then NULL else 
+        (if n = m then der c (NTIMES r n) else
+                       ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
+by pat_completeness auto
 
-  (if m < n then NULL else 
-                              (if n = m then der c (NTIMES r n) else
-                                ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
-*)
-by pat_completeness auto
+lemma bigger1:
+  "\<lbrakk>c < (d::nat); a < b; 0 < a; 0 < c\<rbrakk> \<Longrightarrow> c * a < d * b"
+by (metis le0 mult_strict_mono')
 
 termination der 
 apply(relation "measure (\<lambda>(c, r). M r)") 
-apply(simp_all)
-sorry
-
-
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp_all del: M.simps)
+apply(simp_all only: M.simps)
+defer
+apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n")
+prefer 2
+apply(auto)[1]
+apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc)
+apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)")
+prefer 2
+apply(auto)[1]
+apply(subgoal_tac "Suc n < Suc m")
+prefer 2
+apply(auto)[1]
+apply(subgoal_tac "Suc (M r) * 2 * Suc n < Suc (Suc (M r)) * 2 * Suc m")
+prefer 2
+apply(subgoal_tac "Suc (M r) * 2 < Suc (Suc (M r)) * 2")
+prefer 2
+apply(auto)[1]
+apply(rule bigger1)
+apply(assumption)
+apply(simp)
+apply (metis zero_less_Suc)
+apply (metis mult_is_0 neq0_conv old.nat.distinct(2))
+apply(rotate_tac 4)
+apply(drule_tac a="1" and b="(Suc (Suc m) - Suc n)" in bigger1)
+prefer 4
+apply(simp)
+apply(simp)
+apply (metis zero_less_one)
+apply(simp)
+done
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -306,122 +344,14 @@
 apply(induct rule: der.induct) 
 apply(simp_all add: nullable_correctness 
     Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
-apply(case_tac "[] \<in> L r")
-apply(simp)
-apply(case_tac n)
-apply(auto)[1]
-apply(case_tac m)
-apply(simp)
-apply(auto simp add: )[1]
-apply (metis (full_types, hide_lams) Der_pow Der_seq Suc_le_mono UnCI atLeast0AtMost atMost_iff not_less_eq_eq)
-
-apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl)
-apply (metis Suc_leD atLeastAtMost_iff)
-by (metis atLeastAtMost_iff le_antisym not_less_eq_eq)
-
-(*
-lemma der_correctness:
-  shows "L (der c r) = Der c (L r)"
-apply(induct rule: der.induct) 
-apply(simp_all add: nullable_correctness 
-    Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
-apply(case_tac m)
-apply(simp)
-apply(simp)
+apply(rule impI)+
+apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")
 apply(auto)
-apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl)
-apply (metis Suc_leD atLeastAtMost_iff)
-by (metis atLeastAtMost_iff le_antisym not_less_eq_eq)
-*)
+done
 
 lemma matcher_correctness:
   shows "matcher r s \<longleftrightarrow> s \<in> L r"
 by (induct s arbitrary: r)
    (simp_all add: nullable_correctness der_correctness Der_def)
 
-
-lemma "L (der c (NMTIMES r n m)) = 
-  L ((if m < n then NULL else 
-     (if m = 0 then NULL else
-     (der c (SEQ r (NMTIMES r (n - 1) (m - 1)))))))"
-apply(subst der.simps(12))
-apply(auto simp del: der.simps)
-apply(simp)
-apply(auto)[1]
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(subst (asm) der.simps(12))
-apply(auto)[1]
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(auto simp del: der.simps(12))[1]
-apply(subst (asm) der.simps(12))
-apply(case_tac n)
-apply(simp)
-apply(simp)
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(case_tac "Suc nat = nata")
-apply(simp)
-apply(auto simp del: der.simps(12))[1]
-apply(auto)[1]
-apply(case_tac n)
-apply(simp)
-apply(simp)
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(simp add: Seq_def)
-apply(auto)[1]
-apply (metis atLeastAtMost_iff le_eq_less_or_eq linorder_neqE_nat)
-apply(simp (no_asm) del: der.simps(12))
-apply(auto simp del: der.simps(12))[1]
-apply(case_tac "m = Suc n")
-apply(simp)
-apply(case_tac n)
-apply(simp)
-apply(simp)
-apply(auto simp add: Seq_def del: der.simps(12))[1]
-
-apply(case_tac n)
-apply(simp)
-apply(case_tac m)
-apply(simp)
-apply(simp)
-apply(simp add: Seq_def)
-apply(auto)[1]
-apply(case_tac "nat = 0")
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(case_tac "Suc 0 = nat")
-apply(simp)
-apply(auto simp del: der.simps(12))[1]
-apply(simp)
-apply(case_tac "Suc 0 = nat")
-apply(simp)
-apply(auto simp add: Seq_def del: der.simps(12))[1]
-apply(rule_tac x="s1" in exI)
-apply(rule_tac x="s2" in exI)
-apply(simp)
-apply(rule_tac x="1" in bexI)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(auto simp add: Seq_def)[1]
-apply(case_tac m)
-apply(simp)
-apply(simp)
-
 end    
\ No newline at end of file
afl-material