cs_ap : relation cs_crr;
cs_proof : is_CSetoid cs_crr cs_eq cs_ap}.
-interpretation "setoid equality"
- 'eq x y = (cic:/matita/algebra/CoRN/Setoids/cs_eq.con _ x y).
+interpretation "setoid equality" 'eq x y = (cs_eq _ x y).
-interpretation "setoid apart"
- 'neq x y = (cic:/matita/algebra/CoRN/Setoids/cs_ap.con _ x y).
+interpretation "setoid apart" 'neq x y = (cs_ap _ x y).
(* visto che sia "ap" che "eq" vanno in Prop e data la "tight-apartness",
"cs_neq" e "ap" non sono la stessa cosa? *)
.
interpretation "order relation between positions and contexts"
- 'leq x y = (cic:/matita/LOGIC/CLE/defs/CLE.ind#xpointer(1/1) x y).
+ 'leq x y = (CLE x y).
(* \langle \rangle *)
notation "〈x,y〉" non associative with precedence 80
for @{ 'mk_byte8 $x $y }.
-interpretation "mk_byte8" 'mk_byte8 x y =
- (cic:/matita/freescale/byte8/byte8.ind#xpointer(1/1/1) x y).
+interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
(* operatore = *)
definition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
(* \ominus *)
notation "hvbox(⊖ a)" non associative with precedence 36
for @{ 'not_bool $a }.
-interpretation "not_bool" 'not_bool x =
- (cic:/matita/freescale/extra/not_bool.con x).
+interpretation "not_bool" 'not_bool x = (not_bool x).
(* \otimes *)
notation "hvbox(a break ⊗ b)" left associative with precedence 35
for @{ 'and_bool $a $b }.
-interpretation "and_bool" 'and_bool x y =
- (cic:/matita/freescale/extra/and_bool.con x y).
+interpretation "and_bool" 'and_bool x y = (and_bool x y).
(* \oplus *)
notation "hvbox(a break ⊕ b)" left associative with precedence 34
for @{ 'or_bool $a $b }.
-interpretation "or_bool" 'or_bool x y =
- (cic:/matita/freescale/extra/or_bool.con x y).
+interpretation "or_bool" 'or_bool x y = (or_bool x y).
(* \odot *)
notation "hvbox(a break ⊙ b)" left associative with precedence 33
for @{ 'xor_bool $a $b }.
-interpretation "xor_bool" 'xor_bool x y =
- (cic:/matita/freescale/extra/xor_bool.con x y).
+interpretation "xor_bool" 'xor_bool x y = (xor_bool x y).
(* ProdT e' gia' definito, aggiungo Prod3T e Prod4T e Prod5T *)
non associative with precedence 80 for
@{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
- (cic:/matita/freescale/status/alu_HC05.ind#xpointer(1/1/1) acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
+ (mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
(* ALU dell'HC08/HCS08 *)
record alu_HC08: Type ≝
non associative with precedence 80 for
@{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
- (cic:/matita/freescale/status/alu_HC08.ind#xpointer(1/1/1) acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
+ (mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
(* ALU dell'RS08 *)
record alu_RS08: Type ≝
non associative with precedence 80 for
@{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
- (cic:/matita/freescale/status/alu_RS08.ind#xpointer(1/1/1) acclow pc pcm spc xm psm zfl cfl).
+ (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
(* tipo processore dipendente dalla mcu, varia solo la ALU *)
record any_status (mcu:mcu_type) (t:memory_impl): Type ≝
notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
for @{ 'mk_any_status $alu $mem $chk $clk }.
interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
- (cic:/matita/freescale/status/any_status.ind#xpointer(1/1/1) alu mem chk clk).
+ (mk_any_status alu mem chk clk).
(* **************** *)
(* GETTER SPECIFICI *)
(* \langle \rangle *)
notation "〈x:y〉" non associative with precedence 80
for @{ 'mk_word16 $x $y }.
-interpretation "mk_word16" 'mk_word16 x y =
- (cic:/matita/freescale/word16/word16.ind#xpointer(1/1/1) x y).
+interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
(* operatore = *)
definition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1) (w16l w2)).
notation "hvbox(a break # b)" non associative with precedence 50
for @{ 'apart $a $b}.
-interpretation "bishop_setapartness" 'apart x y =
- (cic:/matita/dama/bishop_set/bs_apart.con _ x y).
+interpretation "bishop_setapartness" 'apart x y = (bs_apart _ x y).
definition bishop_set_of_ordered_set: ordered_set → bishop_set.
intros (E); apply (mk_bishop_set E (λa,b:E. a ≰ b ∨ b ≰ a));
notation "hvbox(a break ≈ b)" non associative with precedence 50
for @{ 'napart $a $b}.
-interpretation "Bishop set alikeness" 'napart a b =
- (cic:/matita/dama/bishop_set/eq.con _ a b).
+interpretation "Bishop set alikeness" 'napart a b = (eq _ a b).
lemma eq_reflexive:∀E:bishop_set. reflexive ? (eq E).
intros (E); unfold; intros (x); apply bs_coreflexive;
definition lt ≝ λE:ordered_set.λa,b:E. a ≤ b ∧ a # b.
-interpretation "ordered sets less than" 'lt a b =
- (cic:/matita/dama/bishop_set/lt.con _ a b).
+interpretation "ordered sets less than" 'lt a b = (lt _ a b).
lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
intros 2 (E x); intro H; cases H (_ ABS);
notation > "'Eq'≈" non associative with precedence 50
for @{'eqrewrite}.
-interpretation "eq_rew" 'eqrewrite =
- (cic:/matita/dama/bishop_set/eq_trans.con _ _ _).
+interpretation "eq_rew" 'eqrewrite = (eq_trans _ _ _).
lemma le_rewl: ∀E:ordered_set.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz);
qed.
notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}.
-interpretation "le_rewl" 'lerewritel = (cic:/matita/dama/bishop_set_rewrite/le_rewl.con _ _ _).
+interpretation "le_rewl" 'lerewritel = (le_rewl _ _ _).
notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}.
-interpretation "le_rewr" 'lerewriter = (cic:/matita/dama/bishop_set_rewrite/le_rewr.con _ _ _).
+interpretation "le_rewr" 'lerewriter = (le_rewr _ _ _).
lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z.
intros (A x z y Exy Ayz); cases (bs_cotransitive ???x Ayz); [2:assumption]
qed.
notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}.
-interpretation "ap_rewl" 'aprewritel = (cic:/matita/dama/bishop_set_rewrite/ap_rewl.con _ _ _).
+interpretation "ap_rewl" 'aprewritel = (ap_rewl _ _ _).
notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
-interpretation "ap_rewr" 'aprewriter = (cic:/matita/dama/bishop_set_rewrite/ap_rewr.con _ _ _).
+interpretation "ap_rewr" 'aprewriter = (ap_rewr _ _ _).
lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
intros (A x z y Exy Ayz); cases (os_cotransitive ??? x Ayz); [2:assumption]
qed.
notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}.
-interpretation "exc_rewl" 'ordered_setrewritel = (cic:/matita/dama/bishop_set_rewrite/exc_rewl.con _ _ _).
+interpretation "exc_rewl" 'ordered_setrewritel = (exc_rewl _ _ _).
notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}.
-interpretation "exc_rewr" 'ordered_setrewriter = (cic:/matita/dama/bishop_set_rewrite/exc_rewr.con _ _ _).
+interpretation "exc_rewr" 'ordered_setrewriter = (exc_rewr _ _ _).
lemma lt_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z < y → z < x.
qed.
notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (cic:/matita/dama/bishop_set_rewrite/lt_rewl.con _ _ _).
+interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (cic:/matita/dama/bishop_set_rewrite/lt_rewr.con _ _ _).
+interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
Left : A → Or A B
| Right : B → Or A B.
-interpretation "constructive or" 'or x y =
- (cic:/matita/dama/cprop_connectives/Or.ind#xpointer(1/1) x y).
+interpretation "constructive or" 'or x y = (Or x y).
inductive And (A,B:CProp) : CProp ≝
| Conj : A → B → And A B.
-interpretation "constructive and" 'and x y =
- (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) x y).
+interpretation "constructive and" 'and x y = (And x y).
inductive exT (A:Type) (P:A→CProp) : CProp ≝
ex_introT: ∀w:A. P w → exT A P.
-interpretation "CProp exists" 'exists \eta.x =
- (cic:/matita/dama/cprop_connectives/exT.ind#xpointer(1/1) _ x).
+interpretation "CProp exists" 'exists \eta.x = (exT _ x).
definition Not : CProp → Prop ≝ λx:CProp.x → False.
-interpretation "constructive not" 'not x =
- (cic:/matita/dama/cprop_connectives/Not.con x).
+interpretation "constructive not" 'not x = (Not x).
definition cotransitive ≝
λC:Type.λlt:C→C→CProp.∀x,y,z:C. lt x y → lt x z ∨ lt z y.
definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b.
-interpretation "ordered sets less than" 'lt a b = (cic:/matita/dama/excess/lt.con _ a b).
+interpretation "ordered sets less than" 'lt a b = (lt _ a b).
lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
intros 2 (E x); intro H; cases H (_ ABS);
qed.
notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (cic:/matita/dama/excess/lt_rewl.con _ _ _).
+interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (cic:/matita/dama/excess/lt_rewr.con _ _ _).
+interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]
os_cotransitive: cotransitive ? os_excess
}.
-interpretation "Ordered set excess" 'nleq a b =
- (cic:/matita/dama/ordered_set/os_excess.con _ a b).
+interpretation "Ordered set excess" 'nleq a b = (os_excess _ a b).
(* Definition 2.2 (3) *)
definition le ≝ λE:ordered_set.λa,b:E. ¬ (a ≰ b).
-interpretation "Ordered set greater or equal than" 'geq a b =
- (cic:/matita/dama/ordered_set/le.con _ b a).
+interpretation "Ordered set greater or equal than" 'geq a b = (le _ b a).
-interpretation "Ordered set less or equal than" 'leq a b =
- (cic:/matita/dama/ordered_set/le.con _ a b).
+interpretation "Ordered set less or equal than" 'leq a b = (le _ a b).
lemma le_reflexive: ∀E.reflexive ? (le E).
unfold reflexive; intros 3 (E x H); apply (os_coreflexive ?? H);
λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
notation < "x \sub \neq" non associative with precedence 91 for @{'bsss $x}.
-interpretation "bs_of_ss" 'bsss x =
- (cic:/matita/dama/ordered_uniform/bs_of_ss.con _ _ _ x).
+interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
lemma segment_ordered_uniform_space:
∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
qed.
interpretation "Ordered uniform space segment" 'segment_set a b =
- (cic:/matita/dama/ordered_uniform/segment_ordered_uniform_space.con _ a b).
+ (segment_ordered_uniform_space _ a b).
(* Lemma 3.2 *)
alias symbol "pi1" = "sigma pi1".
definition hide ≝ λT:Type.λx:T.x.
notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
-interpretation "hide" 'hide =
- (cic:/matita/dama/property_sigma/hide.con _ _).
-interpretation "hide2" 'hide =
- (cic:/matita/dama/property_sigma/hide.con _ _ _).
+interpretation "hide" 'hide = (hide _ _).
+interpretation "hide2" 'hide = (hide _ _ _).
definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
coercion cic:/matita/dama/property_sigma/inject.con 0 1.
apply (le_to_not_lt p q H5);
|2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
apply (le_to_not_lt p r H10);]
-qed.
\ No newline at end of file
+qed.
notation > "x 'is_infimum' s" non associative with precedence 50
for @{'infimum $s $x}.
-interpretation "Ordered set upper bound" 'upper_bound s x =
- (cic:/matita/dama/supremum/upper_bound.con _ s x).
-interpretation "Ordered set lower bound" 'lower_bound s x =
- (cic:/matita/dama/supremum/lower_bound.con _ s x).
-interpretation "Ordered set increasing" 'increasing s =
- (cic:/matita/dama/supremum/increasing.con _ s).
-interpretation "Ordered set decreasing" 'decreasing s =
- (cic:/matita/dama/supremum/decreasing.con _ s).
-interpretation "Ordered set strong sup" 'supremum s x =
- (cic:/matita/dama/supremum/supremum.con _ s x).
-interpretation "Ordered set strong inf" 'infimum s x =
- (cic:/matita/dama/supremum/infimum.con _ s x).
+interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound _ s x).
+interpretation "Ordered set lower bound" 'lower_bound s x = (lower_bound _ s x).
+interpretation "Ordered set increasing" 'increasing s = (increasing _ s).
+interpretation "Ordered set decreasing" 'decreasing s = (decreasing _ s).
+interpretation "Ordered set strong sup" 'supremum s x = (supremum _ s x).
+interpretation "Ordered set strong inf" 'infimum s x = (infimum _ s x).
include "bishop_set.ma".
notation > "s 'is_strictly_increasing'" non associative with precedence 50
for @{'strictly_increasing $s}.
interpretation "Ordered set strict increasing" 'strictly_increasing s =
- (cic:/matita/dama/supremum/strictly_increasing.con _ s).
+ (strictly_increasing _ s).
notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 50
for @{'strictly_decreasing $s}.
notation > "s 'is_strictly_decreasing'" non associative with precedence 50
for @{'strictly_decreasing $s}.
interpretation "Ordered set strict decreasing" 'strictly_decreasing s =
- (cic:/matita/dama/supremum/strictly_decreasing.con _ s).
+ (strictly_decreasing _ s).
notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
interpretation "Ordered set supremum of increasing" 'sup_inc s u =
(cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
- (cic:/matita/dama/supremum/increasing.con _ s)
- (cic:/matita/dama/supremum/supremum.con _ s u)).
+ (increasing _ s)
+ (supremum _ s u)).
notation "a \downarrow u" non associative with precedence 50 for @{'inf_dec $a $u}.
interpretation "Ordered set supremum of increasing" 'inf_dec s u =
(cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
- (cic:/matita/dama/supremum/decreasing.con _ s)
- (cic:/matita/dama/supremum/infimum.con _ s u)).
+ (decreasing _ s)
+ (infimum _ s u)).
include "nat/plus.ma".
include "nat_ordered_set.ma".
for @{'order_converge $a $x}.
notation > "a 'order_converges' x" non associative with precedence 50
for @{'order_converge $a $x}.
-interpretation "Order convergence" 'order_converge s u =
- (cic:/matita/dama/supremum/order_converge.con _ s u).
+interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).
(* Definition 2.8 *)
notation "[a,b]" non associative with precedence 50
for @{'segment $a $b}.
-interpretation "Ordered set sergment" 'segment a b =
- (cic:/matita/dama/supremum/segment.con _ a b).
+interpretation "Ordered set sergment" 'segment a b = (segment _ a b).
notation "hvbox(x \in break [a,b])" non associative with precedence 50
for @{'segment2 $a $b $x}.
-interpretation "Ordered set sergment in" 'segment2 a b x=
- (cic:/matita/dama/supremum/segment.con _ a b x).
+interpretation "Ordered set sergment in" 'segment2 a b x= (segment _ a b x).
coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P.
notation < "'snd' \nbsp x" non associative with precedence 50 for @{'pi2 $x}.
notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}.
notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}.
-interpretation "sigma pi1" 'pi1 x =
- (cic:/matita/dama/supremum/pi1.con _ _ x).
+interpretation "sigma pi1" 'pi1 x = (pi1 _ _ x).
interpretation "Type exists" 'exists \eta.x =
(cic:/matita/dama/supremum/sigma.ind#xpointer(1/1) _ x).
notation "hvbox({[a, break b]})" non associative with precedence 90
for @{'segment_set $a $b}.
interpretation "Ordered set segment" 'segment_set a b =
- (cic:/matita/dama/supremum/segment_ordered_set.con _ a b).
+ (segment_ordered_set _ a b).
(* Lemma 2.9 *)
lemma segment_preserves_supremum:
definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x].
definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y].
-interpretation "pair pi1" 'pi1 x =
- (cic:/matita/dama/supremum/first.con _ _ x).
-interpretation "pair pi2" 'pi2 x =
- (cic:/matita/dama/supremum/second.con _ _ x).
+interpretation "pair pi1" 'pi1 x = (first _ _ x).
+interpretation "pair pi2" 'pi2 x = (second _ _ x).
notation "hvbox(\langle a, break b\rangle)" non associative with precedence 91 for @{ 'pair $a $b}.
-interpretation "pair" 'pair a b =
- (cic:/matita/dama/supremum/pair.ind#xpointer(1/1/1) _ _ a b).
+interpretation "pair" 'pair a b = (prod _ _ a b).
notation "a \times b" left associative with precedence 60 for @{'prod $a $b}.
-interpretation "prod" 'prod a b =
- (cic:/matita/dama/supremum/pair.ind#xpointer(1/1) a b).
+interpretation "prod" 'prod a b = (pair a b).
lemma square_ordered_set: ordered_set → ordered_set.
intro O; apply (mk_ordered_set (O × O));
for @{ 'square $s }.
notation > "s 'square'" non associative with precedence 90
for @{ 'square $s }.
-interpretation "ordered set square" 'square s =
- (cic:/matita/dama/supremum/square_ordered_set.con s).
+interpretation "ordered set square" 'square s = (square_ordered_set s).
definition square_segment ≝
λO:ordered_set.λa,b:O.λx:square_ordered_set O.
notation > "s 'is_upper_located'" non associative with precedence 50
for @{'upper_located $s}.
interpretation "Ordered set upper locatedness" 'upper_located s =
- (cic:/matita/dama/supremum/upper_located.con _ s).
+ (upper_located _ s).
notation < "s \nbsp 'is_lower_located'" non associative with precedence 50
for @{'lower_located $s}.
notation > "s 'is_lower_located'" non associative with precedence 50
for @{'lower_located $s}.
interpretation "Ordered set lower locatedness" 'lower_located s =
- (cic:/matita/dama/supremum/lower_located.con _ s).
+ (lower_located _ s).
(* Lemma 2.12 *)
lemma uparrow_upperlocated:
|2: right; exists [apply u]; split; [apply W|apply H4]]
qed.
-
\ No newline at end of file
+
notation "a \subseteq u" left associative with precedence 70
for @{ 'subset $a $u }.
-interpretation "Bishop subset" 'subset a b =
- (cic:/matita/dama/uniform/subset.con _ a b).
+interpretation "Bishop subset" 'subset a b = (subset _ a b).
notation "hvbox({ ident x : t | break p })" non associative with precedence 50
for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.
definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
-interpretation "explicit set" 'explicitset t =
- (cic:/matita/dama/uniform/mk_set.con _ t).
+interpretation "explicit set" 'explicitset t = (mk_set _ t).
notation < "s 2 \atop \neq" non associative with precedence 90
for @{ 'square2 $s }.
notation > "s 'square'" non associative with precedence 90
for @{ 'square $s }.
-interpretation "bishop set square" 'square x =
- (cic:/matita/dama/uniform/square_bishop_set.con x).
-interpretation "bishop set square" 'square2 x =
- (cic:/matita/dama/uniform/square_bishop_set.con x).
+interpretation "bishop set square" 'square x = (square_bishop_set x).
+interpretation "bishop set square" 'square2 x = (square_bishop_set x).
alias symbol "exists" = "exists".
notation "a \circ b" left associative with precedence 60
for @{'compose $a $b}.
-interpretation "relations composition" 'compose a b =
- (cic:/matita/dama/uniform/compose_relations.con _ a b).
+interpretation "relations composition" 'compose a b = (compose_relations _ a b).
notation "hvbox(x \in break a \circ break b)" non associative with precedence 50
for @{'compose2 $a $b $x}.
interpretation "relations composition" 'compose2 a b x =
- (cic:/matita/dama/uniform/compose_relations.con _ a b x).
+ (compose_relations _ a b x).
definition invert_relation ≝
λC:bishop_set.λU:C square → Prop.
for @{ 'invert2 $s $x}.
notation > "'inv' s" non associative with precedence 90
for @{ 'invert $s }.
-interpretation "relation invertion" 'invert a =
- (cic:/matita/dama/uniform/invert_relation.con _ a).
-interpretation "relation invertion" 'invert2 a x =
- (cic:/matita/dama/uniform/invert_relation.con _ a x).
+interpretation "relation invertion" 'invert a = (invert_relation _ a).
+interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x).
alias symbol "exists" = "CProp exists".
alias symbol "and" (instance 18) = "constructive and".
for @{'cauchy $a}.
notation > "a 'is_cauchy'" non associative with precedence 50
for @{'cauchy $a}.
-interpretation "Cauchy sequence" 'cauchy s =
- (cic:/matita/dama/uniform/cauchy.con _ s).
+interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).
(* Definition 2.15 *)
definition uniform_converge ≝
notation > "a 'uniform_converges' x" non associative with precedence 50
for @{'uniform_converge $a $x}.
interpretation "Uniform convergence" 'uniform_converge s u =
- (cic:/matita/dama/uniform/uniform_converge.con _ s u).
+ (uniform_converge _ s u).
(* Lemma 2.16 *)
lemma uniform_converge_is_cauchy :
(* Definition 2.17 *)
definition mk_big_set ≝
λP:CProp.λF:P→CProp.F.
-interpretation "explicit big set" 'explicitset t =
- (cic:/matita/dama/uniform/mk_big_set.con _ t).
+interpretation "explicit big set" 'explicitset t = (mk_big_set _ t).
definition restrict_uniformity ≝
λC:uniform_space.λX:C→Prop.
non associative with precedence 45
for @{ 'equiv $a $b }.
-interpretation "uguaglianza parziale" 'equiv x y =
- (cic:/matita/tests/decl/eq.ind#xpointer(1/1) _ x y).
+interpretation "uguaglianza parziale" 'equiv x y = (eq _ x y).
coercion cic:/matita/tests/decl/L.ind#xpointer(1/1/2).
axiom Rle: L R→L R→Prop.
axiom Rge: L R→L R→Prop.
-interpretation "real plus" 'plus x y =
- (cic:/matita/tests/decl/Rplus.con x y).
+interpretation "real plus" 'plus x y = (Rplus x y).
-interpretation "real leq" 'leq x y =
- (cic:/matita/tests/decl/Rle.con x y).
+interpretation "real leq" 'leq x y = (Rle x y).
-interpretation "real geq" 'geq x y =
- (cic:/matita/tests/decl/Rge.con x y).
+interpretation "real geq" 'geq x y = (Rge x y).
let rec elev (x:L R) (n:nat) on n: L R ≝
match n with
notation "a '"
non associative with precedence 80
for @{ 'deriv $a }.
-interpretation "function derivative" 'deriv x =
- (cic:/matita/didactic/deriv/De.con x).
-interpretation "function mult" 'mult x y =
- (cic:/matita/didactic/deriv/fmult.con x y).
-interpretation "function compositon" 'compose x y =
- (cic:/matita/didactic/deriv/fcomp.con x y).
+interpretation "function derivative" 'deriv x = (De x).
+interpretation "function mult" 'mult x y = (fmult x y).
+interpretation "function compositon" 'compose x y = (fcomp x y).
notation "hvbox(a break + b)"
right associative with precedence 45
for @{ 'oplus $a $b }.
-interpretation "function plus" 'plus x y =
- (cic:/matita/didactic/deriv/fplus.con x y).
+interpretation "function plus" 'plus x y = (fplus x y).
axiom i:R→F. (*mappatura R in F*)
coercion cic:/matita/didactic/deriv/i.con.
notation "ρ"
non associative with precedence 100
for @{ 'rho }.
-interpretation "function flip" 'rho =
- cic:/matita/didactic/deriv/freflex.con.
+interpretation "function flip" 'rho = freflex.
axiom reflex_ok: ∀f:F. ρ ∘ f = (i (-R1)) · f.
axiom dereflex: ρ ' = i (-R1). (*Togliere*)
right associative with precedence 75
for @{ 'elev $a $b }.
-interpretation "function power" 'elev x y =
- (cic:/matita/didactic/deriv/felev.con x y).
+interpretation "function power" 'elev x y = (felev x y).
axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m).
axiom Rle: R→R→Prop.
axiom Rge: R→R→Prop.
-interpretation "real plus" 'plus x y =
- (cic:/matita/didactic/reals/Rplus.con x y).
+interpretation "real plus" 'plus x y = (Rplus x y).
-interpretation "real opp" 'uminus x =
- (cic:/matita/didactic/reals/Ropp.con x).
+interpretation "real opp" 'uminus x = (Ropp x).
notation "hvbox(a break · b)"
right associative with precedence 55
for @{ 'mult $a $b }.
-interpretation "real mult" 'mult x y =
- (cic:/matita/didactic/reals/Rmult.con x y).
+interpretation "real mult" 'mult x y = (Rmult x y).
-interpretation "real leq" 'leq x y =
- (cic:/matita/didactic/reals/Rle.con x y).
+interpretation "real leq" 'leq x y = (Rle x y).
-interpretation "real geq" 'geq x y =
- (cic:/matita/didactic/reals/Rge.con x y).
+interpretation "real geq" 'geq x y = (Rge x y).
let rec elev (x:R) (n:nat) on n: R ≝
match n with
a_algebra_properties: is_algebra ? ? a_mult a_one
}.
-interpretation "Algebra product" 'times a b =
- (cic:/matita/attic/integration_algebras/a_mult.con _ a b).
+interpretation "Algebra product" 'times a b = (a_mult _ a b).
definition ring_of_algebra ≝
λK.λA:algebra K.
apply (not_eq_zero_one_ ? ? ? (r_ring_properties R)).
qed.
-interpretation "Ring mult" 'times a b =
- (cic:/matita/attic/rings/mult.con _ a b).
+interpretation "Ring mult" 'times a b = (mult _ a b).
notation "1" with precedence 89
for @{ 'one }.
-interpretation "Ring one" 'one =
- (cic:/matita/attic/rings/one.con _).
+interpretation "Ring one" 'one = (one _).
lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
intros;
vs_vector_space_properties :> is_vector_space ? vs_abelian_group emult
}.
-interpretation "Vector space external product" 'times a b =
- (cic:/matita/attic/vector_spaces/emult.con _ _ a b).
+interpretation "Vector space external product" 'times a b = (emult _ _ a b).
record is_semi_norm (R:real) (V: vector_space R) (semi_norm:V→R) : Prop \def
{ sn_positive: ∀x:V. zero R ≤ semi_norm x;
for @{ 'hide_everything_but $a }.
interpretation "mk_bounded_above_sequence" 'hide_everything_but a
-= (cic:/matita/classical_pointfree/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (mk_bounded_above_sequence _ _ a _).
interpretation "mk_bounded_below_sequence" 'hide_everything_but a
-= (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (mk_bounded_below_sequence _ _ a _).
theorem eq_f_sup_sup_f:
∀O':dedekind_sigma_complete_ordered_set.
qed.
interpretation "mk_bounded_sequence" 'hide_everything_but a
-= (cic:/matita/classical_pointfree/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
+= (mk_bounded_sequence _ _ a _ _).
lemma reduce_bas_seq:
∀O:ordered_set.∀a:nat→O.∀p.∀i.
notation "hvbox(x break ∈ A)" with precedence 60
for @{ 'member_of $x $A }.
-interpretation "Member of" 'member_of x A =
- (cic:/matita/classical_pointwise/sets/member_of.con _ A x).
+interpretation "Member of" 'member_of x A = (mk_member_of _ A x).
notation "hvbox(x break ∉ A)" with precedence 60
for @{ 'not_member_of $x $A }.
-interpretation "Not member of" 'not_member_of x A =
- (cic:/matita/logic/connectives/Not.con
- (cic:/matita/classical_pointwise/sets/member_of.con _ A x)).
+interpretation "Not member of" 'not_member_of x A = (Not (member_of _ A x)).
definition emptyset : ∀X.set X ≝ λX:Type.λx:X.False.
notation "∅︀" with precedence 100 for @{ 'emptyset }.
-interpretation "Emptyset" 'emptyset =
- (cic:/matita/classical_pointwise/sets/emptyset.con _).
+interpretation "Emptyset" 'emptyset = (emptyset _).
definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B.
notation "hvbox(A break ⊆ B)" with precedence 60
for @{ 'subset $A $B }.
-interpretation "Subset" 'subset A B =
- (cic:/matita/classical_pointwise/sets/subset.con _ A B).
+interpretation "Subset" 'subset A B = (subset _ A B).
definition intersection: ∀X. set X → set X → set X ≝
λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B.
notation "hvbox(A break ∩ B)" with precedence 70
for @{ 'intersection $A $B }.
-interpretation "Intersection" 'intersection A B =
- (cic:/matita/classical_pointwise/sets/intersection.con _ A B).
+interpretation "Intersection" 'intersection A B = (intersection _ A B).
definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B.
notation "hvbox(A break ∪ B)" with precedence 65
for @{ 'union $A $B }.
-interpretation "Union" 'union A B =
- (cic:/matita/classical_pointwise/sets/union.con _ A B).
+interpretation "Union" 'union A B = (union _ A B).
definition seq ≝ λX:Type.nat → X.
notation "hvbox(A \sub i)" with precedence 100
for @{ 'nth $A $i }.
-interpretation "nth" 'nth A i =
- (cic:/matita/classical_pointwise/sets/nth.con _ A i).
+interpretation "nth" 'nth A i = (nth _ A i).
definition countable_union: ∀X. seq (set X) → set X ≝
λX.λA:seq (set X).λx.∃j.x ∈ A \sub j.
notation "∪ \sub (ident i opt (: ty)) B" with precedence 65
for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
-interpretation "countable_union" 'big_union η.t =
- (cic:/matita/classical_pointwise/sets/countable_union.con _ t).
+interpretation "countable_union" 'big_union η.t = (countable_union _ t).
definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A.
notation "A \sup 'c'" with precedence 100
for @{ 'complement $A }.
-interpretation "Complement" 'complement A =
- (cic:/matita/classical_pointwise/sets/complement.con _ A).
+interpretation "Complement" 'complement A = (complement _ A).
definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝
λX,Y,f,B,x. f x ∈ B.
notation "hvbox(f \sup (-1))" with precedence 100
for @{ 'finverse $f }.
-interpretation "Inverse image" 'finverse f =
- (cic:/matita/classical_pointwise/sets/inverse_image.con _ _ f).
+interpretation "Inverse image" 'finverse f = (inverse_image _ _ f).
Left : A → Or A B
| Right : B → Or A B.
-interpretation "constructive or" 'or x y =
- (cic:/matita/constructive_connectives/Or.ind#xpointer(1/1) x y).
+interpretation "constructive or" 'or x y = (Or x y).
inductive And (A,B:Type) : Type ≝
| Conj : A → B → And A B.
-interpretation "constructive and" 'and x y =
- (cic:/matita/constructive_connectives/And.ind#xpointer(1/1) x y).
+interpretation "constructive and" 'and x y = (And x y).
inductive exT (A:Type) (P:A→Type) : Type ≝
ex_introT: ∀w:A. P w → exT A P.
@{\lambda ${ident i} . $p}}}.
*)
-interpretation "constructive exists" 'exists \eta.x =
- (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).
-interpretation "constructive exists (Type)" 'exists \eta.x =
- (cic:/matita/constructive_connectives/exT.ind#xpointer(1/1) _ x).
+interpretation "constructive exists" 'exists \eta.x = (ex _ x).
+interpretation "constructive exists (Type)" 'exists \eta.x = (exT _ x).
alias id "False" = "cic:/matita/logic/connectives/False.ind#xpointer(1/1)".
definition Not ≝ λx:Type.x → False.
-interpretation "constructive not" 'not x =
- (cic:/matita/constructive_connectives/Not.con x).
+interpretation "constructive not" 'not x = (Not x).
let rec gpow (G : abelian_group) (x : G) (n : nat) on n : G ≝
match n with [ O ⇒ 0 | S m ⇒ x + gpow ? x m].
-interpretation "additive abelian group pow" 'times n x =
- (cic:/matita/divisible_group/gpow.con _ x n).
+interpretation "additive abelian group pow" 'times n x = (gpow _ x n).
record dgroup : Type ≝ {
dg_carr:> abelian_group;
intros (G x n); cases (dg_prop G x n); apply w;
qed.
-interpretation "divisible group divide" 'divide x n =
- (cic:/matita/divisible_group/divide.con _ x n).
+interpretation "divisible group divide" 'divide x n = (divide _ x n).
lemma divide_divides:
∀G:dgroup.∀x:G.∀n. S n * (x / n) ≈ x.
exc_cotransitive: cotransitive ? exc_excess
}.
-interpretation "Excess base excess" 'nleq a b = (cic:/matita/excess/exc_excess.con _ a b).
+interpretation "Excess base excess" 'nleq a b = (exc_excess _ a b).
(* E(#,≰) → E(#,sym(≰)) *)
lemma make_dual_exc: excess_base → excess_base.
}.
notation "hvbox(a break # b)" non associative with precedence 50 for @{ 'apart $a $b}.
-interpretation "apartness" 'apart x y = (cic:/matita/excess/ap_apart.con _ x y).
+interpretation "apartness" 'apart x y = (ap_apart _ x y).
definition apartness_of_excess_base: excess_base → apartness.
intros (E); apply (mk_apartness E (λa,b:E. a ≰ b ∨ b ≰ a));
coercion cic:/matita/excess/exc_ap.con.
interpretation "Excess excess_" 'nleq a b =
- (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess_1.con _) a b).
+ (exc_excess (excess_base_OF_excess_1 _) a b).
record excess : Type ≝ {
excess_carr:> excess_;
}.
interpretation "Excess excess" 'nleq a b =
- (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b).
+ (exc_excess (excess_base_OF_excess1 _) a b).
interpretation "Excess (dual) excess" 'ngeq a b =
- (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess.con _) a b).
+ (exc_excess (excess_base_OF_excess _) a b).
definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y.
definition le ≝ λE:excess_base.λa,b:E. ¬ (a ≰ b).
interpretation "Excess less or equal than" 'leq a b =
- (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b).
+ (le (excess_base_OF_excess1 _) a b).
interpretation "Excess less or equal than" 'geq a b =
- (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess.con _) a b).
+ (le (excess_base_OF_excess _) a b).
lemma le_reflexive: ∀E.reflexive ? (le E).
unfold reflexive; intros 3 (E x H); apply (exc_coreflexive ?? H);
definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b).
notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}.
-interpretation "Apartness alikeness" 'napart a b = (cic:/matita/excess/eq.con _ a b).
-interpretation "Excess alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b).
-interpretation "Excess (dual) alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess.con _) a b).
+interpretation "Apartness alikeness" 'napart a b = (eq _ a b).
+interpretation "Excess alikeness" 'napart a b = (eq (excess_base_OF_excess1 _) a b).
+interpretation "Excess (dual) alikeness" 'napart a b = (eq (excess_base_OF_excess _) a b).
lemma eq_reflexive:∀E:apartness. reflexive ? (eq E).
intros (E); unfold; intros (x); apply ap_coreflexive;
λE,x,y,z.eq_trans_ E x z y.
notation > "'Eq'≈" non associative with precedence 50 for @{'eqrewrite}.
-interpretation "eq_rew" 'eqrewrite = (cic:/matita/excess/eq_trans.con _ _ _).
+interpretation "eq_rew" 'eqrewrite = (eq_trans _ _ _).
alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con".
lemma le_antisymmetric:
definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b.
-interpretation "ordered sets less than" 'lt a b = (cic:/matita/excess/lt.con _ a b).
+interpretation "ordered sets less than" 'lt a b = (lt _ a b).
lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
intros 2 (E x); intro H; cases H (_ ABS);
qed.
notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}.
-interpretation "le_rewl" 'lerewritel = (cic:/matita/excess/le_rewl.con _ _ _).
+interpretation "le_rewl" 'lerewritel = (le_rewl _ _ _).
notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}.
-interpretation "le_rewr" 'lerewriter = (cic:/matita/excess/le_rewr.con _ _ _).
+interpretation "le_rewr" 'lerewriter = (le_rewr _ _ _).
lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
qed.
notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}.
-interpretation "ap_rewl" 'aprewritel = (cic:/matita/excess/ap_rewl.con _ _ _).
+interpretation "ap_rewl" 'aprewritel = (ap_rewl _ _ _).
notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
-interpretation "ap_rewr" 'aprewriter = (cic:/matita/excess/ap_rewr.con _ _ _).
+interpretation "ap_rewr" 'aprewriter = (ap_rewr _ _ _).
alias symbol "napart" = "Apartness alikeness".
lemma exc_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
qed.
notation > "'Ex'≪" non associative with precedence 50 for @{'excessrewritel}.
-interpretation "exc_rewl" 'excessrewritel = (cic:/matita/excess/exc_rewl.con _ _ _).
+interpretation "exc_rewl" 'excessrewritel = (exc_rewl _ _ _).
notation > "'Ex'≫" non associative with precedence 50 for @{'excessrewriter}.
-interpretation "exc_rewr" 'excessrewriter = (cic:/matita/excess/exc_rewr.con _ _ _).
+interpretation "exc_rewr" 'excessrewriter = (exc_rewr _ _ _).
lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x.
intros (A x y z E H); split; elim H;
qed.
notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (cic:/matita/excess/lt_rewl.con _ _ _).
+interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (cic:/matita/excess/lt_rewr.con _ _ _).
+interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]
notation "0" with precedence 89 for @{ 'zero }.
-interpretation "Abelian group zero" 'zero =
- (cic:/matita/group/zero.con _).
+interpretation "Abelian group zero" 'zero = (zero _).
-interpretation "Abelian group plus" 'plus a b =
- (cic:/matita/group/plus.con _ a b).
+interpretation "Abelian group plus" 'plus a b = (plus _ a b).
-interpretation "Abelian group opp" 'uminus a =
- (cic:/matita/group/opp.con _ a).
+interpretation "Abelian group opp" 'uminus a = (opp _ a).
definition minus ≝
λG:abelian_group.λa,b:G. a + -b.
-interpretation "Abelian group minus" 'minus a b =
- (cic:/matita/group/minus.con _ a b).
+interpretation "Abelian group minus" 'minus a b = (minus _ a b).
lemma plus_assoc: ∀G:abelian_group.∀x,y,z:G.x+(y+z)≈x+y+z ≝ plus_assoc_.
lemma plus_comm: ∀G:abelian_group.∀x,y:G.x+y≈y+x ≝ plus_comm_.
notation > "x 'is_strong_sup' s 'in' e" non associative with precedence 50 for @{'strong_sup $e $s $x}.
notation > "x 'is_strong_inf' s 'in' e" non associative with precedence 50 for @{'strong_inf $e $s $x}.
-interpretation "Excess upper bound" 'upper_bound e s x = (cic:/matita/infsup/upper_bound.con e s x).
-interpretation "Excess lower bound" 'lower_bound e s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con e) s x).
-interpretation "Excess increasing" 'increasing e s = (cic:/matita/infsup/increasing.con e s).
-interpretation "Excess decreasing" 'decreasing e s = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con e) s).
-interpretation "Excess strong sup" 'strong_sup e s x = (cic:/matita/infsup/strong_sup.con e s x).
-interpretation "Excess strong inf" 'strong_inf e s x = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con e) s x).
+interpretation "Excess upper bound" 'upper_bound e s x = (upper_bound e s x).
+interpretation "Excess lower bound" 'lower_bound e s x = (upper_bound (dual_exc e) s x).
+interpretation "Excess increasing" 'increasing e s = (increasing e s).
+interpretation "Excess decreasing" 'decreasing e s = (increasing (dual_exc e) s).
+interpretation "Excess strong sup" 'strong_sup e s x = (strong_sup e s x).
+interpretation "Excess strong inf" 'strong_inf e s x = (strong_sup (dual_exc e) s x).
lemma strong_sup_is_weak:
∀O:excess.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x.
}.
notation "a \cross b" left associative with precedence 50 for @{ 'op $a $b }.
-interpretation "semi lattice base operation" 'op a b = (cic:/matita/lattice/sl_op.con _ a b).
+interpretation "semi lattice base operation" 'op a b = (sl_op _ a b).
lemma excess_of_semi_lattice_base: semi_lattice_base → excess.
intro l;
sl_lem: ∀x,y.(sl_meet x y) ≤ y
}.
-interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/sl_meet.con _ a b).
+interpretation "semi lattice meet" 'and a b = (sl_meet _ a b).
lemma sl_feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
definition hole ≝ λT:Type.λx:T.x.
notation < "\ldots" non associative with precedence 50 for @{'hole}.
-interpretation "hole" 'hole = (cic:/matita/lattice/hole.con _ _).
+interpretation "hole" 'hole = (hole _ _).
(* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
lemma subst_excess:
coercion cic:/matita/lattice/latt_jcarr.con.
interpretation "Lattice meet" 'and a b =
- (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _) a b).
+ (sl_meet (latt_mcarr _) a b).
interpretation "Lattice join" 'or a b =
- (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).
+ (sl_meet (latt_jcarr _) a b).
record lattice : Type ≝ {
latt_carr:> lattice_;
notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}.
notation "'lej'" non associative with precedence 50 for @{'lej}.
-interpretation "Lattice meet" 'meet = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_refl" 'meet_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_comm" 'meet_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_assoc" 'meet_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice le_to_eqm" 'le_to_eqm = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice lem" 'lem = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice join" 'join = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_refl" 'join_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_comm" 'join_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_assoc" 'join_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice le_to_eqj" 'le_to_eqj = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice lej" 'lej = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice meet" 'meet = (sl_meet (latt_mcarr _)).
+interpretation "Lattice meet_refl" 'meet_refl = (sl_meet_refl (latt_mcarr _)).
+interpretation "Lattice meet_comm" 'meet_comm = (sl_meet_comm (latt_mcarr _)).
+interpretation "Lattice meet_assoc" 'meet_assoc = (sl_meet_assoc (latt_mcarr _)).
+interpretation "Lattice strong_extm" 'strong_extm = (sl_strong_extm (latt_mcarr _)).
+interpretation "Lattice le_to_eqm" 'le_to_eqm = (sl_le_to_eqm (latt_mcarr _)).
+interpretation "Lattice lem" 'lem = (sl_lem (latt_mcarr _)).
+interpretation "Lattice join" 'join = (sl_meet (latt_jcarr _)).
+interpretation "Lattice join_refl" 'join_refl = (sl_meet_refl (latt_jcarr _)).
+interpretation "Lattice join_comm" 'join_comm = (sl_meet_comm (latt_jcarr _)).
+interpretation "Lattice join_assoc" 'join_assoc = (sl_meet_assoc (latt_jcarr _)).
+interpretation "Lattice strong_extm" 'strong_extj = (sl_strong_extm (latt_jcarr _)).
+interpretation "Lattice le_to_eqj" 'le_to_eqj = (sl_le_to_eqm (latt_jcarr _)).
+interpretation "Lattice lej" 'lej = (sl_lem (latt_jcarr _)).
notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
-interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice feq_jl" 'feq_jl = (sl_feq_ml (latt_jcarr _)).
+interpretation "Lattice feq_jr" 'feq_jr = (sl_feq_mr (latt_jcarr _)).
+interpretation "Lattice feq_ml" 'feq_ml = (sl_feq_ml (latt_mcarr _)).
+interpretation "Lattice feq_mr" 'feq_mr = (sl_feq_mr (latt_mcarr _)).
-interpretation "Lattive meet le" 'leq a b =
- (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
+interpretation "Lattive meet le" 'leq a b = (le (excess_OF_lattice1 _) a b).
interpretation "Lattive join le (aka ge)" 'geq a b =
- (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
+ (le (excess_OF_lattice _) a b).
(* these coercions help unification, handmaking a bit of conversion
over an open term
qed.
coercion cic:/matita/lattice/le_to_ge.con nocomposites.
-coercion cic:/matita/lattice/ge_to_le.con nocomposites.
\ No newline at end of file
+coercion cic:/matita/lattice/ge_to_le.con nocomposites.
notation > "x 'is_limsup' s 'in' e" non associative with precedence 50 for @{'limsup $e $s $x}.
notation > "x 'is_liminf' s 'in' e" non associative with precedence 50 for @{'liminf $e $s $x}.
-interpretation "Excess limsup" 'limsup e s x = (cic:/matita/limit/limsup.con e s x).
-interpretation "Excess liminf" 'liminf e s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con e) s x).
+interpretation "Excess limsup" 'limsup e s x = (limsup e s x).
+interpretation "Excess liminf" 'liminf e s x = (limsup (dual_exc e) s x).
(* 3.29 *)
definition lim ≝
notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $_ $s $x}.
notation > "x 'is_lim' s 'in' e" non associative with precedence 50 for @{'lim $e $s $x}.
-interpretation "Excess lim" 'lim e s x = (cic:/matita/limit/lim.con e s x).
+interpretation "Excess lim" 'lim e s x = (lim e s x).
lemma sup_decreasing:
∀E:excess.∀xn:sequence E.
}.
interpretation "Metric lattice leq" 'leq a b =
- (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice1.con _ _) a b).
+ (le (excess_OF_mlattice1 _ _) a b).
interpretation "Metric lattice geq" 'geq a b =
- (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice.con _ _) a b).
+ (le (excess_OF_mlattice _ _) a b).
lemma eq_to_ndlt0: ∀R.∀ml:mlattice R.∀a,b:ml. a ≈ b → ¬ 0 < δ a b.
intros (R ml a b E); intro H; apply E; apply ml_prop1;
}.
notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
-interpretation "metric" 'delta2 a b = (cic:/matita/metric_space/metric.con _ _ a b).
+interpretation "metric" 'delta2 a b = (metric _ _ a b).
notation "\delta" non associative with precedence 80 for @{ 'delta }.
-interpretation "metric" 'delta = (cic:/matita/metric_space/metric.con _ _).
+interpretation "metric" 'delta = (metric _ _).
lemma apart_of_metric_space: ∀R.metric_space R → apartness.
intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;
join: pml_carr → pml_carr → pml_carr
}.
-interpretation "valued lattice meet" 'and a b =
- (cic:/matita/premetric_lattice/meet.con _ _ a b).
+interpretation "valued lattice meet" 'and a b = (meet _ _ a b).
-interpretation "valued lattice join" 'or a b =
- (cic:/matita/premetric_lattice/join.con _ _ a b).
+interpretation "valued lattice join" 'or a b = (join _ _ a b).
record premetric_lattice_props (R : todgroup) (ml : premetric_lattice_ R) : Prop ≝ {
prop1a: ∀a : ml.δ (a ∧ a) a ≈ 0;
apply (prop5 ? pml pml);]
qed.
-coercion cic:/matita/premetric_lattice/lattice_of_pmlattice.con.
\ No newline at end of file
+coercion cic:/matita/premetric_lattice/lattice_of_pmlattice.con.
meet_join_le: ∀x,y,z. value (meet x y) ≤ value (meet x (join y z))
}.
-interpretation "valued lattice meet" 'and a b =
- (cic:/matita/prevalued_lattice/meet.con _ _ a b).
+interpretation "valued lattice meet" 'and a b = (meet _ _ a b).
-interpretation "valued lattice join" 'or a b =
- (cic:/matita/prevalued_lattice/join.con _ _ a b).
+interpretation "valued lattice join" 'or a b = (join _ _ a b).
notation < "\nbsp \mu a" non associative with precedence 80 for @{ 'value2 $a}.
-interpretation "lattice value" 'value2 a = (cic:/matita/prevalued_lattice/value.con _ _ a).
+interpretation "lattice value" 'value2 a = (value _ _ a).
notation "\mu" non associative with precedence 80 for @{ 'value }.
-interpretation "lattice value" 'value = (cic:/matita/prevalued_lattice/value.con _ _).
+interpretation "lattice value" 'value = (value _ _).
lemma feq_joinr: ∀R.∀L:vlattice R.∀x,y,z:L.
μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y).
λR.λms:metric_space R.λs:sequence ms.λk.λn. δ (s n) k.
notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
-interpretation "tends to" 'tends s x =
- (cic:/matita/tend/tends0.con _ (cic:/matita/tend/d2s.con _ _ s x)).
+interpretation "tends to" 'tends s x = (tends0 _ (d2s _ _ s x)).
notation "hvbox(A break ⊆ B)" with precedence 59
for @{ 'subseteq $A $B}.
-interpretation "Subseteq" 'subseteq A B =
- (cic:/matita/formal_topology/leq.con A B).
+interpretation "Subseteq" 'subseteq A B = (leq A B).
axiom leq_refl: ∀A. A ⊆ A.
axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
notation "hvbox(A break ⊆ B)" with precedence 59
for @{ 'subseteq $A $B}.
-interpretation "Subseteq" 'subseteq A B =
- (cic:/matita/formal_topology/leq.con A B).
+interpretation "Subseteq" 'subseteq A B = (leq A B).
axiom leq_refl: ∀A. A ⊆ A.
axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
theorem th8: ∀A. i (m (i A)) = i (m (i (c (i A)))). intros; auto. qed.
theorem th9: ∀A. i (c (m (c (i A)))) = i (m (i A)). intros; auto depth=4. qed.
-(* theorem th7: ∀A. i (m (i A)) = i (s (i A)). *)
\ No newline at end of file
+(* theorem th7: ∀A. i (m (i A)) = i (s (i A)). *)
notation "1" with precedence 89
for @{ 'unit }.
-interpretation "Unit" 'unit =
- cic:/matita/formal_topology/one.con.
+interpretation "Unit" 'unit = one.
axiom one_left: ∀A. 1 A = A.
axiom one_right: ∀A:S. A 1 = A.
notation "hvbox(A break ⊆ B)" with precedence 59
for @{ 'subseteq $A $B}.
-interpretation "Subseteq" 'subseteq A B =
- (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ A
- (cic:/matita/formal_topology/comp.con
- cic:/matita/formal_topology/eps.con B)).
+interpretation "Subseteq" 'subseteq A B = (eq _ A (comp eps B)).
axiom leq_refl: ∀A. A ⊆ A.
axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
theorem th5: ∀A. i (m A) = i (m (c A)). intros; auto. qed.
theorem th6: ∀A. m (i A) = c (m (i A)). intros; auto. qed.
-theorem th7: ∀A. i (m (i A)) = i (s (i A)).
\ No newline at end of file
+theorem th7: ∀A. i (m (i A)) = i (s (i A)).
| (pos m) \Rightarrow True
| (neg m) \Rightarrow m \leq n ]].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/library_autobatch/Z/orders/Zle.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'neither less nor equal to'" 'nleq x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/Z/orders/Zle.con x y)).
+interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
+interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
definition Zlt : Z \to Z \to Prop \def
\lambda x,y:Z.
| (pos m) \Rightarrow True
| (neg m) \Rightarrow m<n ]].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less than'" 'lt x y = (cic:/matita/library_autobatch/Z/orders/Zlt.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'not less than'" 'nless x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/Z/orders/Zlt.con x y)).
+interpretation "integer 'less than'" 'lt x y = (Zlt x y).
+interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
theorem irreflexive_Zlt: irreflexive Z Zlt.
unfold irreflexive.
| GT \Rightarrow (neg (pred (m-n)))]
| (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer plus" 'plus x y = (cic:/matita/library_autobatch/Z/plus/Zplus.con x y).
+interpretation "integer plus" 'plus x y = (Zplus x y).
theorem Zplus_z_OZ: \forall z:Z. z+OZ = z.
intro.
| (pos n) \Rightarrow (neg n)
| (neg n) \Rightarrow (pos n) ].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer unary minus" 'uminus x = (cic:/matita/library_autobatch/Z/plus/Zopp.con x).
+interpretation "integer unary minus" 'uminus x = (Zopp x).
theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y.
intros.
(* minus *)
definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
-interpretation "integer minus" 'minus x y = (cic:/matita/library_autobatch/Z/plus/Zminus.con x y).
+interpretation "integer minus" 'minus x y = (Zminus x y).
| (pos n) \Rightarrow (neg (pred ((S m) * (S n))))
| (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer times" 'times x y = (cic:/matita/library_autobatch/Z/times/Ztimes.con x y).
+interpretation "integer times" 'times x y = (Ztimes x y).
theorem Ztimes_z_OZ: \forall z:Z. z*OZ = OZ.
intro.
definition congruent: nat \to nat \to nat \to Prop \def
\lambda n,m,p:nat. mod n p = mod m p.
-interpretation "congruent" 'congruent n m p =
- (cic:/matita/library_autobatch/nat/congruence/congruent.con n m p).
+interpretation "congruent" 'congruent n m p = (congruent n m p).
notation < "hvbox(n break \cong\sub p m)"
(*non associative*) with precedence 45
[O \Rightarrow m
| (S p) \Rightarrow mod_aux n n p].
-interpretation "natural remainder" 'module x y =
- (cic:/matita/library_autobatch/nat/div_and_mod/mod.con x y).
+interpretation "natural remainder" 'module x y = (mod x y).
let rec div_aux p m n : nat \def
match (leb m n) with
[O \Rightarrow S n
| (S p) \Rightarrow div_aux n n p].
-interpretation "natural divide" 'divide x y =
- (cic:/matita/library_autobatch/nat/div_and_mod/div.con x y).
+interpretation "natural divide" 'divide x y = (div x y).
theorem le_mod_aux_m_m:
\forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.
[ O \Rightarrow (S O)
| (S p) \Rightarrow (times n (exp n p)) ].
-interpretation "natural exponent" 'exp a b = (cic:/matita/library_autobatch/nat/exp/exp.con a b).
+interpretation "natural exponent" 'exp a b = (exp a b).
theorem exp_plus_times : \forall n,p,q:nat.
n \sup (p + q) = (n \sup p) * (n \sup q).
[ O \Rightarrow (S O)
| (S m) \Rightarrow (S m)*(fact m)].
-interpretation "factorial" 'fact n = (cic:/matita/library_autobatch/nat/factorial/fact.con n).
+interpretation "factorial" 'fact n = (fact n).
theorem le_SO_fact : \forall n. (S O) \le n!.
intro.
[O \Rightarrow (S p)
| (S q) \Rightarrow minus p q ]].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural minus" 'minus x y = (cic:/matita/library_autobatch/nat/minus/minus.con x y).
+interpretation "natural minus" 'minus x y = (minus x y).
theorem minus_n_O: \forall n:nat.n=n-O.
intros.
| le_n : le n n
| le_S : \forall m:nat. le n m \to le n (S m).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/library_autobatch/nat/orders/le.ind#xpointer(1/1) x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'neither less nor equal to'" 'nleq x y =
- (cic:/matita/logic/connectives/Not.con
- (cic:/matita/library_autobatch/nat/orders/le.ind#xpointer(1/1) x y)).
+interpretation "natural 'less or equal to'" 'leq x y = (le x y).
+interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
definition lt: nat \to nat \to Prop \def
\lambda n,m:nat.(S n) \leq m.
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'less than'" 'lt x y = (cic:/matita/library_autobatch/nat/orders/lt.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'not less than'" 'nless x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/nat/orders/lt.con x y)).
+interpretation "natural 'less than'" 'lt x y = (lt x y).
+interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
definition ge: nat \to nat \to Prop \def
\lambda n,m:nat.m \leq n.
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/library_autobatch/nat/orders/ge.con x y).
+interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
definition gt: nat \to nat \to Prop \def
\lambda n,m:nat.m<n.
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'greater than'" 'gt x y = (cic:/matita/library_autobatch/nat/orders/gt.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'not greater than'" 'ngtr x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/nat/orders/gt.con x y)).
+interpretation "natural 'greater than'" 'gt x y = (gt x y).
+interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
theorem transitive_le : transitive nat le.
unfold transitive.
right associative with precedence 71
for @{ 'transposition $i $j $n}.
-interpretation "natural transposition" 'transposition i j n =
- (cic:/matita/library_autobatch/nat/permutation/transpose.con i j n).
+interpretation "natural transposition" 'transposition i j n = (transpose i j n).
lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
intros.
]
]
]
-qed.
\ No newline at end of file
+qed.
[ O \Rightarrow m
| (S p) \Rightarrow S (plus p m) ].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural plus" 'plus x y = (cic:/matita/library_autobatch/nat/plus/plus.con x y).
+interpretation "natural plus" 'plus x y = (plus x y).
theorem plus_n_O: \forall n:nat. n = n+O.
intros.elim n
inductive divides (n,m:nat) : Prop \def
witness : \forall p:nat.m = times n p \to divides n m.
-interpretation "divides" 'divides n m = (cic:/matita/library_autobatch/nat/primes/divides.ind#xpointer(1/1) n m).
-interpretation "not divides" 'ndivides n m =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/nat/primes/divides.ind#xpointer(1/1) n m)).
+interpretation "divides" 'divides n m = (divides n m).
+interpretation "not divides" 'ndivides n m = (Not (divides n m)).
theorem reflexive_divides : reflexive nat divides.
unfold reflexive.
[ O \Rightarrow O
| (S p) \Rightarrow m+(times p m) ].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural times" 'times x y = (cic:/matita/library_autobatch/nat/times/times.con x y).
+interpretation "natural times" 'times x y = (times x y).
theorem times_n_O: \forall n:nat. O = n*O.
intros.elim n
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Q/Qaxioms".
-
include "Z/compare.ma".
include "Z/times.ma".
include "nat/iteration2.ma".
(*
theorem geometric: \forall q.\exists k.
Qlt q (sigma_Q k (\lambda x.true) (\lambda x. frac (S O) x)).
-*)
\ No newline at end of file
+*)
qed.
*)
-Qtimes1 == Qtimes_numerator_denominator
-
(*
definition numQ:Q \to Z \def
\lambda q.
|elim f
[reflexivity
|reflexivity
- |apply Qtimes1.
+ |apply Qtimes_numerator_denominator.
]
]
qed.*)
|elim f
[reflexivity
|reflexivity
- |apply Qtimes1.
+ |apply Qtimes_numerator_denominator.
]
]
qed.*)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Q/Qplus".
-
include "nat/factorization.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/compare".
-
include "Z/orders.ma".
include "nat/compare.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/dirichlet_product".
-
include "nat/primes.ma".
include "Z/sigma_p.ma".
include "Z/times.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/inversion".
-
include "Z/dirichlet_product.ma".
include "Z/moebius.ma".
|assumption
]
qed.
-
\ No newline at end of file
+
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/moebius".
-
include "nat/factorization.ma".
include "Z/sigma_p.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/orders".
-
include "Z/z.ma".
include "nat/orders.ma".
| (pos m) \Rightarrow True
| (neg m) \Rightarrow m \leq n ]].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'neither less nor equal to'" 'nleq x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zle.con x y)).
+interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
+interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
definition Zlt : Z \to Z \to Prop \def
\lambda x,y:Z.
| (pos m) \Rightarrow True
| (neg m) \Rightarrow m<n ]].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'not less than'" 'nless x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)).
+interpretation "integer 'less than'" 'lt x y = (Zlt x y).
+interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
theorem irreflexive_Zlt: irreflexive Z Zlt.
unfold irreflexive.unfold Not.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/plus".
-
include "Z/z.ma".
include "nat/minus.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/sigma_p".
-
include "Z/times.ma".
include "nat/primes.ma".
include "nat/ord.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/times".
-
include "nat/lt_arith.ma".
include "Z/plus.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/z".
-
include "datatypes/bool.ma".
include "nat/nat.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/algebra/finite_groups/".
-
include "algebra/groups.ma".
record finite_enumerable (T:Type) : Type≝
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/algebra/groups/".
-
include "algebra/monoids.ma".
include "nat/le_arith.ma".
include "datatypes/bool.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/algebra/monoids/".
-
include "algebra/semigroups.ma".
record PreMonoid : Type ≝
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/algebra/semigroups".
-
include "higher_order_defs/functions.ma".
(* Magmas *)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/datatypes/bool/".
-
include "logic/equality.ma".
include "higher_order_defs/functions.ma".
rewrite > H.
rewrite > H1.
reflexivity.
-qed.
\ No newline at end of file
+qed.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/datatypes/compare/".
-
inductive compare :Set \def
| LT : compare
| EQ : compare
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/datatypes/constructors/".
include "logic/equality.ma".
inductive void : Set \def.
inductive option (A:Type) : Type ≝
None : option A
- | Some : A → option A.
\ No newline at end of file
+ | Some : A → option A.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/decidable/".
-
(* classical connectives for decidable properties *)
include "decidable_kit/streicher.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/eqtype/".
-
include "decidable_kit/decidable.ma".
include "datatypes/constructors.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/fgraph/".
-
include "decidable_kit/fintype.ma".
definition setA : ∀T:eqType.T → bool := λT,x.true.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/fintype/".
-
include "decidable_kit/eqtype.ma".
include "decidable_kit/list_aux.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/list_aux/".
-
include "list/list.ma".
include "decidable_kit/eqtype.ma".
include "nat/plus.ma".
apply H'; reflexivity;]]]]
qed.
-definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).
\ No newline at end of file
+definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/streicher/".
-
include "logic/connectives.ma".
include "logic/equality.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demo/power_derivative".
-
include "nat/plus.ma".
include "nat/orders.ma".
include "nat/compare.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demo/propositional_sequent_calculus/".
-
include "nat/plus.ma".
include "nat/compare.ma".
include "list/sort.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demo/realisability/".
-
include "logic/connectives.ma".
include "datatypes/constructors.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/higher_order_defs/functions/".
-
include "logic/equality.ma".
definition compose \def
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/higher_order_defs/ordering/".
-
include "logic/equality.ma".
definition antisymmetric: \forall A:Type.\forall R:A \to A \to Prop.Prop
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/higher_order_defs/relations/".
-
include "logic/connectives.ma".
definition relation : Type \to Type
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/list/".
include "logic/equality.ma".
include "datatypes/bool.ma".
include "higher_order_defs/functions.ma".
|simplify;apply (bool_elim ? (p a));intro
[simplify;apply le_S_S;assumption
|simplify;apply le_S;assumption]]
-qed.
\ No newline at end of file
+qed.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/logic/coimplication".
-
include "logic/connectives.ma".
definition Iff : Prop \to Prop \to Prop \def
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/logic/connectives/".
-
inductive True: Prop \def
I : True.
ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q.
definition iff :=
- \lambda A,B. (A -> B) \land (B -> A).
\ No newline at end of file
+ \lambda A,B. (A -> B) \land (B -> A).
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/logic/connectives2".
-
include "higher_order_defs/relations.ma".
theorem reflexive_iff: reflexive ? iff.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/logic/equality/".
-
include "higher_order_defs/relations.ma".
inductive eq (A:Type) (x:A) : A \to Prop \def
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/gcd_properties1".
-
include "nat/gcd.ma".
(* this file contains some important properites of gcd in N *)
(* Code ported from the Coq theorem prover by Claudio Sacerdoti Coen *)
(* Original author: Claudio Sacerdoti Coen. for the Coq system *)
-set "baseuri" "cic:/matita/technicalities/setoids".
-
include "datatypes/constructors.ma".
include "logic/coimplication.ma".
include "logic/connectives2.ma".
projects / helm.git / commitdiff