Changeset 2128 for src/ASM/ASM.ma


Ignore:
Timestamp:
Jun 27, 2012, 5:05:33 PM (8 years ago)
Author:
sacerdot
Message:

Final shuffling around

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2124 r2128  
    244244 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;
    245245 cases (is_a hd am) in ISIN; /2/
     246qed.
     247
     248lemma is_in_monotonic_wrt_append:
     249  ∀m, n: nat.
     250  ∀p: Vector addressing_mode_tag m.
     251  ∀q: Vector addressing_mode_tag n.
     252  ∀to_search: addressing_mode.
     253    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
     254  #m #n #p #q #to_search #assm
     255  elim q try assumption
     256  #n' #hd #tl #inductive_hypothesis
     257  normalize
     258  cases (is_a ??) try @I
     259  >inductive_hypothesis @I
     260qed.
     261
     262corollary is_in_hd_tl:
     263  ∀to_search: addressing_mode.
     264  ∀hd: addressing_mode_tag.
     265  ∀n: nat.
     266  ∀v: Vector addressing_mode_tag n.
     267    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
     268  #to_search #hd #n #v
     269  elim v
     270  [1:
     271    #absurd
     272    normalize in absurd; cases absurd
     273  |2:
     274    #n' #hd' #tl #inductive_hypothesis #assm
     275    >vector_cons_append >(vector_cons_append … hd' tl)
     276    @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
     277    assumption
     278  ]
    246279qed.
    247280
Note: See TracChangeset for help on using the changeset viewer.