Commit fa67ab94 authored by Sven Wille's avatar Sven Wille

finseq continued (bugfix where mmt confuses nat with real)

parent 86748f17
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#0.0.0:2812.73.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#108.4.0:128.4.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#409.15.0:433.15.24"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#0.0.0:3034.76.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#108.4.0:128.4.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#409.15.0:433.15.24"/></metadata></mref></omdoc>
\ No newline at end of file
......@@ -25,6 +25,8 @@ datatypeconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmeti
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?axiom_associativePlus
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?axiom_leftUnitalPlus
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_rightUnitalPlus
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le
theory http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics
HasMeta http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentSymbol
......@@ -327,3 +329,24 @@ DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_r
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_rightUnitalPlus?type http://cds.omdoc.org/urtheories?NatSymbols?NAT?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_rightUnitalPlus?type http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_rightUnitalPlus?definition http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?axiom_plus1?type
Declares http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt
constant http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt?type http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthan?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt?type http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers?succ?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt?type http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt?type http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthan?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt?type http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers?succ?definition
Declares http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le
constant http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers?succ?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leq?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leq?definition
......@@ -10,7 +10,7 @@ theory FinSequences : base:?Logic =
finSeq : ℕ ⟶ type ⟶ type ❘= [n , A] {m : ℕ} ⊦ m < n ⟶ A ❙
disjointFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n,A,fs] ∀[x] ∀[y] ∀ [h : ⊦ x < n] ∀ [h0 : ⊦ y < n] y ≐ x ∨ fs x h ≠ fs y h0❙
// disjointFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n,A,fs] ∀[x] ∀[y] ∀ [h : ⊦ x < n] ∀ [h0 : ⊦ y < n] y ≐ x ∨ fs x h ≠ fs y h0❙
......@@ -18,11 +18,13 @@ theory FinSequences : base:?Logic =
theory FinSeqSum : base:?Logic =
include ?FinSequences ❙
include arith:?RealArithmetics ❙
include arith:?NaturalArithmetics ❙
// this one does the actual recusive summation and is called by finSeqSum ❙
finSeqSumRec : {n : ℕ} {m : ℕ } ⊦ m < n ⟶ finSeq n ℝ ⟶ ℝ ❘# finSeqSumR 2 3 4❙
finSeqSumRecB : {n : ℕ} {sq : finSeq n ℝ} {h : ⊦ 0 < n} ⊦ finSeqSumR 0 h sq ≐ sq 0 h ❙
finSeqSumRecS : {n : ℕ} {m : ℕ} {sq : finSeq n ℝ} {h : ⊦ `arith:?NaturalNumbers?succ m < n}
finSeqSumRec : {n : ℕ} {m : ℕ } ⊦ `arith:?NaturalArithmetics?lessthan m n ⟶ finSeq n ℝ ⟶ ℝ ❘# finSeqSumR 2 3 4❙
finSeqSumRecB : {n : ℕ} {sq : finSeq n ℝ} {h : ⊦ `arith:?NaturalArithmetics?lessthan 0 n} ⊦ finSeqSumRec n 0 h sq ≐ sq 0 h ❙
// finSeqSumRecS : {n : ℕ} {m : ℕ} {sq : finSeq n ℝ} {h : ⊦ `arith:?NaturalNumbers?succ m < n}
⊦ finSeqSumR ( `arith:?NaturalNumbers?succ m) h sq ≐
sq (`arith:?NaturalNumbers?succ m) h + finSeqSumR m (lt_pred_lt h) sq❙
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment