Changeset 1599 for src/ASM/Util.ma
 Timestamp:
 Dec 13, 2011, 1:34:37 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1598 r1599 1 include "basics/list .ma".1 include "basics/lists/list.ma". 2 2 include "basics/types.ma". 3 3 include "arithmetics/nat.ma". 4 5 include "utilities/pair.ma".6 4 include "ASM/JMCoercions.ma". 7 5 … … 649 647 650 648 651 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19652 for @{ match $e in bool with [ true ⇒ $t  false ⇒ $f] }.653 notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp break 'else' \nbsp term 48 f \nbsp)" non associative with precedence 19654 for @{ match $e with [ true ⇒ $t  false ⇒ $f] }.655 656 649 let rec fold_left_i_aux (A: Type[0]) (B: Type[0]) 657 650 (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝ … … 684 677  S o ⇒ f (iterate A f a o) 685 678 ]. 686 687 (* Yeah, I probably ought to do something more general... *)688 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"689 with precedence 90 for @{ 'triple $a $b $c}.690 interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).691 692 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"693 with precedence 90 for @{ 'quadruple $a $b $c $d}.694 interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).695 696 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"697 with precedence 10698 for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }.699 700 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"701 with precedence 10702 for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.703 704 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"705 with precedence 10706 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.707 708 axiom pair_elim':709 ∀A,B,C: Type[0].710 ∀T: A → B → C.711 ∀p.712 ∀P: A×B → C → Prop.713 (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →714 P p (let 〈lft, rgt〉 ≝ p in T lft rgt).715 716 axiom pair_elim'':717 ∀A,B,C,C': Type[0].718 ∀T: A → B → C.719 ∀T': A → B → C'.720 ∀p.721 ∀P: A×B → C → C' → Prop.722 (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →723 P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).724 725 lemma pair_destruct_1:726 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.727 #A #B #a #b *; /2/728 qed.729 730 lemma pair_destruct_2:731 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.732 #A #B #a #b *; /2/733 qed.734 735 736 let rec exclusive_disjunction (b: bool) (c: bool) on b ≝737 match b with738 [ true ⇒739 match c with740 [ false ⇒ true741  true ⇒ false742 ]743  false ⇒744 match c with745 [ false ⇒ false746  true ⇒ true747 ]748 ].749 750 (* dpm: conflicts with library definitions751 interpretation "Nat less than" 'lt m n = (ltb m n).752 interpretation "Nat greater than" 'gt m n = (gtb m n).753 interpretation "Nat greater than eq" 'geq m n = (geb m n).754 *)755 679 756 680 let rec division_aux (m: nat) (n : nat) (p: nat) ≝ … … 891 815 elim b 892 816 normalize 893 [ /2 /817 [ /2 by conj/ 894 818  # K 895 819 destruct
Note: See TracChangeset
for help on using the changeset viewer.