diff -r 4cd75c619e06 -r cf3ca219c727 progs/Matcher2.thy --- 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