source: src/common/Graphs.ma @ 2540

Last change on this file since 2540 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 1.6 KB
Line 
1include "basics/types.ma".
2
3include "ASM/BitVectorTrie.ma".
4include "common/Identifiers.ma".
5include "common/AST.ma".
6
7axiom LabelTag : String.
8
9definition label ≝ identifier LabelTag.
10
11(* o'caml compiler doesn't make distinction between idents and labels *)
12definition label_to_ident: label → ident ≝
13  λl.
14  match l with
15  [ an_identifier l ⇒ an_identifier SymbolTag l
16  ].
17
18definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
19
20definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
21
22definition graph_fold ≝
23  λA, B: Type[0].
24  λf.
25  λgraph: graph A.
26  λseed: B.
27  match graph with
28  [ an_id_map map ⇒ fold A B f map seed
29  ].
30
31axiom graph_add:
32  ∀A: Type[0].
33  ∀g: graph A.
34  ∀l: label.
35  ∀s: A.
36    lookup ? ? (add ? ? g l s) l ≠ None ?.
37
38axiom graph_add_eq:
39  ∀A: Type[0].
40  ∀g: graph A.
41  ∀l: label.
42  ∀s: A.
43    lookup ? ? (add ? ? g l s) l = Some ? s.
44
45axiom graph_add_lookup:
46  ∀A: Type[0].
47  ∀g: graph A.
48  ∀l: label.
49  ∀s: A.
50  ∀to_insert: label.
51    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
52   
53axiom graph_add_preserve :
54  ∀A: Type[0].
55  ∀g: graph A.
56  ∀l: label.
57  ∀s: A.
58  ∀to_insert: label.
59  l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l.
60
61definition graph_num_nodes:
62  ∀A: Type[0].graph A → ℕ ≝ λA,g.|g|.
63 
64lemma graph_num_ind : ∀A : Type[0].∀P : graph A → Prop.
65  (∀g.(∀g'.|g'|<|g| → P g') → P g) → ∀g.P g.
66#A#P#H#g
67lapply (refl ? (|g|))
68generalize in ⊢(???%→?);
69#n lapply g -g
70@(nat_elim1 … n)
71#m #G #g #EQs @H >EQs #g' #DEQ @(G ? DEQ g' (refl …))
72qed.
Note: See TracBrowser for help on using the repository browser.