logic/ltl/concrltl2waaScript.sml

541          >> qabbrev_tac `g2 = (��ls2 e1 sofar.
546           >- (`MEM y (FOLDR (g2 (trans_concr f)) [] (trans_concr f'))` by (
547               qunabbrev_tac `g1` >> qunabbrev_tac `g2` >> fs[]
549              >> `!ls1 ls2. (MEM y (FOLDR (g2 ls2) [] ls1)) ==>
556               >> qunabbrev_tac `g2` >> qunabbrev_tac `g1` >> fs[MEM_MAP]
627                         (FOLDR (��e1 sofar. g2 ls2 e1 sofar) [] ls1)` by (
629                           >> qunabbrev_tac `g1` >> qunabbrev_tac `g2`
666                             (FOLDR (��e1 sofar. g2 ls2 e1 sofar) [] ls1)` by (
668                      >> qunabbrev_tac `g1` >> qunabbrev_tac `g2`
750      in let g2 = FOLDR (\p g. addFrmlToGraph g p) g1 allSucs
754                 (SOME g2) trans
798    ``!aP g fs g2.
801       ��� (expandGraph g fs = SOME g2)
815         (id ��� domain g2.nodeInfo ��� lookup id g2.followers = SOME fls)
820              (lookup id g2.nodeInfo = SOME nL)
827        !g fs g2.
829          ��� (expandGraph g fs = SOME g2)
831          ==> (P g2 ��� C g2)`
1141 (*   ``!aP g fs g2. *)
1142 (*   (wfg g) ��� (expandGraph g fs = SOME g2) *)
1147 (*   (!i n. i ��� (domain g2.nodeInfo) ��� (lookup i g2.nodeInfo = SOME n) *)
1162         ==> (?g2. (expandGraph g fs = SOME g2)
1163               ��� (wfg g2)
1164               ��� (set (graphStates g) ��� set (graphStates g2))
1165               ��� (set (graphStatesWithId g) ��� set (graphStatesWithId g2))
1166               ��� (until_iff_final g ==> until_iff_final g2)
1167               ��� (unique_node_formula g2)
1168               ��� (flws_sorted g2)
1169               (* ��� (first_flw_has_max_counter g2) *))``,
1173        `?g2. ((case A of
1175               | SOME g => (E g)) = SOME g2)
1176           ��� wfg g2
1177           ��� A0 ��� (A2 g2)
1178           ��� C g2
1179           ��� M g2`
1233             >> `���g2. addEdgeToGraph f h x = SOME g2 ��� wfg g2
1234                   ��� set (graphStatesWithId x) = set (graphStatesWithId g2)
1235                   ��� unique_node_formula g2
1236                   (* ��� (flws_sorted g2) *)
1237                  (* ��� first_flw_has_max_counter g2 *)`
1239             >> `flws_sorted g2` by metis_tac[ADDEDGE_COUNTER_LEMM]
1240             >> qexists_tac `g2`  >> simp[] >> qunabbrev_tac `A2`
1241             >> `C g2` by metis_tac[] >> simp[] >> rpt strip_tac
1243             >> `set (graphStates g) ��� set (graphStates g2)` by (
1248                  >> `MEM (q,r.frml) (graphStatesWithId g2)`
1258             >- (`set (graphStates x) = set (graphStates g2)`
1286    >> rpt strip_tac >> qexists_tac `g2` >> fs[]
1293             (!g2.
1304             ��� (expandGraph g ls = SOME g2)
1306          ==> (!x. MEM x (graphStates g2)
1315         >> `g = g2` by fs[expandGraph_def]
1363         >> first_x_assum (qspec_then `g2` mp_tac) >> simp[]
1504    ``!f g ls g2 x. (!x. MEM x (graphStates g) ��� ~ MEM x ls
1507                      ��� (expandGraph g ls = SOME g2)
1513                    ==> (!x. MEM x (graphStates g2)
1515                                 ==> (MEM y (graphStates g2))))``,
1557         >> first_x_assum (qspec_then `g2` mp_tac) >> simp[]
1633    ``!f g ls g2 x.
1637     ��� (expandGraph g ls = SOME g2)
1645     ==> (!x. MEM x (graphStates g2)
1646            ==> (!y. concrTrans g2 (props f) x
1696     >> first_x_assum (qspec_then `g2` mp_tac) >> simp[]
1901     in do g2 <- expandGraph g1 flat_initForms;
1902           SOME (concrAA g2 init_concr (props_concr ��))
2190                            >> `���g2.
2192                                     = SOME g2
2193                                 ��� wfg g2
2194                                 ��� set (graphStates g0) ��� set (graphStates g2)
2196                                      ��� set (graphStatesWithId g2)`
2198                            >> `g = g2` by fs[] >> rw[] >> fs[MEM_toAList]
2238                       >> `?g2. expandGraph G (nub (FLAT (tempDNF_concr ��)))
2239                                    = SOME g2
2240                              ��� wfg g2
2241                              ��� set (graphStates G) ��� set (graphStates g2)
2243                                 ��� set (graphStatesWithId g2)`
2245                       >> `g = g2` by metis_tac[SOME_11] >> rw[]
2339             >> `���g2.
2340                  expandGraph G0 L = SOME g2 ��� wfg g2
2341                ��� set (graphStates G0) ��� set (graphStates g2)
2343                   ��� set (graphStatesWithId g2)
2344                ��� (until_iff_final G0 ��� until_iff_final g2)`
2346             >> `g = g2` by metis_tac[SOME_11] >> rw[]