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