logic/ltl/ltlScript.sml

21   /\ (MODELS w (DISJ f1 f2) = (MODELS w f1) \/ (MODELS w f2))
22   /\ (MODELS w (CONJ f1 f2) = (MODELS w f1) /\ (MODELS w f2))
24   /\ (MODELS w (U f1 f2) =
25         ?n. (MODELS (suff w n) f2) /\ !i. (i < n) ==> (MODELS (suff w i) f1))
26   /\ (MODELS w (R f1 f2) =
27         !n. (MODELS (suff w n) f2) \/ ?i. (i < n) /\ (MODELS (suff w i) f1))`;
31    ``!w f1 f2. (!n. (MODELS (suff w n) f2) \/ ?i. (i < n) /\ (MODELS (suff w i) f1))
32       = ((!n. MODELS (suff w n) f2) \/
33          ?n. MODELS (suff w n) f1 /\ !i. i <= n ==> MODELS (suff w i) f2)``,
35     >- (Cases_on `!n. MODELS (suff w n) f2` >> fs[]
36         >> qabbrev_tac `N = LEAST n. ~MODELS (suff w n) f2`
37         >> `(!i. i < N ==> MODELS (suff w i) f2) ��� ~MODELS (suff w N) f2` by (
42         >> `MODELS (suff w N) f2 ��� ���i. i < N ��� MODELS (suff w i) f1` by metis_tac[]
64     /\ (subForms (DISJ f1 f2) = {DISJ f1 f2} ��� (subForms f1) ��� (subForms f2))
65     /\ (subForms (CONJ f1 f2) = {CONJ f1 f2} ��� (subForms f1) ��� (subForms f2))
67     /\ (subForms (U f1 f2) = {U f1 f2} ��� (subForms f1) ��� (subForms f2))
68     /\ (subForms (R f1 f2) = {R f1 f2} ��� (subForms f1) ��� (subForms f2))`;
77   ``!f1 f2 f3. f1 ��� subForms f2 /\ f2 ��� subForms f3 ==> f1 ��� subForms f3``,
86     /\ (no_tmp_op (DISJ f1 f2) = (no_tmp_op f1) + (no_tmp_op f2))
87     /\ (no_tmp_op (CONJ f1 f2) = (no_tmp_op f1) + (no_tmp_op f2))
89     /\ (no_tmp_op (U f1 f2) =(no_tmp_op f1) + (no_tmp_op f2) +1)
90     /\ (no_tmp_op (R f1 f2) =(no_tmp_op f1) + (no_tmp_op f2) +1)`;
138    ``!f1 f2. (f1 ��� subForms f2) /\ (f2 ��� subForms f1) ==> (f1 = f2)``,
140    >> `!f1 f2. (f1 ��� subForms f2) ==> (no_tmp_op f1 <= no_tmp_op f2)`
142    >- (`no_tmp_op f2 <= no_tmp_op f1` by metis_tac[TMP_OP_DECR_WITH_SF]
143        >> `no_tmp_op (DISJ f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF]
147    >- (`no_tmp_op f2 <= no_tmp_op f1'` by metis_tac[TMP_OP_DECR_WITH_SF]
148        >> `no_tmp_op (DISJ f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF]
152    >- (`no_tmp_op f2 <= no_tmp_op f1` by metis_tac[TMP_OP_DECR_WITH_SF]
153        >> `no_tmp_op (CONJ f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF]
157    >- (`no_tmp_op f2 <= no_tmp_op f1'` by metis_tac[TMP_OP_DECR_WITH_SF]
158        >> `no_tmp_op (CONJ f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF]
162    >- (`no_tmp_op f2 <= no_tmp_op f1` by metis_tac[TMP_OP_DECR_WITH_SF]
163        >> `no_tmp_op (X f1) <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF]
166    >- (`no_tmp_op f2 <= no_tmp_op f1` by metis_tac[TMP_OP_DECR_WITH_SF]
167        >> `no_tmp_op (U f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF]
170    >- (`no_tmp_op f2 <= no_tmp_op f1'` by metis_tac[TMP_OP_DECR_WITH_SF]
171        >> `no_tmp_op (U f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF]
174    >- (`no_tmp_op f2 <= no_tmp_op f1` by metis_tac[TMP_OP_DECR_WITH_SF]
175        >> `no_tmp_op (R f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF]
178    >- (`no_tmp_op f2 <= no_tmp_op f1'` by metis_tac[TMP_OP_DECR_WITH_SF]
179        >> `no_tmp_op (R f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF]
185    (is_until (U f1 f2) = T)
198  /\ (tempSubForms (DISJ f1 f2) = (tempSubForms f1) ��� (tempSubForms f2))
199  /\ (tempSubForms (CONJ f1 f2) = (tempSubForms f1) ��� (tempSubForms f2))
201  /\ (tempSubForms (U f1 f2) = {U f1 f2} ��� (tempSubForms f1) ��� (tempSubForms f2))
202  /\ (tempSubForms (R f1 f2) = {R f1 f2} ��� (tempSubForms f1) ��� (tempSubForms f2))`;
214    >- (`!f1 f2. (U f1 f2) ��� tempSubForms (U f1 f2)` by rw[tempSubForms_def]
216    >- (`!f1 f2. (R f1 f2) ��� tempSubForms (R f1 f2)` by rw[tempSubForms_def]
222    ``!f1 f2 f3. f1 ��� tempSubForms f2 /\ f2 ��� subForms f3 ==> f1 ��� tempSubForms f3``,
262    ``!f1 f2. (f1 ��� tempSubForms f2) /\ (f2 ��� tempSubForms f1) ==> (f1 = f2)``,
287   ``WF (��f1 f2. f1 ��� tempSubForms f2 ��� ~(f1 = f2))``,
308    ``!f f1 f2. ~(DISJ f1 f2 ��� tempSubForms f)``,
313    ``!f f1 f2. ~(CONJ f1 f2 ��� tempSubForms f)``,
326  /\ (tempDNF (DISJ f1 f2) = (tempDNF f1) ��� (tempDNF f2))
327  /\ (tempDNF (CONJ f1 f2) = {f' ��� f'' | (f' ��� tempDNF f1) /\ (f'' ��� tempDNF f2)})
329  /\ (tempDNF (U f1 f2) = {{U f1 f2}})
330  /\ (tempDNF (R f1 f2) = {{R f1 f2}})`;
404     /\ (FLTL_MODELS w (F_CONJ f1 f2) = (FLTL_MODELS w f1) /\ (FLTL_MODELS w f2))
407     /\ (FLTL_MODELS w (F_U f1 f2) =
408         ?n. (FLTL_MODELS (suff w n) f2) /\ !i. (i < n) ==> (FLTL_MODELS (suff w i) f1))`;
412   ��� (NNF (F_CONJ f1 f2) = CONJ (NNF f1) (NNF f2))
414   ��� (NNF (F_NEG (F_CONJ f1 f2)) = DISJ (NNF (F_NEG f1)) (NNF (F_NEG f2)))
417   ��� (NNF (F_NEG (F_U f1 f2)) = R (NNF (F_NEG f1)) (NNF (F_NEG f2)))
419   ��� (NNF (F_U f1 f2) = U (NNF f1) (NNF f2))`;