Definition: bottom
⊥ == fix((λx.x))
Lemma: bottom_diverge
¬(⊥)↓
Definition: callbyvalue
eval x = a in B[x] == PRIMITIVE
Definition: evalall
evalall(t) ==
fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
t
Lemma: evalall-axiom
evalall(Ax) ~ Ax
Lemma: evalall-inl
∀[x:Top]. (evalall(inl x) ~ eval y = evalall(x) in inl y)
Lemma: evalall-inr
∀[x:Top]. (evalall(inr x ) ~ eval y = evalall(x) in inr y )
Lemma: evalall-pair
∀[x,y:Top]. (evalall(<x, y>) ~ eval x' = evalall(x) in eval y' = evalall(y) in <x', y'>)
Definition: callbyvalueall
let x ⟵ a in B[x] == eval x = evalall(a) in B[x]
Definition: subst-exc
subst-exc(e;t)
==r eval x = t in
if x is lambda then λz.subst-exc(e;x z) otherwise if x is a pair then let a,b = x
in eval a' = subst-exc(e;a) in
eval b' = subst-exc(e;b) in
<a', b'>
otherwise if x is inl then eval y = subst-exc(e;outl(x)) in
inl y
else if x is inr then eval y = subst-exc(e;outr(x)) in
inr y
else x?e:v.⊥
Lemma: unit_wf2
Unit ∈ Type
Lemma: sqle_wf_base
∀[a,b:Base]. (a ≤ b ∈ ℙ)
Lemma: istype-sqle
∀[a,b:Base]. istype(a ≤ b)
Definition: is-exception
Howe's `sqle` relation is enough to define the proposition
(about t ∈ Base) that t is an exception.
Note that this is not a decidable proposition!
If being an exception were decidable, then a program could
catch *all* exceptions and we would not be able
to use exceptions to find the modulus of continuity of functionals.
The test ⌜isaxiom(e?n:x.Ax) ∧b isint(e?n:x.2)⌝ can be used to distinguish between
canonical values that are not exceptions and exceptions *with name n*.
But on other exceptions e', this test will raise the exception e'
(as it must, for our construction of the modulus of continuity to work.)
⋅
is-exception(t) == exception(⊥; ⊥) ≤ t
Lemma: is-exception_wf
∀[t:Base]. (is-exception(t) ∈ ℙ)
Definition: exception-with-name
exception-with-name(n;t) == exception(n; ⊥) ≤ t
Lemma: exception-with-name_wf
∀[n:Atom2]. ∀[t:Base]. (exception-with-name(n;t) ∈ ℙ)
Definition: exception-value
exception-value(n;t) == t?n:v.v
Lemma: exception-value_wf
∀[n:Atom2]. ∀[t:Base]. (exception-value(n;t) ∈ Base)
Definition: Exception
The type of terms that are exceptions with name n and values in type T.
Exception(n;T) == {t:Base| exception-with-name(n;t) ∧ (exception-value(n;t) ∈ T)}
Lemma: Exception_wf
∀[n:Atom2]. ∀[T:Type]. (Exception(n;T) ∈ Type)
Lemma: equal-in-unit
∀[x,y:Unit]. (x = y ∈ Unit)
Definition: has-value
If ⌜a⌝ has a value then the call-by-value term
⌜eval a; 0⌝ evaluates to 0. If ⌜a⌝ diverges then so does ⌜eval a; 0⌝.
Thus, ⌜a⌝ has a value if and only if ⌜0 ≤ eval a; 0⌝⋅
(a)↓ == 0 ≤ eval a; 0
Lemma: has-value_wf_base
∀[a:Base]. ((a)↓ ∈ ℙ)
Lemma: member-has-value
∀[a:Base]. Ax ∈ (a)↓ supposing (a)↓
Lemma: has-value-extensionality
∀[a,b:Base]. (a)↓ = (b)↓ ∈ ℙ supposing (a)↓ ⇐⇒ (b)↓
Definition: Value
Value() == {x:Base| (x)↓}
Lemma: Value_wf
Value() ∈ Type
Lemma: ispair-member
∀[T:Type]. ∀[t:Base]. ∀[a,b:T]. if t is a pair then a otherwise b ∈ T supposing (t)↓
Lemma: isinl-member
∀[T:Type]. ∀[t:Base]. ∀[a,b:T]. if t is inl then a else b ∈ T supposing (t)↓
Lemma: isinr-member
∀[T:Type]. ∀[t:Base]. ∀[a,b:T]. if t is inr then a else b ∈ T supposing (t)↓
Lemma: ispair-pair
∀[t,x,y:Base]. t ∈ Top × Top supposing if t is a pair then inl x otherwise inr y ~ inl x
Lemma: not-ispair
∀[t,a,b:Base].
∀[x,y:Top]. (if t is a pair then x otherwise y ~ y) supposing if t is a pair then inl a otherwise inr b ~ inr b
Lemma: ispair-bool-if-has-value
∀[t:Base]. ispair(t) ∈ 𝔹 supposing (t)↓
Lemma: isaxiom-bool-if-has-value
∀[t:Base]. isaxiom(t) ∈ 𝔹 supposing (t)↓
Lemma: isinl-bool-if-has-value
∀[t:Base]. isinl(t) ∈ 𝔹 supposing (t)↓
Lemma: isinr-bool-if-has-value
∀[t:Base]. isinr(t) ∈ 𝔹 supposing (t)↓
Lemma: islambda-bool-if-has-value
∀[t:Base]. islambda(t) ∈ 𝔹 supposing (t)↓
Lemma: isatom-bool-if-has-value
∀[t:Base]. isatom(t) ∈ 𝔹 supposing (t)↓
Lemma: isatom1-bool-if-has-value
∀[t:Base]. isatom1(t) ∈ 𝔹 supposing (t)↓
Lemma: isatom2-bool-if-has-value
∀[t:Base]. isatom2(t) ∈ 𝔹 supposing (t)↓
Lemma: isint-bool-if-has-value
∀[t:Base]. isint(t) ∈ 𝔹 supposing (t)↓
Lemma: decide-pair-if-has-value
∀t:Base. ((t)↓ ⇒ Dec(t ~ <fst(t), snd(t)>))
Lemma: decide-axiom-if-has-value
∀t:Base. ((t)↓ ⇒ Dec(t ~ Ax))
Lemma: decide-inl-if-has-value
∀t:Base. ((t)↓ ⇒ Dec(t ~ inl outl(t)))
Lemma: decide-inr-if-has-value
∀t:Base. ((t)↓ ⇒ Dec(t ~ inr outr(t) ))
Lemma: decide-lambda-if-has-value
∀t:Base. ((t)↓ ⇒ Dec(t ~ λx.(t x)))
Lemma: decide-int-if-has-value
∀t:Base. ((t)↓ ⇒ Dec(t ∈ ℤ))
Lemma: decide-atom-if-has-value
∀t:Base. ((t)↓ ⇒ Dec(t ∈ Atom))
Lemma: decide-atom2-if-has-value
∀t:Base. ((t)↓ ⇒ Dec(t ∈ Atom2))
Lemma: decide-ispair-if-has-value
∀t,a,b:Base. ((t)↓ ⇒ ((if t is a pair then a otherwise b ~ a) ∨ (if t is a pair then a otherwise b ~ b)))
Lemma: decide-isaxiom-if-has-value
∀t,a,b:Base. ((t)↓ ⇒ ((if t = Ax then a otherwise b ~ a) ∨ (if t = Ax then a otherwise b ~ b)))
Lemma: decide-isinl-if-has-value
∀t,a,b:Base. ((t)↓ ⇒ ((if t is inl then a else b ~ a) ∨ (if t is inl then a else b ~ b)))
Lemma: decide-isinr-if-has-value
∀t,a,b:Base. ((t)↓ ⇒ ((if t is inr then a else b ~ a) ∨ (if t is inr then a else b ~ b)))
Lemma: decide-islambda-if-has-value
∀t,a,b:Base. ((t)↓ ⇒ ((if t is lambda then a otherwise b ~ a) ∨ (if t is lambda then a otherwise b ~ b)))
Lemma: decide-isint-if-has-value
∀t,a,b:Base. ((t)↓ ⇒ ((if t is an integer then a else b ~ a) ∨ (if t is an integer then a else b ~ b)))
Lemma: decide-isatom-if-has-value
∀t,a,b:Base. ((t)↓ ⇒ ((if t is an atom then a otherwise b ~ a) ∨ (if t is an atom then a otherwise b ~ b)))
Lemma: decide-isatom2-if-has-value
∀t,a,b:Base. ((t)↓ ⇒ ((isatom2(t;a;b) ~ a) ∨ (isatom2(t;a;b) ~ b)))
Lemma: has-value-implies-dec-ispair
∀t,a,b:Base. ((t)↓ ⇒ ((t ~ <fst(t), snd(t)>) ∨ (if t is a pair then a otherwise b ~ b)))
Lemma: has-value-implies-dec-ispair-2
∀t:Base. ((t)↓ ⇒ ((t ~ <fst(t), snd(t)>) ∨ (∀a,b:Base. (if t is a pair then a otherwise b ~ b))))
Lemma: has-value-implies-dec-isaxiom
∀t,a,b:Base. ((t)↓ ⇒ ((t ~ Ax) ∨ (if t = Ax then a otherwise b ~ b)))
Lemma: has-value-implies-dec-isaxiom-2
∀t:Base. ((t)↓ ⇒ ((t ~ Ax) ∨ (∀a,b:Base. (if t = Ax then a otherwise b ~ b))))
Lemma: has-value-implies-dec-isinl
∀t,a,b:Base. ((t)↓ ⇒ ((t ~ inl outl(t)) ∨ (if t is inl then a else b ~ b)))
Lemma: has-value-implies-dec-isinl-2
∀t:Base. ((t)↓ ⇒ ((t ~ inl outl(t)) ∨ (∀a,b:Base. (if t is inl then a else b ~ b))))
Lemma: has-value-implies-dec-isinr
∀t,a,b:Base. ((t)↓ ⇒ ((t ~ inr outr(t) ) ∨ (if t is inr then a else b ~ b)))
Lemma: has-value-implies-dec-isinr-2
∀t:Base. ((t)↓ ⇒ ((t ~ inr outr(t) ) ∨ (∀a,b:Base. (if t is inr then a else b ~ b))))
Lemma: has-value-implies-dec-islambda
∀t,a,b:Base. ((t)↓ ⇒ ((t ~ λx.(t x)) ∨ (if t is lambda then a otherwise b ~ b)))
Lemma: has-value-implies-dec-islambda-2
∀t:Base. ((t)↓ ⇒ ((t ~ λx.(t x)) ∨ (∀a,b:Base. (if t is lambda then a otherwise b ~ b))))
Lemma: has-value-implies-dec-isint
∀t,a,b:Base. ((t)↓ ⇒ ((t ∈ ℤ) ∨ (if t is an integer then a else b ~ b)))
Lemma: has-value-implies-dec-isint-2
∀t:Base. ((t)↓ ⇒ ((t ∈ ℤ) ∨ (∀a,b:Base. (if t is an integer then a else b ~ b))))
Lemma: has-value-implies-dec-isatom
∀t,a,b:Base. ((t)↓ ⇒ ((t ∈ Atom) ∨ (if t is an atom then a otherwise b ~ b)))
Lemma: has-value-implies-dec-isatom-2
∀t:Base. ((t)↓ ⇒ ((t ∈ Atom) ∨ (∀a,b:Base. (if t is an atom then a otherwise b ~ b))))
Lemma: has-value-implies-dec-isatom2
∀t,a,b:Base. ((t)↓ ⇒ ((t ∈ Atom2) ∨ (isatom2(t;a;b) ~ b)))
Lemma: has-value-implies-dec-isatom2-2
∀t:Base. ((t)↓ ⇒ ((t ∈ Atom2) ∨ (∀a,b:Base. (isatom2(t;a;b) ~ b))))
Definition: is-atomic
is-atomic(x) == if x is a pair then ff otherwise if x is inl then ff else if x is inr then ff else tt
Lemma: is-atomic_wf
∀[x:Value()]. (is-atomic(x) ∈ 𝔹)
Definition: atomic-values
atomic-values() == {x:Value()| ↑is-atomic(x)}
Lemma: atomic-values_wf
atomic-values() ∈ Type
Lemma: atomic-values_subtype_base
atomic-values() ⊆r Base
Lemma: sq_stable__sqle
∀[a,b:Base]. SqStable(a ≤ b)
Definition: strict
strict(F) ==
(∀x:Base. ((F x)↓ ⇒ (x)↓))
∧ (∀u,v:Base. (F (exception(u; v)) ~ exception(u; v)))
∧ (∀z:Base. (is-exception(F z) ⇒ is-exception(z)))
Lemma: strict_wf
∀F:Base. (strict(F) ∈ ℙ)
Lemma: exception-not-bottom_1
∀[nm,val:Base]. ((exception(nm; val) ≤ ⊥) ⇒ False)
Lemma: exception-not-axiom
∀[nm,val:Base]. ((Ax ≤ exception(nm; val)) ⇒ False)
Lemma: exception-not-value_1
∀[nm,val,t:Base]. (exception(nm; val) ≤ t) ⇒ False supposing (t)↓
Lemma: exception-not-value-or-bottom
∀[nm,val,t:Base]. (exception(nm; val) ≤ t) ⇒ False supposing ↓(t)↓ ∨ (t ~ ⊥)
Lemma: exception-not-value2
∀[nm,val,t:Base]. (t ≤ exception(nm; val)) ⇒ False supposing (t)↓
Lemma: not-exception-has-value
∀[nm,val:Base]. ((exception(nm; val))↓ ⇒ False)
Lemma: exception-not-value
∀[t:Base]. is-exception(t) ⇒ False supposing (t)↓
Lemma: exception-not-bottom
is-exception(⊥) ⇒ False
Lemma: bottom-sqle
∀[x:Top]. (⊥ ≤ x)
Lemma: test_stuck_apply
∀[x,y,z:Top]. (<x, y> z ~ ⊥)
Lemma: cbv-reduce-strict
∀[F,a,B:Base].
F[eval x = a in
B[x]] ≤ F[B[a]]
supposing (∀x:Base. ((F[x])↓ ⇒ (x)↓))
∧ (∀u,v,x:Base. ((F[x] ~ exception(u; v)) ⇒ (↓(x ~ exception(u; v)) ∨ (x)↓)))
∧ (∀u,v:Base. (B[exception(u; v)] ~ exception(u; v)))
Definition: strict1
strict1(F) ==
(∀x:Base. ((F x)↓ ⇒ (x)↓))
∧ (∀u,v:Base. (F (exception(u; v)) ~ exception(u; v)))
∧ (∀x:Base. (is-exception(F x) ⇒ (↓(x)↓ ∨ is-exception(x))))
Lemma: strict1_wf
∀[F:Base]. (strict1(F) ∈ ℙ)
Definition: strict2
strict2(F) ==
(∀x,y:Base. ((F x y)↓ ⇒ (x)↓))
∧ (∀y,u,v:Base. (F (exception(u; v)) y ~ exception(u; v)))
∧ (∀x,y:Base. (is-exception(F x y) ⇒ (↓(x)↓ ∨ is-exception(x))))
Lemma: strict2_wf
∀[F:Base]. (strict2(F) ∈ ℙ)
Definition: strict4
strict4(F) ==
(∀x,y,z,w:Base. ((F x y z w)↓ ⇒ (x)↓))
∧ (∀u,v,y,z,w:Base. (F (exception(u; v)) y z w ~ exception(u; v)))
∧ (∀x,y,z,w:Base. (is-exception(F x y z w) ⇒ (↓is-exception(x) ∨ (x)↓)))
Lemma: strict4_wf
∀[F:Base]. (strict4(F) ∈ ℙ)
Lemma: strict1-strict4
∀F:Base. (strict1(F) ⇒ strict4(λx,y,z,w. F[x]))
Lemma: strict-strict1
∀F:Base. (strict(F) ⇒ strict1(λx.F[x]))
Lemma: strict-strict4
∀F:Base. (strict(F) ⇒ strict4(λx,y,z,w. F[x]))
Definition: strict5
strict5(F) ==
(∀x,y,z,w:Base. ((F x y z w)↓ ⇒ (x)↓))
∧ (∀u,v,y,z,w:Base. (F (exception(u; v)) y z w ~ exception(u; v)))
∧ (∀u,v,x,y,z,w:Base. ((F x y z w ~ exception(u; v)) ⇒ (↓(eval y = x in y ~ exception(u; v)) ∨ (x)↓)))
Definition: l-strict
l-strict(F) ==
∀r:Base
((∀x:Base
((F r x)↓
⇒ ((∀a,b:Base. (if x is a pair then a otherwise b ~ a)) ∨ (∀a,b:Base. (if x = Ax then a otherwise b ~ a)))))
∧ (∃G:Base. ∀x,y:Base. ((F r <x, y> ~ G x y (r y)) ∧ strict(G x y))))
Lemma: l-strict_wf
∀[F:Base]. (l-strict(F) ∈ ℙ)
Lemma: ispair-sqequal
∀[C:Base]
∀[A,B,z:Base].
if z is a pair then A z otherwise B z ~ C z
supposing ((z ~ <fst(z), snd(z)>) ⇒ (A <fst(z), snd(z)> ~ C <fst(z), snd(z)>))
∧ ((∀a,b:Base. (if z is a pair then a otherwise b ~ b)) ⇒ (B z ~ C z))
supposing strict(C)
Lemma: isaxiom-sqequal
∀[C:Base]
∀[A,B,z:Base].
if z = Ax then A z otherwise B z ~ C z
supposing (A Ax ~ C Ax) ∧ ((∀a,b:Base. (if z = Ax then a otherwise b ~ b)) ⇒ (B z ~ C z))
supposing strict(C)
Definition: has-valueall
has-valueall(a) == (evalall(a))↓
Definition: value-type
value-type(T) == ∀[x:Base]. (x)↓ supposing x ∈ T
Lemma: value-type_wf
∀[T:Type]. (value-type(T) ∈ Type)
Lemma: value-type_functionality
∀[T,T':Type]. value-type(T) ⇐⇒ value-type(T') supposing T ≡ T'
Definition: valueall-type
valueall-type(T) == ∀[x:Base]. (evalall(x))↓ supposing x ∈ T
Lemma: valueall-type_wf
∀[T:Type]. (valueall-type(T) ∈ Type)
Lemma: valueall-type_functionality
∀[T,T':Type]. valueall-type(T) ⇐⇒ valueall-type(T') supposing T ≡ T'
Lemma: sq_stable__value-type
∀[T:Type]. SqStable(value-type(T))
Lemma: sq_stable__valueall-type
∀[T:Type]. SqStable(valueall-type(T))
Lemma: value-type-has-value
∀[T:Type]. ∀[x:T]. (x)↓ supposing value-type(T)
Lemma: valueall-type-has-valueall
∀[T:Type]. ∀[x:T]. has-valueall(x) supposing valueall-type(T)
Definition: exception-type
exception-type(T) == ∀[x:Base]. is-exception(x) supposing x ∈ T
Lemma: exception-type_wf
∀[T:Type]. (exception-type(T) ∈ Type)
Lemma: sq_stable_sqle
∀[a,b:Base]. SqStable(a ≤ b)
Lemma: sq_stable-exception-type
∀[T:Type]. SqStable(exception-type(T))
Lemma: spread-exception-type
∀[T:Type]. ∀[x:T]. ∀[B:Top]. let u,v = x in B[u;v] ~ x supposing exception-type(T)
Lemma: decide-exception-type
∀[T:Type]. ∀[x:T]. ∀[A,B:Top]. case x of inl(u) => A[u] | inr(v) => B[v] ~ x supposing exception-type(T)
Lemma: callbyvalue-exception-type
∀[T:Type]. ∀[x:T]. ∀[B:Top]. eval z = x in B[z] ~ x supposing exception-type(T)
Lemma: apply-exception-type
∀[T:Type]. ∀[x:T]. ∀[B:Top]. x B ~ x supposing exception-type(T)
Lemma: evalall-atom
∀[x:Atom]. (evalall(x) ~ x)
Lemma: evalall-atom1
∀[x:Atom1]. (evalall(x) ~ x)
Lemma: evalall-atom2
∀[x:Atom2]. (evalall(x) ~ x)
Lemma: evalall-int
∀[x:ℤ]. (evalall(x) ~ x)
Lemma: has-value-wf-value-type
∀[T:Type]. ∀[a:T]. ((a)↓ ∈ ℙ) supposing value-type(T)
Lemma: sq_stable__has-value
∀[a:Base]. SqStable((a)↓)
Lemma: has-valueall_wf_base
∀[a:Base]. (has-valueall(a) ∈ ℙ)
Lemma: member-has-valueall
∀[a:Base]. Ax ∈ has-valueall(a) supposing has-valueall(a)
Lemma: has-valueall-has-value
∀[a:Base]. (a)↓ supposing has-valueall(a)
Lemma: has-valueall-if-has-value-callbyvalueall
∀[a,b:Base]. has-valueall(a) supposing (let x ⟵ a in b[x])↓
Lemma: sq_stable__has-valueall
∀[a:Base]. SqStable(has-valueall(a))
Lemma: has-valueall-pair
∀[a,b:Base]. uiff(has-valueall(<a, b>);has-valueall(a) ∧ has-valueall(b))
Lemma: has-valueall-inl
∀[a:Base]. uiff(has-valueall(inl a);has-valueall(a))
Lemma: has-valueall-inr
∀[a:Base]. uiff(has-valueall(inr a );has-valueall(a))
Lemma: has-valueall-lambda
∀[a:Base]. has-valueall(λx.a[x])
Definition: vatype
ValueAllType == {T:Type| valueall-type(T)}
Lemma: vatype_wf
ValueAllType ∈ 𝕌'
Lemma: subtype_rel_vatype
ValueAllType ⊆r ValueAllType'
Definition: map-eval
map-eval(x.f[x];L) == rec-case(L) of [] => [] | a::b => r.eval a = f[a] in eval b = r in [a / b]
Lemma: void-value-type
value-type(Void)
Lemma: void-valueall-type
valueall-type(Void)
Lemma: product-value-type
∀[A:Type]. ∀[B:A ⟶ Type]. value-type(a:A × B[a])
Lemma: product-valueall-type
∀[A:Type]. ∀[B:A ⟶ Type]. (valueall-type(A) ⇒ (∀a:A. valueall-type(B[a])) ⇒ valueall-type(a:A × B[a]))
Lemma: union-value-type
∀[A,B:Type]. value-type(A + B)
Lemma: union-valueall-type
∀[A,B:Type]. (valueall-type(A) ⇒ valueall-type(B) ⇒ valueall-type(A + B))
Lemma: tunion-value-type
∀[A:Type]. ∀[B:A ⟶ Type]. value-type(⋃a:A.B[a]) supposing ∀a:A. value-type(B[a])
Lemma: tunion-valueall-type
∀[A:Type]. ∀[B:A ⟶ Type]. valueall-type(⋃a:A.B[a]) supposing ∀a:A. valueall-type(B[a])
Lemma: int-valueall-type
valueall-type(ℤ)
Lemma: int-value-type
value-type(ℤ)
Lemma: atom-valueall-type
valueall-type(Atom)
Lemma: atom-value-type
value-type(Atom)
Lemma: atom1-valueall-type
valueall-type(Atom1)
Lemma: atom1-value-type
value-type(Atom1)
Lemma: atom2-valueall-type
valueall-type(Atom2)
Lemma: atom2-value-type
value-type(Atom2)
Lemma: equal-valueall-type
∀[T:Type]. ∀[x,y:T]. valueall-type(x = y ∈ T)
Lemma: equal-value-type
∀[T:Type]. ∀[x,y:T]. value-type(x = y ∈ T)
Lemma: type-value-type
value-type(Type)
Lemma: function-valueall-type
∀[A:Type]. ∀[B:A ⟶ Type]. valueall-type(a:A ⟶ B[a]) supposing ↓∃a:A. value-type(B[a])
Lemma: function-value-type
∀[A:Type]. ∀[B:A ⟶ Type]. value-type(a:A ⟶ B[a]) supposing ↓∃a:A. value-type(B[a])
Lemma: all-value-type
∀[A:Type]. ∀[a:A]. ∀[B:A ⟶ Type]. value-type(∀a:A. B[a]) supposing value-type(B[a])
Lemma: function-not-int
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A ⟶ B[a]]. (isint(f) ~ ff) supposing ↓∃a:A. value-type(B[a])
Lemma: subtype-valueall-type
∀[A,B:Type]. (valueall-type(A)) supposing (valueall-type(B) and (A ⊆r B))
Lemma: subtype-value-type
∀[A,B:Type]. (value-type(A)) supposing (value-type(B) and (A ⊆r B))
Lemma: set-valueall-type
∀[A:Type]. ∀[P:A ⟶ ℙ]. valueall-type({a:A| P[a]} ) supposing valueall-type(A)
Lemma: set-value-type
∀[A:Type]. ∀[P:A ⟶ ℙ]. value-type({a:A| P[a]} ) supposing value-type(A)
Lemma: isect-valueall-type
∀[A:Type]. ∀[B:A ⟶ Type]. ((∃a:A. valueall-type(B[a])) ⇒ valueall-type(⋂a:A. B[a]))
Lemma: isect-value-type
∀[A:Type]. ∀[B:A ⟶ Type]. ((∃a:A. value-type(B[a])) ⇒ value-type(⋂a:A. B[a]))
Lemma: isaxiom-implies
∀[t:Base]. (t ~ Ax) supposing ((↑isaxiom(t)) and (t)↓)
Lemma: isaxiom-implies-sq
∀[t:Base]. t ~ Ax supposing isaxiom(t) ~ tt
Lemma: isaxiom-implies-not-isint
∀[t:Base]. (¬↑isint(t)) supposing ((↑isaxiom(t)) and (t)↓)
Lemma: not-axiom-member-int
¬(Ax ∈ ℤ)
Lemma: ispair-implies
∀[t:Base]. (t ~ <fst(t), snd(t)>) supposing ((↑ispair(t)) and (t)↓)
Lemma: ispair-implies-sq
∀[t:Base]. t ~ <fst(t), snd(t)> supposing ispair(t) ~ tt
Lemma: ispair-implies-not-isint
∀[t:Base]. (¬↑isint(t)) supposing ((↑ispair(t)) and (t)↓)
Lemma: not-pair-member-int
∀[a,b:Base]. (¬(<a, b> ∈ ℤ))
Lemma: ispair-implies-not-isatom
∀[t:Base]. (¬↑isatom(t)) supposing ((↑ispair(t)) and (t)↓)
Lemma: isinl-implies
∀[t:Base]. (t ~ inl outl(t)) supposing ((↑isinl(t)) and (t)↓)
Lemma: isinl-implies-not-isint
∀[t:Base]. (¬↑isint(t)) supposing ((↑isinl(t)) and (t)↓)
Lemma: isinl-implies-not-isatom
∀[t:Base]. (¬↑isatom(t)) supposing ((↑isinl(t)) and (t)↓)
Lemma: isinr-implies
∀[t:Base]. (t ~ inr outr(t) ) supposing ((↑isinr(t)) and (t)↓)
Lemma: isinr-implies-not-isint
∀[t:Base]. (¬↑isint(t)) supposing ((↑isinr(t)) and (t)↓)
Lemma: isinr-implies-not-isatom
∀[t:Base]. (¬↑isatom(t)) supposing ((↑isinr(t)) and (t)↓)
Lemma: isatom-implies-not-isint
∀[t:Base]. (¬↑isint(t)) supposing ((↑isatom(t)) and (t)↓)
Lemma: not-atom-member-int
∀[t:Atom]. (¬(t ∈ ℤ))
Lemma: isatom-implies-not-ispair
∀[t:Base]. (¬↑ispair(t)) supposing ((↑isatom(t)) and (t)↓)
Lemma: isint-implies-not-isatom
∀[t:Base]. (¬↑isatom(t)) supposing ((↑isint(t)) and (t)↓)
Lemma: atom-implies-ispair-right
∀[b,c:Top]. ∀[a:Atom]. (if a is a pair then b otherwise c ~ c)
Definition: any def
We use any x for the witness of x:Void |- C (no matter what C is).
The term ⌜any x⌝ must have type ⌜x:Void ⟶ C⌝, but any term has this type!
Therefore, we could define ⌜any x⌝ to be ⌜⊥⌝, but, because we sometimes
want to compute all the subterms of a extract term, it is safer to define
⌜any x⌝ to be a canonincal term. So we choose ⌜Ax⌝, the "simplest" canonical
term.⋅
any x == Ax
Lemma: base-member-prop
∀[T:Type]. ∀t:Base. (t ∈ T ∈ ℙ)
Lemma: bottom-member-prop
∀[T:Type]. (⊥ ∈ T ∈ ℙ)
Lemma: strict4-apply
strict4(λx,y,z,w. (x y))
Lemma: strict4-divide
strict4(λx,y,z,w. (x ÷ y))
Lemma: subst-exc-basecase
∀[v:Top]. ∀[e:Atom2]. (subst-exc(e;exception(e; v)) ~ ⊥)
Lemma: has-value-try
∀[t,n,B:Base].
↓((t)↓ ∧ (t?n:v.B[v] ~ t)) ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓))
supposing (t?n:v.B[v])↓
Lemma: has-value-try-iff
∀[t,n,B:Base].
uiff((t?n:v.B[v])↓;↓((t)↓ ∧ (t?n:v.B[v] ~ t)) ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓)))
Lemma: try-is-exception
∀[t,n,B,m,x:Base].
exception(m; x) ≤ t?n:v.B[v]
supposing ↓((n ∈ Atom2)
∧ (((m ∈ Atom2) ∧ (exception(m; x) ≤ t) ∧ (¬(n = m ∈ Atom2)))
∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (exception(m; x) ≤ B[u])))))
∨ ((t)↓ ∧ (exception(m; x) ≤ n))
Definition: ex-sqle
ex-sqle(e;t;t') == subst-exc(e;t) ≤ subst-exc(e;t')
Lemma: ex-sqle_wf
∀[e:Atom2]. ∀[t,t':Base]. (ex-sqle(e;t;t') ∈ ℙ)
Lemma: ex-sqle_transitivity
∀[e:Atom2]. ∀[a,b,c:Base]. (ex-sqle(e;a;c)) supposing (ex-sqle(e;b;c) and ex-sqle(e;a;b))
Lemma: ex-sqle-basecase
∀[e:Atom2]. ∀[v,t':Base]. ex-sqle(e;exception(e; v);t')
Home
Index