Changeset 1635 for src/common
- Timestamp:
- Jan 7, 2012, 12:33:17 AM (9 years ago)
- Location:
- src/common
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Graphs.ma
r1515 r1635 36 36 lookup ? ? (add ? ? g l s) l ≠ None ?. 37 37 38 axiom 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 38 45 axiom graph_add_lookup: 39 46 ∀A: Type[0]. … … 43 50 ∀to_insert: label. 44 51 lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?. 52 53 axiom 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. 45 60 46 61 axiom graph_num_nodes: -
src/common/Identifiers.ma
r1631 r1635 40 40 〈id',u'〉 = fresh tag u → 41 41 fresh_for_univ tag id u'. 42 #tag * #id * #id' * #u * #u' normalize #H #E destruct /2 /42 #tag * #id * #id' * #u * #u' normalize #H #E destruct /2 by le_S/ 43 43 qed. 44 44 … … 47 47 〈id',u'〉 = fresh tag u → 48 48 id ≠ id'. 49 #tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2 /49 #tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2 by absurd/ 50 50 qed. 51 51 … … 59 59 env_fresh_for_univ tag A (〈id,a〉::env) u'. 60 60 #tag #A #env * #u * #u' #id #a 61 #H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2 / ]61 #H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2 by fresh_remains_fresh/ ] 62 62 qed. 63 63 … … 77 77 #P #t * #x * #y #T #F 78 78 change with (P (eqb ??)) 79 @(eqb_elim x y P) [ /2 / | * #H @F % #E destruct /2/ ]79 @(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ] 80 80 qed. 81 81 … … 98 98 99 99 lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false. 100 #tag * #x * #y #NE normalize @not_eq_to_eqb_false /2 /100 #tag * #x * #y #NE normalize @not_eq_to_eqb_false /2 by not_to_not/ 101 101 qed. 102 102 … … 105 105 #E [ % | %2 ] 106 106 lapply E @eqb_elim 107 [ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2 / ]107 [ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2 by absurd/ ] 108 108 qed. 109 109 … … 123 123 #tag #A #l elim l 124 124 [ // 125 | * #id #a #tl #IH #r * #H1 #H2 % /2 /125 | * #id #a #tl #IH #r * #H1 #H2 % /2 by All_append_l/ 126 126 ] qed. 127 127 … … 129 129 #tag #A #l elim l 130 130 [ // 131 | * #id #a #tl #IH #r * #H1 #H2 /2 /131 | * #id #a #tl #IH #r * #H1 #H2 /2 by / 132 132 ] qed. 133 133 … … 202 202 lookup tag A (add tag A m j a) i = lookup tag A m i. 203 203 #tag #A * #m * #i * #j #a #H 204 @lookup_opt_insert_miss /2 /204 @lookup_opt_insert_miss /2 by not_to_not/ 205 205 qed. 206 206 … … 224 224 cases (identifier_eq ? i j) 225 225 [ #E >E >lookup_add_hit #H %1 destruct % // 226 | #NE >lookup_add_miss /2 /226 | #NE >lookup_add_miss /2 by or_intror, sym_not_eq/ 227 227 ] qed. 228 228 … … 328 328 #FMU #E destruct lapply (FMU (an_identifier tag u)) whd in ⊢ ((% → %) → ?); 329 329 generalize in ⊢ ((?(??%?) → ?) → ??%?); * 330 [ // | #a #H @False_ind lapply (H ?) /2 / % #E destruct330 [ // | #a #H @False_ind lapply (H ?) /2 by absurd/ % #E destruct 331 331 qed. 332 332
Note: See TracChangeset
for help on using the changeset viewer.