1open HolKernel Parse boolLib bossLib listTheory pred_setTheory; 2 3open sptreeTheory arithmeticTheory; 4 5val _ = new_theory "gfg"; 6 7val _ = ParseExtras.tight_equality() 8val _ = monadsyntax.temp_add_monadsyntax(); 9val _ = overload_on("monad_bind",``OPTION_BIND``); 10 11val _ = Datatype��� 12 gfg = <| nodeInfo : �� spt ; 13 followers : (�� # num) list spt ; 14 preds : (�� # num) list spt ; 15 next : num 16 |>���; 17 18val empty_def = Define��� 19 empty = <| nodeInfo := LN ; followers := LN ; preds := LN; next := 0|>���; 20 21val addNode_def = Define��� 22 addNode i g = g with <| nodeInfo updated_by (insert g.next i) ; 23 next updated_by SUC ; 24 followers updated_by (insert g.next []) ; 25 preds updated_by (insert g.next []) ; |>���; 26 27val addEdge_def = Define` 28 addEdge src (e,tgt) g = 29 if src ��� domain g.nodeInfo ��� tgt ��� domain g.nodeInfo then 30 do 31 followers_old <- lookup src g.followers; 32 preds_old <- lookup tgt g.preds; 33 SOME (g with <| 34 followers updated_by (insert src ((e,tgt)::followers_old)) ; 35 preds updated_by (insert tgt ((e,src)::preds_old)) 36 |>) 37 od 38 else NONE`; 39 40val findNode_def = Define` 41 findNode P g = 42 FIND P (toAList g.nodeInfo)`; 43 44val updateNode_def = Define` 45 updateNode nId node g = 46 if nId ��� domain g.nodeInfo 47 then SOME (g with <| nodeInfo updated_by (insert nId node) ; 48 next := g.next ; 49 followers := g.followers ; 50 preds := g.preds ; |>) 51 else NONE`; 52 53val wfAdjacency_def = Define��� 54 wfAdjacency adjmap ��� 55 ���k nl e n. lookup k adjmap = SOME nl ��� MEM (e,n) nl ��� 56 n ��� domain adjmap���; 57 58val wfg_def = Define��� 59 wfg g ��� (���n. g.next ��� n ��� n ��� domain g.nodeInfo) ��� 60 (domain g.followers = domain g.nodeInfo) ��� 61 (domain g.preds = domain g.nodeInfo) ��� 62 wfAdjacency g.followers ��� wfAdjacency g.preds���; 63 64val empty_is_wfg = Q.store_thm( 65 "empty_is_wfg[simp]", 66 `wfg empty`, 67 simp[empty_def,wfg_def,wfAdjacency_def] >> rpt strip_tac 68 >> fs[lookup_def] 69 ); 70 71val cond_eq = Q.prove( 72 ���((if P then t else e) = v) ��� P ��� t = v ��� ��P ��� e = v���, 73 rw[]); 74 75val addNode_preserves_wfg = Q.store_thm( 76 "addNode_preserves_wfg[simp]", 77 ���wfg g ��� wfg (addNode i g)���, 78 simp[wfg_def, addNode_def] >> 79 dsimp[wfAdjacency_def, lookup_insert, cond_eq] >> metis_tac[]); 80 81Theorem addEdge_preserves_wfg: 82 wfg g ��� (addEdge i (e,s) g = SOME g2) ==> wfg g2 83Proof 84 simp[wfg_def,addEdge_def] >> 85 dsimp[wfAdjacency_def, lookup_insert] >> rpt strip_tac >> rw[] >> fs[] 86 >- metis_tac[] 87 >- (fs[INSERT_DEF,SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> metis_tac[]) 88 >- (fs[INSERT_DEF,SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> metis_tac[]) 89 >- (rename[`lookup k (insert i _ _) = SOME nl`, `MEM (e',n) nl`, 90 ���i ��� domain _���] >> 91 fs[lookup_insert] >> Cases_on `k=i` >> fs[] >> 92 Cases_on `MEM (e',n) followers_old` >> rw[] >> fs[MEM] >> metis_tac[]) 93 >- (rename[`lookup k1 (insert k2 _ _) = SOME nl`, `MEM (e',n) nl`, 94 ���k2 ��� domain _���] >> 95 fs[lookup_insert] >> Cases_on `k1=k2` >> fs[] >> 96 Cases_on `MEM (e',n) preds_old` >> rw[] >> fs[MEM] >> 97 metis_tac[]) 98QED 99 100val addEdge_preserves_nodeInfo = Q.store_thm( 101 "addEdge_preserves_nodeInfo", 102 `(addEdge i (e,s) g) = SOME g2 ==> (g.nodeInfo = g2.nodeInfo)`, 103 rpt strip_tac >> fs[addEdge_def,theorem "gfg_component_equality"] 104 ); 105 106val updateNode_preserves_wfg = Q.store_thm( 107 "updateNode_preserves_wfg[simp]", 108 `wfg g ��� (updateNode id n g = SOME g2) ==> wfg g2`, 109 simp[wfg_def,updateNode_def] 110 >> dsimp[wfAdjacency_def, lookup_insert] 111 >> rw[] >> fs[INSERT_DEF,SET_EQ_SUBSET,SUBSET_DEF] 112 >> rpt strip_tac >> metis_tac[] 113 ); 114 115val updateNode_preserves_edges = Q.store_thm( 116 "updateNode_preserves_edges", 117 `updateNode id n g = SOME g2 118 ==> (g.followers = g2.followers) 119 ��� (g.preds = g2.preds)`, 120 simp[updateNode_def] >> rpt strip_tac 121 >> fs[theorem "gfg_component_equality"] 122 ); 123 124val updateNode_preserves_domain = Q.store_thm( 125 "updateNode_preserves_domain", 126 `updateNode id n g = SOME g2 ==> (domain g.nodeInfo = domain g2.nodeInfo)`, 127 simp[updateNode_def] >> rpt strip_tac >> fs[theorem "gfg_component_equality"] 128 >> `domain g2.nodeInfo = id INSERT (domain g.nodeInfo)` 129 by metis_tac[domain_insert] 130 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> metis_tac[IN_INSERT] 131 ); 132 133val graph_size_def = Define���graph_size g = sptree$size g.nodeInfo���; 134 135val graph_size_addNode = Q.store_thm( 136 "graph_size_addNode[simp]", 137 ���wfg g ��� graph_size (addNode i g) = graph_size g + 1���, 138 simp[graph_size_def, addNode_def, size_insert, wfg_def]); 139 140val _ = export_theory(); 141