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