1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/"); 7loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat 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", "arithmeticTheory"]; 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 arithmeticTheory; 18open Sanity; 19 20val _ = hide "S"; 21val _ = hide "I"; 22val _ = hide "K"; 23 24(* 25show_assums := false; 26show_assums := true; 27show_types := true; 28show_types := false; 29quietdec := false; 30*) 31 32 33val _ = new_theory "symbolic_kripke_structure"; 34 35 36val symbolic_kripke_structure_def = 37 Hol_datatype 38 `symbolic_kripke_structure = 39 <| S0: 'state prop_logic; (*initial states*) 40 R: 'state xprop_logic (*transition function*) 41 |>`; 42 43 44 45val symbolic_kripke_structure_S0 = DB.fetch "-" "symbolic_kripke_structure_S0"; 46val symbolic_kripke_structure_R = DB.fetch "-" "symbolic_kripke_structure_R"; 47val symbolic_kripke_structure_11 = DB.fetch "-" "symbolic_kripke_structure_11"; 48 49val symbolic_kripke_structure_REWRITES = save_thm("symbolic_kripke_structure_REWRITES", LIST_CONJ [symbolic_kripke_structure_S0, symbolic_kripke_structure_R, 50symbolic_kripke_structure_11]); 51 52 53val IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def = 54 Define 55 `IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K p = 56 ((!n. XP_SEM K.R (p n, p (SUC n))))`; 57 58 59val IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def = 60 Define 61 `IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K FC p = 62 (IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K p /\ 63 (!b. MEM b FC ==> (!t0. ?t. t >= t0 /\ (P_SEM (p t) b))))`; 64 65 66val IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___ALTERNATIVE_DEF = 67 store_thm ("IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___ALTERNATIVE_DEF", 68 ``IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K FC p = 69 (IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K p /\ 70 (!b. MEM b FC ==> (!t0. ?t. (P_SEM (p (t0 + t + 1)) b))))``, 71 72 REWRITE_TAC[IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def] THEN 73 BOOL_EQ_STRIP_TAC THEN 74 FORALL_EQ_STRIP_TAC THEN 75 BOOL_EQ_STRIP_TAC THEN 76 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 77 Q_SPEC_NO_ASSUM 0 `SUC t0` THEN 78 CLEAN_ASSUMPTIONS_TAC THEN 79 Q_TAC EXISTS_TAC `PRE (t - t0)` THEN 80 `t0 + PRE (t - t0) + 1 = t` by DECIDE_TAC THEN 81 ASM_REWRITE_TAC[], 82 83 Q_SPEC_NO_ASSUM 0 `t0` THEN 84 CLEAN_ASSUMPTIONS_TAC THEN 85 Q_TAC EXISTS_TAC `t0 + t + 1` THEN 86 ASM_SIMP_TAC arith_ss [] 87 ]); 88 89 90 91 92 93val IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def = 94 Define 95 `IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K p = 96 (IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K p /\ P_SEM (p 0) K.S0)`; 97 98val IS_FAIR_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def = 99 Define 100 `IS_FAIR_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K FC p = 101 (IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K FC p /\ 102 P_SEM (p 0) K.S0)`; 103 104 105val PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES = 106 save_thm ("PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES", 107 LIST_CONJ [IS_FAIR_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 108 IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 109 IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 110 IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def]); 111 112 113val IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___EMPTY_FAIRNESS = 114 store_thm ( 115 "IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___EMPTY_FAIRNESS", 116 ``!K p. (IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K [] p = 117 IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K p) /\ 118 (IS_FAIR_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K [] p = 119 IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K p)``, 120 121 SIMP_TAC list_ss [IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 122 IS_FAIR_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 123 IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def]); 124 125 126 127 128val IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_def = 129 Define 130 `IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE K FC = 131 !p. ~(IS_FAIR_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K FC p)`; 132 133 134val IS_EMPTY_SYMBOLIC_KRIPKE_STRUCTURE_def = 135 Define 136 `IS_EMPTY_SYMBOLIC_KRIPKE_STRUCTURE K = 137 !p. ~(IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE K p)`; 138 139 140val SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def = 141 Define 142 `SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT (K1:'a symbolic_kripke_structure) (K2:'a symbolic_kripke_structure) = 143 symbolic_kripke_structure (P_AND(K1.S0, K2.S0)) (XP_AND(K1.R, K2.R))`; 144 145 146val SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def = 147 Define 148 `SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS (K:'a symbolic_kripke_structure) = 149 (P_USED_VARS K.S0) UNION (XP_USED_VARS K.R)`; 150 151 152val SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING_def = 153 Define 154 `SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING f (K:'a symbolic_kripke_structure) = 155 symbolic_kripke_structure (P_VAR_RENAMING f K.S0) (XP_VAR_RENAMING f K.R)`; 156 157 158 159 160val IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___IDENTIFY_VARIABLES = 161 store_thm ( 162 "IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___IDENTIFY_VARIABLES", 163 164 ``!f K fc. 165 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE K fc ==> 166 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING f K) (MAP (P_VAR_RENAMING f) fc)``, 167 168 SIMP_TAC std_ss [IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_def, 169 PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, 170 SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING_def, 171 symbolic_kripke_structure_REWRITES, 172 MEM_MAP, GSYM LEFT_EXISTS_AND_THM, 173 P_SEM___VAR_RENAMING___NOT_INJ, 174 XP_SEM___VAR_RENAMING___NOT_INJ]); 175 176 177 178val IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___VAR_RENAMING = 179 store_thm ( 180 "IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___VAR_RENAMING", 181 182 ``!f K fc. INJ f 183 (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS K UNION 184 LIST_BIGUNION (MAP P_USED_VARS fc)) UNIV ==> 185 186 (IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE K fc = 187 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING f K) (MAP (P_VAR_RENAMING f) fc))``, 188 189 REPEAT STRIP_TAC THEN EQ_TAC THEN1 REWRITE_TAC[IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___IDENTIFY_VARIABLES] THEN 190 191 SIMP_TAC std_ss [IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_def, 192 PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, 193 SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING_def, 194 symbolic_kripke_structure_REWRITES, 195 MEM_MAP, GSYM LEFT_EXISTS_AND_THM] THEN 196 REPEAT STRIP_TAC THEN 197 `?w. w = PATH_RESTRICT p (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS K UNION 198 LIST_BIGUNION (MAP P_USED_VARS fc))` by PROVE_TAC[] THEN 199 SUBGOAL_TAC `(((?n. ~XP_SEM K.R (p n,p (SUC n))) \/ 200 ?b. MEM b fc /\ ?t0. !t. ~(t >= t0) \/ ~P_SEM (p t) b) \/ 201 ~P_SEM (p 0) K.S0) = 202 (((?n. ~XP_SEM K.R (w n,w (SUC n))) \/ 203 ?b. MEM b fc /\ ?t0. !t. ~(t >= t0) \/ ~P_SEM (w t) b) \/ 204 ~P_SEM (w 0) K.S0)` THEN1 ( 205 ASM_SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def] THEN 206 BINOP_TAC THENL [ 207 BINOP_TAC, 208 ALL_TAC 209 ] THENL [ 210 EXISTS_EQ_STRIP_TAC THEN 211 SIMP_TAC std_ss [] THEN 212 MATCH_MP_TAC XP_USED_VARS_INTER_SUBSET_BOTH_THM THEN 213 SIMP_TAC std_ss [SUBSET_DEF, SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, IN_UNION], 214 215 EXISTS_EQ_STRIP_TAC THEN 216 BOOL_EQ_STRIP_TAC THEN 217 EXISTS_EQ_STRIP_TAC THEN 218 FORALL_EQ_STRIP_TAC THEN 219 BOOL_EQ_STRIP_TAC THEN 220 SIMP_TAC std_ss [] THEN 221 MATCH_MP_TAC P_USED_VARS_INTER_SUBSET_THM THEN 222 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, IN_LIST_BIGUNION, MEM_MAP] THEN 223 PROVE_TAC[], 224 225 SIMP_TAC std_ss [] THEN 226 MATCH_MP_TAC P_USED_VARS_INTER_SUBSET_THM THEN 227 SIMP_TAC std_ss [SUBSET_DEF, SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, IN_UNION] 228 ] 229 ) THEN 230 ONCE_ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 231 232 `!n. w n SUBSET (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS K UNION 233 LIST_BIGUNION (MAP P_USED_VARS fc))` by PROVE_TAC[PATH_RESTRICT_SUBSET] THEN 234 GSYM_NO_TAC 1 THEN 235 236 Q_SPEC_NO_ASSUM 2 `PATH_VAR_RENAMING f w` THEN 237 UNDISCH_HD_TAC THEN 238 SIMP_TAC std_ss [PATH_VAR_RENAMING_def, PATH_MAP_def] THEN 239 IMP_TO_EQ_TAC THEN 240 BINOP_TAC THENL [ 241 BINOP_TAC, 242 ALL_TAC 243 ] THENL [ 244 EXISTS_EQ_STRIP_TAC THEN 245 SIMP_TAC std_ss [] THEN 246 MATCH_MP_TAC (GSYM XP_SEM___VAR_RENAMING) THEN 247 UNDISCH_NO_TAC 2 THEN 248 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 249 SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def] THEN 250 PROVE_TAC[], 251 252 EXISTS_EQ_STRIP_TAC THEN 253 BOOL_EQ_STRIP_TAC THEN 254 EXISTS_EQ_STRIP_TAC THEN 255 FORALL_EQ_STRIP_TAC THEN 256 BOOL_EQ_STRIP_TAC THEN 257 SIMP_TAC std_ss [] THEN 258 MATCH_MP_TAC (GSYM P_SEM___VAR_RENAMING) THEN 259 UNDISCH_NO_TAC 4 THEN 260 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 261 SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, 262 IN_LIST_BIGUNION, MEM_MAP] THEN 263 METIS_TAC[], 264 265 SIMP_TAC std_ss [] THEN 266 MATCH_MP_TAC (GSYM P_SEM___VAR_RENAMING) THEN 267 UNDISCH_NO_TAC 2 THEN 268 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 269 SIMP_ALL_TAC std_ss [SUBSET_DEF, SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, IN_UNION] THEN 270 PROVE_TAC[] 271 ]); 272 273 274val _ = export_theory(); 275