source:src/common/Graphs.ma@2755

Last change on this file since 2755 was 2645, checked in by sacerdot, 7 years ago
1. some broken back-end files repaires, several still to go
2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 1.6 KB
RevLine
[726]1include "basics/types.ma".
[639]2
[726]3include "ASM/BitVectorTrie.ma".
[736]4include "common/Identifiers.ma".
[1082]5include "common/AST.ma".
[639]6
[738]7definition label ≝ identifier LabelTag.
[726]8
[1082]9(* o'caml compiler doesn't make distinction between idents and labels *)
10definition label_to_ident: label → ident ≝
11  λl.
12  match l with
13  [ an_identifier l ⇒ an_identifier SymbolTag l
14  ].
15
[736]16definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
[726]17
[738]18definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
[1077]19
[1253]20definition graph_fold ≝
21  λA, B: Type[0].
22  λf.
23  λgraph: graph A.
24  λseed: B.
25  match graph with
[1515]26  [ an_id_map map ⇒ fold A B f map seed
[1253]27  ].
28
30  ∀A: Type[0].
31  ∀g: graph A.
32  ∀l: label.
33  ∀s: A.
34    lookup ? ? (add ? ? g l s) l ≠ None ?.
35
37  ∀A: Type[0].
38  ∀g: graph A.
39  ∀l: label.
40  ∀s: A.
41    lookup ? ? (add ? ? g l s) l = Some ? s.
42
44  ∀A: Type[0].
45  ∀g: graph A.
46  ∀l: label.
47  ∀s: A.
48  ∀to_insert: label.
[1080]49    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
[1635]50
52  ∀A: Type[0].
53  ∀g: graph A.
54  ∀l: label.
55  ∀s: A.
56  ∀to_insert: label.
57  l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l.
[1080]58
[1882]59definition graph_num_nodes:
60  ∀A: Type[0].graph A → ℕ ≝ λA,g.|g|.
61
62lemma graph_num_ind : ∀A : Type[0].∀P : graph A → Prop.
63  (∀g.(∀g'.|g'|<|g| → P g') → P g) → ∀g.P g.
64#A#P#H#g
65lapply (refl ? (|g|))
66generalize in ⊢(???%→?);
67#n lapply g -g
68@(nat_elim1 … n)
69#m #G #g #EQs @H >EQs #g' #DEQ @(G ? DEQ g' (refl …))
70qed.
Note: See TracBrowser for help on using the repository browser.