From 9eabe046c1182960de8cfdba96c5414224e3a61e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 9 Jun 2008 20:19:41 +0000 Subject: [PATCH] Most of the time, URIs can now be replaced with identifiers in "interpretation". Warning: identifiers are mapped to URIs according to the last declared alias. --- .../contribs/CoRN/algebra/CoRN/Setoids.ma | 6 +- .../matita/contribs/LOGIC/CLE/defs.ma | 2 +- .../contribs/assembly/freescale/byte8.ma | 3 +- .../contribs/assembly/freescale/extra.ma | 12 ++-- .../contribs/assembly/freescale/status.ma | 8 +-- .../contribs/assembly/freescale/word16.ma | 3 +- .../matita/contribs/dama/dama/bishop_set.ma | 9 +-- .../contribs/dama/dama/bishop_set_rewrite.ma | 19 +++--- .../contribs/dama/dama/cprop_connectives.ma | 12 ++-- .../matita/contribs/dama/dama/extra.ma | 6 +- .../matita/contribs/dama/dama/ordered_set.ma | 9 +-- .../contribs/dama/dama/ordered_uniform.ma | 5 +- .../contribs/dama/dama/property_sigma.ma | 8 +-- .../matita/contribs/dama/dama/supremum.ma | 65 +++++++------------ .../matita/contribs/dama/dama/uniform.ma | 31 ++++----- .../contribs/dama/dama_didactic/bottom.ma | 12 ++-- .../contribs/dama/dama_didactic/deriv.ma | 18 ++--- .../contribs/dama/dama_didactic/reals.ma | 15 ++--- .../attic/integration_algebras.ma | 3 +- .../contribs/dama/dama_duality/attic/rings.ma | 6 +- .../dama/dama_duality/attic/vector_spaces.ma | 3 +- .../classical_pointfree/ordered_sets.ma | 4 +- .../classical_pointfree/ordered_sets2.ma | 2 +- .../dama_duality/classical_pointwise/sets.ma | 31 +++------ .../dama_duality/constructive_connectives.ma | 15 ++--- .../dama/dama_duality/divisible_group.ma | 6 +- .../contribs/dama/dama_duality/excess.ma | 40 ++++++------ .../contribs/dama/dama_duality/group.ma | 12 ++-- .../contribs/dama/dama_duality/infsup.ma | 12 ++-- .../contribs/dama/dama_duality/lattice.ma | 53 ++++++++------- .../contribs/dama/dama_duality/limit.ma | 6 +- .../dama/dama_duality/metric_lattice.ma | 4 +- .../dama/dama_duality/metric_space.ma | 4 +- .../dama/dama_duality/premetric_lattice.ma | 8 +-- .../dama/dama_duality/prevalued_lattice.ma | 10 ++- .../matita/contribs/dama/dama_duality/tend.ma | 3 +- .../formal_topology/bin/formal_topology.ma | 3 +- .../formal_topology/formal_topology.ma | 5 +- .../formal_topology/formal_topology2.ma | 10 +-- .../contribs/library_auto/auto/Z/orders.ma | 14 ++-- .../contribs/library_auto/auto/Z/plus.ma | 8 +-- .../contribs/library_auto/auto/Z/times.ma | 3 +- .../library_auto/auto/nat/congruence.ma | 3 +- .../library_auto/auto/nat/div_and_mod.ma | 6 +- .../contribs/library_auto/auto/nat/exp.ma | 2 +- .../library_auto/auto/nat/factorial.ma | 2 +- .../contribs/library_auto/auto/nat/minus.ma | 3 +- .../contribs/library_auto/auto/nat/orders.ma | 25 ++----- .../library_auto/auto/nat/permutation.ma | 5 +- .../contribs/library_auto/auto/nat/plus.ma | 3 +- .../contribs/library_auto/auto/nat/primes.ma | 5 +- .../contribs/library_auto/auto/nat/times.ma | 3 +- helm/software/matita/library/Q/Qaxioms.ma | 4 +- helm/software/matita/library/Q/frac.ma | 6 +- helm/software/matita/library/Q/q/qplus.ma | 2 - helm/software/matita/library/Z/compare.ma | 2 - .../matita/library/Z/dirichlet_product.ma | 2 - helm/software/matita/library/Z/inversion.ma | 4 +- helm/software/matita/library/Z/moebius.ma | 2 - helm/software/matita/library/Z/orders.ma | 16 ++--- helm/software/matita/library/Z/plus.ma | 2 - helm/software/matita/library/Z/sigma_p.ma | 2 - helm/software/matita/library/Z/times.ma | 2 - helm/software/matita/library/Z/z.ma | 2 - .../matita/library/algebra/finite_groups.ma | 2 - .../software/matita/library/algebra/groups.ma | 2 - .../matita/library/algebra/monoids.ma | 2 - .../matita/library/algebra/semigroups.ma | 2 - .../software/matita/library/datatypes/bool.ma | 4 +- .../matita/library/datatypes/compare.ma | 2 - .../matita/library/datatypes/constructors.ma | 3 +- .../matita/library/decidable_kit/decidable.ma | 2 - .../matita/library/decidable_kit/eqtype.ma | 2 - .../matita/library/decidable_kit/fgraph.ma | 2 - .../matita/library/decidable_kit/fintype.ma | 2 - .../matita/library/decidable_kit/list_aux.ma | 4 +- .../matita/library/decidable_kit/streicher.ma | 2 - .../matita/library/demo/power_derivative.ma | 2 - .../demo/propositional_sequent_calculus.ma | 2 - .../matita/library/demo/realisability.ma | 2 - .../library/higher_order_defs/functions.ma | 2 - .../library/higher_order_defs/ordering.ma | 2 - .../library/higher_order_defs/relations.ma | 2 - helm/software/matita/library/list/list.ma | 3 +- .../matita/library/logic/coimplication.ma | 2 - .../matita/library/logic/connectives.ma | 4 +- .../matita/library/logic/connectives2.ma | 2 - .../software/matita/library/logic/equality.ma | 2 - .../matita/library/nat/gcd_properties1.ma | 2 - .../matita/library/technicalities/setoids.ma | 2 - 90 files changed, 232 insertions(+), 439 deletions(-) diff --git a/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma b/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma index ee5f99610..43c2d45c4 100644 --- a/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma +++ b/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma @@ -47,11 +47,9 @@ record CSetoid : Type \def 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? *) diff --git a/helm/software/matita/contribs/LOGIC/CLE/defs.ma b/helm/software/matita/contribs/LOGIC/CLE/defs.ma index 03065ada0..a354790ed 100644 --- a/helm/software/matita/contribs/LOGIC/CLE/defs.ma +++ b/helm/software/matita/contribs/LOGIC/CLE/defs.ma @@ -26,4 +26,4 @@ inductive CLE: Nat \to Context \to Prop \def . 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). diff --git a/helm/software/matita/contribs/assembly/freescale/byte8.ma b/helm/software/matita/contribs/assembly/freescale/byte8.ma index f3d2e10b4..6f1c48404 100644 --- a/helm/software/matita/contribs/assembly/freescale/byte8.ma +++ b/helm/software/matita/contribs/assembly/freescale/byte8.ma @@ -39,8 +39,7 @@ record byte8 : Type ≝ (* \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)). diff --git a/helm/software/matita/contribs/assembly/freescale/extra.ma b/helm/software/matita/contribs/assembly/freescale/extra.ma index 94f4a4754..bc76c4d6b 100644 --- a/helm/software/matita/contribs/assembly/freescale/extra.ma +++ b/helm/software/matita/contribs/assembly/freescale/extra.ma @@ -57,26 +57,22 @@ definition eq_bool ≝ (* \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 *) diff --git a/helm/software/matita/contribs/assembly/freescale/status.ma b/helm/software/matita/contribs/assembly/freescale/status.ma index e9d374145..4072f445f 100644 --- a/helm/software/matita/contribs/assembly/freescale/status.ma +++ b/helm/software/matita/contribs/assembly/freescale/status.ma @@ -70,7 +70,7 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' 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 ≝ @@ -107,7 +107,7 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' 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 ≝ @@ -149,7 +149,7 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' 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 ≝ @@ -171,7 +171,7 @@ 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 *) diff --git a/helm/software/matita/contribs/assembly/freescale/word16.ma b/helm/software/matita/contribs/assembly/freescale/word16.ma index 98d7703b6..c47ff7d51 100644 --- a/helm/software/matita/contribs/assembly/freescale/word16.ma +++ b/helm/software/matita/contribs/assembly/freescale/word16.ma @@ -39,8 +39,7 @@ record word16 : Type ≝ (* \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)). diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma index 1e7436af9..7ac1b83f0 100644 --- a/helm/software/matita/contribs/dama/dama/bishop_set.ma +++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma @@ -26,8 +26,7 @@ record bishop_set: Type ≝ { 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)); @@ -45,8 +44,7 @@ definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b). 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; @@ -78,8 +76,7 @@ qed. 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); diff --git a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma index 19518a67b..7ead93370 100644 --- a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma +++ b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma @@ -22,8 +22,7 @@ lemma eq_trans:∀E:bishop_set.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝ 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); @@ -36,9 +35,9 @@ intro Xyz; apply Exy; left; assumption; 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] @@ -51,9 +50,9 @@ apply bs_symmetric; 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] @@ -66,9 +65,9 @@ cases (Exy); left; 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. @@ -82,7 +81,7 @@ intros (A x y z E H); split; cases H; 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 _ _ _). diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma index a53961733..91a2335c7 100644 --- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma +++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma @@ -18,25 +18,21 @@ inductive Or (A,B:CProp) : CProp ≝ 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. diff --git a/helm/software/matita/contribs/dama/dama/extra.ma b/helm/software/matita/contribs/dama/dama/extra.ma index d36e0db7e..008d84202 100644 --- a/helm/software/matita/contribs/dama/dama/extra.ma +++ b/helm/software/matita/contribs/dama/dama/extra.ma @@ -20,7 +20,7 @@ definition strong_ext ≝ λA:bishop_set.λop:A→A.∀x,y. op x # op y → x # 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); @@ -51,9 +51,9 @@ intros (A x y z E H); split; cases H; 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)] diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma index 4c72cfd98..c161fee45 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_set.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma @@ -22,17 +22,14 @@ record ordered_set: Type ≝ { 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); diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma index 3bdfbe978..1ca01611f 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -86,8 +86,7 @@ lemma bs_of_ss: λ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. @@ -135,7 +134,7 @@ intros (O l r); apply mk_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". diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma index 9d87b28d5..691d21045 100644 --- a/helm/software/matita/contribs/dama/dama/property_sigma.ma +++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma @@ -62,10 +62,8 @@ qed. 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. @@ -122,4 +120,4 @@ apply H15; [3: apply le_n] 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. diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index a3aa83d6a..50b1ebeda 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -53,18 +53,12 @@ notation > "x 'is_supremum' s" non associative with precedence 50 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". @@ -97,24 +91,24 @@ notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50 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". @@ -185,8 +179,7 @@ notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associati 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 *) @@ -195,13 +188,11 @@ definition segment ≝ λO:ordered_set.λa,b:O.λx:O. 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. @@ -211,8 +202,7 @@ notation < "'fst' \nbsp x" non associative with precedence 50 for @{'pi1 $x}. 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). @@ -228,7 +218,7 @@ qed. 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: @@ -247,18 +237,14 @@ coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B. 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)); @@ -275,8 +261,7 @@ notation < "s 2 \atop \nleq" non associative with precedence 90 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. @@ -302,14 +287,14 @@ notation < "s \nbsp 'is_upper_located'" non associative with precedence 50 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: @@ -328,4 +313,4 @@ cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W); |2: right; exists [apply u]; split; [apply W|apply H4]] qed. - \ No newline at end of file + diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma index 41b593ae4..25cfe67cb 100644 --- a/helm/software/matita/contribs/dama/dama/uniform.ma +++ b/helm/software/matita/contribs/dama/dama/uniform.ma @@ -29,23 +29,19 @@ definition subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x. 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". @@ -56,12 +52,11 @@ definition compose_relations ≝ 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. @@ -73,10 +68,8 @@ notation < "s \sup (-1) x" non associative with precedence 90 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". @@ -103,8 +96,7 @@ notation < "a \nbsp 'is_cauchy'" non associative with precedence 50 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 ≝ @@ -116,7 +108,7 @@ notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative 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 : @@ -133,8 +125,7 @@ qed. (* 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. diff --git a/helm/software/matita/contribs/dama/dama_didactic/bottom.ma b/helm/software/matita/contribs/dama/dama_didactic/bottom.ma index 161063b42..a759416ed 100644 --- a/helm/software/matita/contribs/dama/dama_didactic/bottom.ma +++ b/helm/software/matita/contribs/dama/dama_didactic/bottom.ma @@ -30,8 +30,7 @@ notation "hvbox(a break ≡ b)" 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). @@ -62,14 +61,11 @@ axiom Relev: L R→L R→L R. 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 diff --git a/helm/software/matita/contribs/dama/dama_didactic/deriv.ma b/helm/software/matita/contribs/dama/dama_didactic/deriv.ma index 5c2e734c0..232a91b5e 100644 --- a/helm/software/matita/contribs/dama/dama_didactic/deriv.ma +++ b/helm/software/matita/contribs/dama/dama_didactic/deriv.ma @@ -25,19 +25,15 @@ axiom De: F→F. (*funzione derivata*) 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. @@ -48,8 +44,7 @@ axiom freflex:F. 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*) @@ -108,7 +103,6 @@ notation "hvbox(a break ^ b)" 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). diff --git a/helm/software/matita/contribs/dama/dama_didactic/reals.ma b/helm/software/matita/contribs/dama/dama_didactic/reals.ma index 3328c0e96..4dffb53fb 100644 --- a/helm/software/matita/contribs/dama/dama_didactic/reals.ma +++ b/helm/software/matita/contribs/dama/dama_didactic/reals.ma @@ -27,24 +27,19 @@ axiom Relev: R→R→R. 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 diff --git a/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma b/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma index 1b775fa78..da3299b64 100644 --- a/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma +++ b/helm/software/matita/contribs/dama/dama_duality/attic/integration_algebras.ma @@ -312,8 +312,7 @@ record algebra (K: field) : Type \def 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. diff --git a/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma b/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma index d4db003dc..7b9eae009 100644 --- a/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma +++ b/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma @@ -65,14 +65,12 @@ theorem not_eq_zero_one: ∀R:ring.0 ≠ one R. 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; diff --git a/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma b/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma index 5002b022c..71fe1a81b 100644 --- a/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma +++ b/helm/software/matita/contribs/dama/dama_duality/attic/vector_spaces.ma @@ -30,8 +30,7 @@ record vector_space (K:field): Type \def 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; diff --git a/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets.ma b/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets.ma index 2630da77c..280f409cf 100644 --- a/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets.ma +++ b/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets.ma @@ -320,10 +320,10 @@ notation "hvbox(〈a〉)" 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. diff --git a/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets2.ma b/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets2.ma index 7e74cbba2..b48c820a8 100644 --- a/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets2.ma +++ b/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets2.ma @@ -61,7 +61,7 @@ theorem le_to_le_sup_sup: 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. diff --git a/helm/software/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma b/helm/software/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma index f03c3e7f2..5b8bdd7bd 100644 --- a/helm/software/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma +++ b/helm/software/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma @@ -25,30 +25,25 @@ definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x. 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. @@ -56,16 +51,14 @@ definition intersection: ∀X. set X → set X → set X ≝ 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. @@ -74,8 +67,7 @@ definition nth ≝ λX.λA:seq X.λi.A i. 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. @@ -83,16 +75,14 @@ definition countable_union: ∀X. seq (set X) → set X ≝ 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. @@ -100,5 +90,4 @@ definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝ 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). diff --git a/helm/software/matita/contribs/dama/dama_duality/constructive_connectives.ma b/helm/software/matita/contribs/dama/dama_duality/constructive_connectives.ma index 78e2ec571..4d2ea5996 100644 --- a/helm/software/matita/contribs/dama/dama_duality/constructive_connectives.ma +++ b/helm/software/matita/contribs/dama/dama_duality/constructive_connectives.ma @@ -18,14 +18,12 @@ inductive Or (A,B:Type) : Type ≝ 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. @@ -41,13 +39,10 @@ for @{ 'sigma ${default @{\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). diff --git a/helm/software/matita/contribs/dama/dama_duality/divisible_group.ma b/helm/software/matita/contribs/dama/dama_duality/divisible_group.ma index 3a79b11bb..378993550 100644 --- a/helm/software/matita/contribs/dama/dama_duality/divisible_group.ma +++ b/helm/software/matita/contribs/dama/dama_duality/divisible_group.ma @@ -20,8 +20,7 @@ include "group.ma". 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; @@ -32,8 +31,7 @@ lemma divide: ∀G:dgroup.G → nat → G. 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. diff --git a/helm/software/matita/contribs/dama/dama_duality/excess.ma b/helm/software/matita/contribs/dama/dama_duality/excess.ma index 9068d297b..f29c5a362 100644 --- a/helm/software/matita/contribs/dama/dama_duality/excess.ma +++ b/helm/software/matita/contribs/dama/dama_duality/excess.ma @@ -26,7 +26,7 @@ record excess_base : Type ≝ { 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. @@ -62,7 +62,7 @@ record apartness : Type ≝ { }. 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)); @@ -90,7 +90,7 @@ qed. 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_; @@ -99,20 +99,20 @@ record excess : Type ≝ { }. 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); @@ -126,9 +126,9 @@ qed. 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; @@ -153,7 +153,7 @@ lemma eq_trans:∀E:apartness.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝ λ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: @@ -164,7 +164,7 @@ qed. 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); @@ -197,9 +197,9 @@ intro Xyz; apply Exy; apply exc2ap; left; assumption; 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] @@ -212,9 +212,9 @@ apply ap_symmetric; 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. @@ -228,9 +228,9 @@ elim (Exy); apply exc2ap; left; assumption; 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; @@ -243,9 +243,9 @@ 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)] diff --git a/helm/software/matita/contribs/dama/dama_duality/group.ma b/helm/software/matita/contribs/dama/dama_duality/group.ma index 104dcf274..276d409a6 100644 --- a/helm/software/matita/contribs/dama/dama_duality/group.ma +++ b/helm/software/matita/contribs/dama/dama_duality/group.ma @@ -44,20 +44,16 @@ record abelian_group : Type ≝ 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_. diff --git a/helm/software/matita/contribs/dama/dama_duality/infsup.ma b/helm/software/matita/contribs/dama/dama_duality/infsup.ma index cc3292fd0..b5ff03f0a 100644 --- a/helm/software/matita/contribs/dama/dama_duality/infsup.ma +++ b/helm/software/matita/contribs/dama/dama_duality/infsup.ma @@ -39,12 +39,12 @@ notation > "s 'is_decreasing' 'in' e" non associative with precedence 50 for 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. diff --git a/helm/software/matita/contribs/dama/dama_duality/lattice.ma b/helm/software/matita/contribs/dama/dama_duality/lattice.ma index adf751b83..4da043bcc 100644 --- a/helm/software/matita/contribs/dama/dama_duality/lattice.ma +++ b/helm/software/matita/contribs/dama/dama_duality/lattice.ma @@ -24,7 +24,7 @@ record semi_lattice_base : Type ≝ { }. 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; @@ -80,7 +80,7 @@ record semi_lattice : Type ≝ { 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 ⊢ %; @@ -183,7 +183,7 @@ qed. 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: @@ -412,10 +412,10 @@ qed. 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_; @@ -438,36 +438,35 @@ notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}. 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 @@ -481,4 +480,4 @@ intros(l a b H); apply H; 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. diff --git a/helm/software/matita/contribs/dama/dama_duality/limit.ma b/helm/software/matita/contribs/dama/dama_duality/limit.ma index 1250511e8..0b1bd1d3b 100644 --- a/helm/software/matita/contribs/dama/dama_duality/limit.ma +++ b/helm/software/matita/contribs/dama/dama_duality/limit.ma @@ -27,8 +27,8 @@ notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for 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 ≝ @@ -36,7 +36,7 @@ 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. diff --git a/helm/software/matita/contribs/dama/dama_duality/metric_lattice.ma b/helm/software/matita/contribs/dama/dama_duality/metric_lattice.ma index 010360757..45e437955 100644 --- a/helm/software/matita/contribs/dama/dama_duality/metric_lattice.ma +++ b/helm/software/matita/contribs/dama/dama_duality/metric_lattice.ma @@ -40,9 +40,9 @@ record mlattice (R : todgroup) : Type ≝ { }. 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; diff --git a/helm/software/matita/contribs/dama/dama_duality/metric_space.ma b/helm/software/matita/contribs/dama/dama_duality/metric_space.ma index 2266fe9e9..cda8d3fc7 100644 --- a/helm/software/matita/contribs/dama/dama_duality/metric_space.ma +++ b/helm/software/matita/contribs/dama/dama_duality/metric_space.ma @@ -24,9 +24,9 @@ record metric_space (R: todgroup) : Type ≝ { }. 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; diff --git a/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma b/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma index 6c904055c..5c5fca20a 100644 --- a/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma +++ b/helm/software/matita/contribs/dama/dama_duality/premetric_lattice.ma @@ -22,11 +22,9 @@ record premetric_lattice_ (R : todgroup) : Type ≝ { 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; @@ -67,4 +65,4 @@ try (apply ap_symmetric; assumption); intros 4 (x y z H); change with (0 < (δ y 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. diff --git a/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma b/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma index 53b2b0a1b..bf4a26643 100644 --- a/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma +++ b/helm/software/matita/contribs/dama/dama_duality/prevalued_lattice.ma @@ -34,17 +34,15 @@ record vlattice (R : togroup) : Type ≝ { 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). diff --git a/helm/software/matita/contribs/dama/dama_duality/tend.ma b/helm/software/matita/contribs/dama/dama_duality/tend.ma index a5bf7501a..84d30a8fe 100644 --- a/helm/software/matita/contribs/dama/dama_duality/tend.ma +++ b/helm/software/matita/contribs/dama/dama_duality/tend.ma @@ -23,6 +23,5 @@ definition d2s ≝ λ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)). diff --git a/helm/software/matita/contribs/formal_topology/bin/formal_topology.ma b/helm/software/matita/contribs/formal_topology/bin/formal_topology.ma index 1c1d94ad6..e84c0242e 100644 --- a/helm/software/matita/contribs/formal_topology/bin/formal_topology.ma +++ b/helm/software/matita/contribs/formal_topology/bin/formal_topology.ma @@ -22,8 +22,7 @@ axiom leq: S → S → Prop. 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. diff --git a/helm/software/matita/contribs/formal_topology/formal_topology.ma b/helm/software/matita/contribs/formal_topology/formal_topology.ma index 89ab9484c..34a521f35 100644 --- a/helm/software/matita/contribs/formal_topology/formal_topology.ma +++ b/helm/software/matita/contribs/formal_topology/formal_topology.ma @@ -22,8 +22,7 @@ axiom leq: S → S → Prop. 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. @@ -111,4 +110,4 @@ theorem th7: ∀A. i (m (i A)) = i (c (i (m (i A)))). intros; auto. qed. 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)). *) diff --git a/helm/software/matita/contribs/formal_topology/formal_topology2.ma b/helm/software/matita/contribs/formal_topology/formal_topology2.ma index b98865a5c..10666ba35 100644 --- a/helm/software/matita/contribs/formal_topology/formal_topology2.ma +++ b/helm/software/matita/contribs/formal_topology/formal_topology2.ma @@ -27,8 +27,7 @@ axiom one: S. 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. @@ -39,10 +38,7 @@ axiom eps_idempotent: eps = eps eps. 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. @@ -74,4 +70,4 @@ theorem th4: ∀A. c A ⊆ (m (i (m A))). intros; auto. qed. 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)). diff --git a/helm/software/matita/contribs/library_auto/auto/Z/orders.ma b/helm/software/matita/contribs/library_auto/auto/Z/orders.ma index a90ceadce..d74f8de9b 100644 --- a/helm/software/matita/contribs/library_auto/auto/Z/orders.ma +++ b/helm/software/matita/contribs/library_auto/auto/Z/orders.ma @@ -36,11 +36,8 @@ definition Zle : Z \to Z \to Prop \def | (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. @@ -61,11 +58,8 @@ definition Zlt : Z \to Z \to Prop \def | (pos m) \Rightarrow True | (neg m) \Rightarrow m commutative_dirichlet_product |assumption ] qed. - \ No newline at end of file + diff --git a/helm/software/matita/library/Z/moebius.ma b/helm/software/matita/library/Z/moebius.ma index 1eb358521..b9d12c223 100644 --- a/helm/software/matita/library/Z/moebius.ma +++ b/helm/software/matita/library/Z/moebius.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Z/moebius". - include "nat/factorization.ma". include "Z/sigma_p.ma". diff --git a/helm/software/matita/library/Z/orders.ma b/helm/software/matita/library/Z/orders.ma index 06b6a1ec4..1f8a6d337 100644 --- a/helm/software/matita/library/Z/orders.ma +++ b/helm/software/matita/library/Z/orders.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Z/orders". - include "Z/z.ma". include "nat/orders.ma". @@ -36,11 +34,8 @@ definition Zle : Z \to Z \to Prop \def | (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. @@ -61,11 +56,8 @@ definition Zlt : Z \to Z \to Prop \def | (pos m) \Rightarrow True | (neg m) \Rightarrow m H. rewrite > H1. reflexivity. -qed. \ No newline at end of file +qed. diff --git a/helm/software/matita/library/datatypes/compare.ma b/helm/software/matita/library/datatypes/compare.ma index c4fd119a5..57784b2a0 100644 --- a/helm/software/matita/library/datatypes/compare.ma +++ b/helm/software/matita/library/datatypes/compare.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/datatypes/compare/". - inductive compare :Set \def | LT : compare | EQ : compare diff --git a/helm/software/matita/library/datatypes/constructors.ma b/helm/software/matita/library/datatypes/constructors.ma index dd2a1760b..926dd35fc 100644 --- a/helm/software/matita/library/datatypes/constructors.ma +++ b/helm/software/matita/library/datatypes/constructors.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/datatypes/constructors/". include "logic/equality.ma". inductive void : Set \def. @@ -68,4 +67,4 @@ interpretation "Disjoint union" 'plus A B = inductive option (A:Type) : Type ≝ None : option A - | Some : A → option A. \ No newline at end of file + | Some : A → option A. diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma index 9c2f8890b..c1a8d5816 100644 --- a/helm/software/matita/library/decidable_kit/decidable.ma +++ b/helm/software/matita/library/decidable_kit/decidable.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/decidable_kit/decidable/". - (* classical connectives for decidable properties *) include "decidable_kit/streicher.ma". diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma index 35f404df3..4b248a97e 100644 --- a/helm/software/matita/library/decidable_kit/eqtype.ma +++ b/helm/software/matita/library/decidable_kit/eqtype.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/decidable_kit/eqtype/". - include "decidable_kit/decidable.ma". include "datatypes/constructors.ma". diff --git a/helm/software/matita/library/decidable_kit/fgraph.ma b/helm/software/matita/library/decidable_kit/fgraph.ma index 2d02d113d..d22c159d0 100644 --- a/helm/software/matita/library/decidable_kit/fgraph.ma +++ b/helm/software/matita/library/decidable_kit/fgraph.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/decidable_kit/fgraph/". - include "decidable_kit/fintype.ma". definition setA : ∀T:eqType.T → bool := λT,x.true. diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma index 9d6b30e59..e44b64197 100644 --- a/helm/software/matita/library/decidable_kit/fintype.ma +++ b/helm/software/matita/library/decidable_kit/fintype.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/decidable_kit/fintype/". - include "decidable_kit/eqtype.ma". include "decidable_kit/list_aux.ma". diff --git a/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma index a7db00c72..a5bf2edb7 100644 --- a/helm/software/matita/library/decidable_kit/list_aux.ma +++ b/helm/software/matita/library/decidable_kit/list_aux.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/decidable_kit/list_aux/". - include "list/list.ma". include "decidable_kit/eqtype.ma". include "nat/plus.ma". @@ -70,4 +68,4 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ] 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). diff --git a/helm/software/matita/library/decidable_kit/streicher.ma b/helm/software/matita/library/decidable_kit/streicher.ma index 83c6f6169..96903da9e 100644 --- a/helm/software/matita/library/decidable_kit/streicher.ma +++ b/helm/software/matita/library/decidable_kit/streicher.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/decidable_kit/streicher/". - include "logic/connectives.ma". include "logic/equality.ma". diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index 590c5c07e..76fa66115 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/demo/power_derivative". - include "nat/plus.ma". include "nat/orders.ma". include "nat/compare.ma". diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma index fb5278d6b..36bb7e863 100644 --- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma +++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/demo/propositional_sequent_calculus/". - include "nat/plus.ma". include "nat/compare.ma". include "list/sort.ma". diff --git a/helm/software/matita/library/demo/realisability.ma b/helm/software/matita/library/demo/realisability.ma index 0de10940a..93b5e712f 100644 --- a/helm/software/matita/library/demo/realisability.ma +++ b/helm/software/matita/library/demo/realisability.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/demo/realisability/". - include "logic/connectives.ma". include "datatypes/constructors.ma". diff --git a/helm/software/matita/library/higher_order_defs/functions.ma b/helm/software/matita/library/higher_order_defs/functions.ma index a1b54c80c..a6174f48f 100644 --- a/helm/software/matita/library/higher_order_defs/functions.ma +++ b/helm/software/matita/library/higher_order_defs/functions.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/higher_order_defs/functions/". - include "logic/equality.ma". definition compose \def diff --git a/helm/software/matita/library/higher_order_defs/ordering.ma b/helm/software/matita/library/higher_order_defs/ordering.ma index c2b351d7a..c41160e44 100644 --- a/helm/software/matita/library/higher_order_defs/ordering.ma +++ b/helm/software/matita/library/higher_order_defs/ordering.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -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 diff --git a/helm/software/matita/library/higher_order_defs/relations.ma b/helm/software/matita/library/higher_order_defs/relations.ma index 3e92649c1..4d4155c56 100644 --- a/helm/software/matita/library/higher_order_defs/relations.ma +++ b/helm/software/matita/library/higher_order_defs/relations.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/higher_order_defs/relations/". - include "logic/connectives.ma". definition relation : Type \to Type diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma index f9f39bebf..f3738eca1 100644 --- a/helm/software/matita/library/list/list.ma +++ b/helm/software/matita/library/list/list.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/list/". include "logic/equality.ma". include "datatypes/bool.ma". include "higher_order_defs/functions.ma". @@ -194,4 +193,4 @@ intros;elim l |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. diff --git a/helm/software/matita/library/logic/coimplication.ma b/helm/software/matita/library/logic/coimplication.ma index a963846f0..a8fc4a232 100644 --- a/helm/software/matita/library/logic/coimplication.ma +++ b/helm/software/matita/library/logic/coimplication.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/logic/coimplication". - include "logic/connectives.ma". definition Iff : Prop \to Prop \to Prop \def diff --git a/helm/software/matita/library/logic/connectives.ma b/helm/software/matita/library/logic/connectives.ma index 5afc3e5dc..ba229870f 100644 --- a/helm/software/matita/library/logic/connectives.ma +++ b/helm/software/matita/library/logic/connectives.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/logic/connectives/". - inductive True: Prop \def I : True. @@ -83,4 +81,4 @@ inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def 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). diff --git a/helm/software/matita/library/logic/connectives2.ma b/helm/software/matita/library/logic/connectives2.ma index bc577a5f4..a41c691d5 100644 --- a/helm/software/matita/library/logic/connectives2.ma +++ b/helm/software/matita/library/logic/connectives2.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/logic/connectives2". - include "higher_order_defs/relations.ma". theorem reflexive_iff: reflexive ? iff. diff --git a/helm/software/matita/library/logic/equality.ma b/helm/software/matita/library/logic/equality.ma index 01c60e8fc..308652d7d 100644 --- a/helm/software/matita/library/logic/equality.ma +++ b/helm/software/matita/library/logic/equality.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/logic/equality/". - include "higher_order_defs/relations.ma". inductive eq (A:Type) (x:A) : A \to Prop \def diff --git a/helm/software/matita/library/nat/gcd_properties1.ma b/helm/software/matita/library/nat/gcd_properties1.ma index 776b38adf..8174465c6 100644 --- a/helm/software/matita/library/nat/gcd_properties1.ma +++ b/helm/software/matita/library/nat/gcd_properties1.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/gcd_properties1". - include "nat/gcd.ma". (* this file contains some important properites of gcd in N *) diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma index 35f3b0920..fd1fb0037 100644 --- a/helm/software/matita/library/technicalities/setoids.ma +++ b/helm/software/matita/library/technicalities/setoids.ma @@ -15,8 +15,6 @@ (* 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". -- 2.39.2