1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val home_dir = (Globals.HOLDIR ^ "/examples/temporal_deep/"); 7loadPath := (home_dir ^ "src/deep_embeddings") :: 8 (home_dir ^ "src/tools") :: !loadPath; 9 10map load 11 ["xprop_logicTheory", "prop_logicTheory", "infinite_pathTheory", "pred_setTheory", "listTheory", "pairTheory", "set_lemmataTheory", 12 "containerTheory", "prim_recTheory", "tuerk_tacticsLib", "temporal_deep_mixedTheory"]; 13*) 14 15open infinite_pathTheory pred_setTheory listTheory pairTheory xprop_logicTheory 16 containerTheory prop_logicTheory set_lemmataTheory prim_recTheory 17 tuerk_tacticsLib temporal_deep_mixedTheory; 18open Sanity; 19 20val _ = hide "S"; 21val _ = hide "I"; 22 23(* 24show_assums := false; 25show_assums := true; 26show_types := true; 27show_types := false; 28quietdec := false; 29*) 30 31 32val _ = new_theory "semi_automaton"; 33val _ = ParseExtras.temp_loose_equality() 34 35 36 37(*****************************************************************************) 38(* representation of non deterministic semi automata, that use *) 39(* the powerset of a set of propositional varibales as inputs *) 40(*****************************************************************************) 41val semi_automaton_def = 42 Hol_datatype 43 `semi_automaton = 44 <| S: 'state set; (*set of states *) 45 I: 'input set; (*set of inputs *) 46 S0: ('state # 'input set) set; (*initial states*) 47 R: ('state # 'input set # 'state # 'input set) set (*transition relation*) |>`; 48 49 50 51val semi_automaton_S = DB.fetch "-" "semi_automaton_S"; 52val semi_automaton_I = DB.fetch "-" "semi_automaton_I"; 53val semi_automaton_S0 = DB.fetch "-" "semi_automaton_S0"; 54val semi_automaton_R = DB.fetch "-" "semi_automaton_R"; 55val semi_automaton_11 = DB.fetch "-" "semi_automaton_11"; 56 57val semi_automaton_REWRITES = save_thm("semi_automaton_REWRITES", LIST_CONJ [semi_automaton_S, semi_automaton_I, semi_automaton_S0, semi_automaton_R, semi_automaton_11]); 58 59 60val IS_WELL_FORMED_SEMI_AUTOMATON_def = 61 Define 62 `IS_WELL_FORMED_SEMI_AUTOMATON A = 63 (FINITE A.S /\ FINITE A.I /\ A.S0 SUBSET (A.S CROSS (POW A.I)) /\ 64 A.R SUBSET (A.S CROSS ((POW A.I) CROSS (A.S CROSS (POW A.I)))))` 65 66(*****************************************************************************) 67(* RUN A i w is true iff p is a run of i through A *) 68(*****************************************************************************) 69val IS_RUN_THROUGH_SEMI_AUTOMATON_def = 70 Define 71 `IS_RUN_THROUGH_SEMI_AUTOMATON A i w = 72 ((!n. w n IN A.S) /\ 73 ((w 0, (i 0) INTER A.I) IN A.S0) /\ 74 (!n. (w n, (i n) INTER A.I, w (SUC n), (i (SUC n)) INTER A.I) IN A.R))`; 75 76 77val IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE_def = 78 Define 79 `IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE A i w s m = 80 ((!n. n <= m ==> (w n IN A.S)) /\ 81 ((w 0, (i 0) INTER A.I) IN A.S0) /\ (w m = s) /\ 82 (!n. n < m ==> ((w n, (i n) INTER A.I, w (SUC n), (i (SUC n)) INTER A.I) IN A.R)))`; 83 84 85val IS_DET_TOTAL_SEMI_AUTOMATON_def = 86 Define 87 `IS_DET_TOTAL_SEMI_AUTOMATON A = 88 ((!i. ?!x. (x, i INTER A.I) IN A.S0) /\ 89 !s i i'. (s IN A.S /\ i SUBSET A.I /\ i' SUBSET A.I) ==> 90 (?!s'. (s, i, s', i') IN A.R))`; 91 92 93val IS_DET_TOTAL_SEMI_AUTOMATON___UNIQUE_RUN_EXISTS = 94 store_thm ( 95 "IS_DET_TOTAL_SEMI_AUTOMATON___UNIQUE_RUN_EXISTS", 96 97 ``!A. (IS_DET_TOTAL_SEMI_AUTOMATON A /\ 98 IS_WELL_FORMED_SEMI_AUTOMATON A) ==> 99 (!i. ?!w. IS_RUN_THROUGH_SEMI_AUTOMATON A i w)``, 100 101 102 SIMP_TAC std_ss [IS_RUN_THROUGH_SEMI_AUTOMATON_def, 103 EXISTS_UNIQUE_DEF, 104 IS_DET_TOTAL_SEMI_AUTOMATON_def, 105 IS_WELL_FORMED_SEMI_AUTOMATON_def, 106 SUBSET_DEF, IN_CROSS, IN_POW, 107 prove (``!P. (!x. P x) = (!x1 x2 x3 x4. P (x1,x2,x3, x4))``, 108 METIS_TAC[FST, SND, PAIR]) 109 ] THEN 110 REPEAT GEN_TAC THEN STRIP_TAC THEN 111 GEN_TAC THEN 112 Q_SPEC_NO_ASSUM 5 `i 0` THEN 113 SIMP_ALL_TAC std_ss [] THEN 114 REPEAT STRIP_TAC THENL [ 115 `?w. w = CHOOSEN_PATH {x} (\s n. ({s' | (s, i (PRE n) INTER A.I, s', (i n) INTER A.I) IN A.R}))` by METIS_TAC[] THEN 116 `!n. w n IN A.S` by ( 117 Induct_on `n` THENL [ 118 ASM_SIMP_TAC std_ss [CHOOSEN_PATH_def, IN_SING] THEN 119 PROVE_TAC[FST], 120 121 ASM_SIMP_TAC std_ss [CHOOSEN_PATH_def] THEN 122 GSYM_NO_TAC 1 THEN 123 ASM_REWRITE_TAC[] THEN 124 SIMP_TAC std_ss [GSPECIFICATION] THEN 125 SELECT_ELIM_TAC THEN 126 REPEAT STRIP_TAC THENL [ 127 Q_SPECL_NO_ASSUM 8 [`w n`, `i n INTER A.I`, `(i (SUC n)) INTER A.I`] THEN 128 UNDISCH_HD_TAC THEN 129 ASM_SIMP_TAC std_ss [IN_INTER], 130 131 METIS_TAC[] 132 ] 133 ] 134 ) THEN 135 136 Q_TAC EXISTS_TAC `w` THEN 137 REPEAT STRIP_TAC THENL [ 138 PROVE_TAC[], 139 140 `w 0 = x` suffices_by METIS_TAC[] THEN 141 ASM_REWRITE_TAC [CHOOSEN_PATH_def, IN_SING] THEN 142 SIMP_TAC std_ss [], 143 144 ASM_REWRITE_TAC [CHOOSEN_PATH_def] THEN 145 GSYM_NO_TAC 1 THEN 146 ASM_REWRITE_TAC [CHOOSEN_PATH_def] THEN 147 SELECT_ELIM_TAC THEN 148 SIMP_TAC std_ss [GSPECIFICATION] THEN 149 Q_SPECL_NO_ASSUM 8 [`w n`, `i n INTER A.I`, `(i (SUC n)) INTER A.I`] THEN 150 UNDISCH_HD_TAC THEN 151 ASM_SIMP_TAC std_ss [IN_INTER] 152 ], 153 154 155 156 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 157 GEN_TAC THEN 158 Induct_on `x''` THENL [ 159 PROVE_TAC[], 160 161 Q_SPECL_NO_ASSUM 13 [`y x''`, `i x'' INTER A.I`, `i (SUC x'') INTER A.I`] THEN 162 UNDISCH_HD_TAC THEN 163 ASM_SIMP_TAC std_ss [IN_INTER] THEN 164 REPEAT STRIP_TAC THEN 165 PROVE_TAC[] 166 ] 167 ]); 168 169 170 171 172 173 174val SEMI_AUTOMATON_STATE_VAR_RENAMING_def = 175 Define 176 `SEMI_AUTOMATON_STATE_VAR_RENAMING A f g = 177 (semi_automaton (IMAGE f A.S) A.I (\(s,i). (g s, i) IN A.S0) 178 (\(s1, i, s2, i'). (g s1, i, g s2, i') IN A.R))`; 179 180val SEMI_AUTOMATON_STATE_VAR_RENAMING___RUN = 181 store_thm ( 182 "SEMI_AUTOMATON_STATE_VAR_RENAMING___RUN", 183 ``(!A f g i w. 184 IS_WELL_FORMED_SEMI_AUTOMATON A /\ INJ f A.S UNIV /\ 185 (!s. s IN A.S ==> (g (f s) = s)) /\ (!n. w n IN A.S) ==> 186 (IS_RUN_THROUGH_SEMI_AUTOMATON 187 (SEMI_AUTOMATON_STATE_VAR_RENAMING A f g) i 188 (PATH_MAP (\n. f) w) = 189 IS_RUN_THROUGH_SEMI_AUTOMATON A i w)) /\ 190 (!A:('a, 'b) semi_automaton (f:'b -> 'c) g i w. 191 IS_WELL_FORMED_SEMI_AUTOMATON A /\ INJ f A.S UNIV /\ 192 (!s. s IN A.S ==> (g (f s) = s)) /\ 193 (!n. w n IN IMAGE f A.S) ==> 194 (IS_RUN_THROUGH_SEMI_AUTOMATON 195 (SEMI_AUTOMATON_STATE_VAR_RENAMING A f g) i w = 196 IS_RUN_THROUGH_SEMI_AUTOMATON A i (PATH_MAP (\n. g) w)))``, 197 198 199SIMP_TAC std_ss [IS_RUN_THROUGH_SEMI_AUTOMATON_def, 200 SEMI_AUTOMATON_STATE_VAR_RENAMING_def, 201 semi_automaton_REWRITES, IN_IMAGE, 202 PATH_MAP_def, 203 IS_WELL_FORMED_SEMI_AUTOMATON_def, 204 INJ_DEF, SUBSET_DEF, IN_CROSS, 205 prove(``!P x1 x2 x3 x4. (x1, x2, x3, x4) IN (\(x1,x2,x3,x4). P x1 x2 x3 x4) = (P x1 x2 x3 x4)``, 206 SIMP_TAC std_ss [IN_DEF]), 207 prove(``!P x1 x2. (x1, x2) IN (\(x1,x2). P x1 x2) = (P x1 x2)``, 208 SIMP_TAC std_ss [IN_DEF])] THEN 209REPEAT STRIP_TAC THEN 210REPEAT BOOL_EQ_STRIP_TAC THEN 211METIS_TAC[FST, SND]); 212 213 214 215 216 217val _ = export_theory(); 218