Changeset 1459 for src/ASM/Status.ma


Ignore:
Timestamp:
Oct 24, 2011, 2:34:02 PM (9 years ago)
Author:
boender
Message:
  • moved stronger occurs_exactly_once lemma to its proper place in Status
  • renamed 'bla' to something more descriptive
  • finished stuff with sigma types
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1393 r1459  
    11651165qed.
    11661166
     1167lemma occurs_exactly_once_Some_stronger:
     1168  ∀id,id',i,prefix.
     1169    occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →
     1170    (eq_bv ? id' id ∧ does_not_occur id prefix) ∨
     1171    (¬eq_bv ? id' id ∧ occurs_exactly_once id prefix).
     1172 #id #id' #i #prefix elim prefix
     1173 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?)
     1174  change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)
     1175  [ normalize //
     1176  | normalize #H @⊥ @H 
     1177  ]
     1178 | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
     1179   cases he; normalize nodelta
     1180   [ #H @ (IH H)
     1181   | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
     1182     generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id)
     1183     cases (eq_bv ???) in ⊢ (???% → %) #Heq
     1184     [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta
     1185       [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf
     1186       | #H >(does_not_occur_Some)
     1187         [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
     1188           change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
     1189           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??)
     1190           change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 
     1191         | @(sym_eq … H)
     1192         ]
     1193       ]
     1194     | normalize nodelta #H lapply (IH H) -IH -H; #Hor @orb_elim
     1195       generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)
     1196       #Heq2
     1197       [ normalize nodelta <Heq2 in Hor; #Hor normalize in Hor;
     1198         whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
     1199         change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
     1200         cases (does_not_occur id tl) in Hor; normalize nodelta //
     1201       | normalize nodelta whd in match (occurs_exactly_once ??)
     1202         whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)
     1203         >Heq normalize nodelta <Heq2 in Hor; normalize //
     1204       ]
     1205     ] 
     1206   ]
     1207 ]
     1208qed.   
     1209
    11671210let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
    11681211  match l with
Note: See TracChangeset for help on using the changeset viewer.