Commit 39f3a83b by Sven Wille

### subtypes in naturals

parent fa67ab94
 ... ... @@ -72,7 +72,19 @@ theory NaturalArithmetics : base:?Logic = lemma_rightUnitalPlus : {x : ℕ} ⊦ x + 0 ≐ x ❘ = axiom_plus1 ❘ # rightunital_plus_nat ❙ // added by sw ❙ /T usefull lemmata for simple arithmetics ❙ 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❙ // added by sw ❙ // this one is needed to create a possibly empty subset of the natural numbers (this way we can create empty finite sequences)❙ /T finite subset of the natural numbers ❙ between : ℕ ⟶ ℕ ⟶ type ❘= [f,t] ⟨ x : ℕ | ⊦ f ≤ x ∧ x ≤ t⟩ ❙ // convenience function for between ❙ betweenOneAnd : ℕ ⟶ type ❘= [t] ⟨ x : ℕ | ⊦ 1 ≤ x ∧ x ≤ t⟩ ❙ /T convert explicitely a natural number into an "between" ❙ //this function is needed in context wehere a natural number "n" is needed as both natural number and between ❙ // added by sw ❙ natToBetween : {from : ℕ}{to : ℕ} {v : ℕ } ⊦ from ≤ v ∧ v ≤ to ⟶ between from to ❘= [v,h] v❙ ❚
 ... ... @@ -8,7 +8,8 @@ theory FinSequences : base:?Logic = include arith:?NaturalArithmetics ❙ // below : ℕ ⟶ type ❘ = [n] ⟨ x : ℕ | ⊦ x < n⟩ ❙ finSeq : ℕ ⟶ type ⟶ type ❘= [n , A] {m : ℕ} ⊦ m < n ⟶ A ❙ /T finite sequences ❙ finiteSequence : ℕ ⟶ type ⟶ type ❘= [n , A] between 1 n ⟶ A ❘# finSeq 1 2 ❙ // 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❙ ... ... @@ -22,15 +23,20 @@ theory FinSeqSum : base:?Logic = include arith:?NaturalArithmetics ❙ // this one does the actual recusive summation and is called by finSeqSum ❙ 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 ❙ // 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 ≐ 0 ❙ // 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❙ finSeqSumRec : {n : ℕ} betweenOneAnd n ⟶ finSeq n ℝ ⟶ ℝ ❘# finSeqSumR 2 3 4❙ finSeqSumRecB : {n : ℕ} {sq : finSeq n ℝ} ⊦ finSeqSumRec n 1 sq ≐ sq 1 ❙ // 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❙ finSeqSumFn : {n : ℕ} {sq : finSeq n ℝ} ⊦ 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!
Please register or to comment