X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Procedural%2Falgebra%2FBasics.mma;h=5e862ff9fa749223008dea9d99392bad18dc5b36;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=598f294a1b03a5e6864376c23f59d77994f636f9;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Procedural/algebra/Basics.mma b/helm/software/matita/contribs/CoRN-Procedural/algebra/Basics.mma index 598f294a1..5e862ff9f 100644 --- a/helm/software/matita/contribs/CoRN-Procedural/algebra/Basics.mma +++ b/helm/software/matita/contribs/CoRN-Procedural/algebra/Basics.mma @@ -42,26 +42,26 @@ include "algebra/ListType.ma". This is random stuff that should be in the Coq basic library. *) -inline procedural "cic:/CoRN/algebra/Basics/lt_le_dec.con". +inline procedural "cic:/CoRN/algebra/Basics/lt_le_dec.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/lt_z_two.con". +inline procedural "cic:/CoRN/algebra/Basics/lt_z_two.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/le_pred.con". +inline procedural "cic:/CoRN/algebra/Basics/le_pred.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/lt_mult_right.con". +inline procedural "cic:/CoRN/algebra/Basics/lt_mult_right.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/le_mult_right.con". +inline procedural "cic:/CoRN/algebra/Basics/le_mult_right.con" as lemma. (*#* The power function does not exist in the standard library *) -inline procedural "cic:/CoRN/algebra/Basics/power.con". +inline procedural "cic:/CoRN/algebra/Basics/power.con" as definition. (*#* Factorial function. Does not exist in Arith. Needed for special operations on polynomials. *) -inline procedural "cic:/CoRN/algebra/Basics/fac.con". +inline procedural "cic:/CoRN/algebra/Basics/fac.con" as definition. -inline procedural "cic:/CoRN/algebra/Basics/nat_fac_gtzero.con". +inline procedural "cic:/CoRN/algebra/Basics/nat_fac_gtzero.con" as lemma. (* needed for computational behavior of "Inversion" tactic *) @@ -119,9 +119,9 @@ Intros. Right. Reflexivity. Qed. *) -inline procedural "cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con". +inline procedural "cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con". +inline procedural "cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con" as lemma. (* begin hide *) @@ -148,31 +148,31 @@ cic:/Coq/ZArith/BinInt/Z_of_nat.con (* end hide *) -inline procedural "cic:/CoRN/algebra/Basics/POS_anti_convert.con". +inline procedural "cic:/CoRN/algebra/Basics/POS_anti_convert.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/NEG_anti_convert.con". +inline procedural "cic:/CoRN/algebra/Basics/NEG_anti_convert.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con". +inline procedural "cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con". +inline procedural "cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con". +inline procedural "cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/convert_is_POS.con". +inline procedural "cic:/CoRN/algebra/Basics/convert_is_POS.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/min_convert_is_NEG.con". +inline procedural "cic:/CoRN/algebra/Basics/min_convert_is_NEG.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/inject_nat_convert.con". +inline procedural "cic:/CoRN/algebra/Basics/inject_nat_convert.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/Z_exh.con". +inline procedural "cic:/CoRN/algebra/Basics/Z_exh.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/nats_Z_ind.con". +inline procedural "cic:/CoRN/algebra/Basics/nats_Z_ind.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con". +inline procedural "cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con". +inline procedural "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con". +inline procedural "cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con" as lemma. (* begin hide *) @@ -186,7 +186,7 @@ Unset Strict Implicit. (* end hide *) -inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff.con". +inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff.con" as definition. (* begin hide *) @@ -200,25 +200,25 @@ Unset Implicit Arguments. (* end hide *) -inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_O.con". +inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_O.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con". +inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con". +inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/proper_caseZ_diff.con". +inline procedural "cic:/CoRN/algebra/Basics/proper_caseZ_diff.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/diff_Z_ind.con". +inline procedural "cic:/CoRN/algebra/Basics/diff_Z_ind.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con". +inline procedural "cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/Zlt_opp.con". +inline procedural "cic:/CoRN/algebra/Basics/Zlt_opp.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con". +inline procedural "cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/Zgt_not_eq.con". +inline procedural "cic:/CoRN/algebra/Basics/Zgt_not_eq.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/Zmult_absorb.con". +inline procedural "cic:/CoRN/algebra/Basics/Zmult_absorb.con" as lemma. (* UNEXPORTED Section Well_foundedT @@ -242,7 +242,7 @@ Section AccT alias id "A" = "cic:/CoRN/algebra/Basics/AccT/A.var". -inline procedural "cic:/CoRN/algebra/Basics/well_founded.con". +inline procedural "cic:/CoRN/algebra/Basics/well_founded.con" as definition. (* UNEXPORTED End AccT @@ -268,9 +268,9 @@ alias id "P" = "cic:/CoRN/algebra/Basics/IndT/AccIter/P.var". alias id "F" = "cic:/CoRN/algebra/Basics/IndT/AccIter/F.var". -inline procedural "cic:/CoRN/algebra/Basics/Acc_inv.con". +inline procedural "cic:/CoRN/algebra/Basics/Acc_inv.con" as lemma. -inline procedural "cic:/CoRN/algebra/Basics/Acc_iter.con". +inline procedural "cic:/CoRN/algebra/Basics/Acc_iter.con" as definition. (* UNEXPORTED End AccIter @@ -278,7 +278,7 @@ End AccIter alias id "Rwf" = "cic:/CoRN/algebra/Basics/IndT/Rwf.var". -inline procedural "cic:/CoRN/algebra/Basics/well_founded_induction_type.con". +inline procedural "cic:/CoRN/algebra/Basics/well_founded_induction_type.con" as theorem. (* UNEXPORTED End IndT @@ -292,11 +292,11 @@ alias id "A" = "cic:/CoRN/algebra/Basics/InductionT/A.var". alias id "f" = "cic:/CoRN/algebra/Basics/InductionT/f.var". -inline procedural "cic:/CoRN/algebra/Basics/ltof.con". +inline procedural "cic:/CoRN/algebra/Basics/ltof.con" as definition. -inline procedural "cic:/CoRN/algebra/Basics/well_founded_ltof.con". +inline procedural "cic:/CoRN/algebra/Basics/well_founded_ltof.con" as theorem. -inline procedural "cic:/CoRN/algebra/Basics/induction_ltof2T.con". +inline procedural "cic:/CoRN/algebra/Basics/induction_ltof2T.con" as theorem. (* UNEXPORTED End InductionT @@ -306,7 +306,7 @@ End InductionT Section InductionTT *) -inline procedural "cic:/CoRN/algebra/Basics/lt_wf_rect.con". +inline procedural "cic:/CoRN/algebra/Basics/lt_wf_rect.con" as lemma. (* UNEXPORTED End InductionTT