1(*---------------------------------------------------------------------------*) 2(* even(n) predicate realized by regexp *) 3(*---------------------------------------------------------------------------*) 4 5app load ["numposrepTheory","regexpLib", "wordsLib"]; 6 7open Regexp_Type regexpSyntax regexpTheory FormalLangTheory 8 numposrepTheory stringTheory arithmeticTheory; 9 10(*---------------------------------------------------------------------------*) 11(* Boilerplate *) 12(*---------------------------------------------------------------------------*) 13 14fun qspec q th = th |> Q.SPEC q 15fun qspec_arith q th = qspec q th |> SIMP_RULE arith_ss []; 16 17val [regexp_lang_chset,regexp_lang_cat, regexp_lang_star, 18 regexp_lang_neg, regexp_lang_or] = CONJUNCTS regexp_lang_def; 19 20val dot_star_lem = regexp_lang_dot_star 21 |> SIMP_RULE std_ss [DOT_def,charsetTheory.charset_full_thm] 22; 23 24(*---------------------------------------------------------------------------*) 25(* Build regexp (LSB) *) 26(*---------------------------------------------------------------------------*) 27 28val small_evens = filter (fn x => x mod 2 = 0) (upto 0 255); 29val sme_charset = Regexp_Type.charset_of (map Char.chr small_evens); 30val even_regexp = Cat(Chset sme_charset,Star DOT); 31val even_regexp_term = regexpSyntax.regexp_to_term even_regexp; 32 33(*---------------------------------------------------------------------------*) 34(* Support lemmas *) 35(*---------------------------------------------------------------------------*) 36 37val lemA = Q.prove 38(`!n. EVEN(n) <=> EVEN (n MOD 256)`, 39 metis_tac 40 [DIVISION |> qspec_arith `256` 41 |> qspec `n` 42 |> Q.AP_TERM `EVEN` 43 |> SIMP_RULE arith_ss [EVEN_ADD,EVEN_MULT,EVAL ``EVEN 256``]] 44); 45 46val lemB = Q.prove 47(`!n. EVEN(n) <=> HD (n2l 256 n) IN {n | n < 256 /\ EVEN n}`, 48 qsuff_tac 49 `!B n. (B=256) ==> (EVEN(n) <=> HD (n2l B n) IN {n | n < B /\ EVEN(n)})` 50 >- metis_tac [] 51 >- (recInduct n2l_ind 52 >> rw_tac list_ss [] 53 >> rw_tac list_ss [Once n2l_def] 54 >- rw_tac (list_ss ++ pred_setLib.PRED_SET_ss) [EVEN_MOD2] 55 >- (fs[] >> metis_tac [lemA])) 56); 57 58(*---------------------------------------------------------------------------*) 59(* Characterize sme_charset *) 60(*---------------------------------------------------------------------------*) 61 62val lemC = Q.prove 63(`!s. s IN regexp_lang(^(regexp_to_term (Chset sme_charset))) 64 <=> 65 ?c. (s = [c]) /\ EVEN(ORD c)`, 66 rw_tac (list_ss ++ pred_setLib.PRED_SET_ss ++ regexpLib.charset_conv_ss) 67 [EQ_IMP_THM,EVEN_MOD2] 68 >> EVAL_TAC 69 >> pop_assum mp_tac 70 >> Q.ID_SPEC_TAC `c` 71 >> HO_MATCH_MP_TAC CHAR_INDUCT_THM 72 >> simp_tac std_ss [ORD_CHR_RWT] 73 >> CONV_TAC (REPEATC(numLib.BOUNDED_FORALL_CONV EVAL)) 74 >> metis_tac []); 75 76(*---------------------------------------------------------------------------*) 77(* The main theorem *) 78(*---------------------------------------------------------------------------*) 79 80val EVEN_REGEXP_THM = Q.prove 81(`!n. EVEN(n) <=> MAP CHR (n2l 256 n) IN regexp_lang ^even_regexp_term`, 82 rw_tac (list_ss ++ pred_setLib.PRED_SET_ss) 83 [regexp_lang_cat,IN_dot,dot_star_lem,lemC,PULL_EXISTS,Once lemB] 84 >> ONCE_REWRITE_TAC [n2l_def] 85 >> rw_tac list_ss [EQ_IMP_THM,ORD_CHR_RWT]); 86 87(*---------------------------------------------------------------------------*) 88(* compile regexp to DFA *) 89(*---------------------------------------------------------------------------*) 90 91val [dfa_lang_thm,table_def, finals_def, start_def] = 92 CONJUNCTS 93 (regexpLib.dfa_by_proof ("even_regexp", even_regexp)); 94 95(*---------------------------------------------------------------------------*) 96(* |- !n. EVEN n <=> *) 97(* exec_dfa even_regexp_finals even_regexp_table even_regexp_start *) 98(* (MAP CHR (n2l 256 n)) *) 99(*---------------------------------------------------------------------------*) 100 101val EVEN_IFF_DFA = 102 SIMP_RULE std_ss [GSYM dfa_lang_thm,IN_DEF] EVEN_REGEXP_THM; 103 104fun EVEN_BY_DFA_CONV tm = 105 let val thm = SPEC tm EVEN_IFF_DFA 106 val tm = rhs(concl thm) 107 in 108 TRANS thm (EVAL tm) 109 end; 110 111val even_by_dfa = EVEN_BY_DFA_CONV o numSyntax.mk_numeral o Arbnum.fromLargeInt 112 113(*--------------------------------------------------------------------------- 114 map even_by_dfa [0,1,2,4,8,16,32,64,128,256,512,1024,1025, 2048, 65536, 65537, 115 24524542352452435245452345000929592934535252]; 116 117 Note that REDUCE_CONV is faster, since it just looks at the last "digit" of 118 the number, while the DFA has to process the entire string. The DFA could 119 be optimized so that when it enters a state that is guaranteed to lead to 120 acceptance (or to rejection), the rest of the string doesn't need 121 processing. 122 ---------------------------------------------------------------------------*) 123