(* app load ["bossLib", "numLib", "pairTheory", "schneiderUtils", "Past_Temporal_LogicTheory"]; *) open HolKernel Parse boolLib Rsyntax schneiderUtils numLib numTheory prim_recTheory arithmeticTheory pairTheory Temporal_LogicTheory Past_Temporal_LogicTheory; infixr 3 -->; infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL; val _ = Rewrite.add_implicit_rewrites pairTheory.pair_rws; val ZERO_LEMMA = ARITH_PROVE(--`~(x'state. (q t0 = InitVal) /\ (!t. q(t+(t0+1)) = TransRel((i(t+t0):'input),q(t+t0))) /\ Accept(i,(\t.q(t+t0)))) = (!q:num->'state. (q t0 = InitVal) /\ (!t. q(t+(t0+1)) = TransRel((i(t+t0):'input),q(t+t0))) ==> Accept(i,(\t.q(t+t0)))) `--), EQ_TAC THEN REPEAT STRIP_TAC THENL[ MY_MP_TAC (--`(\t.q'(t+t0))=((\t.q(t+t0)):num->'state)`--) THENL[ CONV_TAC FUN_EQ_CONV THEN BETA_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,ADD1,SYM(SPEC_ALL ADD_ASSOC)], DISCH_TAC] THEN ASM_REWRITE_TAC[], (* ------------------------------------------------------------------------ *) ASSUME_TAC(EXISTENCE(REWRITE_RULE[ADD1](BETA_RULE (ISPECL[(--`InitVal:'state`--), (--`\x:'state.\t:num.TransRel((i(t+t0)):'input,x):'state`--)] num_Axiom_old)))) THEN LEFT_EXISTS_TAC THEN EXISTS_TAC (--`\t:num.fn1(t-t0):'state`--) THEN LEFT_NO_FORALL_TAC 1 (--`\t:num.fn1(t-t0):'state`--) THEN UNDISCH_HD_TAC THEN BETA_TAC THEN ASM_REWRITE_TAC[ EQT_ELIM(ARITH_CONV(--`n-n=0`--)), EQT_ELIM(ARITH_CONV(--`(t+t0)-t0=t`--)), EQT_ELIM(ARITH_CONV(--`(t+(t0+1))-t0=t+1`--))] ]); val NEG_DET_AUTOMATA = TAC_PROOF( ([],--` ~(?q. (q(t0) = (InitVal:'state)) /\ (!t. q(t+(t0+1)) = TransRel((i(t+t0):'input),(q(t+t0):'state))) /\ Accept(i,\t. q(t+t0)) ) = ?q. (q(t0) = InitVal) /\ (!t. q(t+(t0+1)) = TransRel((i(t+t0):'input),(q(t+t0):'state))) /\ ~Accept(i,\t. q(t+t0)) `--), SUBST1_TAC DET_OMEGA_EXISTS_FORALL_THEOREM THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV) THEN REWRITE_TAC[TAC_PROOF(([],--`(a==>b) = (~a\/b)`--),PROP_TAC)] THEN REWRITE_TAC[DE_MORGAN_THM] THEN REWRITE_TAC[TAC_PROOF(([],--`((a/\b)/\c) = (a/\b/\c)`--),PROP_TAC)] ); val OMEGA_CONJ_CLOSURE = TAC_PROOF( let val cb1 = (--`?q1. Phi_I1(q1 t0) /\ (!t. Phi_R1((i(t+t0):'a),(q1(t+t0):'b1))) /\ Psi1(i,q1)`--) val cb2 = (--`?q2. Phi_I2(q2 t0) /\ (!t. Phi_R2((i(t+t0):'a),(q2(t+t0):'b2))) /\ Psi2(i,q2)`--) in ([],--`(^cb1 /\ ^cb2) = ? q1 q2. (Phi_I1(q1 t0) /\ Phi_I2(q2 t0)) /\ (!t. Phi_R1((i(t+t0):'a),(q1(t+t0):'b1)) /\ Phi_R2((i(t+t0):'a),(q2(t+t0):'b2)) ) /\ (Psi1(i,q1) /\ Psi2(i,q2)) `--) end, EQ_TAC THEN REPEAT STRIP_TAC THENL[ EXISTS_TAC(--`q1:num->'b1`--) THEN EXISTS_TAC(--`q2:num->'b2`--), EXISTS_TAC(--`q1:num->'b1`--), EXISTS_TAC(--`q2:num->'b2`--) ] THEN ASM_REWRITE_TAC[]) val OMEGA_DISJ_CLOSURE = TAC_PROOF( let val cb1 = (--`?q1. Phi_I1(q1 t0) /\ (!t. Phi_R1((i(t+t0):'a),(q1(t+t0):'b1))) /\ Psi1(i,q1)`--) val cb2 = (--`?q2. Phi_I2(q2 t0) /\ (!t. Phi_R2((i(t+t0):'a),(q2(t+t0):'b2))) /\ Psi2(i,q2)`--) in ([],--`(^cb1 \/ ^cb2) = ?p q1 q2. (~p(t0) /\ Phi_I1(q1 t0) \/ p(t0) /\ Phi_I2(q2 t0) ) /\ (!t. ~p(t+t0) /\ Phi_R1((i(t+t0):'a),(q1(t+t0):'b1)) /\ ~p(t+(t0+1)) \/ p(t+t0) /\ Phi_R2((i(t+t0):'a),(q2(t+t0):'b2)) /\ p(t+(t0+1)) ) /\ (~p t0 /\ Psi1(i,q1) \/ p t0 /\ Psi2(i,q2)) `--) end, EQ_TAC THEN REPEAT STRIP_TAC THENL[ EXISTS_TAC (--`\t:num.F`--) THEN EXISTS_TAC (--`q1:num->'b1`--) THEN EXISTS_TAC (--`q2:num->'b2`--) THEN ASM_REWRITE_TAC[], EXISTS_TAC (--`\t:num.T`--) THEN EXISTS_TAC (--`q1:num->'b1`--) THEN EXISTS_TAC (--`q2:num->'b2`--) THEN ASM_REWRITE_TAC[], MY_MP_TAC (--`!t. ~p(t+t0)`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 2 (--`t:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD1)] THEN STRIP_TAC, DISCH_TAC ] THEN DISJ1_TAC THEN EXISTS_TAC(--`q1:num->'b1`--) THEN POP_ASSUM (fn x => RULE_ASSUM_TAC(REWRITE_RULE[x]) THEN ASSUME_TAC x) THEN ASM_REWRITE_TAC[], MY_MP_TAC (--`!t. p(t+t0)`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 2 (--`t:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD1)] THEN STRIP_TAC, DISCH_TAC ] THEN DISJ2_TAC THEN EXISTS_TAC(--`q2:num->'b2`--) THEN POP_ASSUM (fn x => RULE_ASSUM_TAC(REWRITE_RULE[x]) THEN ASSUME_TAC x) THEN ASM_REWRITE_TAC[] ]) (* ******************************************************************** *) (* some facts about the boolean closure of NDET_G-automata *) (* ******************************************************************** *) val NEG_G = TAC_PROOF( ([],--`~(!t:num.a(t+t0)) = (?t. ~a(t+t0))`--), CONV_TAC (DEPTH_CONV NOT_FORALL_CONV) THEN REWRITE_TAC[]) val CONJ_G = TAC_PROOF( ([],--`(!t:num.a(t+t0)) /\ (!t. b(t+t0)) = (!t. a(t+t0) /\ b(t+t0))`--), EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]) val DISJ_G = TAC_PROOF( ([],--`(!t. a(t+t0)) \/ (!t. b(t+t0)) = (?p q. (~p t0 /\ ~q t0) /\ (!t. (p(t+(t0+1)) = p(t+t0) \/ ~a(t+t0)) /\ (q(t+(t0+1)) = q(t+t0) \/ ~b(t+t0)) ) /\ (!t.~p(t+t0) \/ ~q(t+t0))) `--), REWRITE_TAC[ONE,ADD_CLAUSES] THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL[ ASSUME_TAC(EXISTENCE(BETA_RULE (ISPECL[(--`F`--),(--`\x:bool.\t:num. x`--)]num_Axiom_old))) THEN ASSUME_TAC(EXISTENCE(BETA_RULE (ISPECL[(--`F`--),(--`\x:bool.\t:num. x\/~b(t+t0)`--)]num_Axiom_old))) THEN LEFT_EXISTS_TAC THEN LEFT_NO_EXISTS_TAC 1 THEN EXISTS_TAC (--`\t.fn1'(t-t0):bool`--) THEN EXISTS_TAC (--`\t.fn1(t-t0):bool`--) THEN BETA_TAC THEN ASM_REWRITE_TAC[ EQT_ELIM(ARITH_CONV(--`t0-t0=0`--)), EQT_ELIM(ARITH_CONV(--`(t+t0)-t0 = t`--)), EQT_ELIM(ARITH_CONV(--`SUC(t+t0)-t0 = SUC t`--))] THEN MY_MP_TAC (--`!t:num.~fn1' t`--) THENL[INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES],DISCH_TAC] THEN ASM_REWRITE_TAC[], ASSUME_TAC(EXISTENCE(BETA_RULE (ISPECL[(--`F`--),(--`\x:bool.\t:num. x\/~a(t+t0)`--)]num_Axiom_old))) THEN ASSUME_TAC(EXISTENCE(BETA_RULE (ISPECL[(--`F`--),(--`\x:bool.\t:num. x`--)]num_Axiom_old))) THEN LEFT_EXISTS_TAC THEN LEFT_NO_EXISTS_TAC 1 THEN EXISTS_TAC (--`\t.fn1'(t-t0):bool`--) THEN EXISTS_TAC (--`\t.fn1(t-t0):bool`--) THEN BETA_TAC THEN ASM_REWRITE_TAC[ EQT_ELIM(ARITH_CONV(--`t0-t0=0`--)), EQT_ELIM(ARITH_CONV(--`(t+t0)-t0 = t`--)), EQT_ELIM(ARITH_CONV(--`SUC(t+t0)-t0 = SUC t`--))] THEN MY_MP_TAC (--`!t:num.~fn1 t`--) THENL[INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES],DISCH_TAC] THEN ASM_REWRITE_TAC[], ALL_TAC] (* ---------------------------------------------------------------------------- *) (* Here comes the real problem that is to be proved: *) (* *) (* (--`(!t. a (t + t0)) \/ (!t. b (t + t0))`--) *) (* ____________________________ *) (* (--`~(p t0)`--) *) (* (--`~(q t0)`--) *) (* (--`!t. *) (* (p (SUC (t + t0)) = p (t + t0) \/ ~(a (t + t0))) /\ *) (* (q (SUC (t + t0)) = q (t + t0) \/ ~(b (t + t0)))`--) *) (* (--`!t. ~(p (t + t0)) \/ ~(q (t + t0))`--) *) (* ---------------------------------------------------------------------------- *) THEN DISJ_CASES_TAC(SPEC(--`p:num->bool`--)(GEN(--`b:num->bool`--)DELTA_CASES)) THEN DISJ_CASES_TAC(SPEC(--`q:num->bool`--)(GEN(--`b:num->bool`--)DELTA_CASES)) THEN UNDISCH_NO_TAC 3 THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`SUC(t+t0) = (SUC t)+t0`--))] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN LEFT_NO_EXISTS_TAC 1 THEN LEFT_NO_EXISTS_TAC 2 THEN MY_MP_TAC (--`!x. q(x+(d+t0))`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`SUC(x+(d+t0))=(SUC(x+d))+t0`--))] THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)], DISCH_TAC] THEN MY_MP_TAC (--`!x. p(x+(d'+t0))`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`SUC(x+(d'+t0))=(SUC(x+d'))+t0`--))] THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)], DISCH_TAC] THEN LEFT_NO_FORALL_TAC 5 (--`d+d'`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)] THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV(--`(d+(d'+t0))=(d'+(d+t0))`--))) THEN ASM_REWRITE_TAC[] ); val BOOLEAN_CLOSURE_G = TAC_PROOF( ([],--` ( ~(!t:num.a(t+t0)) = (?t. ~a(t+t0)) ) /\ ( (!t:num.a(t+t0)) /\ (!t. b(t+t0)) = (!t. a(t+t0) /\ b(t+t0)) ) /\ ( (!t. a(t+t0)) \/ (!t. b(t+t0)) = (?p q. (~p t0 /\ ~q t0) /\ (!t. (p(t+(t0+1)) = p(t+t0) \/ ~a(t+t0)) /\ (q(t+(t0+1)) = q(t+t0) \/ ~b(t+t0)) ) /\ (!t.~p(t+t0) \/ ~q(t+t0))) ) `--), REWRITE_TAC[NEG_G,CONJ_G,DISJ_G]); (* ******************************************************************** *) (* some facts about the boolean closure of NDET_F-automata *) (* ******************************************************************** *) val NEG_F = TAC_PROOF( ([],--`~(?t:num.a(t+t0)) = (!t. ~a(t+t0))`--), CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) THEN REWRITE_TAC[]) val CONJ_F = TAC_PROOF( ([],--`(?t. a(t+t0)) /\ (?t. b(t+t0)) = (?p q. (~p t0 /\ ~q t0) /\ (!t. (p(t+(t0+1)) = p(t+t0) \/ a(t+t0)) /\ (q(t+(t0+1)) = q(t+t0) \/ b(t+t0)) ) /\ (?t. p(t+t0) /\ q(t+t0))) `--), REWRITE_TAC[ONE,ADD_CLAUSES] THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL[ (* ---------------------------------------------------------------------------- *) ASSUME_TAC(EXISTENCE(BETA_RULE (ISPECL[(--`F`--),(--`\x:bool.\t:num. x\/a(t+t0)`--)]num_Axiom_old))) THEN ASSUME_TAC(EXISTENCE(BETA_RULE (ISPECL[(--`F`--),(--`\x:bool.\t:num. x\/b(t+t0)`--)]num_Axiom_old))) THEN LEFT_EXISTS_TAC THEN LEFT_NO_EXISTS_TAC 1 THEN EXISTS_TAC (--`\t.fn1'(t-t0):bool`--) THEN EXISTS_TAC (--`\t.fn1(t-t0):bool`--) THEN BETA_TAC THEN ASM_REWRITE_TAC[ EQT_ELIM(ARITH_CONV(--`t0-t0=0`--)), EQT_ELIM(ARITH_CONV(--`(t+t0)-t0 = t`--)), EQT_ELIM(ARITH_CONV(--`SUC(t+t0)-t0 = SUC t`--))] THEN MY_MP_TAC (--`!x:num.fn1'(SUC(x+t))`--) THENL[ INDUCT_TAC THENL[ ASM_REWRITE_TAC[ADD_CLAUSES], ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[ADD_CLAUSES] THEN POP_ASSUM REWRITE1_TAC], DISCH_TAC] THEN MY_MP_TAC (--`!x:num.fn1(SUC(x+t'))`--) THENL[ INDUCT_TAC THENL[ ASM_REWRITE_TAC[ADD_CLAUSES], ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[ADD_CLAUSES] THEN POP_ASSUM REWRITE1_TAC], DISCH_TAC] THEN EXISTS_TAC (--`SUC(t+t')`--) THEN REWRITE_TAC[ADD_CLAUSES] THEN POP_ASSUM REWRITE1_TAC THEN ONCE_REWRITE_TAC[ADD_SYM] THEN POP_ASSUM REWRITE1_TAC, (* ---------------------------------------------------------------------------- *) DISJ_CASES_TAC(SPEC(--`p:num->bool`--)(GEN(--`b:num->bool`--)DELTA_CASES)) THENL[ALL_TAC,UNDISCH_NO_TAC 2 THEN ASM_REWRITE_TAC[]] THEN LEFT_EXISTS_TAC THEN MY_MP_TAC (--`0bool`--)(GEN(--`b:num->bool`--)DELTA_CASES)) THENL[ALL_TAC,UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[]] THEN LEFT_EXISTS_TAC THEN MY_MP_TAC (--`0~b(t+t0)|a(t+t0))) /\ !t1.?t2. q(t1+(t2+t0)) /\ b(t1+(t2+t0)))`--), REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL[ (* ---------------------------------------------------------------------------- *) ASSUME_TAC(EXISTENCE(BETA_RULE (ISPECL[(--`F`--),(--`\x (t:num). x=>~b(t+t0)|a(t+t0)`--)]num_Axiom_old))) THEN LEFT_EXISTS_TAC THEN EXISTS_TAC (--`\t.fn1(t-t0):bool`--) THEN BETA_TAC THEN ASM_REWRITE_TAC[ EQT_ELIM(ARITH_CONV(--`n-n=0`--)), EQT_ELIM(ARITH_CONV(--`(t+t0)-t0=t`--)), EQT_ELIM(ARITH_CONV(--`(t+(t0+1))-t0=t+1`--))] (* ------------------------------------------------------------------------ *) THEN MY_MP_TAC (--`!t. fn1 t ==> (?d. fn1(t+d) /\ b(t+(d+t0)))`--) (* ------------------------------------------------------------------------ *) THENL[ GEN_TAC THEN DISCH_TAC THEN LEFT_NO_FORALL_TAC 2 (--`t:num`--) THEN POP_ASSUM (fn x=>ASSUME_TAC(MATCH_MP (BETA_RULE(SPEC(--`\t2.b(t+(t2+t0)):bool`--)WOP)) x)) THEN LEFT_EXISTS_TAC THEN MY_MP_TAC (--`!m. m<=n ==> fn1(t+m)`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN IMP_RES_TAC OR_LESS THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ THEN RES_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)], DISCH_TAC] THEN EXISTS_TAC(--`n:num`--) THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(EQT_ELIM(ARITH_CONV(--`(n=0)\/(0 (p (p<=n)`--))) THEN RES_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)], DISCH_TAC] (* ------------------------------------------------------------------------ *) THEN MY_MP_TAC (--`!t. ~fn1 t ==> (?d. ~fn1(t+d) /\ a(t+(d+t0)))`--) (* ------------------------------------------------------------------------ *) THENL[ GEN_TAC THEN DISCH_TAC THEN LEFT_NO_FORALL_TAC 4 (--`t:num`--) THEN POP_ASSUM (fn x=>ASSUME_TAC(MATCH_MP (BETA_RULE(SPEC(--`\t2.a(t+(t2+t0)):bool`--)WOP)) x)) THEN LEFT_EXISTS_TAC THEN MY_MP_TAC (--`!m. m<=n ==> ~fn1(t+m)`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN IMP_RES_TAC OR_LESS THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ THEN RES_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)], DISCH_TAC] THEN EXISTS_TAC(--`n:num`--) THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(EQT_ELIM(ARITH_CONV(--`(n=0)\/(0 (p (p<=n)`--))) THEN RES_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)], DISCH_TAC] (* ------------------------------------------------------------------------ *) THEN ASM_REWRITE_TAC[ADD_CLAUSES,num_CONV(--`1`--)] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`(t1+(t2+t0))-t0=t1+t2`--))] THEN GEN_TAC THEN DISJ_CASES_TAC(SPEC(--`(fn1:num->bool) t1`--)BOOL_CASES_AX) THENL[ LEFT_NO_FORALL_TAC 2 (--`t1:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[], LEFT_NO_FORALL_TAC 1 (--`t1:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MY_MP_TAC (--`fn1(SUC(t1+d)):bool`--) THENL[ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)],DISCH_TAC] THEN LEFT_NO_FORALL_TAC 4 (--`SUC(t1+d)`--) THEN UNDISCH_HD_TAC THEN POP_NO_TAC 4 THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD_ASSOC)] THEN STRIP_TAC THEN EXISTS_TAC(--`SUC(d+d')`--) THEN ASM_REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD_ASSOC)] ], (* ---------------------------------------------------------------------------- *) COPY_ASM_NO 0 THEN LEFT_FORALL_TAC (--`t1:num`--) THEN LEFT_EXISTS_TAC THEN DISCH_TAC THEN MY_MP_TAC (--`~q((t1+t2)+(t0+1)):bool`--) THENL[ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)],DISCH_TAC] THEN LEFT_NO_FORALL_TAC 1 (--`SUC(t1+t2)`--) THEN UNDISCH_HD_TAC THEN CONV_TAC CONTRAPOS_CONV THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV) THEN REPEAT STRIP_TAC THEN POP_NO_TAC 0 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD_ASSOC)] THEN RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES,SYM(SPEC_ALL ADD_ASSOC),ONE]) THEN SPEC_TAC((--`t2':num`--),(--`t2':num`--)) THEN INDUCT_TAC THENL[ASM_REWRITE_TAC[ADD_CLAUSES], ALL_TAC] THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV (--`SUC(t1+(t2+(SUC t2'+t0))) = SUC((t1+(t2+(SUC t2')))+t0)`--))) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD_ASSOC)] THEN ASM_TAC 0 REWRITE1_TAC THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV (--`SUC(t1+(t2+(t2'+t0))) = t1+(SUC(t2+t2')+t0)`--))) THEN ASM_TAC 1 REWRITE1_TAC, (* ---------------------------------------------------------------------------- *) LEFT_FORALL_TAC (--`t1:num`--) THEN LEFT_EXISTS_TAC THEN EXISTS_TAC (--`t2:num`--) THEN ASM_REWRITE_TAC[] (* ---------------------------------------------------------------------------- *) ]); val DISJ_FG = TAC_PROOF( ([],--`!a b. (?t1.!t2. a(t1+(t2+t0))) \/ (?t1.!t2. b(t1+(t2+t0))) = (?q. ~q t0 /\ (!t. q(t+(t0+1)) = (q(t+t0) => b(t+t0) | ~a(t+t0))) /\ ?t1.!t2. ~q(t1+(t2+t0)) \/ b(t1+(t2+t0)))`--), REPEAT GEN_TAC THEN PURE_ONCE_REWRITE_TAC[TAC_PROOF(([],--`(a=b)=(~a=~b)`--),PROP_TAC)] THEN PURE_REWRITE_TAC[DE_MORGAN_THM] THEN CONV_TAC(REPEATC(CHANGED_CONV(DEPTH_CONV (NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV)))) THEN SUBST1_TAC(BETA_RULE(SPECL [(--`\t:num. ~a(t)`--),(--`\t:num. ~b(t)`--)] CONJ_GF)) THEN REWRITE_TAC[TAC_PROOF(([],--`~(a/\b/\c) = (a/\b) ==> ~c`--),PROP_TAC)] THEN REWRITE_TAC[ADD_CLAUSES,num_CONV(--`1`--)] THEN EQ_TAC THEN REPEAT STRIP_TAC THENL[ (* ---------------------------------------------------------------- *) MY_MP_TAC (--`!t:num. q'(t+t0) = (q:num->bool)(t+t0)`--) THENL[INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES], DISCH_TAC] THEN LEFT_NO_FORALL_TAC 4 (--`t1:num`--) THEN LEFT_EXISTS_TAC THEN LEFT_NO_FORALL_TAC 2 (--`t2:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[ADD_ASSOC] THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)], (* ---------------------------------------------------------------- *) ASSUME_TAC(EXISTENCE(BETA_RULE (ISPECL[(--`F`--),(--`\x t:num. x => b(t+t0) | ~a(t+t0)`--)] num_Axiom_old))) THEN LEFT_EXISTS_TAC THEN EXISTS_TAC (--`\t.(fn1(t-t0)):bool`--) THEN LEFT_NO_FORALL_TAC 1 (--`\t.(fn1(t-t0)):bool`--) THEN UNDISCH_HD_TAC THEN BETA_TAC THEN ASM_REWRITE_TAC[ EQT_ELIM(ARITH_CONV(--`n-n=0`--)), EQT_ELIM(ARITH_CONV(--`(t+t0)-t0=t`--)), EQT_ELIM(ARITH_CONV(--`SUC(t+t0)-t0=SUC t`--))] THEN CONV_TAC(REPEATC(CHANGED_CONV(DEPTH_CONV (NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV)))) THEN REWRITE_TAC[DE_MORGAN_THM] (* ---------------------------------------------------------------- *) ]) val CONJ_FG = TAC_PROOF( ([],--`!a b. (?t1.!t2.a(t1+(t2+t0))) /\ (?t1.!t2.b(t1+(t2+t0))) = ?t1.!t2. a(t1+(t2+t0)) /\ b(t1+(t2+t0))`--), REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL[ DISJ_CASES_TAC (SPECL[(--`t1:num`--),(--`t1':num`--)]LESS_CASES) THENL[ IMP_RES_TAC LESS_ADD_1 THEN EXISTS_TAC (--`t1+(p+1)`--) THEN GEN_TAC THEN POP_ASSUM (fn x=>RULE_ASSUM_TAC(SUBS[x])) THEN LEFT_NO_FORALL_TAC 2 (--`p+(1+t2)`--) THEN ASM_REWRITE_TAC[] THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_ASSOC], IMP_RES_TAC LESS_EQUAL_ADD THEN EXISTS_TAC (--`t1'+p`--) THEN GEN_TAC THEN POP_ASSUM (fn x=>RULE_ASSUM_TAC(SUBS[x])) THEN LEFT_NO_FORALL_TAC 1 (--`p+t2`--) THEN ASM_REWRITE_TAC[] THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_ASSOC] ], EXISTS_TAC(--`t1:num`--) THEN GEN_TAC THEN LEFT_FORALL_TAC (--`t2:num`--) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`t1:num`--) THEN GEN_TAC THEN LEFT_FORALL_TAC (--`t2:num`--) THEN ASM_REWRITE_TAC[] ]); val DISJ_GF = TAC_PROOF( ([],--`!a b. (!t1.?t2.a(t1+(t2+t0))) \/ (!t1.?t2.b(t1+(t2+t0))) = !t1.?t2. a(t1+(t2+t0)) \/ b(t1+(t2+t0))`--), REPEAT GEN_TAC THEN PURE_ONCE_REWRITE_TAC[TAC_PROOF(([],--`(a=b)=(~a=~b)`--),PROP_TAC)] THEN PURE_REWRITE_TAC[DE_MORGAN_THM] THEN CONV_TAC(REPEATC(CHANGED_CONV(DEPTH_CONV (NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV)))) THEN SUBST1_TAC(BETA_RULE(SPECL [(--`\t:num. ~a(t)`--),(--`\t:num. ~b(t)`--)] CONJ_FG)) THEN REWRITE_TAC[DE_MORGAN_THM] ) val BOOLEAN_CLOSURE_FG = TAC_PROOF( ([],--` ( ~(?t1.!t2. a(t1+(t2+t0))) = (!t1.?t2. ~a(t1+(t2+t0))) ) /\ ( (?t1.!t2.a(t1+(t2+t0))) /\ (?t1.!t2.b(t1+(t2+t0))) = ?t1.!t2. a(t1+(t2+t0)) /\ b(t1+(t2+t0)) ) /\ ( (?t1.!t2. a(t1+(t2+t0))) \/ (?t1.!t2. b(t1+(t2+t0))) = (?q. ~q t0 /\ (!t. q(t+(t0+1)) = (q(t+t0) => b(t+t0) | ~a(t+t0))) /\ ?t1.!t2. ~q(t1+(t2+t0)) \/ b(t1+(t2+t0))) ) `--), REWRITE_TAC[NEG_FG,CONJ_FG,DISJ_FG]); val BOOLEAN_CLOSURE_GF = TAC_PROOF( ([],--` ( ~(!t1.?t2. a(t1+(t2+t0))) = (?t1.!t2. ~a(t1+(t2+t0))) ) /\ ( (!t1.?t2.a(t1+(t2+t0))) \/ (!t1.?t2.b(t1+(t2+t0))) = !t1.?t2. a(t1+(t2+t0)) \/ b(t1+(t2+t0))) /\ ( (!t1.?t2. a(t1+(t2+t0))) /\ (!t1.?t2. b(t1+(t2+t0))) = (?q. ~q t0 /\ (!t. q(t+(t0+1)) = (q(t+t0) =>~b(t+t0)|a(t+t0))) /\ !t1.?t2. q(t1+(t2+t0)) /\ b(t1+(t2+t0))) ) `--), REWRITE_TAC[NEG_GF,CONJ_GF,DISJ_GF]); (* ******************************************************************** *) (* some facts on the Borel Hierarchy *) (* ******************************************************************** *) val G_AS_NDET_F = TAC_PROOF( ([],--` (!t.a(t+t0)) = ?q. q t0 /\ (!t. q(t+t0) /\ a(t+t0) /\ q(SUC(t+t0))) /\ (?t. q(t+t0)) `--), EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC (--`\t:num. T`--) THEN BETA_TAC THEN REWRITE_TAC[] ) val G_AS_NDET_FG = TAC_PROOF( ([],--` (!t.a(t+t0)) = ?q. q t0 /\ (!t. q(SUC(t+t0)) = q(t+t0) /\ a(t+t0)) /\ (?t1.!t2. q(t1+(t2+t0))) `--), EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL[EXISTS_TAC (--`\t:num. T`--) THEN BETA_TAC THEN REWRITE_TAC[],ALL_TAC] THEN UNDISCH_HD_TAC THEN CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV) THEN MY_MP_TAC (--`!x. ~q(SUC(x+(t+t0)))`--) THENL[ INDUCT_TAC THENL[ASM_REWRITE_TAC[ADD_CLAUSES],ALL_TAC] THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV(--`SUC((SUC x)+(t+t0))=SUC((SUC(x+t))+t0)`--))) THEN ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD_ASSOC)] THEN POP_ASSUM REWRITE1_TAC, DISCH_TAC] THEN POP_NO_TAC 2 THEN EXISTS_TAC(--`SUC t`--) THEN ASM_REWRITE_TAC[ADD_CLAUSES] ) val G_AS_NDET_GF = TAC_PROOF( ([],--` (!t.a(t+t0)) = ?q. q t0 /\ (!t. q(SUC(t+t0)) = q(t+t0) /\ a(t+t0)) /\ (!t1.?t2. q(t1+(t2+t0))) `--), EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL[EXISTS_TAC (--`\t:num. T`--) THEN BETA_TAC THEN REWRITE_TAC[],ALL_TAC] THEN UNDISCH_HD_TAC THEN CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV) THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV) THEN MY_MP_TAC (--`!x. ~q(SUC(x+(t+t0)))`--) THENL[ INDUCT_TAC THENL[ASM_REWRITE_TAC[ADD_CLAUSES],ALL_TAC] THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV(--`SUC((SUC x)+(t+t0))=SUC((SUC(x+t))+t0)`--))) THEN ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD_ASSOC)] THEN POP_ASSUM REWRITE1_TAC, DISCH_TAC] THEN POP_NO_TAC 2 THEN EXISTS_TAC(--`SUC t`--) THEN ONCE_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`(SUC t)+(t2+t0) = (SUC t2)+(t+t0)`--))] THEN ASM_REWRITE_TAC[ADD_CLAUSES] ) val F_AS_NDET_GF = TAC_PROOF( ([],--`(?t.a(t+t0)) = ?q. ~q t0 /\ (!t. q(SUC(t+t0)) = q(t+t0) \/ a(t+t0)) /\ (!t1.?t2. q(t1+(t2+t0)))`--), EQ_TAC THEN REPEAT STRIP_TAC THENL[ ASSUME_TAC(EXISTENCE(BETA_RULE (ISPECL[(--`F`--),(--`\x (t:num). x \/ a(t+t0)`--)]num_Axiom_old))) THEN LEFT_EXISTS_TAC THEN EXISTS_TAC (--`\t.(fn1(t-t0)):bool`--) THEN BETA_TAC THEN ASM_REWRITE_TAC[ EQT_ELIM(ARITH_CONV(--`n-n=0`--)), EQT_ELIM(ARITH_CONV(--`(t+t0)-t0=t`--)), EQT_ELIM(ARITH_CONV(--`(t1+(t2+t0))-t0=t1+t2`--)), EQT_ELIM(ARITH_CONV(--`SUC(t+t0)-t0=SUC t`--))] THEN GEN_TAC THEN EXISTS_TAC (--`SUC t`--) THEN SPEC_TAC((--`t1:num`--),(--`t1:num`--)) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN ASM_REWRITE_TAC[], LEFT_FORALL_TAC (--`SUC 0`--) THEN UNDISCH_HD_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[ADD_CLAUSES] THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) THEN DISCH_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] ]) val F_AS_NDET_FG = TAC_PROOF( ([],--`(?t.a(t+t0)) = ?q. ~q t0 /\ (!t. q(SUC(t+t0)) = q(t+t0) \/ a(t+t0)) /\ (?t1.!t2. q(t1+(t2+t0)))`--), EQ_TAC THEN REPEAT STRIP_TAC THENL[ ASSUME_TAC(EXISTENCE(BETA_RULE (ISPECL[(--`F`--),(--`\x (t:num). x \/ a(t+t0)`--)]num_Axiom_old))) THEN LEFT_EXISTS_TAC THEN EXISTS_TAC (--`\t.(fn1(t-t0)):bool`--) THEN BETA_TAC THEN ASM_REWRITE_TAC[ EQT_ELIM(ARITH_CONV(--`n-n=0`--)), EQT_ELIM(ARITH_CONV(--`(t+t0)-t0=t`--)), EQT_ELIM(ARITH_CONV(--`(t1+(t2+t0))-t0=t1+t2`--)), EQT_ELIM(ARITH_CONV(--`SUC(t+t0)-t0=SUC t`--))] THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC (--`SUC t`--) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN ASM_REWRITE_TAC[], UNDISCH_HD_TAC THEN CONV_TAC CONTRAPOS_CONV THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) THEN CONV_TAC (DEPTH_CONV NOT_FORALL_CONV) THEN DISCH_TAC THEN MY_MP_TAC (--`!t:num. ~q(t+t0)`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES], DISCH_TAC] THEN ASM_REWRITE_TAC[ADD_ASSOC] ]) val FG_AS_NDET_F = TAC_PROOF( ([],--`(?t1.!t2.a(t1+(t2+t0))) = ?q. ~q t0 /\ (!t. q(t+t0) ==> a(t+t0) /\ q(SUC(t+t0))) /\ (?t. q(t+t0))`--), EQ_TAC THEN REPEAT STRIP_TAC THENL[ EXISTS_TAC(--`\x:num. (t1+t0 t1 < SUC t`--))) THEN ASM_REWRITE_TAC[] THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV(--`((t1+((p+1))+t0)) = (t1+((p+1)+t0))`--))) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`t:num`--) THEN MY_MP_TAC (--`!x. q(t+(x+t0))`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,ADD_ASSOC] THEN RULE_ASSUM_TAC(REWRITE_RULE[ADD_ASSOC]) THEN RES_TAC, DISCH_TAC] THEN GEN_TAC THEN LEFT_FORALL_TAC(--`t2:num`--) THEN REWRITE_TAC[ADD_ASSOC] THEN RULE_ASSUM_TAC(REWRITE_RULE[ADD_ASSOC]) THEN RES_TAC ]) val FG_AS_NDET_GF = TAC_PROOF( ([],--`(?t1.!t2. a(t1+(t2+t0))) = (?p q. (~p t0 /\ ~q t0) /\ (!t. (p(t+t0) ==> p(SUC(t+t0))) /\ (p(SUC(t+t0)) ==> p(t+t0) \/ ~q(t+t0)) /\ (q(SUC(t+t0)) = (p(t+t0)/\~q(t+t0)/\~a(t+t0)) \/ (p(t+t0) /\ q(t+t0)))) /\ !t1.?t2. p(t1+(t2+t0)) /\ ~q(t1+(t2+t0)))`--), EQ_TAC THEN STRIP_TAC THENL[ EXISTS_TAC (--`\t.t1+t0b)`--),PROP_TAC)] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`t1 t1 !t2. p(t1+(t2+t0)) /\ q(t1+(t2+t0))`--) THENL[ GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL[ ASM_REWRITE_TAC[ADD_CLAUSES], LEFT_NO_FORALL_TAC 4 (--`t1+t2`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD_ASSOC)] ], DISCH_TAC] THEN MY_MP_TAC (--`!t:num.~(p(t+t0) /\ q(t+t0))`--) THENL[ UNDISCH_NO_TAC 2 THEN CONV_TAC CONTRAPOS_CONV THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV) THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV) THEN REWRITE_TAC[] THEN STRIP_TAC THEN RES_TAC THEN EXISTS_TAC (--`t':num`--) THEN ASM_REWRITE_TAC[], DISCH_TAC] THEN MY_MP_TAC (--`!d. p(t+(d+t0)) /\ ~q(t+(d+t0)) /\ a(t+(d+t0))`--) THENL[ INDUCT_TAC THENL[ LEFT_FORALL_TAC (--`SUC t`--) THEN UNDISCH_HD_TAC THEN LEFT_NO_FORALL_TAC 3 (--`t:num`--) THEN UNDISCH_HD_TAC THEN BOOL_CASES_TAC (--`p(SUC t):bool`--) THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN ASM_REWRITE_TAC[], REWRITE_TAC[ADD_CLAUSES] THEN UNDISCH_HD_TAC THEN COPY_ASM_NO 4 THEN LEFT_FORALL_TAC (--`t+d`--) THEN DISCH_TAC THEN LEFT_FORALL_TAC (--`SUC(t+d)`--) THEN UNDISCH_HD_TAC THEN UNDISCH_HD_TAC THEN LEFT_FORALL_TAC (--`SUC(SUC(t+d))`--) THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES,ADD_ASSOC] THEN PROP_TAC ], DISCH_TAC] THEN EXISTS_TAC (--`t:num`--) THEN ASM_REWRITE_TAC[] ]) val BOREL_HIERARCHY_G = TAC_PROOF( ([],--` ( (!t.a(t+t0)) = ?q. q t0 /\ (!t. q(t+t0) /\ a(t+t0) /\ q(SUC(t+t0))) /\ (?t. q(t+t0)) ) /\ ( (!t.a(t+t0)) = ?q. q t0 /\ (!t. q(SUC(t+t0)) = q(t+t0) /\ a(t+t0)) /\ (?t1.!t2. q(t1+(t2+t0))) ) /\ ( (!t.a(t+t0)) = ?q. q t0 /\ (!t. q(SUC(t+t0)) = q(t+t0) /\ a(t+t0)) /\ (!t1.?t2. q(t1+(t2+t0))) ) `--), REWRITE_TAC(map SYM [G_AS_NDET_F,G_AS_NDET_FG,G_AS_NDET_GF])); val BOREL_HIERARCHY_F = TAC_PROOF( ([],--` ( (?t.a(t+t0)) = ?q. ~q t0 /\ (!t. q(SUC(t+t0)) = q(t+t0) \/ a(t+t0)) /\ (?t1.!t2. q(t1+(t2+t0))) ) /\ ( (?t.a(t+t0)) = ?q. ~q t0 /\ (!t. q(SUC(t+t0)) = q(t+t0) \/ a(t+t0)) /\ (!t1.?t2. q(t1+(t2+t0))) ) `--), REWRITE_TAC(map SYM [F_AS_NDET_FG,F_AS_NDET_GF])); val BOREL_HIERARCHY_FG = TAC_PROOF( ([],--` ( (?t1. !t2. a(t1+(t2+t0))) = (?q. ~q t0 /\ (!t. q(t+t0) ==> a(t+t0) /\ q (SUC(t+t0))) /\ (?t. q(t+t0))) ) /\ ( (?t1. !t2. a(t1+(t2+t0))) = (?p q. (~p t0 /\ ~q t0) /\ (!t. (p(t+t0) ==> p (SUC(t+t0))) /\ (p (SUC(t+t0)) ==> p(t+t0) \/ ~(q(t+t0))) /\ (q (SUC(t+t0)) = p(t+t0) /\ ~(q(t+t0)) /\ ~(a(t+t0)) \/ p(t+t0) /\ q(t+t0))) /\ (!t1. ?t2. p(t1+(t2+t0)) /\ ~(q(t1+(t2+t0))))) ) `--), REWRITE_TAC(map SYM [FG_AS_NDET_F,FG_AS_NDET_GF])); (* ************************************************************************************ *) (* All temporal expressions can be translated into equivalent Buechi automata. For this *) (* purpose, the following theorems are of interest. However, they require that the term *) (* has to be transformed into definitional normal form and then only a satisfiability *) (* equivalent automaton is computed. *) (* ************************************************************************************ *) val WHEN2BUECHI_THM = TAC_PROOF( ([],--`(l = (a WHEN b)) = (!t. l t = (b t => a t | l(t+1))) /\ (!t1.?t2. l(t1+t2) \/ b(t1+t2))`--), REWRITE_TAC[BETA_RULE(CONV_RULE (DEPTH_CONV FUN_EQ_CONV) WHEN_FIX)] THEN CONV_TAC(DEPTH_CONV FUN_EQ_CONV) THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL[ (* ---- Proving !t1. ?t2. (a SWHEN b) (t1 + t2) ==> b (t1 + t2) ---- *) POP_NO_TAC 0 THEN GEN_TAC THEN DISJ_CASES_TAC (SPEC(--`t1:num`--)(GEN(--`t0:num`--)DELTA_CASES)) THENL[ LEFT_EXISTS_TAC THEN EXISTS_TAC (--`d:num`--) THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[], ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[WHEN_SIGNAL,ADD_ASSOC]], (* ---- Proving --------------------------------------------------- *) (* (!t1. ?t2. (a WHEN b) (t1 + t2) ==> b (t1 + t2)) ==> *) (* (!n. (a WHEN b) n = (a SWHEN b) n) *) (* ---------------------------------------------------------------- *) UNDISCH_HD_TAC THEN POP_ASSUM REWRITE1_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[TAC_PROOF(([],--`(a:bool=b) = (b=a)`--),PROP_TAC)] THEN MY_MP_TAC (--` (!n. EVENTUAL b n) ==> !n. (a WHEN b) n = (a SWHEN b) n`--) THENL[ DISCH_TAC THEN GEN_TAC THEN MATCH_MP_TAC (snd(EQ_IMP_RULE(SYM(hd(CONJUNCTS SOME_EVENT))))) THEN ASM_REWRITE_TAC[], DISCH_TAC] THEN POP_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN LEFT_FORALL_TAC (--`n:num`--) THEN DISJ_CASES_TAC (SPEC(--`n:num`--)(GEN(--`t0:num`--)DELTA_CASES)) THENL[ LEFT_EXISTS_TAC THEN REWRITE_TAC[EVENTUAL] THEN EXISTS_TAC(--`d:num`--) THEN ASM_REWRITE_TAC[], UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[SWHEN_SIGNAL] THEN ONCE_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`t+(n+t2) = (t+t2)+n`--))] THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[] ] ]); val SWHEN2BUECHI_THM = TAC_PROOF( ([],--`(l = (a SWHEN b)) = (!t. l t = (b t => a t | l(t+1))) /\ (!t1.?t2. l(t1+t2) ==> b(t1+t2))`--), REWRITE_TAC[BETA_RULE(CONV_RULE (DEPTH_CONV FUN_EQ_CONV) WHEN_FIX)] THEN CONV_TAC(DEPTH_CONV FUN_EQ_CONV) THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL[ (* ---- Proving !t1. ?t2. (a SWHEN b) (t1 + t2) ==> b (t1 + t2) ---- *) POP_NO_TAC 0 THEN GEN_TAC THEN DISJ_CASES_TAC (SPEC(--`t1:num`--)(GEN(--`t0:num`--)DELTA_CASES)) THENL[ LEFT_EXISTS_TAC THEN EXISTS_TAC (--`d:num`--) THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[], ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[SWHEN_SIGNAL,ADD_ASSOC]], (* ---- Proving --------------------------------------------------- *) (* (!t1. ?t2. (a WHEN b) (t1 + t2) ==> b (t1 + t2)) ==> *) (* (!n. (a WHEN b) n = (a SWHEN b) n) *) (* ---------------------------------------------------------------- *) UNDISCH_HD_TAC THEN POP_ASSUM REWRITE1_TAC THEN DISCH_TAC THEN MY_MP_TAC (--` (!n. EVENTUAL b n) ==> !n. (a WHEN b) n = (a SWHEN b) n`--) THENL[ DISCH_TAC THEN GEN_TAC THEN MATCH_MP_TAC (snd(EQ_IMP_RULE(SYM(hd(CONJUNCTS SOME_EVENT))))) THEN ASM_REWRITE_TAC[], DISCH_TAC] THEN POP_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN LEFT_FORALL_TAC (--`n:num`--) THEN DISJ_CASES_TAC (SPEC(--`n:num`--)(GEN(--`t0:num`--)DELTA_CASES)) THENL[ LEFT_EXISTS_TAC THEN REWRITE_TAC[EVENTUAL] THEN EXISTS_TAC(--`d:num`--) THEN ASM_REWRITE_TAC[], UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[WHEN_SIGNAL] THEN ONCE_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`delta+(n+t2) = (delta+t2)+n`--))] THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[] ] ]); val UNTIL2BUECHI_THM = TAC_PROOF( ([],--`(l = (a UNTIL b)) = (!t. l t = ~b t ==> a t /\ l(t+1)) /\ (!t1.?t2. ~l(t1+t2) ==> ~a(t1+t2) \/ b(t1+t2))`--), REWRITE_TAC[UNTIL_AS_WHEN,WHEN2BUECHI_THM] THEN BETA_TAC THEN REWRITE_TAC[TAC_PROOF (([],--`((a ==> b) => b | l) = (~b ==> a /\ l)`--),PROP_TAC)] THEN REWRITE_TAC[TAC_PROOF (([],--`(l \/(a==>b)) = (~l ==> (~a\/b))`--),PROP_TAC)]); val SUNTIL2BUECHI_THM = TAC_PROOF( ([],--`(l = (a SUNTIL b)) = (!t. l t = ~b t ==> a t /\ l(t+1)) /\ (!t1.?t2. l(t1+t2) ==> ~a(t1+t2) \/ b(t1+t2))`--), REWRITE_TAC[SUNTIL_AS_SWHEN,SWHEN2BUECHI_THM] THEN BETA_TAC THEN REWRITE_TAC[TAC_PROOF (([],--`((a ==> b) => b | l) = (~b ==> a /\ l)`--),PROP_TAC)] THEN REWRITE_TAC[TAC_PROOF (([],--`(l ==> a==>b) = (l ==> ~a \/ b)`--),PROP_TAC)]); val BEFORE2BUECHI_THM = TAC_PROOF( ([],--`(l = (a BEFORE b)) = (!t. l t = ~b t /\ (a t \/ l(t+1))) /\ (!t1.?t2. ~l(t1+t2) ==> a(t1+t2) \/ b(t1+t2))`--), REWRITE_TAC[BEFORE_AS_SUNTIL] THEN REWRITE_TAC[TAC_PROOF (([],--`(l = ~b/\(a\/l1)) = (~l = ~b ==>~a/\~l1)`--),PROP_TAC)] THEN ONCE_REWRITE_TAC[TAC_PROOF (([],--`(~l ==> a \/b) = (~l ==> ~~a \/ b)`--),PROP_TAC)] THEN REWRITE1_TAC(SYM(BETA_RULE (SPEC(--`\t:num.~l t`--)(GEN(--`l:num->bool`--) (SPEC(--`\t:num.~a t`--)(GEN(--`a:num->bool`--) SUNTIL2BUECHI_THM)))) )) THEN CONV_TAC(DEPTH_CONV FUN_EQ_CONV) THEN BETA_TAC THEN ONCE_REWRITE_TAC[TAC_PROOF (([],--`(a = ~b) = (~a = b)`--),PROP_TAC)] THEN REWRITE_TAC[]); val SBEFORE2BUECHI_THM = TAC_PROOF( ([],--`(l = (a SBEFORE b)) = (!t. l t = ~b t /\ (a t \/ l(t+1))) /\ (!t1.?t2. l(t1+t2) ==> a(t1+t2) \/ b(t1+t2))`--), REWRITE_TAC[SBEFORE_AS_UNTIL] THEN REWRITE_TAC[TAC_PROOF (([],--`(l = ~b/\(a\/l1)) = (~l = ~b ==>~a/\~l1)`--),PROP_TAC)] THEN REWRITE1_TAC(SYM(REWRITE_RULE[](BETA_RULE (SPEC(--`\t:num.~l t`--)(GEN(--`l:num->bool`--) (SPEC(--`\t:num.~a t`--)(GEN(--`a:num->bool`--) UNTIL2BUECHI_THM)))) ))) THEN CONV_TAC(DEPTH_CONV FUN_EQ_CONV) THEN BETA_TAC THEN ONCE_REWRITE_TAC[TAC_PROOF (([],--`(a = ~b) = (~a = b)`--),PROP_TAC)] THEN REWRITE_TAC[]); val ALWAYS2BUECHI_THM = TAC_PROOF( ([],--`(l = (ALWAYS a)) = (!t. l t = a t /\ l(t+1)) /\ (!t1.?t2. a(t1+t2) ==> l(t1+t2))`--), REWRITE_TAC[ALWAYS_AS_UNTIL,UNTIL2BUECHI_THM] THEN BETA_TAC THEN REWRITE_TAC[TAC_PROOF (([],--`(~a ==> ~l) =( l ==> a)`--),PROP_TAC)]); val EVENTUAL2BUECHI_THM = TAC_PROOF( ([],--`(l = (EVENTUAL a)) = (!t. l t = a t \/ l(t+1)) /\ (!t1.?t2. l(t1+t2) ==> a(t1+t2))`--), REWRITE_TAC[EVENTUAL_AS_SUNTIL,SUNTIL2BUECHI_THM] THEN BETA_TAC THEN REWRITE_TAC[TAC_PROOF (([],--`(~a ==> l) = (a \/ l)`--),PROP_TAC)]); val PSNEXT_PEVENTUAL2OMEGA = TAC_PROOF( ([],--` (l = PSNEXT(PEVENTUAL a)) = (l 0 = F) /\ (!t. l(SUC t) = a t \/ l t) `--), EQ_TAC THEN STRIP_TAC THENL[ ASM_REWRITE_TAC[PSNEXT,LESS_REFL] THEN INDUCT_TAC THEN REWRITE_TAC[PRE,LESS_REFL,LESS_0,INITIALISATION] THEN CONV_TAC(LHS_CONV(ONCE_REWRITE_CONV[RECURSION])) THEN BETA_TAC THEN REWRITE_TAC[PSNEXT,ZERO_LEMMA,PRE], CONV_TAC FUN_EQ_CONV THEN INDUCT_TAC THEN ASM_REWRITE_TAC[PSNEXT,PRE,LESS_0,LESS_REFL] THEN DISJ_CASES_TAC(EQT_ELIM(ARITH_CONV(--`(n=0)\/(0 l(t1+t2)) ) /\ ((l = (EVENTUAL a)) = T /\ (!t. l t = a t \/ l(SUC t)) /\ (!t1.?t2. l(t1+t2) ==> a(t1+t2)) ) /\ ((l = (a SUNTIL b)) = T /\ (!t. l t = ~b t ==> a t /\ l(SUC t)) /\ (!t1.?t2. l(t1+t2) ==> ~a(t1+t2) \/ b(t1+t2)) ) /\ ((l = (a SWHEN b)) = T /\ (!t. l t = (b t => a t | l(SUC t))) /\ (!t1.?t2. l(t1+t2) ==> b(t1+t2)) ) /\ ((l = (a SBEFORE b)) = T /\ (!t. l t = ~b t /\ (a t \/ l(SUC t))) /\ (!t1.?t2. l(t1+t2) ==> a(t1+t2) \/ b(t1+t2)) ) /\ ((l = (a UNTIL b)) = T /\ (!t. l t = ~b t ==> a t /\ l(SUC t)) /\ (!t1.?t2. ~l(t1+t2) ==> ~a(t1+t2) \/ b(t1+t2)) ) /\ ((l = (a WHEN b)) = T /\ (!t. l t = (b t => a t | l(SUC t))) /\ (!t1.?t2. l(t1+t2) \/ b(t1+t2)) ) /\ ((l = (a BEFORE b)) = T /\ (!t. l t = ~b t /\ (a t \/ l(SUC t))) /\ (!t1.?t2. ~l(t1+t2) ==> a(t1+t2) \/ b(t1+t2)) ) /\ ((l = PNEXT a) = (l 0 = T) /\ (!t. l(SUC t) = a t) /\ T ) /\ ((l = PSNEXT a) = (l 0 = F) /\ (!t. l(SUC t) = a t) /\ T ) /\ ((l = PNEXT(PALWAYS a)) = (l 0 = T) /\ (!t. l(SUC t) = a t /\ l t) /\ T ) /\ ((l = PSNEXT(PEVENTUAL a)) = (l 0 = F) /\ (!t. l(SUC t) = a t \/ l t) /\ T ) /\ ((l = PSNEXT(a PSUNTIL b)) = (l 0 = F) /\ (!t. l(SUC t) = b t \/ a t /\ l t) /\ T ) /\ ((l = PSNEXT(a PSWHEN b)) = (l 0 = F) /\ (!t. l(SUC t) = a t /\ b t \/ ~b t /\ l t) /\ T ) /\ ((l = PSNEXT(a PSBEFORE b)) = (l 0 = F) /\ (!t. l(SUC t) = ~b t /\ (a t \/ l t)) /\ T ) /\ ((l = PNEXT(a PUNTIL b)) = (l 0 = T) /\ (!t. l(SUC t) = b t \/ a t /\ l t) /\ T ) /\ ((l = PNEXT(a PWHEN b)) = (l 0 = T) /\ (!t. l(SUC t) = a t /\ b t \/ ~b t /\ l t) /\ T ) /\ ((l = PNEXT(a PBEFORE b)) = (l 0 = T) /\ (!t. l(SUC t) = ~b t /\ (a t \/ l t)) /\ T ) `--), REWRITE_TAC[ PSNEXT_PEVENTUAL2OMEGA,PSNEXT_PALWAYS2OMEGA, PSNEXT_PSUNTIL2OMEGA,PSNEXT_PUNTIL2OMEGA, PSNEXT_PSWHEN2OMEGA,PSNEXT_PWHEN2OMEGA, PSNEXT_PSBEFORE2OMEGA,PSNEXT_PBEFORE2OMEGA ] THEN REWRITE_TAC[ ADD1, ALWAYS2BUECHI_THM,EVENTUAL2BUECHI_THM, SUNTIL2BUECHI_THM,UNTIL2BUECHI_THM, WHEN2BUECHI_THM,SWHEN2BUECHI_THM, SBEFORE2BUECHI_THM,BEFORE2BUECHI_THM ] THEN CONV_TAC(DEPTH_CONV FUN_EQ_CONV) THEN REWRITE_TAC[NEXT] THEN BETA_TAC THEN REWRITE_TAC[ADD1] THEN CONJ_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL[ ASM_REWRITE_TAC[INITIALISATION], ASM_REWRITE_TAC[PNEXT,SYM(SPEC_ALL ADD1),PRE,ZERO_LEMMA], SPEC_TAC((--`n:num`--),(--`n:num`--)) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[INITIALISATION,ADD1] THEN REWRITE_TAC[PNEXT,SYM(SPEC_ALL ADD1),PRE,ZERO_LEMMA], UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[INITIALISATION], ASM_REWRITE_TAC[PSNEXT,SYM(SPEC_ALL ADD1),PRE,ZERO_LEMMA], SPEC_TAC((--`n:num`--),(--`n:num`--)) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[INITIALISATION,ADD1] THEN REWRITE_TAC[PSNEXT,SYM(SPEC_ALL ADD1),PRE,ZERO_LEMMA] ] ); (*--------------------------------------------------------------------------- Closure theorems, leading to a translation theorem. ---------------------------------------------------------------------------*) val AUTOMATON_AUTOMATON_CLOSURE = TAC_PROOF( ([],--` (?q1:num->'a. Phi_I1(q1) /\ Phi_R1(q1) /\ ?q2:num->'b. Phi_I2(q2) /\ Phi_R2(q2,q1) /\ Phi_F(q1,q2) ) = ?q1:num->'a. ?q2:num->'b. (Phi_I1(q1) /\ Phi_I2(q2)) /\ (Phi_R1(q1) /\ Phi_R2(q2,q1)) /\ Phi_F(q1,q2) `--), EQ_TAC THEN REPEAT STRIP_TAC THENL[ EXISTS_TAC(--`q1:num->'a`--) THEN EXISTS_TAC(--`q2:num->'b`--) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`q1:num->'a`--) THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC(--`q2:num->'b`--) THEN ASM_REWRITE_TAC[] ]); val AUTOMATON_NEXT_CLOSURE = TAC_PROOF( ([],--` Phi(NEXT phi) = ? q0 q1. (!t. (q0(t) = phi(t)) /\ (q1(t) = q0(t+1))) /\ Phi(q1) `--), EQ_TAC THEN REPEAT STRIP_TAC THENL[ EXISTS_TAC (--`phi:num->bool`--) THEN EXISTS_TAC(--`NEXT phi`--) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[NEXT,num_CONV(--`1`--),ADD_CLAUSES] THEN BETA_TAC THEN REWRITE_TAC[], MY_MP_TAC (--`NEXT phi = q1`--) THENL[ CONV_TAC FUN_EQ_CONV THEN ASM_REWRITE_TAC[NEXT,num_CONV(--`1`--),ADD_CLAUSES] THEN BETA_TAC THEN REWRITE_TAC[], DISCH_TAC] THEN ASM_REWRITE_TAC[] ]); val AUTOMATON_PNEXT_CLOSURE = TAC_PROOF( ([],--` Phi(PNEXT phi) = ?q. q(0) /\ (!t. q(t+1) = phi(t)) /\ Phi(q) `--), EQ_TAC THEN REPEAT STRIP_TAC THENL[ EXISTS_TAC(--`PNEXT phi`--) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[SYM(SPEC_ALL ADD1),PNEXT,PRE] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(SUC t = 0)`--))], MY_MP_TAC (--`PNEXT phi = q`--) THENL[ CONV_TAC FUN_EQ_CONV THEN INDUCT_TAC THEN ASM_REWRITE_TAC[PNEXT,PRE,ADD1] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(t+1 = 0)`--))], DISCH_TAC] THEN ASM_REWRITE_TAC[] ]); val AUTOMATON_PSNEXT_CLOSURE = TAC_PROOF( ([],--` Phi(PSNEXT phi) = ?q. ~q(0) /\ (!t. q(t+1) = phi(t)) /\ Phi(q) `--), EQ_TAC THEN REPEAT STRIP_TAC THENL[ EXISTS_TAC(--`PSNEXT phi`--) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[SYM(SPEC_ALL ADD1),PSNEXT,PRE] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(0<0)`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`(0'a. Phi_I1(q1) /\ Phi_R1(q1) /\ ?q2:num->'b. Phi_I2(q2) /\ Phi_R2(q2,q1) /\ Phi_F(q1,q2) ) = ?q1:num->'a. ?q2:num->'b. (Phi_I1(q1) /\ Phi_I2(q2)) /\ (Phi_R1(q1) /\ Phi_R2(q2,q1)) /\ Phi_F(q1,q2) ) /\ (Phi(NEXT phi) = ? q0 q1. T /\ (!t. (q0(t) = phi(t)) /\ (q1(t) = q0(t+1))) /\ Phi(q1) ) /\ (Phi(PNEXT phi) = ?q. q(0) /\ (!t. q(t+1) = phi(t)) /\ Phi(q) ) /\ (Phi(PSNEXT phi) = ?q. ~q(0) /\ (!t. q(t+1) = phi(t)) /\ Phi(q) ) /\ (Phi(PNEXT(PALWAYS a)) = ?q. q(0) /\ (!t. q(t+1) = a t /\ q t) /\ Phi(q) ) /\ (Phi(PSNEXT(PEVENTUAL a)) = ?q. ~q(0) /\ (!t. q(t+1) = a t \/ q t) /\ Phi(q) ) /\ (Phi(PSNEXT(a PSUNTIL b)) = ?q. ~q(0) /\ (!t. q(t+1) = b t \/ a t /\ q t) /\ Phi(q) ) /\ (Phi(PSNEXT(a PSWHEN b)) = ?q. ~q(0) /\ (!t. q(t+1) = a t /\ b t \/ ~b t /\ q t) /\ Phi(q) ) /\ (Phi(PSNEXT(a PSBEFORE b)) = ?q. ~q(0) /\ (!t. q(t+1) = ~b t /\(a t \/ q t)) /\ Phi(q) ) /\ (Phi(PNEXT(a PUNTIL b)) = ?q. q(0) /\ (!t. q(t+1) = b t \/ a t /\ q t) /\ Phi(q) ) /\ (Phi(PNEXT(a PWHEN b)) = ?q. q(0) /\ (!t. q(t+1) = a t /\ b t \/ ~b t /\ q t) /\ Phi(q) ) /\ (Phi(PNEXT(a PBEFORE b)) = ?q. q(0) /\ (!t. q(t+1) = ~b t /\ (a t \/ q t)) /\ Phi(q) ) `--), REPEAT CONJ_TAC THENL[ REWRITE_TAC[AUTOMATON_AUTOMATON_CLOSURE], REWRITE_TAC[AUTOMATON_NEXT_CLOSURE], REWRITE_TAC[AUTOMATON_PNEXT_CLOSURE], REWRITE_TAC[AUTOMATON_PSNEXT_CLOSURE], REWRITE_TAC[AUTOMATON_PALWAYS_CLOSURE], REWRITE_TAC[AUTOMATON_PEVENTUAL_CLOSURE], REWRITE_TAC[AUTOMATON_PSUNTIL_CLOSURE], REWRITE_TAC[AUTOMATON_PSWHEN_CLOSURE], REWRITE_TAC[AUTOMATON_PSBEFORE_CLOSURE], REWRITE_TAC[AUTOMATON_PUNTIL_CLOSURE], REWRITE_TAC[AUTOMATON_PWHEN_CLOSURE], REWRITE_TAC[AUTOMATON_PBEFORE_CLOSURE] ]); val BUECHI_TRANSLATION = TAC_PROOF( ([],--` (Phi(NEXT phi) = ? q0 q1. T /\ (!t. (q0(t) = phi(t)) /\ (q1(t) = q0(t+1))) /\ Phi(q1) ) /\ (Phi(ALWAYS a) = ?q. T /\ (!t. q t = a t /\ q(t+1)) /\ ( (!t1.?t2. a(t1+t2) ==> q(t1+t2)) /\ Phi(q) ) ) /\ (Phi(EVENTUAL a) = ?q. T /\ (!t. q t = a t \/ q(t+1)) /\ ( (!t1.?t2. q(t1+t2) ==> a(t1+t2)) /\ Phi(q) ) ) /\ (Phi(a SUNTIL b) = ?q. T /\ (!t. q t = b t \/ a t /\ q(t+1)) /\ ( (!t1.?t2. q(t1+t2) ==> ~a(t1+t2) \/ b(t1+t2)) /\ Phi(q) ) ) /\ (Phi(a UNTIL b) = ?q. T /\ (!t. q t = b t \/ a t /\ q(t+1)) /\ ( (!t1.?t2. ~q(t1+t2) ==> ~a(t1+t2) \/ b(t1+t2)) /\ Phi(q) ) ) /\ (Phi(a SWHEN b) = ?q. T /\ (!t. q t = (b t => a t | q(t+1))) /\ ( (!t1.?t2. q(t1+t2) ==> b(t1+t2)) /\ Phi(q) ) ) /\ (Phi(a WHEN b) = ?q. T /\ (!t. q t = (b t => a t | q(t+1))) /\ ( (!t1.?t2. q(t1+t2) \/ b(t1+t2)) /\ Phi(q) ) ) /\ (Phi(a SBEFORE b) = ?q. T /\ (!t. q t = ~b t /\ (a t \/ q(t+1))) /\ ( (!t1.?t2. q(t1+t2) ==> a(t1+t2) \/ b(t1+t2)) /\ Phi(q) ) ) /\ (Phi(a BEFORE b) = ?q. T /\ (!t. q t = ~b t /\ (a t \/ q(t+1))) /\ ( (!t1.?t2. ~q(t1+t2) ==> a(t1+t2) \/ b(t1+t2)) /\ Phi(q) ) ) `--), REWRITE_TAC[AUTOMATON_NEXT_CLOSURE] THEN REWRITE_TAC[TAC_PROOF(([],--`a/\(b/\c) = (a/\b)/\c`--),PROP_TAC)] THEN REWRITE_TAC[TAC_PROOF(([],--`b\/a/\q = ~b==>a/\q`--),PROP_TAC)] THEN REWRITE_TAC(map SYM (CONJUNCTS (REWRITE_RULE[ADD1]TEMP_OPS_DEFS_TO_OMEGA))) THEN REPEAT CONJ_TAC THEN EQ_TAC THEN STRIP_TAC THENL[ EXISTS_TAC(--`ALWAYS a`--) THEN ASM_REWRITE_TAC[], POP_NO_ASSUM 1 (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`EVENTUAL a`--) THEN ASM_REWRITE_TAC[], POP_NO_ASSUM 1 (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`a SUNTIL b`--) THEN ASM_REWRITE_TAC[], POP_NO_ASSUM 1 (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`a UNTIL b`--) THEN ASM_REWRITE_TAC[], POP_NO_ASSUM 1 (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`a SWHEN b`--) THEN ASM_REWRITE_TAC[], POP_NO_ASSUM 1 (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`a WHEN b`--) THEN ASM_REWRITE_TAC[], POP_NO_ASSUM 1 (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`a SBEFORE b`--) THEN ASM_REWRITE_TAC[], POP_NO_ASSUM 1 (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`a BEFORE b`--) THEN ASM_REWRITE_TAC[], POP_NO_ASSUM 1 (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[] ]); (*--------------------------------------------------------------------------- Co-Buechi closure theorems. ---------------------------------------------------------------------------*) (* ========================== CO_BUECHI_CONJ_CLOSURE ================================== *) (* *) (* Co-Buechi automata are closed under conjunction. The conjunction is computed as: *) (* *) (* |- (?q1. *) (* Phi_I1(q1 t0) /\ *) (* (!t. Phi_R1(i(t+t0),q1(t+t0))) /\ *) (* (?t1. !t2. Psi1(i(t1+t2+t0),q1(t1+t2+t0))) *) (* ) *) (* /\ *) (* (?q2. *) (* Phi_I2(q2 t0) /\ *) (* (!t. Phi_R2(i(t+t0),q2(t+t0))) /\ *) (* (?t1. !t2. Psi2(i(t1+t2+t0),q2(t1+t2+t0))) *) (* ) *) (* = *) (* (?q1 q2. *) (* (Phi_I1(q1 t0) /\ Phi_I2(q2 t0)) /\ *) (* (!t.Phi_R1(i(t+t0),q1(t+t0)) /\ Phi_R2(i(t+t0),q2(t+t0))) /\ *) (* (?t1. !t2. Psi1(i(t1+t2+t0),q1(t1+t2+t0)) /\ Psi2(i(t1+t2+t0),q2(t1+t2+t0))) *) (* ) *) (* *) (* ==================================================================================== *) val CO_BUECHI_CONJ_CLOSURE = TAC_PROOF( let val cb1 = (--`?q1. Phi_I1(q1 t0) /\ (!t. Phi_R1((i(t+t0):'a),(q1(t+t0):'b1))) /\ (?t1. !t2. Psi1(i(t1+(t2+t0)),q1(t1+(t2+t0))))`--) val cb2 = (--`?q2. Phi_I2(q2 t0) /\ (!t. Phi_R2((i(t+t0):'a),(q2(t+t0):'b2))) /\ (?t1. !t2. Psi2(i(t1+(t2+t0)),q2(t1+(t2+t0))))`--) in ([],--`(^cb1 /\ ^cb2) = ? q1 q2. (Phi_I1(q1 t0) /\ Phi_I2(q2 t0)) /\ (!t. Phi_R1((i(t+t0):'a),(q1(t+t0):'b1)) /\ Phi_R2((i(t+t0):'a),(q2(t+t0):'b2)) ) /\ ?t1. !t2. Psi1(i(t1+(t2+t0)),q1(t1+(t2+t0))) /\ Psi2(i(t1+(t2+t0)),q2(t1+(t2+t0))) `--) end, REWRITE_TAC[ REWRITE_RULE[SYM(SPEC_ALL ADD_ASSOC)] (SYM(BETA_RULE (SPECL[(--`\t:num. Psi1(((i t):'a),((q1 t):'b1)):bool`--), (--`\t:num. Psi2(((i t):'a),((q2 t):'b2)):bool`--) ] CONJ_FG )))] THEN EQ_TAC THEN REPEAT STRIP_TAC THENL[ EXISTS_TAC(--`q1:num->'b1`--) THEN EXISTS_TAC(--`q2:num->'b2`--), EXISTS_TAC(--`q1:num->'b1`--), EXISTS_TAC(--`q2:num->'b2`--) ] THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THENL[ EXISTS_TAC(--`t1:num`--) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`t1':num`--) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`t1:num`--) THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`t1':num`--) THEN ASM_REWRITE_TAC[] ]) ; (* ========================== CO_BUECHI_DISJ_CLOSURE ================================== *) (* *) (* Co-Buechi automata are closed under disjunction. The disjunction is computed as: *) (* *) (* |- (?q1. *) (* Phi_I1(q1 t0) /\ *) (* (!t. Phi_R1(i(t+t0),q1(t+t0))) /\ *) (* (?t1. !t2. Psi1(i(t1+t2+t0),q1(t1+t2+t0))) *) (* ) *) (* \/ *) (* (?q2. *) (* Phi_I2(q2 t0) /\ *) (* (!t. Phi_R2(i(t+t0),q2(t+t0))) /\ *) (* (?t1. !t2. Psi2(i(t1+t2+t0),q2(t1+t2+t0))) *) (* ) *) (* = *) (* (?p q1 q2. *) (* (~p(t0) /\ Phi_I1(q1 t0) \/ *) (* p(t0) /\ Phi_I2(q2 t0) *) (* ) /\ *) (* (!t. ~p(t+t0) /\ Phi_R1((i(t+t0):'a),(q1(t+t0):'b1)) /\ ~p(t+t0+1) \/ *) (* p(t+t0) /\ Phi_R2((i(t+t0):'a),(q2(t+t0):'b2)) /\ p(t+t0+1) *) (* ) /\ *) (* ?t1. !t2. ~p(t+t0) /\ Psi1(i(t1+t2+t0),q1(t1+t2+t0)) \/ *) (* p(t+t0) /\ Psi2(i(t1+t2+t0),q2(t1+t2+t0)) *) (* ) *) (* *) (* ==================================================================================== *) val CO_BUECHI_DISJ_CLOSURE = TAC_PROOF( let val cb1 = (--`?q1. Phi_I1(q1 t0) /\ (!t. Phi_R1((i(t+t0):'a),(q1(t+t0):'b1))) /\ (?t1. !t2. Psi1(i(t1+(t2+t0)),q1(t1+(t2+t0))))`--) val cb2 = (--`?q2. Phi_I2(q2 t0) /\ (!t. Phi_R2((i(t+t0):'a),(q2(t+t0):'b2))) /\ (?t1. !t2. Psi2(i(t1+(t2+t0)),q2(t1+(t2+t0))))`--) in ([],--`(^cb1 \/ ^cb2) = ?p q1 q2. (~p(t0) /\ Phi_I1(q1 t0) \/ p(t0) /\ Phi_I2(q2 t0) ) /\ (!t. ~p(t+t0) /\ Phi_R1((i(t+t0):'a),(q1(t+t0):'b1)) /\ ~p(t+(t0+1)) \/ p(t+t0) /\ Phi_R2((i(t+t0):'a),(q2(t+t0):'b2)) /\ p(t+(t0+1)) ) /\ ?t1. !t2. ~p(t+t0) /\ Psi1(i(t1+(t2+t0)),q1(t1+(t2+t0))) \/ p(t+t0) /\ Psi2(i(t1+(t2+t0)),q2(t1+(t2+t0))) `--) end, EQ_TAC THEN REPEAT STRIP_TAC THENL[ EXISTS_TAC (--`\t:num.F`--) THEN EXISTS_TAC (--`q1:num->'b1`--) THEN EXISTS_TAC (--`q2:num->'b2`--) THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC (--`t1:num`--) THEN ASM_REWRITE_TAC[], EXISTS_TAC (--`\t:num.T`--) THEN EXISTS_TAC (--`q1:num->'b1`--) THEN EXISTS_TAC (--`q2:num->'b2`--) THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC (--`t1:num`--) THEN ASM_REWRITE_TAC[], MY_MP_TAC (--`!t. ~p(t+t0)`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 2 (--`t':num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD1)] THEN STRIP_TAC, DISCH_TAC ] THEN DISJ1_TAC THEN EXISTS_TAC(--`q1:num->'b1`--) THEN POP_ASSUM (fn x => RULE_ASSUM_TAC(REWRITE_RULE[x]) THEN ASSUME_TAC x) THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC (--`t1:num`--) THEN ASM_REWRITE_TAC[], MY_MP_TAC (--`!t. p(t+t0)`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 2 (--`t':num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD1)] THEN STRIP_TAC, DISCH_TAC ] THEN DISJ2_TAC THEN EXISTS_TAC(--`q2:num->'b2`--) THEN POP_ASSUM (fn x => RULE_ASSUM_TAC(REWRITE_RULE[x]) THEN ASSUME_TAC x) THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC (--`t1:num`--) THEN ASM_REWRITE_TAC[] ]) ; (* ========================== CO_BUECHI_NEXT_CLOSURE ================================== *) (* *) (* The next theorem shows that co-Buechi automata are closed under an appliation of a *) (* NEXT operator. *) (* *) (* |- (NEXT *) (* (\t0. *) (* ?q. *) (* Phi_I (q t0) /\ *) (* (!t. Phi_R (i (t+t0),q (t+t0))) /\ *) (* (?t1. !t2. Psi (i (t1+t2+t0),q (t1+t2+t0))))) *) (* t0 = *) (* (?p q. *) (* ((p t0 = F) /\ (q t0 = c)) /\ *) (* (!t. *) (* (~p(t+t0) /\ (q(t+t0) = c) /\ p(t+t0+1) /\ Phi_I(q(t+t0+1))) *) (* \/ ( p(t+t0) /\ Phi_R((i(t+t0):'a),(q(t+t0):'b)) /\ p(t+t0+1)) *) (* ) /\ *) (* ?t1. !t2. Psi(i(t1+t2+t0),q(t1+t2+t0)) *) (* *) (* ==================================================================================== *) val NEXT2 = prove(``NEXT P x = P (SUC x)``, REWRITE_TAC [NEXT] THEN BETA_TAC THEN REWRITE_TAC []); val CO_BUECHI_NEXT_CLOSURE = TAC_PROOF( let val cb = (--`?q. Phi_I(q t0) /\ (!t. Phi_R((i(t+t0):'a),(q(t+t0):'b))) /\ (?t1. !t2. Psi(i(t1+(t2+t0)),q(t1+(t2+t0))))`--) in ([],--`(NEXT (\t0:num. ^cb)) t0 = ?p q. ((p t0 = F) /\ (q t0 = c)) /\ (!t. (~p(t+t0) /\ (q(t+t0) = c) /\ p(t+(t0+1)) /\ Phi_I(q(t+(t0+1)))) \/ ( p(t+t0) /\ Phi_R((i(t+t0):'a),(q(t+t0):'b)) /\ p(t+(t0+1))) ) /\ ?t1. !t2. Psi(i(t1+(t2+t0)),q(t1+(t2+t0))) `--) end, PURE_REWRITE_TAC[NEXT2] THEN BETA_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL[ (* ---------------------------------------------------------------------------- *) (* first implication: from left to right *) (* ---------------------------------------------------------------------------- *) EXISTS_TAC(--`\t:num.t0(c:'b) | q t`--) THEN BETA_TAC THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(x'b`--) THEN MY_MP_TAC (--`!t. p(t+(t0+1))`--) THENL[ INDUCT_TAC THENL[ LEFT_NO_FORALL_TAC 1 (--`0`--) THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC, LEFT_NO_FORALL_TAC 2 (--`t+1`--) THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD1)] THEN STRIP_TAC ], DISCH_TAC ] THEN REPEAT STRIP_TAC THENL[ (* ---------------------------------------------------------------- *) (* correctness of initial states *) (* ---------------------------------------------------------------- *) LEFT_NO_FORALL_TAC 2 (--`0`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD1)], (* ---------------------------------------------------------------- *) (* correctness of transition relation *) (* ---------------------------------------------------------------- *) LEFT_NO_FORALL_TAC 2 (--`SUC t`--) THEN UNDISCH_HD_TAC THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD1)] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC, (* ---------------------------------------------------------------- *) (* correctness of acceptance condition *) (* ---------------------------------------------------------------- *) EXISTS_TAC (--`t1:num`--) THEN GEN_TAC THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`t1+(t2+(SUC t0)) = t1+(SUC t2+t0)`--))] ] ]) ; (* ========================== CO_BUECHI_SUNTIL_CLOSURE ================================ *) (* *) (* The next theorem shows that co-Buechi automata are closed under an appliation of a *) (* SUNTIL operator, provided that the left hand side argument is propositional. *) (* *) (* |- (phi SUNTIL *) (* (\t0. *) (* ?q. *) (* Phi_I (q t0) /\ *) (* (!t. Phi_R (i (t+t0),q (t+t0))) /\ *) (* (?t1. !t2. Psi (i (t1+t2+t0),q (t1+t2+t0))))) *) (* t0 = *) (* (?p q. *) (* ((p t0) => (Phi_I (q t0)) | (q t0 = c)) /\ *) (* (!t. *) (* ~p(t+t0) /\ (q(t+t0) = c) /\ phi(t+t0) /\ ~p(t+t0+1) /\ (q(t+t0+1) = c) \/ *) (* ~p(t+t0) /\ (q(t+t0) = c) /\ phi(t+t0) /\ p(t+t0+1) /\ Phi_I(q(t+t0+1)) \/ *) (* p(t+t0) /\ Phi_R(i(t+t0),q(t+t0)) /\ p(t+t0+1) *) (* ) /\ *) (* (?t1. !t2. p(t1+t2+t0) /\ Psi(i(t1+t2+t0),q(t1+t2+t0)))) *) (* *) (* ==================================================================================== *) val SUNTIL_WEAK_SIGNAL = TAC_PROOF( ([],--`(a SUNTIL b) t0 = ?delta. (!t. t a(t+t0)) /\ b(delta+t0)`--), REWRITE_TAC[SUNTIL_SIGNAL] THEN EQ_TAC THEN STRIP_TAC THENL[ EXISTS_TAC(--`delta:num`--) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN RES_TAC, ALL_TAC] THEN DISJ_CASES_TAC DELTA_CASES THENL[ALL_TAC,RES_TAC] THEN LEFT_EXISTS_TAC THEN MY_MP_TAC (--`d<=delta`--) THENL[ DISJ_CASES_TAC(SPECL[(--`delta:num`--),(--`d:num`--)]LESS_CASES) THEN ASM_REWRITE_TAC[] THEN RES_TAC, DISCH_TAC] THEN EXISTS_TAC(--`d:num`--) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN RES_TAC THEN POP_NO_ASSUM 5 (fn x => MATCH_MP_TAC x) THEN UNDISCH_NO_TAC 1 THEN UNDISCH_NO_TAC 1 THEN CONV_TAC ARITH_CONV ); val CO_BUECHI_SUNTIL_CLOSURE = TAC_PROOF( let val cb = (--`?q. Phi_I(q t0) /\ (!t. Phi_R((i(t+t0):'a),(q(t+t0):'b))) /\ (?t1. !t2. Psi(i(t1+(t2+t0)),q(t1+(t2+t0))))`--) in ([],--`(phi SUNTIL (\t0:num. ^cb)) t0 = ?p q. (p t0 => Phi_I(q t0) | (q t0 = c)) /\ (!t. ~p(t+t0) /\ (q(t+t0) = c) /\ phi(t+t0) /\ ~p(t+(t0+1)) /\ (q(t+(t0+1)) = c) \/ ~p(t+t0) /\ (q(t+t0) = c) /\ phi(t+t0) /\ p(t+(t0+1)) /\ Phi_I(q(t+(t0+1))) \/ p(t+t0) /\ Phi_R((i(t+t0):'a),(q(t+t0):'b)) /\ p(t+(t0+1)) ) /\ ?t1. !t2. p(t1+(t2+t0)) /\ Psi(i(t1+(t2+t0)),q(t1+(t2+t0))) `--) end, PURE_REWRITE_TAC[SUNTIL_WEAK_SIGNAL] THEN BETA_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL[ (* ---------------------------------------------------------------------------- *) (* first implication: from left to right *) (* ---------------------------------------------------------------------------- *) DISJ_CASES_TAC(SPEC(--`delta:num`--)num_CASES) THENL[ (* ------ 2nd subgoal: delta = 0 --------------- *) POP_ASSUM (fn x=> RULE_ASSUM_TAC(REWRITE_RULE[x])) THEN RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES]) THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC(--`\t:num.T`--) THEN EXISTS_TAC(--`q:num->'b`--) THEN BETA_TAC THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC (--`t1:num`--) THEN ASM_REWRITE_TAC[], (* ------ 2nd subgoal: delta > 0 --------------- *) LEFT_EXISTS_TAC THEN POP_ASSUM (fn x=> RULE_ASSUM_TAC(REWRITE_RULE[x])) THEN EXISTS_TAC(--`\t.t>n+t0`--) THEN EXISTS_TAC(--`\t.t<=n+t0 => (c:'b) | q t`--) THEN BETA_TAC THEN REPEAT STRIP_TAC THENL[ (* ------------ correct initialization ------------ *) REWRITE_TAC[ARITH_CONV(--`t0 <= n + t0`--)] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(t0 > n+t0)`--))], (* ------------ correct transitions --------------- *) DISJ_CASES_TAC(SPECL[(--`n:num`--),(--`t:num`--)]LESS_LESS_CASES) THENL[ALL_TAC,POP_ASSUM DISJ_CASES_TAC] THENL[ (* ------------ when the subautomaton starts -------- *) ASM_TAC 0 (fn x => REWRITE_TAC[(SYM x)]) THEN DISJ2_TAC THEN DISJ1_TAC THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(n+t0 > n+t0)`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`n+(t0+1)>n+t0`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(n+(t0+1) <= n+t0)`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`n+t0 <= n+t0`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`n+(t0+1) = (SUC n)+t0`--))] THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`(n = t) ==> t t+t0 > n+t0`--))) THEN POP_ASSUM (fn x => REWRITE_TAC[x]) THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`n < t ==> ~(t+t0 <= n+t0)`--))) THEN POP_ASSUM (fn x => REWRITE_TAC[x]) THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`n < t ==> t+(t0+1) > n+t0`--))) THEN POP_ASSUM (fn x => REWRITE_TAC[x]) THEN IMP_RES_TAC LESS_ADD_1 THEN POP_ASSUM (fn x => REWRITE_TAC[x]) THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`(n+(p+1))+t0 = p+(SUC n+t0)`--))] THEN ASM_REWRITE_TAC[], (* ----------- before the subautomaton started -------- *) DISJ1_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`t ~(t+t0 > n+t0)`--))) THEN POP_ASSUM (fn x => REWRITE_TAC[x]) THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`t (t+t0 <= n+t0)`--))) THEN POP_ASSUM (fn x => REWRITE_TAC[x]) THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`t ~(t+(t0+1) > n+t0)`--))) THEN POP_ASSUM (fn x => REWRITE_TAC[x]) THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`t (t+(t0+1) <= n+t0)`--))) THEN POP_ASSUM (fn x => REWRITE_TAC[x]) THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`t t < SUC n`--))) THEN RES_TAC ], (* ------------ correct acceptance ---------------- *) EXISTS_TAC(--`t1+SUC n`--) THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~((t1+SUC n)+(t_2+t0) <= n+t0)`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV (--`(t1+SUC n)+(t2+t0) = t1+(t2+(SUC n+t0))`--))] THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_CONV ] ], (* ---------------------------------------------------------------------------- *) (* second implication: from right to left *) (* ---------------------------------------------------------------------------- *) DISJ_CASES_TAC(SPEC(--`(p:num->bool) t0`--) BOOL_CASES_AX) THENL[ (* -------------------------------------------------------------------- *) (* 1st subgoal: p holds from the begining, i.e., the subautomaton runs *) (* from the begining and therefore, phi need never hold. *) (* -------------------------------------------------------------------- *) MY_MP_TAC (--`!t. p(t+t0)`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 3 (--`t:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`t+(t0+1)=SUC(t+t0)`--))] THEN STRIP_TAC, DISCH_TAC ] THEN POP_ASSUM (fn x => RULE_ASSUM_TAC(REWRITE_RULE[x]) THEN ASSUME_TAC x) THEN EXISTS_TAC (--`0`--) THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(t<0)`--))] THEN REWRITE_TAC[ADD_CLAUSES] THEN EXISTS_TAC(--`q:num->'b`--) THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL[ UNDISCH_NO_TAC 4 THEN LEFT_FORALL_TAC (--`0`--) THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN ASM_REWRITE_TAC[], EXISTS_TAC(--`t1:num`--) THEN ASM_REWRITE_TAC[] ], (* -------------------------------------------------------------------- *) (* 2nd subgoal: p is initially false, i.e., the subautomaton must be *) (* started later on and until then, phi must hold. *) (* -------------------------------------------------------------------- *) MY_MP_TAC (--`!t1. p(t1+t0) ==> !t. p(t+(t1+t0))`--) THENL[ GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 4 (--`t+t1'`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`(t+t1')+t0 = t+(t1'+t0)`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`t+(t1'+(t0+1))=SUC(t+(t1'+t0))`--))] THEN STRIP_TAC, DISCH_TAC ] THEN MY_MP_TAC (--`?t1. p(t1+t0)`--) THENL[ EXISTS_TAC(--`t1:num`--) THEN LEFT_NO_FORALL_TAC 2 (--`0`--) THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC, DISCH_TAC ] THEN ASSUME_TAC(BETA_RULE(SPEC(--`\t1.p(t1+t0):bool`--)WOP)) THEN UNDISCH_HD_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x]) THEN STRIP_TAC THEN EXISTS_TAC(--`n:num`--) THEN LEFT_NO_FORALL_TAC 2 (--`n:num`--) THEN UNDISCH_HD_TAC THEN POP_NO_ASSUM 1 (fn x => REWRITE_TAC[x]) THEN DISCH_TAC THEN CONJ_TAC (* -------------------------------------------------------------------- *) (* splits in two subgoals here: *) (* (--`!t. t < n ==> phi (t + t0) `--) *) (* (--`?q. *) (* Phi_I (q (n + t0)) /\ *) (* (!t. Phi_R (i (t + n + t0),q (t + n + t0))) /\ *) (* (?t1. !t2. Psi (i (t1 + t2 + n + t0), *) (* q (t1 + t2 + n + t0)))`--) *) (* *) (* -------------------------------------------------------------------- *) THENL[ INDUCT_TAC THENL[ DISCH_TAC THEN LEFT_NO_FORALL_TAC 5 (--`0`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC, DISCH_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`SUC t t'b`--) THEN REPEAT STRIP_TAC THENL[ (* ............................................................ *) (* first prove that Phi_I (q (n + t0)) holds *) (* ............................................................ *) MY_MP_TAC(--`?n'. n = SUC n'`--) THENL[ LEFT_FORALL_TAC(--`0`--) THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN DISJ_CASES_TAC(SPEC(--`n:num`--)num_CASES) THEN ASM_REWRITE_TAC[ADD_CLAUSES], STRIP_TAC ] THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`(n = SUC n') ==> n''b). *) (* (~p1 t0 /\ ~p2 t0 /\ (q t0 = c) \/ *) (* p1 t0 /\ ~p2 t0 /\ Phi_I(q t0) *) (* ) /\ *) (* (!t. *) (* ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) *) (* /\ ~p1(t+t0+1) /\ ~p2(t+t0+1) /\ (q(t+t0+1) = c) *) (* \/ ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) *) (* /\ p1(t+t0+1) /\ ~p2(t+t0+1) /\ Phi_I(q(t+t0+1)) *) (* \/ p1(t+t0) /\ ~p2(t+t0) /\ ~phi(t+t0) /\ Phi_I(q(t+t0)) *) (* /\ Phi_R((i(t+t0):'a),q(t+t0)) /\ p1(t+t0+1) /\ p2(t+t0+1) *) (* \/ p1(t+t0) /\ p2(t+t0) /\ Phi_R((i(t+t0):'a),q(t+t0)) *) (* /\ p1(t+t0+1) /\ p2(t+t0+1) *) (* ) /\ *) (* ?t1. !t2. ~p1(t1+t2+t0) \/ Psi(i(t1+t2+t0),q(t1+t2+t0)) *) (* *) (* *) (* ==================================================================================== *) val CO_BUECHI_BEFORE_CLOSURE = TAC_PROOF( let val cb = (--`?q. Phi_I(q t0) /\ (!t. Phi_R((i(t+t0):'a),(q(t+t0):'b))) /\ (?t1. !t2. Psi(i(t1+(t2+t0)),q(t1+(t2+t0))))`--) in ([],--`((\t0:num. ^cb) BEFORE phi) t0 = ?p1 p2 (q:num->'b). (~p1 t0 /\ ~p2 t0 /\ (q t0 = c) \/ p1 t0 /\ ~p2 t0 /\ Phi_I(q t0) ) /\ (!t. ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) /\ ~p1(t+(t0+1)) /\ ~p2(t+(t0+1)) /\ (q(t+(t0+1)) = c) \/ ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) /\ p1(t+(t0+1)) /\ ~p2(t+(t0+1)) /\ Phi_I(q(t+(t0+1))) \/ p1(t+t0) /\ ~p2(t+t0) /\ ~phi(t+t0) /\ Phi_I(q(t+t0)) /\ Phi_R((i(t+t0):'a),q(t+t0)) /\ p1(t+(t0+1)) /\ p2(t+(t0+1)) \/ p1(t+t0) /\ p2(t+t0) /\ Phi_R((i(t+t0):'a),q(t+t0)) /\ p1(t+(t0+1)) /\ p2(t+(t0+1)) ) /\ ?t1. !t2. ~p1(t1+(t2+t0)) \/ Psi(i(t1+(t2+t0)),q(t1+(t2+t0))) `--) end, PURE_REWRITE_TAC[BEFORE_SIGNAL] THEN BETA_TAC THEN EQ_TAC THENL[ (* ---------------------------------------------------------------------------- *) (* first implication: from left to right *) (* ---------------------------------------------------------------------------- *) REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SPEC(--`phi:num->bool`--)(GEN(--`b:num->bool`--)DELTA_CASES)) THENL[ (* ------------------------------------------------------------------------ *) (* phi holds at least once, so that the before operation really takes care *) (* ------------------------------------------------------------------------ *) LEFT_EXISTS_TAC THEN LEFT_NO_FORALL_TAC 1 (--`d:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN RES_TAC THEN EXISTS_TAC (--`\x:num. (x>=t+t0)`--) THEN EXISTS_TAC (--`\x:num. (x> t+t0)`--) THEN EXISTS_TAC (--`\x:num. (x c:'b | q(x)`--) THEN BETA_TAC THEN REWRITE_TAC[] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`t0>=t+t0 = ~(0t+t0)`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`t0=t+t0 = ~(t' t+t0 = (t=t+t0 = ~(t'+1 t+t0 = (t (t=0)`--))) THEN UNDISCH_NO_TAC 5 THEN ASM_REWRITE_TAC[ADD_CLAUSES], (* -------------------------------------------------------------------- *) (* correct transition relation *) (* -------------------------------------------------------------------- *) DISJ_CASES_TAC(EQT_ELIM(ARITH_CONV(--`(t' t' ~(t ~(t t'+1 (t'+(t0+1) = t+t0)`--))) THEN ASM_REWRITE_TAC[], (* ---------------------------------------------------------------- *) (* case t'=t, i.e. subautomaton starts at t+t0=t'+t0 *) (* ---------------------------------------------------------------- *) REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(t ~(t' ((t'-t)+(t+t0)=t'+t0)`--))) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN UNDISCH_NO_TAC 5 THEN CONV_TAC ARITH_CONV ], (* -------------------------------------------------------------------- *) (* correct acceptance condition *) (* -------------------------------------------------------------------- *) EXISTS_TAC(--`t+t1`--) THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~((t+t1)+(t2+t0) d = a ==> b ==> c ==>d`--),PROP_TAC)] THEN REPEAT DISCH_TAC THEN LEFT_EXISTS_TAC THEN REPEAT STRIP_TAC (* ---------------------------------------------------------------------------- *) THEN MY_MP_TAC(--`0 RULE_ASSUM_TAC(REWRITE_RULE[x,ADD_CLAUSES])) THEN LEFT_NO_FORALL_TAC 3 (--`0`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN UNDISCH_NO_TAC 3 THEN BOOL_CASES_TAC (--`(p2:num->bool) t0`--) THEN REWRITE_TAC[], DISCH_TAC ] (* ---------------------------------------------------------------------------- *) (* We now prove that the subautomaton must really be started because phi is *) (* true at delta+t0. Note that staying in the newly added initial state is only *) (* possible if phi is false. *) (* ---------------------------------------------------------------------------- *) THEN MY_MP_TAC(--`?x. p1(x+t0) /\ ~p2(x+t0) /\ ~phi(x+t0) /\ Phi_I(q(x+t0):'b) /\ (x ~p1(x+t0) /\ ~p2(x+t0) /\ (q(x+t0) = (c:'b))`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,ADD1] THEN DISCH_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`x+1 x p SUBST1_TAC(SYM x)) THEN STRIP_TAC THEN ASM_REWRITE_TAC[], DISCH_TAC ] (* ---------------------------------------------------------------------------- *) (* Having proved that we finally enter at some point of time x+t0 with x'b`--) THEN ASM_REWRITE_TAC[] (* ---------------------------------------------------------------------------- *) (* The following subgoals remain: *) (* the transition relation: !t'. Phi_R(i(t'+x+t0),q(t'+x+t0)) *) (* the acceptance condition: ?t1.!t2. Psi(i(t1+t2+x+t0),q(t1+t2+x+t0)) *) (* to prove them, some further lemmata are helpful: *) (* ---------------------------------------------------------------------------- *) (* ---------------------------------------------------------------------------- *) THEN MY_MP_TAC(--`!y. p1(y+(x+t0))`--) (* ---------------------------------------------------------------------------- *) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 6 (--`y+x`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC),ADD1] THEN STRIP_TAC, DISCH_TAC ] (* ---------------------------------------------------------------------------- *) THEN MY_MP_TAC(--`p2(x+(t0+1)):bool`--) (* ---------------------------------------------------------------------------- *) THENL[ LEFT_NO_FORALL_TAC 6 (--`x:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC),ADD1] THEN STRIP_TAC, DISCH_TAC ] (* ---------------------------------------------------------------------------- *) THEN MY_MP_TAC(--`!y. p2(y+(x+(t0+1)))`--) (* ---------------------------------------------------------------------------- *) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 8 (--`y+(x+1)`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC),ADD1] THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`y+(x+(1+t0)) = (y+1)+(x+t0)`--))] THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`(y+1)+(x+t0) = y+(x+(t0+1))`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`y+(x+((t0+1)+1)) = y+(x+(t0+(1+1)))`--))] THEN STRIP_TAC, DISCH_TAC ] THEN CONJ_TAC THENL[ (* ------------------------------------------------------------------------ *) (* the transition relation: !t'. Phi_R(i(t'+x+t0),q(t'+x+t0)) *) (* ------------------------------------------------------------------------ *) Q.X_GEN_TAC `tt` THEN LEFT_NO_FORALL_TAC 8 (--`tt+x`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)] THEN STRIP_TAC, (* ------------------------------------------------------------------------ *) (* the acceptance condition: ?t1.!t2. Psi(i(t1+t2+x+t0),q(t1+t2+x+t0)) *) (* ------------------------------------------------------------------------ *) EXISTS_TAC (--`t1:num`--) THEN GEN_TAC THEN LEFT_NO_FORALL_TAC 7 (--`t2+x`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`t1+((t2+x)+t0) = (t1+t2)+(x+t0)`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`(t1+t2)+(x+t0) = t1+(t2+(x+t0))`--))] ] ] ); (* ========================== CO_BUECHI_UNTIL_CLOSURE ================================= *) (* *) (* The next theorem shows that co-Buechi automata are closed under an appliation of a *) (* UNTIL operator, provided that the left hand side argument is propositional. *) (* *) (* |- (phi UNTIL *) (* (\t0. *) (* ?q. *) (* Phi_I (q t0) /\ *) (* (!t. Phi_R (i (t+t0),q (t+t0))) /\ *) (* (?t1. !t2. Psi (i (t1+t2+t0),q (t1+t2+t0))))) *) (* t0 = *) (* (?p q. *) (* ((p t0) => (Phi_I (q t0)) | (q t0 = c)) /\ *) (* (!t. *) (* ~p(t+t0) /\ (q(t+t0) = c) /\ phi(t+t0) /\ ~p(t+t0+1) /\ (q(t+t0+1) = c) \/ *) (* ~p(t+t0) /\ (q(t+t0) = c) /\ phi(t+t0) /\ p(t+t0+1) /\ Phi_I(q(t+t0+1)) \/ *) (* p(t+t0) /\ Phi_R(i(t+t0),q(t+t0)) /\ p(t+t0+1) *) (* ) /\ *) (* (?t1. !t2. ~p(t1+t2+t0) \/ Psi(i(t1+t2+t0),q(t1+t2+t0)))) *) (* *) (* ==================================================================================== *) val CO_BUECHI_UNTIL_CLOSURE = TAC_PROOF( let val cb = (--`?q. Phi_I(q t0) /\ (!t. Phi_R((i(t+t0):'a),(q(t+t0):'b))) /\ (?t1. !t2. Psi(i(t1+(t2+t0)),q(t1+(t2+t0))))`--) in ([],--`(phi UNTIL (\t0:num. ^cb)) t0 = ?p q. (p t0 => Phi_I(q t0) | (q t0 = c)) /\ (!t. ~p(t+t0) /\ (q(t+t0) = c) /\ phi(t+t0) /\ ~p(t+(t0+1)) /\ (q(t+(t0+1)) = c) \/ ~p(t+t0) /\ (q(t+t0) = c) /\ phi(t+t0) /\ p(t+(t0+1)) /\ Phi_I(q(t+(t0+1))) \/ p(t+t0) /\ Phi_R((i(t+t0):'a),(q(t+t0):'b)) /\ p(t+(t0+1)) ) /\ ?t1. !t2. ~p(t1+(t2+t0)) \/ Psi(i(t1+(t2+t0)),q(t1+(t2+t0))) `--) end, PURE_REWRITE_TAC[UNTIL_AS_SUNTIL,ALWAYS_SIGNAL] THEN BETA_TAC THEN DISJ_CASES_TAC (SPEC(--`!t'. phi(t'+t0)`--)BOOL_CASES_AX) THEN SUBST1_TAC CO_BUECHI_SUNTIL_CLOSURE THEN ASM_REWRITE_TAC[] THENL[ (* this is the case where (--`!t'. phi(t'+t0)`--) holds *) EXISTS_TAC (--`\t:num.F`--) THEN EXISTS_TAC (--`\t:num.c:'b`--) THEN BETA_TAC THEN RULE_ASSUM_TAC EQT_ELIM THEN ASM_REWRITE_TAC[], (* in the other case, we have phi UNTIL cb = phi SUNITL cb *) EQ_TAC THEN REPEAT STRIP_TAC THEN EXISTS_TAC (--`p:num->bool`--) THEN EXISTS_TAC (--`q:num->'b`--) THEN ASM_REWRITE_TAC[] THENL[EXISTS_TAC (--`t1:num`--) THEN ASM_REWRITE_TAC[], ALL_TAC] THEN MY_MP_TAC (--`(?t. ~phi(t+t0)) ==> (?t. p(t+t0))`--) THENL[ CONV_TAC CONTRAPOS_CONV THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV) THEN REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM (fn x=> RULE_ASSUM_TAC(REWRITE_RULE[x]) THEN ASSUME_TAC x) THEN GEN_TAC THEN LEFT_NO_FORALL_TAC 2 (--`t:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`t+(t0+1) = (t+1)+t0`--))] THEN STRIP_TAC, DISCH_TAC ] THEN UNDISCH_NO_TAC 4 THEN REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV) THEN STRIP_TAC THEN RES_TAC THEN MY_MP_TAC (--`!x. p(x+(t+t0))`--) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 5 (--`x+t`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC),ADD1] THEN STRIP_TAC, DISCH_TAC ] THEN DISJ_CASES_TAC(SPECL[(--`t1:num`--),(--`t:num`--)]LESS_CASES) THENL[ (* --------- case t1 SUBST1_TAC x THEN ASSUME_TAC x) THEN POP_ASSUM (fn x => RULE_ASSUM_TAC(REWRITE_RULE[x])) THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV(--`(t+p')+(t2+t0) = (p'+t2)+(t+t0)`--))) THEN ASM_REWRITE_TAC[] THEN LEFT_NO_FORALL_TAC 5 (--`t2:num`--) THEN UNDISCH_HD_TAC THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV(--`(t+p')+(t2+t0) = (p'+t2)+(t+t0)`--))) THEN ASM_REWRITE_TAC[] ] ] ); (* ========================== CO_BUECHI_SBEFORE_CLOSURE =============================== *) (* *) (* The next theorem shows that co-Buechi automata are closed under an appliation of a *) (* SBEFORE operator, provided that the right hand side argument is propositional. *) (* *) (* |- ( (\t0. *) (* ?q. *) (* Phi_I(q t0) /\ *) (* (!t. Phi_R(i(t+t0),q(t+t0))) /\ *) (* (?t1. !t2. Psi(i(t1+t2+t0),q(t1+t2+t0))) *) (* ) *) (* SBEFORE *) (* phi *) (* ) *) (* t0 = *) (* (?p1 p2 (q:num->'b). *) (* (~p1 t0 /\ ~p2 t0 /\ (q t0 = c) \/ *) (* p1 t0 /\ ~p2 t0 /\ Phi_I(q t0) *) (* ) /\ *) (* (!t. *) (* ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) *) (* /\ ~p1(t+t0+1) /\ ~p2(t+t0+1) /\ (q(t+t0+1) = c) *) (* \/ ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) *) (* /\ p1(t+t0+1) /\ ~p2(t+t0+1) /\ Phi_I(q(t+t0+1)) *) (* \/ p1(t+t0) /\ ~p2(t+t0) /\ ~phi(t+t0) /\ Phi_I(q(t+t0)) *) (* /\ Phi_R((i(t+t0):'a),q(t+t0)) /\ p1(t+t0+1) /\ p2(t+t0+1) *) (* \/ p1(t+t0) /\ p2(t+t0) /\ Phi_R((i(t+t0):'a),q(t+t0)) *) (* /\ p1(t+t0+1) /\ p2(t+t0+1) *) (* ) /\ *) (* ?t1. !t2. p1(t1+t2+t0) /\ Psi(i(t1+t2+t0),q(t1+t2+t0)) *) (* *) (* *) (* ==================================================================================== *) val CO_BUECHI_SBEFORE_CLOSURE = TAC_PROOF( let val cb = (--`?q. Phi_I(q t0) /\ (!t. Phi_R((i(t+t0):'a),(q(t+t0):'b))) /\ (?t1. !t2. Psi(i(t1+(t2+t0)),q(t1+(t2+t0))))`--) in ([],--`((\t0:num. ^cb) SBEFORE phi) t0 = ?p1 p2 (q:num->'b). (~p1 t0 /\ ~p2 t0 /\ (q t0 = c) \/ p1 t0 /\ ~p2 t0 /\ Phi_I(q t0) ) /\ (!t. ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) /\ ~p1(t+(t0+1)) /\ ~p2(t+(t0+1)) /\ (q(t+(t0+1)) = c) \/ ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) /\ p1(t+(t0+1)) /\ ~p2(t+(t0+1)) /\ Phi_I(q(t+(t0+1))) \/ p1(t+t0) /\ ~p2(t+t0) /\ ~phi(t+t0) /\ Phi_I(q(t+t0)) /\ Phi_R((i(t+t0):'a),q(t+t0)) /\ p1(t+(t0+1)) /\ p2(t+(t0+1)) \/ p1(t+t0) /\ p2(t+t0) /\ Phi_R((i(t+t0):'a),q(t+t0)) /\ p1(t+(t0+1)) /\ p2(t+(t0+1)) ) /\ ?t1. !t2. p1(t1+(t2+t0)) /\ Psi(i(t1+(t2+t0)),q(t1+(t2+t0))) `--) end, PURE_REWRITE_TAC[SBEFORE_SIGNAL] THEN BETA_TAC THEN EQ_TAC THENL[ (* ---------------------------------------------------------------------------- *) (* first implication: from left to right *) (* ---------------------------------------------------------------------------- *) REPEAT STRIP_TAC THEN EXISTS_TAC(--`\x. delta+t0<=x`--) THEN EXISTS_TAC(--`\x. delta+t0 q x | (c:'b)`--) THEN BETA_TAC THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(delta+t0 ~(delta <= t)`--))) THEN POP_ASSUM REWRITE1_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`(t ~(delta < t)`--))) THEN POP_ASSUM REWRITE1_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV (--`(t ~(delta+t0 ~(delta+t0<=t+(t0+1)) \/ (t+(t0+1)=delta+t0)`--))) THEN LEFT_FORALL_TAC (--`t0:num`--) THEN POP_ASSUM DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THENL[ POP_NO_ASSUM 2 MATCH_MP_TAC THEN UNDISCH_NO_TAC 1 THEN CONV_TAC ARITH_CONV, ASM_REWRITE_TAC[LESS_EQ_REFL] THEN POP_NO_ASSUM 2 MATCH_MP_TAC THEN UNDISCH_NO_TAC 1 THEN CONV_TAC ARITH_CONV ], (* here is the case (delta=t) *) POP_ASSUM (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[LESS_EQ_REFL,LESS_REFL] THEN LEFT_FORALL_TAC (--`delta:num`--) THEN UNDISCH_HD_TAC THEN LEFT_NO_FORALL_TAC 1 (--`0`--) THEN UNDISCH_HD_TAC THEN REWRITE_TAC[LESS_EQ_REFL,ADD_CLAUSES] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_CONV, (* here is the case (delta (delta<=t)`--))) THEN POP_ASSUM REWRITE1_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV (--`(delta (delta+t0 (delta+t0<=t+(t0+1))`--))) THEN POP_ASSUM REWRITE1_TAC THEN IMP_RES_TAC LESS_ADD_1 THEN POP_ASSUM REWRITE1_TAC THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV (--`(delta+(p+1))+t0 = (p+1)+(delta+t0)`--))] ], (* -------------------------------------------------------------------- *) (* acceptance condition *) (* -------------------------------------------------------------------- *) EXISTS_TAC(--`t1+delta`--) THEN GEN_TAC THEN REWRITE_TAC[ARITH_CONV(--`delta+t0<=(t1+delta)+(t2+t0)`--)] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV (--`(t1+delta)+(t2+t0) = t1+(t2+(delta+t0))`--))] THEN ASM_REWRITE_TAC[] ], (* ---------------------------------------------------------------------------- *) (* second implication: from right to left *) (* ---------------------------------------------------------------------------- *) REPEAT STRIP_TAC THENL[ ALL_TAC, (* -------------------------------------------------------------------- *) (* First consider the case where the automaton starts in state *) (* p1 t0 /\ ~p2 t0 /\ Phi_I(q t0), i.e. the subautomaton starts right *) (* now. Hence, instantiate delta := 0 in the SBEFORE_SIGNAL_THM. *) (* -------------------------------------------------------------------- *) MY_MP_TAC(--`!y. p1(y+t0)`--) (* -------------------------------------------------------------------- *) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 2 (--`y:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC),ADD1] THEN STRIP_TAC, DISCH_TAC ] THEN POP_ASSUM (fn x => RULE_ASSUM_TAC(REWRITE_RULE[x]) THEN ASSUME_TAC x) THEN EXISTS_TAC(--`0`--) THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN REPEAT STRIP_TAC THENL[ ALL_TAC, IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`(t<=0) ==> (t=0)`--))) THEN POP_ASSUM (fn x => RULE_ASSUM_TAC(REWRITE_RULE[x])) THEN UNDISCH_HD_TAC THEN LEFT_NO_FORALL_TAC 3 (--`0`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC ] THEN EXISTS_TAC(--`q:num->'b`--) THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL[ ALL_TAC, EXISTS_TAC(--`t1:num`--) THEN GEN_TAC THEN ASM_REWRITE_TAC[] ] THEN GEN_TAC THEN LEFT_NO_FORALL_TAC 2 (--`t:num`--) THEN UNDISCH_HD_TAC THEN STRIP_TAC ] (* ------------------------------------------------------------------------ *) (* Now consider the case where the automaton starts in state *) (* ~p1 t0 /\ ~p2 t0 /\ (q t0 = c), i.e. the subautomaton starts at a later *) (* point of time. We first prove that the automaton will eventually start. *) (* ------------------------------------------------------------------------ *) (* We first prove that the automaton will move from at some time d+t0 to *) (* state p1(d+t0) /\ ~p2(d+t0) /\ Phi_I(q(d+t0)) and stays until then in *) (* in the initial state, i.e., ~p1(x+t0) /\ ~p2(x+t0) /\ (q(x+t0) = c) *) (* holds for all x ~p1(t+t0)) /\ p1(d+t0)`--) (* ------------------------------------------------------------------------ *) THENL[ DISJ_CASES_TAC(SPEC(--`p1:num->bool`--)(GEN(--`b:num->bool`--)DELTA_CASES)) THEN ASM_REWRITE_TAC[] THEN UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[ADD_ASSOC], STRIP_TAC] (* ------------------------------------------------------------------------ *) THEN MY_MP_TAC(--`!t. t ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = (c:'b))`--) (* ------------------------------------------------------------------------ *) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`(SUC t (t ~phi(t+t0)`--) (* ------------------------------------------------------------------------ *) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THENL[ LEFT_NO_FORALL_TAC 5 (--`0`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC, RES_TAC THEN LEFT_NO_FORALL_TAC 9 (--`SUC t`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC], DISCH_TAC ] (* ------------------------------------------------------------------------ *) THEN MY_MP_TAC(--`0 RULE_ASSUM_TAC(REWRITE_RULE[x])) THEN COPY_ASM_NO 6 THEN LEFT_FORALL_TAC(--`p+1`--) THEN DISCH_TAC THEN LEFT_FORALL_TAC (--`p:num`--) THEN UNDISCH_HD_TAC THEN UNDISCH_HD_TAC THEN POP_NO_TAC 0 THEN LEFT_FORALL_TAC(--`p:num`--) THEN LEFT_NO_FORALL_TAC 1(--`p:num`--) THEN UNDISCH_HD_TAC THEN UNDISCH_HD_TAC THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`p ~phi(t+t0))`--) *) (* *) (* We clearly instantiate delta:=d, and q:= q prove the arising subgoals. *) (* ------------------------------------------------------------------------ *) THEN EXISTS_TAC (--`d:num`--) THEN CONJ_TAC THENL[ ALL_TAC, (* prove that (!t. t <= d ==> ~phi(t+t0)) holds (by previous lemmata) *) GEN_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN RES_TAC] THEN EXISTS_TAC(--`q:num->'b`--) THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL[ (* -------------------------------------------------------------------- *) (* the transition relation: !t'. Phi_R(i(t'+d+t0),q(t'+d+t0)) *) (* -------------------------------------------------------------------- *) GEN_TAC THEN LEFT_NO_FORALL_TAC 10 (--`t+d`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC)] THEN STRIP_TAC, (* -------------------------------------------------------------------- *) (* the acceptance condition: ?t1.!t2. Psi(i(t1+t2+d+t0),q(t1+t2+d+t0)) *) (* -------------------------------------------------------------------- *) EXISTS_TAC (--`t1:num`--) THEN GEN_TAC THEN LEFT_NO_FORALL_TAC 9 (--`t2+d`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`t1+((t2+d)+t0) = (t1+t2)+(d+t0)`--))] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`(t1+t2)+(d+t0) = t1+(t2+(d+t0))`--))] ] ] ); (* ========================== CO_BUECHI_SWHEN_CLOSURE =============================== *) (* *) (* The next theorem shows that co-Buechi automata are closed under an appliation of a *) (* SWHEN operator, provided that the right hand side argument is propositional. *) (* *) (* |- ( (\t0. *) (* ?q. *) (* Phi_I(q t0) /\ *) (* (!t. Phi_R(i(t+t0),q(t+t0))) /\ *) (* (?t1. !t2. Psi(i(t1+t2+t0),q(t1+t2+t0))) *) (* ) *) (* SWHEN *) (* phi *) (* ) *) (* t0 = *) (* (?p1 p2 (q:num->'b). *) (* (~p1 t0 /\ ~p2 t0 /\ (q t0 = c) \/ *) (* p1 t0 /\ ~p2 t0 /\ Phi_I(q t0) *) (* ) /\ *) (* (!t. *) (* ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) *) (* /\ ~p1(t+t0+1) /\ ~p2(t+t0+1) /\ (q(t+t0+1) = c) *) (* \/ ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) *) (* /\ p1(t+t0+1) /\ ~p2(t+t0+1) /\ Phi_I(q(t+t0+1)) *) (* \/ p1(t+t0) /\ ~p2(t+t0) /\ phi(t+t0) /\ Phi_I(q(t+t0)) *) (* /\ Phi_R((i(t+t0):'a),q(t+t0)) /\ p1(t+t0+1) /\ p2(t+t0+1) *) (* \/ p1(t+t0) /\ p2(t+t0) /\ Phi_R((i(t+t0):'a),q(t+t0)) *) (* /\ p1(t+t0+1) /\ p2(t+t0+1) *) (* ) /\ *) (* ?t1. !t2. p1(t1+t2+t0) /\ Psi(i(t1+t2+t0),q(t1+t2+t0)) *) (* *) (* *) (* ==================================================================================== *) val CO_BUECHI_SWHEN_CLOSURE = TAC_PROOF( let val cb = (--`?q. Phi_I(q t0) /\ (!t. Phi_R((i(t+t0):'a),(q(t+t0):'b))) /\ (?t1. !t2. Psi(i(t1+(t2+t0)),q(t1+(t2+t0))))`--) in ([],--`((\t0:num. ^cb) SWHEN phi) t0 = ?p1 p2 (q:num->'b). (~p1 t0 /\ ~p2 t0 /\ (q t0 = c) \/ p1 t0 /\ ~p2 t0 /\ Phi_I(q t0) ) /\ (!t. ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) /\ ~p1(t+(t0+1)) /\ ~p2(t+(t0+1)) /\ (q(t+(t0+1)) = c) \/ ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = c) /\ ~phi(t+t0) /\ p1(t+(t0+1)) /\ ~p2(t+(t0+1)) /\ Phi_I(q(t+(t0+1))) \/ p1(t+t0) /\ ~p2(t+t0) /\ phi(t+t0) /\ Phi_I(q(t+t0)) /\ Phi_R((i(t+t0):'a),q(t+t0)) /\ p1(t+(t0+1)) /\ p2(t+(t0+1)) \/ p1(t+t0) /\ p2(t+t0) /\ Phi_R((i(t+t0):'a),q(t+t0)) /\ p1(t+(t0+1)) /\ p2(t+(t0+1)) ) /\ ?t1. !t2. p1(t1+(t2+t0)) /\ Psi(i(t1+(t2+t0)),q(t1+(t2+t0))) `--) end, PURE_REWRITE_TAC[SWHEN_SIGNAL] THEN BETA_TAC THEN EQ_TAC THENL[ (* ---------------------------------------------------------------------------- *) (* first implication: from left to right *) (* ---------------------------------------------------------------------------- *) REPEAT STRIP_TAC THEN EXISTS_TAC(--`\x. delta+t0<=x`--) THEN EXISTS_TAC(--`\x. delta+t0 q x | (c:'b)`--) THEN BETA_TAC THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV(--`~(delta+t0 ~(delta <= t)`--))) THEN POP_ASSUM REWRITE1_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`(t ~(delta < t)`--))) THEN POP_ASSUM REWRITE1_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV (--`(t ~(delta+t0 ~(delta+t0<=t+(t0+1)) \/ (t+(t0+1)=delta+t0)`--))) THEN LEFT_FORALL_TAC (--`t0:num`--) THEN POP_ASSUM DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THENL[ POP_NO_ASSUM 6 MATCH_MP_TAC THEN ASM_REWRITE_TAC[], ASM_REWRITE_TAC[LESS_EQ_REFL] THEN POP_NO_ASSUM 6 MATCH_MP_TAC THEN ASM_REWRITE_TAC[] ], (* here is the case (delta=t) *) POP_ASSUM (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[LESS_EQ_REFL,LESS_REFL] THEN LEFT_NO_FORALL_TAC 1 (--`0`--) THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_CONV, (* here is the case (delta (delta<=t)`--))) THEN POP_ASSUM REWRITE1_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV (--`(delta (delta+t0 (delta+t0<=t+(t0+1))`--))) THEN POP_ASSUM REWRITE1_TAC THEN IMP_RES_TAC LESS_ADD_1 THEN POP_ASSUM REWRITE1_TAC THEN ASM_REWRITE_TAC[EQT_ELIM(ARITH_CONV (--`(delta+(p+1))+t0 = (p+1)+(delta+t0)`--))] ], (* -------------------------------------------------------------------- *) (* acceptance condition *) (* -------------------------------------------------------------------- *) EXISTS_TAC(--`t1+delta`--) THEN GEN_TAC THEN REWRITE_TAC[ARITH_CONV(--`delta+t0<=(t1+delta)+(t2+t0)`--)] THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV (--`(t1+delta)+(t2+t0) = t1+(t2+(delta+t0))`--))] THEN ASM_REWRITE_TAC[] ], (* ---------------------------------------------------------------------------- *) (* second implication: from right to left *) (* ---------------------------------------------------------------------------- *) REPEAT STRIP_TAC THENL[ ALL_TAC, (* -------------------------------------------------------------------- *) (* First consider the case where the automaton starts in state *) (* p1 t0 /\ ~p2 t0 /\ Phi_I(q t0), i.e. the subautomaton starts right *) (* now. Hence, instantiate delta := 0 in the SWHEN_SIGNAL_THM. *) (* -------------------------------------------------------------------- *) MY_MP_TAC(--`!y. p1(y+t0)`--) (* -------------------------------------------------------------------- *) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN LEFT_NO_FORALL_TAC 2 (--`y:num`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[SYM(SPEC_ALL ADD_ASSOC),ADD1] THEN STRIP_TAC, DISCH_TAC ] THEN POP_ASSUM (fn x => RULE_ASSUM_TAC(REWRITE_RULE[x]) THEN ASSUME_TAC x) THEN EXISTS_TAC(--`0`--) THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[NOT_LESS_0] THEN REPEAT STRIP_TAC THENL[ LEFT_NO_FORALL_TAC 2 (--`0`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC, EXISTS_TAC(--`q:num->'b`--) THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL[ GEN_TAC THEN LEFT_NO_FORALL_TAC 2 (--`t:num`--) THEN UNDISCH_HD_TAC THEN STRIP_TAC, EXISTS_TAC(--`t1:num`--) THEN ASM_REWRITE_TAC[] ] ] ] (* ------------------------------------------------------------------------ *) (* Now consider the case where the automaton starts in state *) (* ~p1 t0 /\ ~p2 t0 /\ (q t0 = c), i.e. the subautomaton starts at a later *) (* point of time. We first prove that the automaton will eventually start. *) (* ------------------------------------------------------------------------ *) (* We first prove that the automaton will move from at some time d+t0 to *) (* state p1(d+t0) /\ ~p2(d+t0) /\ Phi_I(q(d+t0)) and stays until then in *) (* in the initial state, i.e., ~p1(x+t0) /\ ~p2(x+t0) /\ (q(x+t0) = c) *) (* holds for all x ~p1(t+t0)) /\ p1(d+t0)`--) (* ------------------------------------------------------------------------ *) THENL[ DISJ_CASES_TAC(SPEC(--`p1:num->bool`--)(GEN(--`b:num->bool`--)DELTA_CASES)) THEN ASM_REWRITE_TAC[] THEN UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[ADD_ASSOC], STRIP_TAC] (* ------------------------------------------------------------------------ *) THEN MY_MP_TAC(--`!t. t ~p1(t+t0) /\ ~p2(t+t0) /\ (q(t+t0) = (c:'b))`--) (* ------------------------------------------------------------------------ *) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV(--`(SUC t (t ~phi(t+t0)`--) (* ------------------------------------------------------------------------ *) THENL[ INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THENL[ LEFT_NO_FORALL_TAC 5 (--`0`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC, RES_TAC THEN LEFT_NO_FORALL_TAC 9 (--`SUC t`--) THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC], DISCH_TAC ] (* ------------------------------------------------------------------------ *) THEN MY_MP_TAC(--`0 RULE_ASSUM_TAC(REWRITE_RULE[x])) THEN COPY_ASM_NO 6 THEN LEFT_FORALL_TAC(--`p+1`--) THEN DISCH_TAC THEN LEFT_FORALL_TAC (--`p:num`--) THEN UND