open HolKernel Parse boolLib bossLib; (* quietdec := true; val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/"); loadPath := (concat home_dir "src/deep_embeddings") :: (concat home_dir "src/translations") :: (concat home_dir "src/tools") :: (concat hol_dir "examples/PSL/path") :: (concat hol_dir "examples/PSL/1.1/official-semantics") :: !loadPath; map load ["full_ltlTheory", "arithmeticTheory", "automaton_formulaTheory", "xprop_logicTheory", "prop_logicTheory", "infinite_pathTheory", "tuerk_tacticsLib", "symbolic_semi_automatonTheory", "listTheory", "pred_setTheory", "pred_setTheory", "rich_listTheory", "set_lemmataTheory", "temporal_deep_mixedTheory", "pairTheory", "symbolic_kripke_structureTheory", "numLib", "semi_automatonTheory", "omega_automatonTheory", "omega_automaton_translationsTheory", "ctl_starTheory", "ltl_to_automaton_formulaTheory", "containerTheory", "psl_to_rltlTheory", "rltl_to_ltlTheory", "temporal_deep_simplificationsLib", "congLib", "kripke_structureTheory"]; *) open full_ltlTheory arithmeticTheory automaton_formulaTheory xprop_logicTheory prop_logicTheory infinite_pathTheory tuerk_tacticsLib symbolic_semi_automatonTheory listTheory pred_setTheory pred_setTheory rich_listTheory set_lemmataTheory temporal_deep_mixedTheory pairTheory symbolic_kripke_structureTheory numLib semi_automatonTheory omega_automatonTheory omega_automaton_translationsTheory ctl_starTheory ltl_to_automaton_formulaTheory containerTheory psl_to_rltlTheory rltl_to_ltlTheory temporal_deep_simplificationsLib congLib kripke_structureTheory; open Sanity; val _ = hide "K"; val _ = hide "S"; val _ = hide "I"; (* show_assums := false; show_assums := true; show_types := true; show_types := false; quietdec := false; *) val _ = new_theory "ibm"; val A_UNIV___LTL_KS_SEM___CONCRETE_THM = store_thm ( "A_UNIV___LTL_KS_SEM___CONCRETE_THM", ``!A ac l. (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l)) ==> (!i w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w ==> (((A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = LTL_SEM i l) = LTL_SEM (INPUT_RUN_PATH_UNION A i w) (LTL_EQUIV (ACCEPT_COND_TO_LTL ac, l)))))``, REPEAT STRIP_TAC THEN SIMP_TAC std_ss [A_SEM_THM, SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE___INITIAL_PATH] THEN `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w` by PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN WEAKEN_HD_TAC THEN `(!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w ==> ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac) = ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac` by METIS_TAC[] THEN ASM_SIMP_TAC std_ss [LTL_SEM_THM, ACCEPT_COND_TO_LTL_THM] THEN MATCH_MP_TAC (prove (``(A = C) ==> ((B = A) = (B = C))``, PROVE_TAC[])) THEN ONCE_REWRITE_TAC[LTL_USED_VARS_INTER_THM] THEN AP_THM_TAC THEN AP_TERM_TAC THEN ONCE_REWRITE_TAC [FUN_EQ_THM] THEN GEN_TAC THEN UNDISCH_NO_TAC 3 (*DISJOINT A.S (LTL_USED_VARS l)*) THEN `PATH_SUBSET w A.S` by FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN UNDISCH_HD_TAC THEN REPEAT WEAKEN_HD_TAC THEN SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, DISJOINT_DISJ_THM, INPUT_RUN_PATH_UNION_def, EXTENSION, INPUT_RUN_STATE_UNION_def, IN_UNION, IN_INTER, IN_DIFF, PATH_SUBSET_def, SUBSET_DEF] THEN METIS_TAC[] ); val A_UNIV___A_SEM___CONCRETE_THM = store_thm ( "A_UNIV___A_SEM___CONCRETE_THM", ``!A ac (l:'a ltl). (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l) /\ FINITE A.S /\ INFINITE (UNIV:'a set)) ==> (?A' fc p. FINITE A'.S /\ (!i. (((A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = LTL_SEM i l) = (A_SEM i (A_UNIV (A', A_IMPL(A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc), ACCEPT_COND_PROP p))))))))``, REPEAT STRIP_TAC THEN ASSUME_TAC A_UNIV___LTL_KS_SEM___CONCRETE_THM THEN Q_SPECL_NO_ASSUM 0 [`A`, `ac`, `l`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC std_ss [] THEN `?pf DS. (pf, DS) = LTL_TO_GEN_BUECHI (LTL_EQUIV (ACCEPT_COND_TO_LTL ac,l)) F T` by METIS_TAC[PAIR] THEN `?UV. UV = (P_USED_VARS A.S0 UNION XP_USED_VARS A.R UNION (ACCEPT_COND_USED_VARS ac) UNION LTL_USED_VARS l UNION A.S)` by METIS_TAC[] THEN SUBGOAL_TAC `DS.IV SUBSET UV` THEN1 ( `DS.IV = LTL_USED_VARS (LTL_EQUIV (ACCEPT_COND_TO_LTL ac,l))` by METIS_TAC[LTL_TO_GEN_BUECHI___USED_INPUT_VARS, SND] THEN ASM_SIMP_TAC std_ss [SUBSET_DEF, LTL_USED_VARS_EVAL, LTL_USED_VARS___ACCEPT_COND_TO_LTL, DISJOINT_DISJ_THM, IN_UNION] THEN PROVE_TAC[] ) THEN SUBGOAL_TAC `FINITE UV` THEN1 ( ASM_SIMP_TAC std_ss [FINITE_UNION, FINITE___P_USED_VARS, FINITE___XP_USED_VARS, FINITE___LTL_USED_VARS, FINITE___ACCEPT_COND_USED_VARS] ) THEN `?sv. IS_ELEMENT_ITERATOR sv DS.SN UV` by METIS_TAC[IS_ELEMENT_ITERATOR_EXISTS] THEN ASSUME_TAC LTL_TO_GEN_BUECHI_DS___SEM___MIN THEN Q_SPECL_NO_ASSUM 0 [`DS`, `LTL_EQUIV (ACCEPT_COND_TO_LTL ac,l)`, `pf`, `sv`, `F`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( REPEAT STRIP_TAC THENL [ ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def] THEN PROVE_TAC[IS_ELEMENT_ITERATOR_SUBSET], METIS_TAC[LTL_TO_GEN_BUECHI_THM, SND, FST], METIS_TAC[LTL_TO_GEN_BUECHI_THM, SND, FST] ] ) THEN FULL_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN SIMP_ALL_TAC std_ss [LTL_TO_GEN_BUECHI_DS___A_UNIV_def, LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def] THEN Q.ABBREV_TAC `B = (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv)` THEN Q_TAC EXISTS_TAC `PRODUCT_SEMI_AUTOMATON A B` THEN Q_TAC EXISTS_TAC `MAP (\x. x sv) DS.FC` THEN Q_TAC EXISTS_TAC `pf sv` THEN REPEAT STRIP_TAC THENL [ Q.UNABBREV_TAC `B` THEN ASM_SIMP_TAC std_ss [PRODUCT_SEMI_AUTOMATON_REWRITES, FINITE_UNION, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS___FINITE], `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w` by PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN Q_SPECL_NO_ASSUM 8 [`i`, `w`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN SIMP_TAC std_ss [MAP_MAP_o, combinTheory.o_DEF] THEN ASSUME_TAC (SIMP_RULE std_ss [RIGHT_FORALL_IMP_THM] (GSYM TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_PRODUCT_THM)) THEN Q_SPECL_NO_ASSUM 0 [`A`, `B`, `i`, `w`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( Q.UNABBREV_TAC `B` THEN ASM_SIMP_TAC std_ss [DISJOINT_DISJ_THM, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, IN_ABS] THEN SIMP_ALL_TAC std_ss [IS_ELEMENT_ITERATOR_def] THEN GEN_TAC THEN RIGHT_DISJ_TAC THEN SIMP_ALL_TAC std_ss [] THEN `~(x IN UV)` by METIS_TAC[] THEN UNDISCH_HD_TAC THEN ASM_SIMP_TAC std_ss [IN_UNION] ) THEN ASM_SIMP_TAC std_ss [] ] ); val IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS = store_thm ( "IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS", ``!A p (l:'a ltl). INFINITE (UNIV:'a set) /\ FINITE A.S ==> ((!K. (A_KS_SEM K (A_UNIV (A, ACCEPT_COND_G p)) = LTL_KS_SEM K l)) = (!i. A_SEM i (A_UNIV (A, ACCEPT_COND_G p)) = LTL_SEM i l))``, REPEAT STRIP_TAC THEN EQ_TAC THENL [ ALL_TAC, SIMP_TAC std_ss [A_KS_SEM_def, LTL_KS_SEM_def] ] THEN REPEAT STRIP_TAC THEN CCONTR_TAC THEN REMAINS_TAC `?i'. IS_ULTIMATIVELY_PERIODIC_PATH i' /\ ~(A_SEM i' (A_UNIV (A,ACCEPT_COND_G p)) = LTL_SEM i' l)` THEN1 ( `?V. V = SEMI_AUTOMATON_USED_INPUT_VARS A UNION (P_USED_VARS p DIFF A.S) UNION LTL_USED_VARS l` by METIS_TAC[] THEN ASSUME_TAC ULTIMALTIVELY_PERIODIC_PATH_CORRESPONDING_TO_UNIQUE_PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURES THEN Q_SPECL_NO_ASSUM 0 [`i'`, `V`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( ASM_SIMP_TAC std_ss [FINITE_UNION, FINITE___LTL_USED_VARS, FINITE___SEMI_AUTOMATON_USED_INPUT_VARS, FINITE___P_USED_VARS, FINITE_DIFF] ) THEN CLEAN_ASSUMPTIONS_TAC THEN SUBGOAL_TAC `!i. LTL_SEM i l = LTL_SEM (PATH_RESTRICT i V) l` THEN1 ( SIMP_TAC std_ss [LTL_SEM_def] THEN METIS_TAC[LTL_USED_VARS_INTER_SUBSET_THM, SUBSET_UNION] ) THEN SUBGOAL_TAC `!i. A_SEM i (A_UNIV (A,ACCEPT_COND_G p)) = A_SEM (PATH_RESTRICT i V) (A_UNIV (A,ACCEPT_COND_G p))` THEN1 ( MATCH_MP_TAC A_USED_INPUT_VARS_INTER_SUBSET_THM THEN ASM_SIMP_TAC std_ss [A_USED_INPUT_VARS_def, A_UNIV_def, ACCEPT_COND_G_def, ACCEPT_COND_USED_VARS_def, SUBSET_DEF, IN_UNION] ) THEN Q_SPEC_NO_ASSUM 8 `M` THEN UNDISCH_HD_TAC THEN SIMP_TAC std_ss [A_KS_SEM_def, LTL_KS_SEM_def] THEN METIS_TAC[] ) THEN WEAKEN_NO_TAC 1 (*clean up LTL_KS_SEM M ...*) THEN ASSUME_TAC SYMBOLIC___UNIV_G___TO___DET_GF___EXISTS_THM THEN Q_SPECL_NO_ASSUM 0 [`LTL_USED_VARS l`, `A`, `p`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[FINITE___LTL_USED_VARS] THEN CLEAN_ASSUMPTIONS_TAC THEN FULL_SIMP_TAC std_ss [ACCEPT_COND_GF_def] THEN WEAKEN_NO_TAC 4 THEN ASSUME_TAC A_UNIV___A_SEM___CONCRETE_THM THEN Q_SPECL_NO_ASSUM 0 [`A'`, `ACCEPT_G (ACCEPT_F (ACCEPT_PROP p'))`, `l`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN FULL_SIMP_TAC std_ss [] THEN FULL_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN SUBGOAL_TAC `?B fc' p'. FINITE B.S /\ IS_SIMPLE_SYMBOLIC_SEMI_AUTOMATON B /\ (!i. A_SEM i (A_UNIV (A'', A_IMPL (A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc), ACCEPT_COND_PROP p))) = A_SEM i (A_UNIV (B, A_IMPL (A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc'), ACCEPT_COND_PROP p'))))` THEN1 ( SUBGOAL_TAC `!i A fc p. A_SEM i (A_UNIV (A, A_IMPL (A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc), ACCEPT_COND_PROP p))) = A_SEM i (A_UNIV (A, ACCEPT_COND (ACCEPT_IMPL (ACCEPT_BIGAND (MAP (\x. ACCEPT_G (ACCEPT_F (ACCEPT_PROP x))) fc), ACCEPT_PROP p))))` THEN1 ( ASM_SIMP_TAC std_ss [A_SEM_THM, A_BIGAND_SEM, MEM_MAP, GSYM LEFT_FORALL_IMP_THM, ACCEPT_COND_GF_def, A_SEM_def, ACCEPT_COND_SEM_def, ACCEPT_COND_PROP_def, ACCEPT_IMPL_def, ACCEPT_OR_def, ACCEPT_COND_SEM_TIME_def, ACCEPT_BIGAND_SEM] THEN METIS_TAC[] ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN Q.ABBREV_TAC `ac = (ACCEPT_IMPL (ACCEPT_BIGAND (MAP (\x. ACCEPT_G (ACCEPT_F (ACCEPT_PROP x))) fc),ACCEPT_PROP p))` THEN SUBGOAL_TAC `?f. INJ f (SEMI_AUTOMATON_USED_INPUT_VARS A'') UNIV /\ DISJOINT (IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A'') ) (SEMI_AUTOMATON_USED_VARS A'' UNION ACCEPT_COND_USED_VARS ac)` THEN1 ( MATCH_MP_TAC (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] FINITE_INJ_EXISTS) THEN ASM_SIMP_TAC std_ss [FINITE___SEMI_AUTOMATON_USED_INPUT_VARS, FINITE_UNION, SEMI_AUTOMATON_USED_VARS_def, FINITE___ACCEPT_COND_USED_VARS] ) THEN SUBGOAL_TAC `?SA. IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON SA A'' f` THEN1 ( FULL_SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_UNION, IN_IMAGE, SEMI_AUTOMATON_USED_VARS_def, IN_DIFF, IN_SING, IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def] THEN REPEAT STRIP_TAC THENL [ METIS_TAC[], METIS_TAC[], FULL_SIMP_TAC std_ss [INJ_DEF, IN_UNIV] THEN METIS_TAC[] ] ) THEN ASSUME_TAC A_UNIV___SIMPLIFIED_SEMI_AUTOMATON_THM THEN Q_SPECL_NO_ASSUM 0 [`A''`, `SA`, `f`, `ac`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( FULL_SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_UNION, IN_IMAGE, SEMI_AUTOMATON_USED_VARS_def, IN_DIFF, IN_SING] THEN METIS_TAC[] ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN Q.UNABBREV_TAC `ac` THEN SIMP_TAC std_ss [ACCEPT_VAR_RENAMING_def, ACCEPT_IMPL_def, ACCEPT_OR_def, ACCEPT_BIGAND___VAR_RENAMING, MAP_MAP_o, combinTheory.o_DEF, ACCEPT_F_def] THEN Q_TAC EXISTS_TAC `SA` THEN Q_TAC EXISTS_TAC `MAP (P_VAR_RENAMING (\x. (if x IN SEMI_AUTOMATON_USED_INPUT_VARS A'' then f x else x))) fc` THEN Q_TAC EXISTS_TAC `P_VAR_RENAMING (\x. (if x IN SEMI_AUTOMATON_USED_INPUT_VARS A'' then f x else x)) p` THEN REPEAT STRIP_TAC THENL [ SIMP_ALL_TAC std_ss [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def] THEN ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES, FINITE_UNION, IMAGE_FINITE, FINITE___SEMI_AUTOMATON_USED_INPUT_VARS], METIS_TAC[IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUNS], SIMP_TAC std_ss [MAP_MAP_o, combinTheory.o_DEF] ] ) THEN FULL_SIMP_TAC std_ss [] THEN (*cleanup*) WEAKEN_HD_TAC THEN WEAKEN_NO_TAC 2 (*FINITE A''.S*) THEN NTAC 4 (WEAKEN_NO_TAC 2) (*A'*) THEN WEAKEN_NO_TAC 3 (*A*) THEN FULL_SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_PROP_def, ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, A_BIGAND_SEM, MEM_MAP, GSYM LEFT_FORALL_IMP_THM, ACCEPT_COND_GF_def, ACCEPT_F_def, IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_def, IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_THM] THEN SUBGOAL_TAC `?e. !n:num. ?m:num. m > n /\ (w m = e)` THEN1 ( ASSUME_TAC (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] (INST_TYPE [alpha |-> alpha --> bool] INF_ELEMENTS_OF_PATH_NOT_EMPTY)) THEN Q_SPECL_NO_ASSUM 0 [`POW B.S`, `w`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( FULL_SIMP_TAC std_ss [PATH_SUBSET_def, IN_POW, FINITE_POW_IFF] ) THEN FULL_SIMP_TAC std_ss [GSYM MEMBER_NOT_EMPTY, INF_ELEMENTS_OF_PATH_def, GSPECIFICATION] THEN METIS_TAC[] ) THEN `?n0. w n0 = e` by METIS_TAC[] THEN SUBGOAL_TAC `?m':num. (m' > n0) /\ (!x. MEM x fc' ==> ?t. n0 <= t /\ t < m' /\ P_SEM (INPUT_RUN_PATH_UNION B i w t) x)` THEN1 ( Induct_on `fc'` THENL [ SIMP_TAC list_ss [] THEN Q_TAC EXISTS_TAC `SUC n0` THEN DECIDE_TAC, SIMP_TAC list_ss [DISJ_IMP_THM, FORALL_AND_THM] THEN REPEAT STRIP_TAC THEN PROVE_CONDITION_NO_ASSUM 2 THEN1 ASM_REWRITE_TAC[] THEN Q_SPEC_NO_ASSUM 2 `n0` THEN FULL_SIMP_TAC std_ss [] THEN rename1 `P_SEM (INPUT_RUN_PATH_UNION B i w t2) h` THEN Q_TAC EXISTS_TAC `MAX m' (SUC t2)` THEN ASM_SIMP_TAC arith_ss [GREATER_DEF, MAX_LT] THEN REPEAT STRIP_TAC THENL [ Q_TAC EXISTS_TAC `t2` THEN ASM_SIMP_TAC arith_ss [], METIS_TAC[] ] ] ) THEN SUBGOAL_TAC `?m. (m + n0) >= m' /\ (w (m + n0) = e)` THEN1 ( Q_SPEC_NO_ASSUM 3 `m'` THEN CLEAN_ASSUMPTIONS_TAC THEN Q_TAC EXISTS_TAC `m - n0` THEN ASM_SIMP_TAC arith_ss [] ) THEN Q_TAC EXISTS_TAC `CUT_PATH_PERIODICALLY i n0 m` THEN STRIP_TAC THEN1 ( REWRITE_TAC[IS_ULTIMATIVELY_PERIODIC_PATH_def] THEN Q_TAC EXISTS_TAC `n0` THEN Q_TAC EXISTS_TAC `m` THEN ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___IS_ULTIMATIVELY_PERIODIC] ) THEN Q_TAC EXISTS_TAC `CUT_PATH_PERIODICALLY w n0 m` THEN REPEAT STRIP_TAC THENL [ SIMP_ALL_TAC std_ss [PATH_SUBSET_def, CUT_PATH_PERIODICALLY_def] THEN METIS_TAC[], FULL_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___BEGINNING, INPUT_RUN_PATH_UNION_def], Cases_on `SUC n < m + n0` THEN1 ( ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___BEGINNING] ) THEN ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY_def] THEN Cases_on `m = 1` THEN1 ( ASM_SIMP_TAC std_ss [MOD_1] THEN `m + n0 = SUC n0` by DECIDE_TAC THEN METIS_TAC[] ) THEN SUBGOAL_TAC `(SUC n - n0) MOD m = (1 + (n - n0) MOD m) MOD m` THEN1 ( SUBGOAL_TAC `1 MOD m = 1` THEN1 ( MATCH_RIGHT_EQ_MP_TAC X_MOD_Y_EQ_X THEN DECIDE_TAC ) THEN GSYM_NO_TAC 0 THEN ONCE_ASM_REWRITE_TAC [] THEN WEAKEN_HD_TAC THEN ASM_SIMP_TAC arith_ss [MOD_PLUS] THEN AP_THM_TAC THEN AP_TERM_TAC THEN DECIDE_TAC ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN Q.ABBREV_TAC `r = (n - n0) MOD m` THEN Cases_on `1 + r < m` THENL [ ASM_SIMP_TAC arith_ss [] THEN `n0 + (r + 1) = SUC (n0 + r)` by DECIDE_TAC THEN METIS_TAC[], SUBGOAL_TAC `1 + r = m` THEN1 ( `0 < m` by DECIDE_TAC THEN `r < m` by METIS_TAC [DIVISION] THEN DECIDE_TAC ) THEN ASM_SIMP_TAC arith_ss [] THEN `SUC (n0 + r) = (m + n0)` by DECIDE_TAC THEN METIS_TAC[] ], RES_TAC THEN rename1 `(_ >= t') /\ P_SEM _ p` THEN Q_TAC EXISTS_TAC `m * t' + t` THEN SUBGOAL_TAC `m * t' >= t'` THEN1 ( `m > 0` by DECIDE_TAC THEN UNDISCH_HD_TAC THEN SIMP_TAC arith_ss [GREATER_EQ] ) THEN ASM_SIMP_TAC arith_ss [] THEN WEAKEN_HD_TAC THEN SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def, CUT_PATH_PERIODICALLY_def] THEN ASM_SIMP_TAC arith_ss [] THEN REMAINS_TAC `(n0 + (t + m * t' - n0) MOD m) = t` THEN1 ( ASM_REWRITE_TAC[] ) THEN `(t + m * t' - n0) = ((t - n0) + m * t')` by DECIDE_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN `0 < m` by DECIDE_TAC THEN ASSUME_TAC MOD_MULT THEN Q_SPECL_NO_ASSUM 0 [`m`, `t - n0`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 FULL_SIMP_TAC arith_ss [] THEN Q_SPEC_NO_ASSUM 0 `t'` THEN UNDISCH_HD_TAC THEN SIMP_TAC std_ss [ADD_SYM, MULT_SYM] THEN DECIDE_TAC, UNDISCH_HD_TAC THEN FULL_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___BEGINNING, INPUT_RUN_PATH_UNION_def] ]); val SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___TO___AUTOMATON = store_thm ( "SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___TO___AUTOMATON", ``!K A p. (DISJOINT (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS K) A.S) ==> ((CTL_KS_SEM (SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K A) (CTL_A_ALWAYS (CTL_PROP p))) = A_KS_SEM K (A_UNIV (A, ACCEPT_COND_G p)))``, SIMP_TAC std_ss [CTL_KS_SEM_def, SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT, symbolic_kripke_structure_REWRITES, CTL_SEM_THM, PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, P_SEM_THM, XP_SEM_THM, GSYM RIGHT_FORALL_IMP_THM, A_KS_SEM_def, A_SEM_THM, ACCEPT_COND_G_def, ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, IS_TRANSITION_def, GSYM SUBSET_COMPL_DISJOINT, SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, UNION_SUBSET] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ rename1 `P_SEM (INPUT_RUN_PATH_UNION A i w t') p` THEN REMAINS_TAC `P_SEM (INPUT_RUN_PATH_UNION A i w 0) K.S0 /\ !n. XP_SEM K.R (INPUT_RUN_STATE_UNION A (i n) (w n), INPUT_RUN_STATE_UNION A (i (SUC n)) (w (SUC n)))` THEN1 ( Q_SPECL_NO_ASSUM 7 [`INPUT_RUN_PATH_UNION A i w`, `t'`] THEN FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def] ) THEN SUBGOAL_TAC `!n. (INPUT_RUN_STATE_UNION A (i n) (w n)) INTER (COMPL A.S) = (i n) INTER (COMPL A.S)` THEN1 ( SIMP_ALL_TAC std_ss [INPUT_RUN_STATE_UNION_def, EXTENSION, IN_INTER, IN_COMPL, IN_UNION, IN_DIFF, PATH_SUBSET_def, PATH_MAP_def, SUBSET_DEF] THEN PROVE_TAC[] ) THEN SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def] THEN REPEAT STRIP_TAC THENL [ METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM] ], Q_SPECL_NO_ASSUM 3 [`p'`, `PATH_RESTRICT p' A.S`, `k`] THEN SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def, PATH_RESTRICT_def, PATH_MAP_def, INPUT_RUN_STATE_UNION___SPLIT, PATH_SUBSET_def, INTER_SUBSET] THEN PROVE_TAC[] ]); val SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___CLEAN_STATE_VARS = store_thm ( "SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___CLEAN_STATE_VARS", ``!K A p. (CTL_KS_SEM (SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K A) (CTL_A_ALWAYS (CTL_PROP p))) = (CTL_KS_SEM (SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K (symbolic_semi_automaton EMPTY A.S0 A.R)) (CTL_A_ALWAYS (CTL_PROP p)))``, SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT_def, SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def, symbolic_kripke_structure_REWRITES, symbolic_semi_automaton_REWRITES] ); val A_KS_SEM___cong = store_thm ( "A_KS_SEM___cong", ``!A1 A2. AUTOMATON_EQUIV A1 A2 ==> !K. (A_KS_SEM K A1 = A_KS_SEM K A2)``, SIMP_TAC std_ss [A_KS_SEM_def, AUTOMATON_EQUIV_def]); val A_UNIV___LTL_KS_SEM___THM = store_thm ( "A_UNIV___LTL_KS_SEM___THM", ``!A ac l. (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l)) ==> ((!i. A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = LTL_SEM i l) = LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE A) (LTL_EQUIV (ACCEPT_COND_TO_LTL ac, l)))``, REPEAT STRIP_TAC THEN SIMP_TAC std_ss [LTL_KS_SEM_def, A_SEM_THM, SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE___INITIAL_PATH] THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ Q_SPEC_NO_ASSUM 1 `p` THEN `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A p w` by PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN `LTL_SEM p l = ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A p (PATH_RESTRICT p A.S)) ac` by METIS_TAC[] THEN FULL_SIMP_TAC std_ss [LTL_SEM_THM, ACCEPT_COND_TO_LTL_THM, INPUT_RUN_PATH_UNION___SPLIT], `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w` by PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN `(!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w ==> ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac) = ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac` by METIS_TAC[] THEN ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN Q_SPEC_NO_ASSUM 2 `INPUT_RUN_PATH_UNION A i w` THEN SUBGOAL_TAC `IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A (INPUT_RUN_PATH_UNION A i w) (PATH_RESTRICT (INPUT_RUN_PATH_UNION A i w) A.S)` THEN1 ( UNDISCH_NO_TAC 1 THEN SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, INPUT_RUN_PATH_UNION_def, PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, INTER_SUBSET, INPUT_RUN_STATE_UNION_def, IS_TRANSITION_def] THEN SUBGOAL_TAC `!n. ((w n UNION (i n DIFF A.S)) INTER A.S UNION (w n UNION (i n DIFF A.S) DIFF A.S)) = (w n UNION (i n DIFF A.S))` THEN1 ( SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_INTER, IN_DIFF] THEN METIS_TAC[] ) THEN ASM_SIMP_TAC std_ss [] ) THEN FULL_SIMP_TAC std_ss [LTL_SEM_THM, GSYM ACCEPT_COND_TO_LTL_THM, ACCEPT_COND_SEM_def] THEN ONCE_REWRITE_TAC[LTL_USED_VARS_INTER_THM] THEN AP_THM_TAC THEN AP_TERM_TAC THEN `PATH_SUBSET w A.S` by FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SIMP_ALL_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, EXTENSION, IN_INTER, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, IN_UNION, IN_DIFF, PATH_SUBSET_def, SUBSET_DEF, GSYM SUBSET_COMPL_DISJOINT, IN_COMPL] THEN METIS_TAC[] ]); val PROBLEM_TO_LTL_KS_SEM = store_thm ("PROBLEM_TO_LTL_KS_SEM", ``!A p psl i0 s0 f f'. (F_CLOCK_SERE_FREE psl /\ ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\ (A.S = (INTERVAL_SET (SUC i0) s0)) /\ (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\ (i0 <= s0) /\ (f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)))) /\ (f' = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)) + 2**(SUC(s0-i0))))) ==> ((LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE (SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON (symbolic_semi_automaton (INTERVAL_SET (SUC i0) (SUC s0)) (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0)) (XP_AND (XP_EQUIV (XP_NEXT_PROP (SUC s0), XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),A.R))) f f' (P_PROP (SUC s0)))) (LTL_EQUIV (LTL_ALWAYS (LTL_EVENTUAL (LTL_PROP (P_NOT (P_BIGOR (SET_TO_LIST (IMAGE (\s. P_PROP (f' s)) (POW (INTERVAL_SET (SUC i0) (SUC s0))))))))), PSL_TO_LTL psl)) ) = (!K. ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) = UF_KS_SEM K psl)))``, REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [PSL_TO_LTL___UF_KS_SEM] THEN ASSUME_TAC (INST_TYPE [alpha |-> num] IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS) THEN Q_SPECL_NO_ASSUM 0 [`A`, `p`, `(PSL_TO_LTL psl)`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( ASM_REWRITE_TAC[FINITE_INTERVAL_SET, INFINITE_UNIV] THEN Q_TAC EXISTS_TAC `SUC` THEN SIMP_TAC arith_ss [] THEN EXISTS_TAC ``0:num`` THEN SIMP_TAC arith_ss [] ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN SUBGOAL_TAC `!i. A_SEM i (A_UNIV (A,ACCEPT_COND_G p)) = ~A_SEM i (A_NDET (A,ACCEPT_COND_F (P_NOT p)))` THEN1 ( SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_G_def, ACCEPT_COND_F_def, ACCEPT_F_def, ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, P_SEM_def] THEN PROVE_TAC[] ) THEN FULL_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN ASSUME_TAC (INST_TYPE [alpha |-> num] A_SEM___NDET_F___TO___NDET_FG) THEN Q_SPECL_NO_ASSUM 0 [`A`, `P_NOT p`, `SUC s0`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, P_USED_VARS_def, IN_UNION, IN_INTERVAL_SET, SUBSET_DEF] THEN `~(SUC s0 <= i0) /\ ~(SUC s0 <= s0)` by DECIDE_TAC THEN PROVE_TAC[] ) THEN SIMP_ALL_TAC std_ss [AUTOMATON_EQUIV_def] THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN SUBGOAL_TAC `SUC s0 INSERT INTERVAL_SET (SUC i0) s0 = INTERVAL_SET (SUC i0) (SUC s0)` THEN1 ( ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN SIMP_TAC std_ss [IN_INTERVAL_SET, IN_INSERT] THEN DECIDE_TAC ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN ASSUME_TAC (INST_TYPE [alpha |-> num] SYMBOLIC___NDET_FG___TO___DET_FG___CONCRETE_THM) THEN Q_SPECL_NO_ASSUM 0 [`symbolic_semi_automaton ((INTERVAL_SET (SUC i0) (SUC s0))) (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0)) (XP_AND (XP_EQUIV (XP_NEXT_PROP (SUC s0), XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),A.R))`, `P_PROP (SUC s0)`, `f`, `f'`] THEN SIMP_ALL_TAC std_ss [symbolic_semi_automaton_REWRITES] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( SUBGOAL_TAC `SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)` THEN1 ( FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, IN_UNION, SUBSET_DEF, IN_INTERVAL_SET] THEN REPEAT STRIP_TAC THEN `x <= i0` by PROVE_TAC[] THEN DECIDE_TAC ) THEN SUBGOAL_TAC `(SEMI_AUTOMATON_USED_VARS (symbolic_semi_automaton (INTERVAL_SET (SUC i0) (SUC s0)) (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0)) (XP_AND (XP_EQUIV (XP_NEXT_PROP (SUC s0), XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),A.R)))) SUBSET (INTERVAL_SET 0 (SUC s0))` THEN1 ( SIMP_ALL_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, symbolic_semi_automaton_REWRITES, P_USED_VARS_EVAL, XP_USED_VARS_EVAL, SUBSET_DEF, IN_INTERVAL_SET, IN_UNION, IN_SING, IN_INSERT] THEN REPEAT STRIP_TAC THEN ( RES_TAC THEN ASM_SIMP_TAC arith_ss [] ) ) THEN REPEAT STRIP_TAC THENL [ REWRITE_TAC[FINITE_INTERVAL_SET], ASM_SIMP_TAC std_ss [P_USED_VARS_def, SUBSET_DEF, IN_INTERVAL_SET, IN_SING], ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SET_BINARY_ENCODING_SHIFT___INJ THEN ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET, FINITE_INTERVAL_SET], ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SET_BINARY_ENCODING_SHIFT___INJ THEN ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET, FINITE_INTERVAL_SET], MATCH_MP_TAC DISJOINT_SUBSET THEN Q_TAC EXISTS_TAC `INTERVAL_SET (0) (SUC s0)` THEN ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN PROVE_TAC[], MATCH_MP_TAC DISJOINT_SUBSET THEN Q_TAC EXISTS_TAC `INTERVAL_SET (0) (SUC s0)` THEN ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN REPEAT WEAKEN_HD_TAC THEN GEN_TAC THEN RIGHT_DISJ_TAC THEN SIMP_ALL_TAC std_ss [] THEN WEAKEN_NO_TAC 1 THEN DECIDE_TAC, ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN REPEAT WEAKEN_HD_TAC THEN GEN_TAC THEN `?a:num. 2 ** SUC (s0 - i0) = a` by PROVE_TAC[] THEN ASM_REWRITE_TAC[] THEN SUBGOAL_TAC `~(a = 0)` THEN1 ( GSYM_NO_TAC 0 THEN ASM_SIMP_TAC std_ss [EXP_EQ_0] ) THEN WEAKEN_NO_TAC 1 THEN DECIDE_TAC ] ) THEN SIMP_ALL_TAC std_ss [FORALL_AND_THM] THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN SUBGOAL_TAC `!A i (p:num prop_logic). ~(A_SEM i (A_NDET (A, ACCEPT_COND_FG p))) = A_SEM i (A_UNIV (A, ACCEPT_COND_GF (P_NOT p)))` THEN1 ( REPEAT WEAKEN_HD_TAC THEN SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_GF_def, ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, ACCEPT_COND_FG_def, ACCEPT_F_def, P_SEM_def] THEN METIS_TAC[] ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN SIMP_TAC std_ss [ACCEPT_COND_GF_def] THEN Q.MATCH_ABBREV_TAC `LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE B) l' = !i. A_SEM i (A_UNIV (B, ACCEPT_COND ac')) = LTL_SEM i (PSL_TO_LTL psl)` THEN ASSUME_TAC (INST_TYPE [alpha |-> num] A_UNIV___LTL_KS_SEM___THM) THEN Q_SPECL_NO_ASSUM 0 [`B`, `ac'`, `PSL_TO_LTL psl`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( REPEAT STRIP_TAC THENL [ PROVE_TAC[], Q.UNABBREV_TAC `B` THEN ASM_SIMP_TAC std_ss [SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, symbolic_semi_automaton_REWRITES, SET_BINARY_ENCODING_SHIFT___IMAGE_THM, PSL_TO_LTL_def, RLTL_USED_VARS___PSL_TO_RLTL, LTL_USED_VARS___RLTL_TO_LTL, P_USED_VARS_EVAL, UNION_EMPTY] THEN SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET, DISJOINT_DISJ_THM] THEN GEN_TAC THEN LEFT_DISJ_TAC THEN `x <= i0` by PROVE_TAC[] THEN ASM_SIMP_TAC arith_ss [] ] ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN Q.UNABBREV_TAC `l'` THEN Q.UNABBREV_TAC `ac'` THEN MATCH_MP_TAC (prove (``LTL_EQUIVALENT l1 l2 ==> (LTL_KS_SEM M l1 = LTL_KS_SEM M l2)``, SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_KS_SEM_def, LTL_SEM_def])) THEN SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_EQUIV_SEM] THEN REPEAT GEN_TAC THEN MATCH_MP_TAC (prove (``(A = B) ==> ((A = x) = (B = x))``, PROVE_TAC[])) THEN SIMP_TAC std_ss [ACCEPT_COND_TO_LTL_def, LTL_SEM_THM, ACCEPT_F_def, P_SEM_def] ); val PROBLEM_TO_LTL_KS_SEM___TOTAL = store_thm ("PROBLEM_TO_LTL_KS_SEM___TOTAL", ``!A p psl i0 s0 f. (F_CLOCK_SERE_FREE psl /\ IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A /\ ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\ (A.S = (INTERVAL_SET (SUC i0) s0)) /\ (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\ (i0 <= s0) /\ (f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC s0))) ==> ((LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE (RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f)) (LTL_EQUIV (LTL_ALWAYS (LTL_PROP ( (P_FORALL (SET_TO_LIST A.S) (P_IMPL (VAR_RENAMING_HASHTABLE A.S f,p))))), PSL_TO_LTL psl)) ) = (!K. ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) = UF_KS_SEM K psl)))``, REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [PSL_TO_LTL___UF_KS_SEM] THEN ASSUME_TAC (INST_TYPE [alpha |-> num] IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS) THEN Q_SPECL_NO_ASSUM 0 [`A`, `p`, `(PSL_TO_LTL psl)`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( ASM_REWRITE_TAC[FINITE_INTERVAL_SET, INFINITE_UNIV] THEN Q_TAC EXISTS_TAC `SUC` THEN SIMP_TAC arith_ss [] THEN EXISTS_TAC ``0:num`` THEN SIMP_TAC arith_ss [] ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN SUBGOAL_TAC `DISJOINT (IMAGE f (POW A.S)) (SEMI_AUTOMATON_USED_VARS A UNION P_USED_VARS p)` THEN1 ( ASM_REWRITE_TAC[DISJOINT_DISJ_THM] THEN Cases_on `i0 = s0` THENL [ SUBGOAL_TAC `INTERVAL_SET (SUC i0) s0 = EMPTY` THEN1 ( ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY] ) THEN ASM_REWRITE_TAC[IN_IMAGE, IN_POW, SUBSET_EMPTY] THEN SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT_def, SET_BINARY_ENCODING_def, IMAGE_EMPTY, SUM_IMAGE_THM] THEN FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, SUBSET_DEF, IN_INTERVAL_SET, SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_DIFF, NOT_IN_EMPTY] THEN `~(SUC s0 <= s0)` by DECIDE_TAC THEN METIS_TAC[], `SUC i0 <= s0` by DECIDE_TAC THEN ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, SUBSET_DEF, IN_INTERVAL_SET, SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_DIFF, NOT_IN_EMPTY] THEN GEN_TAC THEN `~(SUC s0 <= s0)` by DECIDE_TAC THEN Cases_on `x <= s0` THEN1 ASM_SIMP_TAC std_ss [] THEN `~(x <= i0)` by DECIDE_TAC THEN METIS_TAC[] ] ) THEN ASSUME_TAC (INST_TYPE [alpha |-> num] SYMBOLIC___TOTAL_UNIV_G___TO___DET_G___CONCRETE_THM) THEN Q_SPECL_NO_ASSUM 0 [`A`, `p`, `f`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( ASM_REWRITE_TAC[FINITE_INTERVAL_SET] THEN MATCH_MP_TAC SET_BINARY_ENCODING_SHIFT___INJ THEN ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET, FINITE_INTERVAL_SET] ) THEN SIMP_ALL_TAC std_ss [FORALL_AND_THM] THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN SIMP_TAC std_ss [ACCEPT_COND_G_def] THEN Q.MATCH_ABBREV_TAC `LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE B) l' = !i. A_SEM i (A_UNIV (B, ACCEPT_COND ac')) = LTL_SEM i (PSL_TO_LTL psl)` THEN ASSUME_TAC (INST_TYPE [alpha |-> num] A_UNIV___LTL_KS_SEM___THM) THEN Q_SPECL_NO_ASSUM 0 [`B`, `ac'`, `PSL_TO_LTL psl`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( REPEAT STRIP_TAC THENL [ PROVE_TAC[], Q.UNABBREV_TAC `B` THEN ASM_SIMP_TAC std_ss [RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def, symbolic_semi_automaton_REWRITES, PSL_TO_LTL_def, RLTL_USED_VARS___PSL_TO_RLTL, LTL_USED_VARS___RLTL_TO_LTL, P_USED_VARS_EVAL, UNION_EMPTY] THEN SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET, DISJOINT_DISJ_THM] THEN GEN_TAC THEN LEFT_DISJ_TAC THEN `x <= i0` by PROVE_TAC[] THEN Cases_on `i0 = s0` THENL [ SUBGOAL_TAC `INTERVAL_SET (SUC i0) s0 = EMPTY` THEN1 ( ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY] ) THEN ASM_REWRITE_TAC[IN_IMAGE, IN_POW, SUBSET_EMPTY] THEN SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT_def, SET_BINARY_ENCODING_def, IMAGE_EMPTY, SUM_IMAGE_THM] THEN DECIDE_TAC, `SUC i0 <= s0` by DECIDE_TAC THEN ASM_SIMP_TAC arith_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, IN_INTERVAL_SET] ] ] ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN Q.UNABBREV_TAC `l'` THEN Q.UNABBREV_TAC `ac'` THEN SIMP_TAC std_ss [ACCEPT_COND_TO_LTL_def] ); val P_EXISTS___SET_TO_LIST___INTERVAL_SET = store_thm ("P_EXISTS___SET_TO_LIST___INTERVAL_SET", ``(!n1 n2 p. PROP_LOGIC_EQUIVALENT (P_EXISTS (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (P_EXISTS (INTERVAL_LIST n1 n2) p))``, SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def, P_EXISTS_SEM, SET_TO_LIST_INV, FINITE_INTERVAL_SET, LIST_TO_SET___INTERVAL_LIST] ) val P_FORALL___SET_TO_LIST___INTERVAL_SET = store_thm ("P_FORALL___SET_TO_LIST___INTERVAL_SET", ``(!n1 n2 p. PROP_LOGIC_EQUIVALENT (P_FORALL (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (P_FORALL (INTERVAL_LIST n1 n2) p))``, SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def, P_FORALL_SEM, SET_TO_LIST_INV, FINITE_INTERVAL_SET, LIST_TO_SET___INTERVAL_LIST] ) val P_BIGOR___SET_TO_LIST___INTERVAL_SET = store_thm ("P_BIGOR___SET_TO_LIST___INTERVAL_SET", ``!n1 n2 f. (PROP_LOGIC_EQUIVALENT (P_BIGOR (SET_TO_LIST (IMAGE f (INTERVAL_SET n1 n2)))) (P_BIGOR (MAP f (INTERVAL_LIST n1 n2))))``, REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def, P_BIGOR_SEM, MEM_MAP, GSYM LEFT_EXISTS_AND_THM, MEM_INTERVAL_LIST, MEM_SET_TO_LIST, IMAGE_FINITE, FINITE_INTERVAL_SET, IN_IMAGE, IN_INTERVAL_SET] ) val XP_BIGOR___SET_TO_LIST___INTERVAL_SET = store_thm ("XP_BIGOR___SET_TO_LIST___INTERVAL_SET", ``!n1 n2 f. (XPROP_LOGIC_EQUIVALENT (XP_BIGOR (SET_TO_LIST (IMAGE f (INTERVAL_SET n1 n2)))) (XP_BIGOR (MAP f (INTERVAL_LIST n1 n2))))``, REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_BIGOR_SEM, MEM_MAP, GSYM LEFT_EXISTS_AND_THM, MEM_INTERVAL_LIST, MEM_SET_TO_LIST, IMAGE_FINITE, FINITE_INTERVAL_SET, IN_IMAGE, IN_INTERVAL_SET] ) val XP_NEXT_EXISTS___SET_TO_LIST___INTERVAL_SET = store_thm ("XP_NEXT_EXISTS___SET_TO_LIST___INTERVAL_SET", ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_NEXT_EXISTS (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_NEXT_EXISTS (INTERVAL_LIST n1 n2) p)``, SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_NEXT_EXISTS_SEM, SET_TO_LIST_INV, FINITE_INTERVAL_SET, LIST_TO_SET___INTERVAL_LIST]); val XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET = store_thm ("XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET", ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_CURRENT_EXISTS (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_CURRENT_EXISTS (INTERVAL_LIST n1 n2) p)``, SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_CURRENT_EXISTS_SEM, SET_TO_LIST_INV, FINITE_INTERVAL_SET, LIST_TO_SET___INTERVAL_LIST]); val XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET = store_thm ("XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET", ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_NEXT_FORALL (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_NEXT_FORALL (INTERVAL_LIST n1 n2) p)``, SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_NEXT_FORALL_SEM, SET_TO_LIST_INV, FINITE_INTERVAL_SET, LIST_TO_SET___INTERVAL_LIST]); val XP_CURRENT_FORALL___SET_TO_LIST___INTERVAL_SET = store_thm ("XP_CURRENT_FORALL___SET_TO_LIST___INTERVAL_SET", ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_CURRENT_FORALL (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_CURRENT_FORALL (INTERVAL_LIST n1 n2) p)``, SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_CURRENT_FORALL_SEM, SET_TO_LIST_INV, FINITE_INTERVAL_SET, LIST_TO_SET___INTERVAL_LIST]); val IS_EMPTY_FAIR_KRIPKE_STRUCTURE_cong = store_thm ("IS_EMPTY_FAIR_KRIPKE_STRUCTURE_cong", ``!S0 S0' R R' FC FC'. ( PROP_LOGIC_EQUIVALENT S0 S0' ==> XPROP_LOGIC_EQUIVALENT R R' ==> (FC = FC') ==> ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0 R) FC) = (IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0' R') FC')))``, SIMP_TAC std_ss [IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_def, PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, symbolic_kripke_structure_REWRITES, PROP_LOGIC_EQUIVALENT_def, XPROP_LOGIC_EQUIVALENT_def]); val ks_congset = mk_congset ([merge_cs [ (CSFRAG {rewrs = [], relations = [], dprocs = [], congs = [IS_EMPTY_FAIR_KRIPKE_STRUCTURE_cong]}), xprop_logic_CS, prop_logic_CS]]); val XP_COND___XP_NEXT_FORALL___REWRITE = store_thm ("XP_COND___XP_NEXT_FORALL___REWRITE", ``!c l p1 p2. DISJOINT (XP_USED_X_VARS c) (LIST_TO_SET l) ==> ( XPROP_LOGIC_EQUIVALENT (XP_COND (c, XP_NEXT_FORALL l p1, XP_NEXT_FORALL l p2)) (XP_NEXT_FORALL l (XP_COND (c, p1,p2))))``, REPEAT STRIP_TAC THEN SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_SEM_THM, XP_NEXT_FORALL_SEM] THEN REPEAT GEN_TAC THEN SUBGOAL_TAC `!l'. l' SUBSET LIST_TO_SET l ==> (XP_SEM c (s1,s2 DIFF LIST_TO_SET l UNION l') = XP_SEM c (s1,s2))` THEN1 ( REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[XP_USED_VARS_INTER_THM] THEN AP_TERM_TAC THEN SIMP_TAC std_ss [] THEN ONCE_REWRITE_TAC[EXTENSION] THEN SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, SUBSET_DEF, IN_INTER, IN_DIFF, IN_UNION] THEN PROVE_TAC[] ) THEN ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN METIS_TAC[]); val XP_COND___XP_CURRENT_EXISTS___REWRITE = store_thm ("XP_COND___XP_CURRENT_EXISTS___REWRITE", ``!c l p1 p2. DISJOINT (XP_USED_CURRENT_VARS c) (LIST_TO_SET l) ==> ( XPROP_LOGIC_EQUIVALENT (XP_COND (c, XP_CURRENT_EXISTS l p1, XP_CURRENT_EXISTS l p2)) (XP_CURRENT_EXISTS l (XP_COND (c, p1,p2))))``, REPEAT STRIP_TAC THEN SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_SEM_THM, XP_CURRENT_EXISTS_SEM] THEN REPEAT GEN_TAC THEN SUBGOAL_TAC `!l'. l' SUBSET LIST_TO_SET l ==> (XP_SEM c (s1 DIFF LIST_TO_SET l UNION l', s2) = XP_SEM c (s1,s2))` THEN1 ( REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[XP_USED_VARS_INTER_THM] THEN AP_TERM_TAC THEN SIMP_TAC std_ss [] THEN ONCE_REWRITE_TAC[EXTENSION] THEN SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, SUBSET_DEF, IN_INTER, IN_DIFF, IN_UNION] THEN PROVE_TAC[] ) THEN METIS_TAC[]); val VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def = Define `(VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING [] n n0 = P_PROP n) /\ (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (e::l) n n0 = P_OR (P_AND (P_PROP e, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l ((2**(e-n0)) + n) n0), P_AND (P_NOT (P_PROP e), VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l n n0)))`; val VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___CLEAN_OFFSET = store_thm ("VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___CLEAN_OFFSET", ``!l n n0 m:num d. ((d <= n) /\ (d >= m) /\ (!e. MEM e l ==> e < m)) ==> (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l n n0 = (P_VAR_RENAMING (\x. if (x >= m) then x + (n-d) else x)) (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l d n0))``, Induct_on `l` THENL [ SIMP_TAC list_ss [VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, P_VAR_RENAMING_EVAL], SIMP_TAC list_ss [VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, P_VAR_RENAMING_EVAL, P_OR_def, prop_logic_11] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN `h < m` by PROVE_TAC[] THEN ASM_SIMP_TAC arith_ss [] THEN REPEAT STRIP_TAC THENL [ Q_SPECL_NO_ASSUM 4 [`n + (2:num) ** (h - n0)`, `n0`, `m`, `d + (2:num) ** (h - n0)`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC arith_ss [] THEN FULL_SIMP_TAC arith_ss [], Q_SPECL_NO_ASSUM 4 [`n`, `n0`, `m`, `d`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN ASM_SIMP_TAC std_ss [] THEN FULL_SIMP_TAC arith_ss [] ] ]); val VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST = store_thm ("VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST", ``!n1 n2 n3 n4. (n3 <= n1) ==> (VAR_RENAMING_HASHTABLE_LIST (INTERVAL_LIST n1 n2) {} (SET_BINARY_ENCODING_SHIFT n3 n4) = VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST n1 n2) n4 n3)``, NTAC 2 GEN_TAC THEN Cases_on `n2 < n1` THENL [ ASM_SIMP_TAC std_ss [INTERVAL_LIST_THM, VAR_RENAMING_HASHTABLE_LIST_def, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, SET_BINARY_ENCODING_SHIFT_def, IMAGE_EMPTY, SET_BINARY_ENCODING_def, SUM_IMAGE_THM], Induct_on `n2 - n1` THENL [ REPEAT STRIP_TAC THEN `n2 = n1` by DECIDE_TAC THEN NTAC 2 (WEAKEN_NO_TAC 2) THEN ASM_SIMP_TAC std_ss [INTERVAL_LIST_THM, VAR_RENAMING_HASHTABLE_LIST_def, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, SET_BINARY_ENCODING_SHIFT_def, IMAGE_SING, SET_BINARY_ENCODING_def, SUM_IMAGE_SING, IMAGE_EMPTY, SUM_IMAGE_THM], REPEAT STRIP_TAC THEN `INTERVAL_LIST n1 n2 = n1::INTERVAL_LIST (SUC n1) n2` by ASM_SIMP_TAC arith_ss [INTERVAL_LIST_THM] THEN ASM_SIMP_TAC std_ss [VAR_RENAMING_HASHTABLE_LIST_def, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, P_OR_def, prop_logic_11] THEN REPEAT STRIP_TAC THENL [ ONCE_REWRITE_TAC[VAR_RENAMING_HASHTABLE_LIST___CLEAN_VAR_SET] THEN REMAINS_TAC `!x. (x SUBSET {} UNION (LIST_TO_SET (INTERVAL_LIST (SUC n1) n2))) ==> ((\x. SET_BINARY_ENCODING_SHIFT n3 n4 (x UNION {n1})) x = SET_BINARY_ENCODING_SHIFT n3 (2**(n1 - n3) + n4) x)` THEN1 ( ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___FUN_RESTRICT) THEN Q_SPECL_NO_ASSUM 0 [`INTERVAL_LIST (SUC n1) n2`, `EMPTY:num set`, `\x. SET_BINARY_ENCODING_SHIFT n3 n4 (x UNION {n1})`, `SET_BINARY_ENCODING_SHIFT n3 (2**(n1 - n3) + n4)`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN Q_SPECL_NO_ASSUM 6 [`n2`, `SUC n1`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN Q_SPECL_NO_ASSUM 0 [`n3`, `(2 ** (n1 - n3) + n4)`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN ASM_REWRITE_TAC[] ) THEN SIMP_TAC std_ss [UNION_EMPTY, LIST_TO_SET___INTERVAL_LIST] THEN REPEAT STRIP_TAC THEN `FINITE x` by PROVE_TAC[FINITE_INTERVAL_SET, SUBSET_FINITE] THEN SUBGOAL_TAC `~(n1 IN x)` THEN1 ( SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_INTERVAL_SET] THEN `~(SUC n1 <= n1)` by DECIDE_TAC THEN PROVE_TAC[] ) THEN ASM_SIMP_TAC arith_ss [FUN_EQ_THM, UNION_SING, SET_BINARY_ENCODING_SHIFT_def, IMAGE_INSERT, SET_BINARY_ENCODING_def, SUM_IMAGE_THM, IMAGE_FINITE] THEN AP_TERM_TAC THEN SIMP_TAC std_ss [EXTENSION, IN_IMAGE, IN_DELETE] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ PROVE_TAC[], PROVE_TAC[], `~(n1 = n)` by PROVE_TAC[] THEN `n < n3` by DECIDE_TAC THEN `n IN INTERVAL_SET (SUC n1) n2` by PROVE_TAC[SUBSET_DEF] THEN SIMP_ALL_TAC std_ss [IN_INTERVAL_SET] THEN DECIDE_TAC ], Q_SPECL_NO_ASSUM 4 [`n2`, `SUC n1`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN Q_SPECL_NO_ASSUM 0 [`n3`, `n4`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN ASM_REWRITE_TAC[] ] ] ]); val PROBLEM_TO_KRIPKE_STRUCTURE = store_thm ("PROBLEM_TO_KRIPKE_STRUCTURE", ``!A p psl i0 s0 DS S0 R l' pf sv a. (F_CLOCK_SERE_FREE psl /\ ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\ (A.S = (INTERVAL_SET (SUC i0) s0)) /\ (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\ (i0 <= s0) /\ (sv = \n:num. 2 * 2**(SUC s0 - i0) + s0 + 3 + n) /\ LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l',a,T,pf) IN DS.B /\ DS.IV SUBSET INTERVAL_SET 0 (2 * 2**(SUC s0 - i0) + s0 + 2) /\ LTL_EQUIVALENT_INITIAL (LTL_EQUIV (LTL_ALWAYS (LTL_EVENTUAL (LTL_PROP (P_NOT (P_BIGOR (MAP (\p. P_PROP p) (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0)) (SUC (SUC s0) + 2 ** SUC (s0 - i0) + PRE (2 ** SUC (s0 - i0))))))))), PSL_TO_LTL psl)) l' /\ (PROP_LOGIC_EQUIVALENT (P_AND (P_FORALL (INTERVAL_LIST (SUC i0) (SUC s0)) (P_EQUIV (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0), VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) (SUC i0))), P_AND (P_NOT (P_BIGOR (MAP P_PROP (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0)) (PRE (2 ** SUC (s0 - i0)) + (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))), P_AND (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv, P_NOT (pf sv))))) S0) /\ (XPROP_LOGIC_EQUIVALENT (XP_AND (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) (SUC s0)) (XP_EQUIV (XP_NEXT (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) (SUC i0)), XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) (SUC s0)) (XP_AND (XP_EQUIV (XP_NEXT_PROP (SUC s0), XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))), XP_AND (A.R, XP_CURRENT (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) (SUC i0))))))), XP_AND (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) (SUC s0)) (XP_EQUIV (XP_NEXT (P_VAR_RENAMING (\n. (if n >= SUC (SUC s0) then n + (2:num) ** SUC (s0 - i0) else n)) (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) (SUC i0))), XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) (SUC s0)) (XP_AND (XP_EQUIV (XP_NEXT_PROP (SUC s0), XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))), XP_AND (A.R, XP_AND (XP_NEXT (P_PROP (SUC s0)), XP_COND (XP_BIGOR (MAP XP_PROP (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0)) (PRE (2 ** SUC (s0 - i0)) + (SUC (SUC s0) + 2 ** SUC (s0 - i0))))), XP_CURRENT (P_VAR_RENAMING (\n. (if n >= SUC (SUC s0) then n + 2 ** SUC (s0 - i0) else n)) (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) (SUC i0))), XP_CURRENT (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) (SUC i0))))))))), XP_BIGAND (MAP (\xp. xp sv) DS.R)))) R) ) ==> ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0 R) (MAP (\x. x sv) DS.FC)) = (!K. ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) = UF_KS_SEM K psl)))``, REPEAT STRIP_TAC THEN `?f. f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)))` by METIS_TAC[] THEN `?f'. f' = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)) + 2**(SUC(s0-i0)))` by METIS_TAC[] THEN ASSUME_TAC (GSYM PROBLEM_TO_LTL_KS_SEM) THEN Q_SPECL_NO_ASSUM 0 [`A`, `p`, `psl`, `i0`, `s0`, `f`, `f'`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC std_ss [] THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN MATCH_MP_TAC (prove (``!M X f f'. (LTL_EQUIVALENT_INITIAL f f' /\ (X = LTL_KS_SEM M f)) ==> (X = LTL_KS_SEM M f')``, SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def, LTL_KS_SEM_def] THEN PROVE_TAC[])) THEN Q_TAC EXISTS_TAC `l'` THEN REPEAT STRIP_TAC THEN1 ( SUBGOAL_TAC `!S. (IMAGE (\s. P_PROP (f' s)) S) = (IMAGE (\p. P_PROP p) (IMAGE f' S))` THEN1 ( SIMP_TAC std_ss [GSYM IMAGE_COMPOSE, combinTheory.o_DEF] ) THEN UNDISCH_HD_TAC THEN ASM_SIMP_TAC std_ss [] THEN DISCH_TAC THEN WEAKEN_HD_TAC THEN ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM] THEN ASM_CONGRUENCE_SIMP_TAC ltl_cs std_ss [P_BIGOR___SET_TO_LIST___INTERVAL_SET] THEN PROVE_TAC[LTL_EQUIVALENT_INITIAL_def] ) THEN WEAKEN_NO_TAC 4 (*LTL_EQUIVALENT_INITIAL l'*) THEN GSYM_NO_TAC 7 (*Def sv*) THEN NTAC 2 (GSYM_NO_TAC 2) (*Def f, f'*) THEN ASM_SIMP_TAC std_ss [] THEN Q.MATCH_ABBREV_TAC `IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0 R) (MAP (\x. x sv) DS.FC) = LTL_KS_SEM KS l'` THEN ASSUME_TAC (INST_TYPE [alpha |-> num] LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE) THEN Q_SPECL_NO_ASSUM 0 [`DS`, `l'`, `pf`, `sv`, `KS`, `a`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( ASM_REWRITE_TAC[] THEN SUBGOAL_TAC `SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS KS SUBSET INTERVAL_SET 0 (2 * 2**(SUC s0 - i0) + s0 + 2)` THEN1 ( Q.UNABBREV_TAC `KS` THEN ASM_SIMP_TAC std_ss [] THEN Q.MATCH_ABBREV_TAC `SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE (SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON A' f f' (P_PROP (SUC s0)))) SUBSET INTERVAL_SET 0 (2 * 2 ** (SUC s0 - i0) + s0 + 2)` THEN REMAINS_TAC `SEMI_AUTOMATON_USED_VARS ((SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON A' f f' (P_PROP (SUC s0)))) SUBSET INTERVAL_SET 0 (2 * 2 ** (SUC s0 - i0) + s0 + 2)` THEN1 ( UNDISCH_HD_TAC THEN MATCH_MP_TAC (prove (``(C SUBSET A) ==> (A SUBSET B ==> C SUBSET B)``, METIS_TAC[SUBSET_TRANS])) THEN SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, symbolic_kripke_structure_REWRITES, SUBSET_DEF, IN_UNION] ) THEN SUBGOAL_TAC `SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)` THEN1 ( ASM_REWRITE_TAC[SEMI_AUTOMATON_USED_VARS_def] THEN SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET] THEN REPEAT STRIP_TAC THEN RES_TAC THEN DECIDE_TAC ) THEN ASSUME_TAC (INST_TYPE [alpha |-> num] SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS) THEN Q_SPECL_NO_ASSUM 0 [`A'`, `f`, `f'`, `P_PROP (SUC s0)`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( Q.UNABBREV_TAC `A'` THEN NTAC 2 (GSYM_NO_TAC 2) (*f, f'*) THEN ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES, FINITE_INTERVAL_SET, SET_BINARY_ENCODING_SHIFT___IMAGE_THM, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, P_USED_VARS_EVAL, XP_USED_VARS_EVAL, DISJOINT_DISJ_THM] THEN SIMP_ALL_TAC std_ss [IN_UNION, SUBSET_DEF, IN_INTERVAL_SET, IN_SING, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN REPEAT STRIP_TAC THEN ( LEFT_DISJ_TAC THEN SIMP_ALL_TAC std_ss [] THEN RES_TAC THEN ASM_SIMP_TAC arith_ss [] ) ) THEN ASM_REWRITE_TAC[SEMI_AUTOMATON_USED_VARS_def, SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, symbolic_semi_automaton_REWRITES] THEN Q.UNABBREV_TAC `A'` THEN NTAC 2 (GSYM_NO_TAC 3) THEN ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, symbolic_semi_automaton_REWRITES, SEMI_AUTOMATON_USED_INPUT_VARS_def, P_USED_VARS_EVAL, XP_USED_VARS_EVAL] THEN `(SUC s0) - i0 = SUC (s0 - i0)` by DECIDE_TAC THEN SUBGOAL_TAC `~(2:num ** (s0 - i0) = 0)` THEN1 ( SIMP_TAC std_ss [EXP_EQ_0] ) THEN `?a. (2 :num) ** (s0 - i0) = a` by METIS_TAC[] THEN FULL_SIMP_TAC std_ss [EXP] THEN UNDISCH_NO_TAC 1 (*~a = 0*) THEN UNDISCH_NO_TAC 5 (*SEMI_AUTOMATON_USED_VARS*) THEN UNDISCH_NO_TAC 12 (*i0 <= s0*) THEN UNDISCH_NO_TAC 12 (*P_USED_VARS p *) THEN REPEAT WEAKEN_HD_TAC THEN SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, IN_DIFF, IN_SING, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_INTERVAL_SET, EXP] THEN REPEAT STRIP_TAC THEN ( RES_TAC THEN DECIDE_TAC ) ) THEN UNDISCH_HD_TAC THEN UNDISCH_NO_TAC 9 (*i0 <= s0*) THEN UNDISCH_NO_TAC 6 (*DS.IV*) THEN GSYM_NO_TAC 3 (*def sv*) THEN ASM_SIMP_TAC std_ss [] THEN REPEAT WEAKEN_HD_TAC THEN SIMP_TAC std_ss [IS_ELEMENT_ITERATOR_def, IN_UNION, SUBSET_DEF, IN_INTERVAL_SET] THEN REPEAT STRIP_TAC THENL [ RES_TAC THEN DECIDE_TAC, RES_TAC THEN DECIDE_TAC ] ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN Q.UNABBREV_TAC `KS` THEN NTAC 3 (GSYM_NO_TAC 2) (*Def f, f', sv*) THEN ASM_SIMP_TAC std_ss [] THEN SUBGOAL_TAC `!n1 n2 S. (IMAGE (\s. P_PROP (SET_BINARY_ENCODING_SHIFT n1 n2 s)) S) = (IMAGE P_PROP (IMAGE (SET_BINARY_ENCODING_SHIFT n1 n2) S))` THEN1 ( SIMP_TAC std_ss [GSYM IMAGE_COMPOSE, combinTheory.o_DEF] ) THEN SUBGOAL_TAC `!n1 n2 S. (IMAGE (\s. XP_PROP (SET_BINARY_ENCODING_SHIFT n1 n2 s)) S) = (IMAGE XP_PROP (IMAGE (SET_BINARY_ENCODING_SHIFT n1 n2) S))` THEN1 ( SIMP_TAC std_ss [GSYM IMAGE_COMPOSE, combinTheory.o_DEF] ) THEN ASM_SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def, SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, symbolic_semi_automaton_REWRITES, symbolic_kripke_structure_REWRITES, SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, SET_BINARY_ENCODING_SHIFT___IMAGE_THM] THEN NTAC 2 WEAKEN_HD_TAC THEN ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET) THEN Q_SPEC_NO_ASSUM 0 `INTERVAL_LIST (SUC i0) (SUC s0)` THEN SIMP_ALL_TAC std_ss [LIST_TO_SET___INTERVAL_LIST] THEN GSYM_NO_TAC 3 (*sv*) THEN ASM_SIMP_TAC std_ss [] THEN ASM_CONGRUENCE_SIMP_TAC ks_congset arith_ss [P_BIGOR___SET_TO_LIST___INTERVAL_SET, XP_BIGOR___SET_TO_LIST___INTERVAL_SET, P_FORALL___SET_TO_LIST___INTERVAL_SET, XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET, XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET, VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST] THEN ASSUME_TAC (SIMP_RULE std_ss [RIGHT_FORALL_IMP_THM] (INST_TYPE [alpha |-> num] XP_COND___XP_NEXT_FORALL___REWRITE)) THEN Q_SPECL_NO_ASSUM 0 [`XP_BIGOR (MAP XP_PROP (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0)) (PRE (2 ** SUC (s0 - i0)) + (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))`, `(INTERVAL_LIST (SUC i0) (SUC s0))`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( ASM_SIMP_TAC list_ss [DISJOINT_DISJ_THM, XP_BIGOR___XP_USED_VARS, IN_LIST_BIGUNION, MAP_MAP_o, combinTheory.o_DEF, XP_USED_VARS_EVAL, MEM_MAP, GSYM LEFT_FORALL_OR_THM, NOT_IN_EMPTY] ) THEN `?ht. VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) (SUC i0) = ht` by METIS_TAC[] THEN SUBGOAL_TAC `(VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0) + 2 ** SUC (s0 - i0)) (SUC i0)) = P_VAR_RENAMING (\n:num. if (n >= (SUC (SUC s0))) then n + 2 ** SUC (s0 - i0) else n) ht` THEN1 ( GSYM_NO_TAC 0 THEN ASM_REWRITE_TAC[] THEN ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___CLEAN_OFFSET) THEN Q_SPECL_NO_ASSUM 0 [`INTERVAL_LIST (SUC i0) (SUC s0)`, `(SUC (SUC s0) + 2 ** SUC (s0 - i0))`, `(SUC i0)`, `SUC (SUC s0)`, `SUC (SUC s0)`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 SIMP_TAC arith_ss [MEM_INTERVAL_LIST] THEN ASM_REWRITE_TAC[] THEN SIMP_TAC arith_ss [] ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN ASSUME_TAC (SIMP_RULE std_ss [RIGHT_FORALL_IMP_THM] (INST_TYPE [alpha |-> num] XP_COND___XP_CURRENT_EXISTS___REWRITE)) THEN Q_SPECL_NO_ASSUM 0 [`XP_BIGOR (MAP XP_PROP (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0)) (PRE (2 ** SUC (s0 - i0)) + (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))`, `(INTERVAL_LIST (SUC i0) (SUC s0))`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( ASM_SIMP_TAC list_ss [DISJOINT_DISJ_THM, XP_BIGOR___XP_USED_VARS, IN_LIST_BIGUNION, MAP_MAP_o, combinTheory.o_DEF, XP_USED_VARS_EVAL, MEM_MAP, GSYM LEFT_FORALL_OR_THM, IN_SING] THEN REWRITE_TAC [MEM_INTERVAL_LIST] THEN REPEAT WEAKEN_HD_TAC THEN GEN_TAC THEN LEFT_DISJ_TAC THEN FULL_SIMP_TAC arith_ss [] ) THEN GSYM_NO_TAC 1 THEN ASM_CONGRUENCE_SIMP_TAC ks_congset arith_ss [] ); val PROBLEM_TO_KRIPKE_STRUCTURE___TOTAL = store_thm ("PROBLEM_TO_KRIPKE_STRUCTURE___TOTAL", ``!A p psl i0 s0 DS S0 R l' pf sv a. ( F_CLOCK_SERE_FREE psl /\ IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A /\ ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\ (A.S = (INTERVAL_SET (SUC i0) s0)) /\ (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\ (i0 <= s0) /\ (sv = \n:num. 2**(s0 - i0) + s0 + 1 + n) /\ LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l',a,T,pf) IN DS.B /\ DS.IV SUBSET INTERVAL_SET 0 (2**(s0 - i0) + s0) /\ LTL_EQUIVALENT_INITIAL (LTL_EQUIV (LTL_ALWAYS (LTL_PROP (P_FORALL (INTERVAL_LIST (SUC i0) s0) (P_IMPL (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0), p)))), PSL_TO_LTL psl)) l' /\ (PROP_LOGIC_EQUIVALENT (P_AND (P_FORALL (INTERVAL_LIST (SUC i0) s0) (P_EQUIV (A.S0, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0))), P_AND (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv,P_NOT (pf sv)))) S0) /\ (XPROP_LOGIC_EQUIVALENT (XP_AND (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) s0) (XP_EQUIV (XP_NEXT (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0)), XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) s0) (XP_AND (A.R, XP_CURRENT (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0)))))), XP_BIGAND (MAP (\xp. xp sv) DS.R))) R) ) ==> ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0 R) (MAP (\x. x sv) DS.FC)) = (!K. ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) = UF_KS_SEM K psl)))``, REPEAT STRIP_TAC THEN `?f. f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC s0)` by METIS_TAC[] THEN ASSUME_TAC (GSYM PROBLEM_TO_LTL_KS_SEM___TOTAL) THEN Q_SPECL_NO_ASSUM 0 [`A`, `p`, `psl`, `i0`, `s0`, `f`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC std_ss [] THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN MATCH_MP_TAC (prove (``!M X f f'. (LTL_EQUIVALENT_INITIAL f f' /\ (X = LTL_KS_SEM M f)) ==> (X = LTL_KS_SEM M f')``, SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def, LTL_KS_SEM_def] THEN PROVE_TAC[])) THEN Q_TAC EXISTS_TAC `l'` THEN REPEAT STRIP_TAC THEN1 ( FULL_SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def] THEN GSYM_NO_TAC 3 THEN ASM_SIMP_TAC arith_ss [LTL_SEM_THM, P_FORALL_SEM, LIST_TO_SET___INTERVAL_LIST, SET_TO_LIST_INV, FINITE_INTERVAL_SET, P_SEM_THM, GSYM VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST, GSYM (SIMP_RULE std_ss [PROP_LOGIC_EQUIVALENT_def] VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET)] ) THEN WEAKEN_NO_TAC 3 (*LTL_EQUIVALENT_INITIAL l'*) THEN GSYM_NO_TAC 6 (*Def sv*) THEN GSYM_NO_TAC 1 (*Def f*) THEN ASM_SIMP_TAC std_ss [] THEN Q.ABBREV_TAC `KS = (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE (RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f))` THEN ASSUME_TAC (INST_TYPE [alpha |-> num] LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE) THEN Q_SPECL_NO_ASSUM 0 [`DS`, `l'`, `pf`, `sv`, `KS`, `a`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( ASM_REWRITE_TAC[] THEN SUBGOAL_TAC `SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS KS SUBSET INTERVAL_SET 0 (2**(s0 - i0) + s0)` THEN1 ( Q.UNABBREV_TAC `KS` THEN REMAINS_TAC `SEMI_AUTOMATON_USED_VARS (RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f) SUBSET INTERVAL_SET 0 (2 ** (s0 - i0) + s0)` THEN1 ( UNDISCH_HD_TAC THEN MATCH_MP_TAC (prove (``(C SUBSET A) ==> (A SUBSET B ==> C SUBSET B)``, METIS_TAC[SUBSET_TRANS])) THEN SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, symbolic_kripke_structure_REWRITES, SUBSET_DEF, IN_UNION] ) THEN SUBGOAL_TAC `SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)` THEN1 ( ASM_REWRITE_TAC[SEMI_AUTOMATON_USED_VARS_def] THEN SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET] THEN REPEAT STRIP_TAC THEN RES_TAC THEN DECIDE_TAC ) THEN ASSUME_TAC (INST_TYPE [alpha |-> num] RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS) THEN Q_SPECL_NO_ASSUM 0 [`A`, `f`] THEN PROVE_CONDITION_NO_ASSUM 0 THEN1 ( GSYM_NO_TAC 1 (*Def f*) THEN ASM_SIMP_TAC std_ss [FINITE_INTERVAL_SET, DISJOINT_DISJ_THM, SEMI_AUTOMATON_USED_VARS_def, IN_UNION] THEN GEN_TAC THEN LEFT_DISJ_TAC THEN SUBGOAL_TAC `x <= s0` THEN1 ( CLEAN_ASSUMPTIONS_TAC THENL [ `x IN INTERVAL_SET 0 i0` by METIS_TAC[UNION_SUBSET, SUBSET_DEF] THEN FULL_SIMP_TAC arith_ss [IN_INTERVAL_SET], FULL_SIMP_TAC arith_ss [IN_INTERVAL_SET] ] ) THEN Cases_on `i0 = s0` THENL [ SUBGOAL_TAC `INTERVAL_SET (SUC i0) s0 = EMPTY` THEN1 ( ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY] ) THEN ASM_REWRITE_TAC[IN_IMAGE, IN_POW, SUBSET_EMPTY] THEN SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT_def, SET_BINARY_ENCODING_def, IMAGE_EMPTY, SUM_IMAGE_THM] THEN DECIDE_TAC, `SUC i0 <= s0` by DECIDE_TAC THEN ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, DISJOINT_DISJ_THM, IN_INTERVAL_SET] ] ) THEN ASM_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def, symbolic_semi_automaton_REWRITES, UNION_SUBSET, SUBSET_DEF, IN_INTERVAL_SET, IN_UNION] THEN REPEAT STRIP_TAC THENL [ `x IN INTERVAL_SET 0 i0` by PROVE_TAC[UNION_SUBSET, SUBSET_DEF] THEN UNDISCH_HD_TAC THEN ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET], UNDISCH_HD_TAC THEN GSYM_NO_TAC 2 (*Def f*) THEN ASM_REWRITE_TAC[] THEN Cases_on `i0 = s0` THENL [ SUBGOAL_TAC `INTERVAL_SET (SUC s0) s0 = EMPTY` THEN1 ( ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY] ) THEN ASM_REWRITE_TAC[IN_IMAGE, IN_POW, SUBSET_EMPTY] THEN SIMP_TAC arith_ss [SET_BINARY_ENCODING_SHIFT_def, SET_BINARY_ENCODING_def, IMAGE_EMPTY, SUM_IMAGE_THM], `SUC i0 <= s0` by DECIDE_TAC THEN `SUC (s0 - SUC i0) = (s0 - i0)` by DECIDE_TAC THEN ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN WEAKEN_HD_TAC THEN `~((2:num)**(s0 - i0) = 0)` by SIMP_TAC std_ss [EXP_EQ_0] THEN DECIDE_TAC ] ] ) THEN GSYM_NO_TAC 3 THEN ASM_SIMP_TAC std_ss [IS_ELEMENT_ITERATOR_def, IN_UNION] THEN REPEAT STRIP_TAC THEN ( `2 ** (s0 - i0) + s0 + 1 + i IN INTERVAL_SET 0 (2 ** (s0 - i0) + s0)` by METIS_TAC[SUBSET_DEF] THEN UNDISCH_HD_TAC THEN SIMP_TAC arith_ss [IN_INTERVAL_SET] ) ) THEN ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN Q.UNABBREV_TAC `KS` THEN NTAC 2 (GSYM_NO_TAC 1) (*Def f, sv*) THEN ASM_SIMP_TAC std_ss [RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def, SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def, SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, symbolic_semi_automaton_REWRITES, symbolic_kripke_structure_REWRITES] THEN ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET) THEN Q_SPEC_NO_ASSUM 0 `INTERVAL_LIST (SUC i0) s0` THEN SIMP_ALL_TAC std_ss [LIST_TO_SET___INTERVAL_LIST] THEN GSYM_NO_TAC 2 (*sv*) THEN ASM_SIMP_TAC std_ss [] THEN ASM_CONGRUENCE_SIMP_TAC ks_congset arith_ss [P_BIGOR___SET_TO_LIST___INTERVAL_SET, XP_BIGOR___SET_TO_LIST___INTERVAL_SET, P_FORALL___SET_TO_LIST___INTERVAL_SET, XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET, XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET, VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST] ); val _ = export_theory();