1open HolKernel Parse boolLib bossLib;
2
3val _ = new_theory "regexSemantics";
4
5
6
7(* 3.1 basic regular expression semantics *)
8(* -------------------------------------------------------------------------------------------------- *)
9val _ = Datatype regexDatatypes.Reg_datatype_quot;
10
11val language_of_def = Define `
12         (language_of (Eps)        = {[]}                                                       ) /\
13         (language_of (Sym (c:'a)) = {[c]}                                                      ) /\
14         (language_of (Alt r1 r2)  = { w      | w IN (language_of r1) \/ w IN (language_of r2) }) /\
15         (language_of (Seq r1 r2)  = { u ++ v | u IN (language_of r1) /\ v IN (language_of r2) }) /\
16         (language_of (Rep r)      = { FLAT l | EVERY (\w. w IN (language_of r)) l }            )
17`;
18
19
20
21
22(* rewrite theorems *)
23(* ----------------------------------------------------------------------------- *)
24val language_of_DEFs = store_thm ("language_of_DEFs", ``
25         (        language_of (Eps)        = {[]}                                                       ) /\
26         (!c.     language_of (Sym c)      = {[c]}                                                      ) /\
27         (!r1 r2. language_of (Alt r1 r2)  = { w      | w IN (language_of r1) \/ w IN (language_of r2) }) /\
28         (!r1 r2. language_of (Seq r1 r2)  = { u ++ v | u IN (language_of r1) /\ v IN (language_of r2) }) /\
29         (!r.     language_of (Rep r)      = { FLAT l | EVERY (\w. w IN (language_of r)) l }            )
30``,
31
32  REWRITE_TAC [language_of_def]
33);
34
35
36
37
38(* sanity check and helper lemmata *)
39(* ----------------------------------------------------------------------------- *)
40val language_of_Alt_OR = store_thm ("language_of_Alt_OR", ``
41         (!w r1 r2. w IN language_of (Alt r1 r2) <=> w IN language_of r1 \/ w IN language_of r2)
42``,
43
44  SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss) [language_of_DEFs, pred_setTheory.IN_UNION]
45);
46
47(* val IN_GSPEC_IFF_GEN = Q.GENL [`P`, `y`] pred_setTheory.IN_GSPEC_IFF; *)
48val language_of_Seq_APPEND = store_thm ("language_of_Seq_APPEND", ``
49         (!u v r1 r2. (u IN language_of r1 /\ v IN language_of r2) ==> (u ++ v) IN language_of (Seq r1 r2))
50``,
51
52  SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss) [language_of_DEFs] >>
53  METIS_TAC []
54);
55
56val language_of_Rep_empty = store_thm ("language_of_Rep_empty", ``
57         (!r. [] IN language_of (Rep r))
58``,
59
60  SIMP_TAC (list_ss++pred_setSimps.PRED_SET_ss) [language_of_DEFs] >>
61  GEN_TAC >> Q.EXISTS_TAC `[]` >>
62  SIMP_TAC list_ss []
63);
64
65(* ok, but not quite all - just 2 *)
66val language_of_Rep_APPEND2 = store_thm ("language_of_Rep_APPEND2", ``
67         (!u v r. (u IN language_of r /\ v IN language_of r) ==> (u ++ v) IN language_of (Rep r))
68``,
69
70  REPEAT STRIP_TAC >>
71  SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss) [language_of_DEFs] >>
72  Q.EXISTS_TAC `[u;v]` >>
73  ASM_SIMP_TAC list_ss []
74);
75
76val language_of_Rep_APPEND_rec = store_thm ("language_of_Rep_APPEND_rec", ``
77         (!u v r. (u IN language_of (Rep r) /\ v IN language_of (Rep r)) ==> (u ++ v) IN language_of (Rep r))
78``,
79
80  REPEAT STRIP_TAC >>
81  FULL_SIMP_TAC (bool_ss++pred_setSimps.PRED_SET_ss) [language_of_DEFs, GSYM rich_listTheory.FLAT_FOLDL] >>
82  rename1 `FLAT l1 ++ FLAT l2` >>
83
84  Q.LIST_EXISTS_TAC [`l1++l2`] >>
85  ASM_SIMP_TAC list_ss []
86);
87
88
89
90
91
92
93
94
95
96
97val _ = export_theory();
98