Commit 74f9cbc6 authored by Sven Wille's avatar Sven Wille

more partial functions (finished)

parent 6237918b
......@@ -38,5 +38,5 @@ theory FinSequences : base:?Logic =
// belowShift : {n : ℕ , m : ℕ} below n ⟶ below (n + m)❙
// belowShift_base : {n, b} ⊦ belowShift n 0 b ≐ b❙
// finSeqSum : {n : ℕ , b : below n}
// finSeqSum : {n : ℕ , b : below n}
......@@ -2,6 +2,7 @@ namespace http://mathhub.info/MitM/smglom/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
import fnd http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
import sub http://gl.mathhub.info/MMT/LFX/Subtyping ❚
// SW this file is mainly for documentation purposes on different ways on how to implement partial functions ❚
theory partialFunctions1 : base:?Logic =
......@@ -16,27 +17,38 @@ theory partialFunctions2 : base:?Logic =
include ts:?TypedSets ❙
// SW not completely correct implementation of partial functions since the argument that holds the proof is not discarded
and could lead to problems in certain cases ❙
partialFunction : {d : type} set d ⟶ type ⟶ type ❘ = [d,s,c] {v : d} ⊦ s v ⟶ c ❘# { 1 ;; 2 } ⟶p 3
partialFunction : {d : type} set d ⟶ type ⟶ type ❘ = [d,s,c] {v : d} ⊦ s v ⟶ c ❙
theory partialFunctions3 : base:?Logic =
include ts:?TypedSets ❙
// SW I think this one leads to problems when used with finite types.
// SW I think this one leads to problems when used with finite types. the undefined is not supposed to be in the set
that makes up the retur type. This version just uses undefined as a potential return value for normal functions
this version is basically translated from isabelle/hol (found in HOL.thy) ❙
undefined : {a : type} a ❙
paritalFunction : { a : type } set a ⟶ type ⟶ type ❘ = [a,s,b] ⟨ f : s ⟶ a ⟶ b | ⊦ ∃ P f = ([ss,v] ) ⟩❙
theory partialFunctions4 : base:?Logic =
partialFunction : {d : type} set d ⟶ type ⟶ type ❘ = [d,s,c] {v : d} ⊦ s v ⟶ c ❘# { 1 ;; 2 } ⟶p 3 ❙
include ts:?TypedSets ❙
// SW this version doesn't create a special type for partial function but uses a "special" function to simulate parital functions❙
applyPartialFunction : {d : type} {s : set d} {e : type} {f : d ⟶ e} {v : d} ⊦ s v ⟶ e ❘ = [d,s,e,f,v,prf] f v ❙
theory partialFunctions4 : base:?Logic =
partialFunction : {d : type} set d ⟶ type ⟶ type ❘ = [d,s,c] {v : d} ⊦ s v ⟶ c ❘# { 1 ;; 2 } ⟶p 3 ❙
theory partialFunctions5 : base:?Logic =
include ts:?TypedSets ❙
include sub:?LFSubtyped ❙
// SW this version make partialFuncions a subtype of normal functions (I think it should be the other way arround , but thats not possible)
and forces that the function throws away the proof argument
partialFunction : {d : type} set d ⟶ type ⟶ type ❘ = [d,s,c] ⟨ f : {v : d} ⊦ s v ⟶ c | ⊦ ∃ [fn] f ≐ ([x,y] fn x) ⟩❙
// set as type version
// use sigma types with special Notation to make it more feel like a normal lf function ❚
// use of subtype
// use subset with proof ❚
\ No newline at end of file
theory partialFunctions6 : base:?Logic =
include ts:?TypedSets ❙
include sub:?LFSubtyped ❙
// SW this version basically enforces via the type waht version 2 need explicitely❙
partialFunction : {d : type} (d ⟶ bool) ⟶ type ⟶ type ❘ = [d,p,r] ⟨ x : d | ⊦ p x ⟩ ⟶ r ❙
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