Commit 86748f17 by Sven Wille

### finseq continued

parent b6140c48
 ... ... @@ -70,6 +70,9 @@ theory NaturalArithmetics : base:?Logic = axiom_associativePlus : {x: ℕ,y,z} ⊦ x + (y + z) ≐ (x + y) + z ❘ # associative_plus_nat 1 2 3❙ axiom_leftUnitalPlus : {x : ℕ} ⊦ 0 + x ≐ x ❘ # leftunital_plus_nat ❙ lemma_rightUnitalPlus : {x : ℕ} ⊦ x + 0 ≐ x ❘ = axiom_plus1 ❘ # rightunital_plus_nat ❙ // added by sw ❙ lemma_lt_pred_lt : {x : ℕ , n : ℕ } ⊦ `?NaturalNumbers?succ x < n ⟶ ⊦ x < n ❘# lt_pred_lt 3❙ lemma_le_pred_le : {x : ℕ , n : ℕ } ⊦ (`?NaturalNumbers?succ : ℕ ⟶ ℕ) x ≤ n ⟶ ⊦ x ≤ n ❘# le_pred_le 3❙ ❚
 ... ... @@ -5,38 +5,30 @@ import base http://mathhub.info/MitM/Foundation ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory FinSequences : base:?Logic = include arith:?RealArithmetics ❙ below : ℕ ⟶ type ❘ = [n] ⟨ x : ℕ | ⊦ x < n ⟩ ❙ // toBelow : {n : ℕ} below (Succ n) ❘# toB 1❙ // succBelow : {n : ℕ} below n ⟶ below (Succ n) ❘# succB 2❙ // belowIsSubtypeOfNat : {n : ℕ} (below n) <* ℕ ❙ // belowToNat : {n : ℕ} below (Succ n) ⟶ ℕ ❘# btn 1 2❙ // belowToNatBaseCase : {m : ℕ} ⊦ belowToNat m (toBelow m) ≐ m❙ // belowToNatRecCase : {m : ℕ, b : below (Succ m)} ⊦ belowToNat (Succ m) (succBelow (Succ m) b) ≐ belowToNat m b ❙ // belowToNatExample : ⊦ btn 3 (toB 3) ≐ 3❙ // belowToNatExample2 : ⊦ btn 4 (succB (toB 3)) ≐ 3 ❙ // belwoToNatExample2_2 : ⊦ belowToNat (Succ 3) (succBelow (Succ 3) (toBelow 3)) ≐ 3❙ // belowToNat2 : {n : ℕ} below (Succ n) ⟶ ℕ ❘= [n, b] n ❘# btn2 %I1 ❙ // belowToNat3 : {n : ℕ, m : ℕ} below n ⟶ ⊦ m < n ⟶ ℕ ❘= [n , m , b, p ] m ❘# btn3 %I1 ❙ // belowToNat4 : {n : ℕ} below n ⟶ ⟨ ℕ | [x] ⊦ x < n⟩ ❘# btn4 %I1❙ finSeq : ℕ ⟶ type ⟶ type ❘= [n , A] below n ⟶ A ❙ nonEmptyFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n, A , f] 0 < n ❘# nefs %I1 %I2 ❙ disjointFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n,A,fs] ∀[x] ∀[y] y ≐ x ∨ fs x ≠ fs y❙ // disjointFinSeq_prop_trivial : {A : type,f : finSeq 0 A} ⊦ disjointFinSeq_prop 0 A f ≐ true❙ // disjointFinSeq_prop_step // : {A : type , n : ℕ , f : finSeq (succ n) A} ⊦ disjointFinSeq_prop (succ n) A f ≐ ∀ [m1 : below (succ n)] ∀ [m2 : below (succ n)] ⊦ m1 ≠ m2 ⟶ ⊦ true ❙ // belowShift : {n : ℕ , m : ℕ} below n ⟶ below (n + m)❙ // belowShift_base : {n, b} ⊦ belowShift n 0 b ≐ b❙ finSeqSum : {n : ℕ} finSeq n ℝ ⟶ ℝ❙ include arith:?NaturalArithmetics ❙ // below : ℕ ⟶ type ❘ = [n] ⟨ x : ℕ | ⊦ x < n⟩ ❙ 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❙ ❚ theory FinSeqSum : base:?Logic = include ?FinSequences ❙ // 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} ⊦ finSeqSumR ( `arith:?NaturalNumbers?succ m) h sq ≐ sq (`arith:?NaturalNumbers?succ m) h + finSeqSumR m (lt_pred_lt h) sq❙ finSeqSum : {n : ℕ} finSeq n ℝ ⟶ ℝ❙ finSeqSumZero : {sq} ⊦ finSeqSum 0 sq ≐ 0 ❙ // finSeqSumFn : {n} {sq} ⊦ finSeqSum n sq ≐ finSeqSumRec n n sq❙ ❚ \ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!