Mercurial Mercurial > hg > afl-material / comparison
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 971 51e00f223792
parent 456 2fddf8ab744f
child 972 ebb4a40d9bae
equal deleted inserted replaced
970:1d4659dd83fe 971:51e00f223792 
     9 lemma Suc_reduce_Union:
 
     9 lemma Suc_reduce_Union:
 
    10   "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"
 
    10   "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"
 
    11 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)
 
    11 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)
 
    12 
    12 
    13 
    13 
    14 section {* Regular Expressions *}
 
    14 section \<open>Regular Expressions\<close>
 
    15 
    15 
    16 datatype rexp =
 
    16 datatype rexp =
 
    17   NULL
 
    17   NULL
 
    18 | EMPTY
 
    18 | EMPTY
 
    19 | CHAR char
 
    19 | CH char
 
    20 | SEQ rexp rexp
 
    20 | SEQ rexp rexp
 
    21 | ALT rexp rexp
 
    21 | ALT rexp rexp
 
    22 | STAR rexp
 
    22 | STAR rexp
 
    23 | NOT rexp
 
    23 | NOT rexp
 
    24 | PLUS rexp
 
    24 | PLUS rexp
 
    26 | NTIMES rexp nat
 
    26 | NTIMES rexp nat
 
    27 | NMTIMES rexp nat nat
 
    27 | NMTIMES rexp nat nat
 
    28 | UPNTIMES rexp nat
 
    28 | UPNTIMES rexp nat
 
    29 
    29 
    30 
    30 
    31 section {* Sequential Composition of Sets *}
 
    31 section \<open>Sequential Composition of Sets\<close>
 
    32 
    32 
    33 definition
 
    33 definition
 
    34   Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 
    34   Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 
    35 where 
    35 where 
    36   "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
 
    36   "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
 
    37 
    37 
    38 text {* Two Simple Properties about Sequential Composition *}
 
    38 text \<open>Two Simple Properties about Sequential Composition\<close>
 
    39 
    39 
    40 lemma seq_empty [simp]:
 
    40 lemma seq_empty [simp]:
 
    41   shows "A ;; {[]} = A"
 
    41   shows "A ;; {[]} = A"
 
    42   and   "{[]} ;; A = A"
 
    42   and   "{[]} ;; A = A"
 
    43 by (simp_all add: Seq_def)
 
    43 by (simp_all add: Seq_def)
 
    66 apply(metis append_assoc)
 
    66 apply(metis append_assoc)
 
    67 apply(metis)
 
    67 apply(metis)
 
    68 done
 
    68 done
 
    69 
    69 
    70 
    70 
    71 section {* Power for Sets *}
 
    71 section \<open>Power for Sets\<close>
 
    72 
    72 
    73 fun 
    73 fun 
    74   pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101)
 
    74   pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101)
 
    75 where
 
    75 where
 
    76    "A \<up> 0 = {[]}"
 
    76    "A \<up> 0 = {[]}"
 
    82 
    82 
    83 lemma pow_plus:
 
    83 lemma pow_plus:
 
    84   "A \<up> (n + m) = A \<up> n ;; A \<up> m"
 
    84   "A \<up> (n + m) = A \<up> n ;; A \<up> m"
 
    85 by (induct n) (simp_all add: seq_assoc)
 
    85 by (induct n) (simp_all add: seq_assoc)
 
    86 
    86 
    87 section {* Kleene Star for Sets *}
 
    87 section \<open>Kleene Star for Sets\<close>
 
    88 
    88 
    89 inductive_set
 
    89 inductive_set
 
    90   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
 
    90   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
 
    91   for A :: "string set"
 
    91   for A :: "string set"
 
    92 where
 
    92 where
 
    93   start[intro]: "[] \<in> A\<star>"
 
    93   start[intro]: "[] \<in> A\<star>"
 
    94 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
 
    94 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
 
    95 
    95 
    96 text {* A Standard Property of Star *}
 
    96 text \<open>A Standard Property of Star\<close>
 
    97 
    97 
    98 lemma star_decomp: 
    98 lemma star_decomp: 
    99   assumes a: "c # x \<in> A\<star>" 
    99   assumes a: "c # x \<in> A\<star>" 
   100   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
 
   100   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
 
   101 using a 
   101 using a 
   130 using Star_in_Pow Pow_in_Star
 
   130 using Star_in_Pow Pow_in_Star
 
   131 by (auto)
 
   131 by (auto)
 
   132 
   132 
   133 
   133 
   134 
   134 
   135 section {* Semantics of Regular Expressions *}
 
   135 section \<open>Semantics of Regular Expressions\<close>
 
   136  
   136  
   137 fun
 
   137 fun
 
   138   L :: "rexp \<Rightarrow> string set"
 
   138   L :: "rexp \<Rightarrow> string set"
 
   139 where
 
   139 where
 
   140   "L (NULL) = {}"
 
   140   "L (NULL) = {}"
 
   141 | "L (EMPTY) = {[]}"
 
   141 | "L (EMPTY) = {[]}"
 
   142 | "L (CHAR c) = {[c]}"
 
   142 | "L (CH c) = {[c]}"
 
   143 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
   143 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
   144 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
   144 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
   145 | "L (STAR r) = (L r)\<star>"
 
   145 | "L (STAR r) = (L r)\<star>"
 
   146 | "L (NOT r) = UNIV - (L r)"
 
   146 | "L (NOT r) = UNIV - (L r)"
 
   147 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 
   147 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 
   152 
   152 
   153 lemma "L (NOT NULL) = UNIV"
 
   153 lemma "L (NOT NULL) = UNIV"
 
   154 apply(simp)
 
   154 apply(simp)
 
   155 done
 
   155 done
 
   156 
   156 
   157 section {* The Matcher *}
 
   157 section \<open>The Matcher\<close>
 
   158 
   158 
   159 fun
 
   159 fun
 
   160  nullable :: "rexp \<Rightarrow> bool"
 
   160  nullable :: "rexp \<Rightarrow> bool"
 
   161 where
 
   161 where
 
   162   "nullable (NULL) = False"
 
   162   "nullable (NULL) = False"
 
   163 | "nullable (EMPTY) = True"
 
   163 | "nullable (EMPTY) = True"
 
   164 | "nullable (CHAR c) = False"
 
   164 | "nullable (CH c) = False"
 
   165 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
   165 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
   166 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
   166 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
   167 | "nullable (STAR r) = True"
 
   167 | "nullable (STAR r) = True"
 
   168 | "nullable (NOT r) = (\<not>(nullable r))"
 
   168 | "nullable (NOT r) = (\<not>(nullable r))"
 
   169 | "nullable (PLUS r) = (nullable r)"
 
   169 | "nullable (PLUS r) = (nullable r)"
 
   174 
   174 
   175 fun M :: "rexp \<Rightarrow> nat"
 
   175 fun M :: "rexp \<Rightarrow> nat"
 
   176 where
 
   176 where
 
   177   "M (NULL) = 0"
 
   177   "M (NULL) = 0"
 
   178 | "M (EMPTY) = 0"
 
   178 | "M (EMPTY) = 0"
 
   179 | "M (CHAR char) = 0"
 
   179 | "M (CH char) = 0"
 
   180 | "M (SEQ r1 r2) = Suc ((M r1) + (M r2))"
 
   180 | "M (SEQ r1 r2) = Suc ((M r1) + (M r2))"
 
   181 | "M (ALT r1 r2) = Suc ((M r1) + (M r2))"
 
   181 | "M (ALT r1 r2) = Suc ((M r1) + (M r2))"
 
   182 | "M (STAR r) = Suc (M r)"
 
   182 | "M (STAR r) = Suc (M r)"
 
   183 | "M (NOT r) = Suc (M r)"
 
   183 | "M (NOT r) = Suc (M r)"
 
   184 | "M (PLUS r) = Suc (M r)"
 
   184 | "M (PLUS r) = Suc (M r)"
 
   189 
   189 
   190 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   190 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   191 where
 
   191 where
 
   192   "der c (NULL) = NULL"
 
   192   "der c (NULL) = NULL"
 
   193 | "der c (EMPTY) = NULL"
 
   193 | "der c (EMPTY) = NULL"
 
   194 | "der c (CHAR d) = (if c = d then EMPTY else NULL)"
 
   194 | "der c (CH d) = (if c = d then EMPTY else NULL)"
 
   195 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 
   195 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 
   196 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"
 
   196 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"
 
   197 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 
   197 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 
   198 | "der c (NOT r) = NOT(der c r)"
 
   198 | "der c (NOT r) = NOT(der c r)"
 
   199 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 
   199 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 
   230 defer
 
   230 defer
 
   231 defer
 
   231 defer
 
   232 defer
 
   232 defer
 
   233 apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n")
 
   233 apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n")
 
   234 prefer 2
 
   234 prefer 2
 
   235 apply(auto)[1]
 
   235      apply(auto)[1]
 
       
   236 
   236 (*
 
   237 (*
 
   237 apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc)
 
   238 apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc)
 
   238 apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)")
 
   239 apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)")
 
   239 prefer 2
 
   240 prefer 2
 
   240 apply(auto)[1]
 
   241 apply(auto)[1]
 
   272   matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool"
 
   273   matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool"
 
   273 where
 
   274 where
 
   274   "matcher r s = nullable (ders s r)"
 
   275   "matcher r s = nullable (ders s r)"
 
   275 
   276 
   276 
   277 
   277 section {* Correctness Proof of the Matcher *}
 
   278 section \<open>Correctness Proof of the Matcher\<close>
 
   278 
   279 
   279 lemma nullable_correctness:
 
   280 lemma nullable_correctness:
 
   280   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 
   281   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 
   281 apply(induct r) 
   282 apply(induct r) 
   282 apply(auto simp add: Seq_def) 
   283 apply(auto simp add: Seq_def) 
   283 done
 
   284 done
 
   284 
   285 
   285 section {* Left-Quotient of a Set *}
 
   286 section \<open>Left-Quotient of a Set\<close>
 
   286 
   287 
   287 definition
 
   288 definition
 
   288   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
 
   289   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
 
   289 where
 
   290 where
 
   290   "Der c A \<equiv> {s. [c] @ s \<in> A}"
 
   291   "Der c A \<equiv> {s. [c] @ s \<in> A}"
 
   332     unfolding Seq_def Der_def
 
   333     unfolding Seq_def Der_def
 
   333     by (auto dest: star_decomp)
 
   334     by (auto dest: star_decomp)
 
   334   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
 
   335   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
 
   335 qed
 
   336 qed
 
   336 
   337 
       
   338 lemma test:
 
       
   339   assumes "[] \<in> A"
 
       
   340   shows "Der c (A \<up> n) \<subseteq> (Der c A) ;; (A \<up> n)"
 
       
   341   using assms
 
       
   342   apply(induct n)
 
       
   343    apply(simp)
 
       
   344   apply(simp)
 
       
   345   apply(auto simp add: Der_def Seq_def)
 
       
   346   apply blast
 
       
   347   by force
 
       
   348 
       
   349 lemma Der_ntimes [simp]:
 
       
   350   shows "Der c (A  \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
 
       
   351 proof -    
       
   352   have "Der c (A  \<up> (Suc n)) = Der c (A ;; A \<up> n)"
 
       
   353     by(simp)
 
       
   354   also have "... = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
 
       
   355     by simp
 
       
   356   also have "... =  (Der c A) ;; (A \<up> n)"
 
       
   357     using test by force
 
       
   358   finally show "Der c (A  \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" .
 
       
   359 qed
 
       
   360 
       
   361 
       
   362 
   337 lemma Der_UNIV [simp]:
 
   363 lemma Der_UNIV [simp]:
 
   338   "Der c (UNIV - A) = UNIV - Der c A"
 
   364   "Der c (UNIV - A) = UNIV - Der c A"
 
   339 unfolding Der_def
 
   365 unfolding Der_def
 
   340 by (auto)
 
   366 by (auto)
 
   341 
   367 
   344 unfolding Der_def 
   370 unfolding Der_def 
   345 by(auto simp add: Cons_eq_append_conv Seq_def)
 
   371 by(auto simp add: Cons_eq_append_conv Seq_def)
 
   346 
   372 
   347 lemma Der_UNION [simp]: 
   373 lemma Der_UNION [simp]: 
   348   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
 
   374   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
 
   349 by (auto simp add: Der_def)
 
   375   by (auto simp add: Der_def)
 
       
   376 
       
   377 lemma if_f:
 
       
   378   shows "f(if B then C else D) = (if B then f(C) else f(D))"
 
       
   379   by simp
 
       
   380 
       
   381 
       
   382 lemma der_correctness:
 
       
   383   shows "L (der c r) = Der c (L r)"
 
       
   384 proof(induct r)
 
       
   385   case NULL
 
       
   386   then show ?case by simp
 
       
   387 next
 
       
   388   case EMPTY
 
       
   389   then show ?case by simp
 
       
   390 next
 
       
   391   case (CH x)
 
       
   392   then show ?case by simp
 
       
   393 next
 
       
   394   case (SEQ r1 r2)
 
       
   395   then show ?case
 
       
   396     by (simp add: nullable_correctness) 
       
   397 next
 
       
   398   case (ALT r1 r2)
 
       
   399   then show ?case by simp
 
       
   400 next
 
       
   401   case (STAR r)
 
       
   402   then show ?case
 
       
   403     by simp 
       
   404 next
 
       
   405   case (NOT r)
 
       
   406   then show ?case by simp
 
       
   407 next
 
       
   408   case (PLUS r)
 
       
   409   then show ?case by simp
 
       
   410 next
 
       
   411   case (OPT r)
 
       
   412   then show ?case by simp
 
       
   413 next
 
       
   414   case (NTIMES r n)
 
       
   415   then show ?case
 
       
   416     apply(induct n)
 
       
   417      apply(simp)
 
       
   418     apply(simp only: L.simps)
 
       
   419     apply(simp only: Der_pow)
 
       
   420     apply(simp only: der.simps L.simps)
 
       
   421     apply(simp only: nullable_correctness)
 
       
   422     apply(simp only: if_f)
 
       
   423     by simp
 
       
   424 next
 
       
   425   case (NMTIMES r n m)
 
       
   426   then show ?case 
       
   427     apply(case_tac n)
 
       
   428     sorry
 
       
   429 next
 
       
   430   case (UPNTIMES r x2)
 
       
   431   then show ?case sorry
 
       
   432 qed
 
       
   433 
       
   434 
       
   435 
   350 
   436 
   351 lemma der_correctness:
 
   437 lemma der_correctness:
 
   352   shows "L (der c r) = Der c (L r)"
 
   438   shows "L (der c r) = Der c (L r)"
 
   353 apply(induct rule: der.induct) 
   439 apply(induct rule: der.induct) 
   354 apply(simp_all add: nullable_correctness 
   440 apply(simp_all add: nullable_correctness 
   377 
   463 
   378 lemma "L(der c (UPNTIMES r 0)) = {}"
 
   464 lemma "L(der c (UPNTIMES r 0)) = {}"
 
   379 by simp
 
   465 by simp
 
   380 
   466 
   381 lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
 
   467 lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
 
   382 using assms
 
       
   383 proof(induct n)
 
   468 proof(induct n)
 
   384   case 0 show ?case by simp
 
   469   case 0 show ?case by simp
 
   385 next
 
   470 next
 
   386   case (Suc n)
 
   471   case (Suc n)
 
   387   have IH: "L (der c (UPNTIMES r (Suc n))) = L (SEQ (der c r) (UPNTIMES r n))" by fact
 
   472   have IH: "L (der c (UPNTIMES r (Suc n))) = L (SEQ (der c r) (UPNTIMES r n))" by fact
afl-material