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