Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Coqlib.ma

    r473 r487  
    1919
    2020include "binary/Z.ma".
    21 include "datatypes/sums.ma".
    22 include "datatypes/list.ma".
     21include "basics/types.ma".
     22include "basics/list.ma".
    2323
    2424include "extralib.ma".
     
    350350(* * Properties of powers of two. *)
    351351
    352 nlemma two_power_nat_O : two_power_nat O = one.
    353 //; nqed.
    354 
    355 nlemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0.
    356 //; nqed.
    357 
    358 nlemma two_power_nat_two_p:
     352lemma two_power_nat_O : two_power_nat O = one.
     353// qed.
     354
     355lemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0.
     356// qed.
     357
     358lemma two_power_nat_two_p:
    359359  ∀x. Z_two_power_nat x = two_p (Z_of_nat x).
    360 #x; ncases x;
    361 ##[ //;
    362 ##| nnormalize; #p; nelim p; //; #p' H; nrewrite > (nat_succ_pos …); //;
    363 ##] nqed.
     360#x cases x
     361[ //
     362| normalize #p elim p // #p' #H >(nat_succ_pos …) //
     363] qed.
    364364(*
    365365Lemma two_p_monotone:
     
    576576(*naxiom align : Z → Z → Z.*)
    577577
    578 ndefinition align ≝ λn: Z. λamount: Z.
     578definition align ≝ λn: Z. λamount: Z.
    579579  ((n + amount - 1) / amount) * amount.
    580580(*
     
    600600(* * Mapping a function over an option type. *)
    601601
    602 ndefinition option_map ≝ λA,B.λf:A→B.λv:option A.
     602definition option_map ≝ λA,B.λf:A→B.λv:option A.
    603603  match v with [ Some v' ⇒ Some ? (f v') | None ⇒ None ? ].
    604604
     
    794794  induction l; simpl; congruence.
    795795Qed.
    796 *)
    797 nlemma list_in_map_inv:
    798   ∀A,B: Type. ∀f: A -> B. ∀l: list A. ∀y: B.
     796*) (*
     797lemma list_in_map_inv:
     798  ∀A,B: Type[0]. ∀f: A -> B. ∀l: list A. ∀y: B.
    799799  in_list ? y (map ?? f l) → ∃x:A. y = f x ∧ in_list ? x l.
    800800#A B f l; nelim l;
     
    808808      nelim (IH h H1); #x'; *; #IH1 IH2; @x'; @; /2/;
    809809  ##]
    810 ##] nqed.
     810##] nqed.*)
    811811(*
    812812Lemma list_append_map:
     
    841841(* * [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements
    842842  in common. *)
    843 
    844 ndefinition list_disjoint : ∀A:Type. list A → list A → Prop ≝
     843(*
     844definition list_disjoint : ∀A:Type[0]. list A → list A → Prop ≝
    845845  λA,l1,l2.
    846846  ∀x,y: A. in_list A x l1 → in_list A y l2 → x ≠ y.
    847847
    848 nlemma list_disjoint_cons_left:
    849   ∀A: Type. ∀a: A. ∀l1,l2: list A.
     848lemma list_disjoint_cons_left:
     849  ∀A: Type[0]. ∀a: A. ∀l1,l2: list A.
    850850  list_disjoint A (a :: l1) l2 → list_disjoint A l1 l2.
    851851#A;#a;#l1;#l2;nwhd in ⊢ (% → %); #H;
     
    874874nwhd in ⊢ (% → %);
    875875#H;#x;#y;#H1;#H2; napply sym_neq; /2/;
    876 nqed.
     876nqed.*)
     877
    877878(*
    878879Lemma list_disjoint_dec:
     
    898899(* * [list_norepet l] holds iff the list [l] contains no repetitions,
    899900  i.e. no element occurs twice. *)
    900 
    901 ninductive list_norepet (A: Type) : list A → Prop ≝
     901(*
     902inductive list_norepet (A: Type[0]) : list A → Prop ≝
    902903  | list_norepet_nil:
    903904      list_norepet A (nil A)
    904905  | list_norepet_cons:
    905906      ∀hd,tl.
    906       ¬(in_list A hd tl) → list_norepet A tl → list_norepet A (hd :: tl).
     907      ¬(in_list A hd tl) → list_norepet A tl → list_norepet A (hd :: tl).*)
    907908(*
    908909Lemma list_norepet_dec:
Note: See TracChangeset for help on using the changeset viewer.