Commit 598a53f5 authored by MoritzBloecher's avatar MoritzBloecher
Browse files

Adding data types related to functional programming

parent 54b33a86
......@@ -35,9 +35,6 @@ file source/logic/model_theory/build.msl
// This is used in particular to obtain the theory of types and inherit abbreviations from it into typed languages.
build MMT/LATIN2 mmt-omdoc category_theory
// Multiple type theoretical features are based on endofunctors on the category of types, such as lists or sets over a type.
file source/type_theory/endofunctors/build.msl
// Set theory defines ZFC-style languages using FOL as the meta-theory.
file source/set_theory/build.msl
......@@ -54,6 +51,9 @@ file source/domain_theories/build.msl
// depends on natural numbers
build MMT/LATIN2 mmt-omdoc type_theory/vector_types.mmt
// Multiple type theoretical features are based on endofunctors on the category of types, such as lists or sets over a type.
file source/type_theory/endofunctors/build.msl
// Meta-theorems stating the algebraic properties of logic, formalized as theory morphisms from algebraic to logical theories.
build MMT/LATIN2 mmt-omdoc algebraic_logic/pl_semilattice.mmt
......
file ../../../build_config.msl
// numbers
build MMT/LATIN2 mmt-omdoc ./numbers.mmt
build MMT/LATIN2 mmt-omdoc domain_theories/numbers/numbers.mmt
// natural numbers
build MMT/LATIN2 mmt-omdoc ./nat_axiomatic.mmt
build MMT/LATIN2 mmt-omdoc domain_theories/numbers/nat_axiomatic.mmt
build MMT/LATIN2 mmt-omdoc ./nat_binary.mmt
build MMT/LATIN2 mmt-omdoc ./nat_church.mmt
build MMT/LATIN2 mmt-omdoc ./nat_realm.mmt
......@@ -13,5 +13,7 @@ build MMT/LATIN2 mmt-omdoc ./upto.mmt
// integer numbers
build MMT/LATIN2 mmt-omdoc ./int_axiomatic.mmt
//rational numbers
build MMT/LATIN2 mmt-omdoc ./rat_axiomatic.mmt
// non-canonical
// build MMT/LATIN2 mmt-omdoc numbers/nat_induct.mmt
\ No newline at end of file
......@@ -8,14 +8,24 @@ import uom scala://uom.api.mmt.kwarc.info❚
theory IntUnary =
include ?NatUnary❙
pred: tm num ⟶ tm num❙
pred: tm num ⟶ tm num ❘# p 1❙
inv: tm num ⟶ tm num❘ # %n 1 prec 32❙
pred_succ: {x} ⊦ (p x') =ͭ x ❘ role Simplify ❙
succ_pred: {x} ⊦ (p x)' =ͭ x ❘ role Simplify ❙
inv_zero: ⊦ inv zero =ͭ zero ❘ role Simplify ❙
inv_succ: {x} ⊦ (inv x' ) =ͭ p inv x ❘ role Simplify ❙
inv_pred: {x} ⊦ (inv p x) =ͭ ( inv x)' ❘ role Simplify ❙
// axioms for succ and pred inverse❙
theory IntPlus =
include ?IntUnary❙
include ?NatPlus❙
plus_pred_l : {x,y} ⊦ (p x + y) =ͭ p(x + y) ❘ role Simplify ❙
plus_pred_r : {x,y} ⊦ (x + p y) =ͭ p(x + y) ❘ role Simplify ❙
plus_inv : {x,y} ⊦ inv (x + y) =ͭ (inv x) + (inv y) ❘ role Simplify ❙
// axiom for + and pred❙
......@@ -23,10 +33,55 @@ theory IntPlusTimes =
include ?IntUnary❙
include ?NatPlusTimes❙
times_pred_l : {x,y} ⊦ ( (p x) * y) =ͭ ((x*y)+ inv y) ❘ role Simplify ❙
times_pred_r : {x,y} ⊦ ( x* (p y)) =ͭ ((x*y)+ inv x) ❘ role Simplify ❙
times_inv : {x,y} ⊦ inv (x*y) =ͭ (inv x)*y❘ role Simplify ❙
// axiom for * and pred❙
theory IntSub =
include ?IntPlusTimes ❙
sub: tm num ⟶ tm num ⟶ tm num ❘ # 1 - 2 prec 31❙
sub_zero_r : {x} ⊦ (x - zero) =ͭ x ❘role Simplify❙
sub_zero_l: {y} ⊦ (zero - y) =ͭ inv y ❘role Simplify❙
sub_succ_l : {x,y} ⊦ x' - y =ͭ ( x - y )'❘role Simplify❙
sub_succ_r : {x,y} ⊦ x - (y') =ͭ p( x - y )❘role Simplify❙
sub_pred_l : {x,y} ⊦ (p x) - y =ͭ x - (p y)❘role Simplify❙
sub_pred_r : {x,y} ⊦ x - (p y) =ͭ (x - y)'❘role Simplify❙
sub_inv: {x,y} ⊦ inv(x - y) =ͭ ( inv x) - (inv y )❘role Simplify❙
theory IntSpec =
include ?NatSpec ❙
include ?IntSub❙
theory Int =
include ?IntPlusTimes❙
theory Int_realization =
structure int : ?IntSpec =
num # integer ❙
Nat # ℤ ❙
zero # zero ❙
succ # S 1 prec 31 ❙
pred # Pre 1 prec 31 ❙
plus # 1 + 2 prec 40 ❙
times # 1 * 2 prec 45 ❙
rule rules?Realize int/Nat uom?StandardInt❙
rule rules?Realize zero uom?Arithmetic/Zero❙
\ No newline at end of file
......@@ -22,22 +22,36 @@ theory NatPeano =
inductive_fun : {B, P: ℕ ⟶ tm B} tm B ⟶ (ℕ ⟶ tm B ⟶ tm B) ⟶ ℕ ⟶ tm B❙
inductive_pred : {P: ℕ ⟶ prop} prop ⟶ (ℕ ⟶ prop ⟶ prop) ⟶ ℕ ⟶ prop❙
inductive_proof : {P: ℕ ⟶ prop} ⊦ P zero ⟶ ({n} ⊦ P n ⟶ ⊦ P (n')) ⟶ {n} ⊦ P n❙
theory NatPlus =
include ?NatUnary❙
include ?Plus❙
plus_zero : {n} ⊦ n + zero =ͭ n❙
plus_succ : {m, n} ⊦ n + m' =ͭ (n + m)'❙
plus_zero : {n} ⊦ n + zero =ͭ n❘role Simplify ❙
plus_zero_r : {n} ⊦ zero + n =ͭ n❘role Simplify ❙
plus_succ : {m, n} ⊦ n + m' =ͭ (n + m)'❘role Simplify❙
plus_succ_l : {m, n} ⊦ n' + m =ͭ (n + m)'❘role Simplify❙
assoc_plus : {l,m,n} ⊦ (l+m)+n =ͭ l+(m+n) ❙
comm_plus : {m,n} ⊦ m+n =ͭ n+m ❙
theory NatPlusTimes =
include ?NatPlus❙
include ?Times❙
times_zero : {n} ⊦ zero * n =ͭ zero❙
times_succ : {m,n} ⊦ n' * m =ͭ (n * m) + m❙
times_zero : {n} ⊦ zero * n =ͭ zero ❘role Simplify ❙
times_zero_l : {n} ⊦ n * zero =ͭ zero ❘role Simplify ❙
times_succ : {m,n} ⊦ n' * m =ͭ (n * m) + m❘role Simplify ❙
times_succ_r : {m,n} ⊦ n * m' =ͭ (n * m) + n❘role Simplify ❙
assoc_times: {l,m,n} ⊦ (l*m)*n =ͭ l*(m*n) ❙
comm_times : {m,n} ⊦ m*n =ͭ n*m ❙
theory NatParity =
......@@ -66,4 +80,41 @@ theory Nat =
include ?NatPlusTimes❙
include ?NatParity❙
include ?NatLiterals❙
\ No newline at end of file
theory NatSpec =
include ?NatPlusTimes❙
include ?NatParity❙
lesser: tm num ⟶ tm num ⟶ prop❘# 1 < 2 prec 30❙
lesser_zero_r: {n} ⊦ ¬(n < zero)❘role Simplify ❙
lesser_zero_l: {n} ⊦ (zero < n')❘role Simplify ❙
lesser_succ: {x,y} ⊦ (x < y) ⇔ ( x' < y')❘role Simplify ❙
greater: tm num ⟶ tm num⟶ prop ❘# 1 > 2 prec 30❘
= [x,y] y < x❙
lesserequal: tm num ⟶ tm num ⟶ prop ❘# 1 %n 2 prec 30❘
= [x,y] ¬ (x < y) ❙
greaterequal: tm num ⟶ tm num ⟶ prop ❘# 1 ≥ 2 prec 30❘
= [x,y] ¬ (x < y ) ❙
distributive: {l,m,n} ⊦ (l+m)*n =ͭ (l*n)+(m*n)❙
theory Nat_realization =
structure nat : ?NatSpec =
num # naturalnumber ❙
Nat # ℕ ❙
zero # zero ❙
succ # S 1 prec 31 ❙
plus # 1 + 2 prec 40 ❙
times # 1 * 2 prec 45 ❙
include ?NatPeano ❙
rule rules?Realize nat/Nat uom?StandardNat❙
rule rules?Realize zero uom?Arithmetic/Zero❙
namespace latin:/❚
fixmeta latin:/?SFOLEQND❚
import rules scala://lf.mmt.kwarc.info❚
import uom scala://uom.api.mmt.kwarc.info❚
theory RatDiv =
include ?IntSub❙
div : tm num ⟶ tm num ⟶ tm num ❘ # 1 / 2 prec 31 ❙
div_zero : {x} ⊦ zero / x =ͭ zero ❘# role Simplify ❙
div_one : {x} ⊦ x / (zero ') =ͭ x ❘# role Simplify ❙
div_succ : {x,y} ⊦ (x / y)' =ͭ (x / y) + zero'❘# role Simplify ❙
div_pred: {x,y} ⊦ (p (x / y) ) =ͭ (x / y) - zero'❘# role Simplify ❙
div_1 : {x,y} ⊦ (x * y) / y =ͭ x❘# role Simplify❙
div_2 : {x,y,z} ⊦ (x /y) / z =ͭ x / (y*z)❘# role Simplify❙
div_3 : {x,y,z} ⊦ x / (y / z) =ͭ (x*z)/y❘# role Simplify❙
times_div: {w,x,y,z} ⊦ (w /x) * (y/ z) =ͭ (w*y)/(x*z) ❘# role Simplify❙
add_div : {x,y,z} ⊦ (x / z) + (y / z)=ͭ (x+y)/z❘# role Simplify❙
sub_div: {x,y,z} ⊦ (x / z) - (y / z)=ͭ (x-y)/z❘# role Simplify❙
inv_div: {x,y} ⊦ inv (x / y) =ͭ (inv x)/y❘# role Simplify❙
theory RatSpec =
include ?IntSpec ❙
include ?RatDiv ❙
sin: tm num ⟶ tm num ⟶ tm num ❘# %n ❙
cos: tm num ⟶ tm num ⟶ tm num ❘# %n ❙
tan: tm num ⟶ tm num ⟶ tm num ❘# %n ❙
theory Rat =
structure rat : ?RatSpec =
num # rationalnumber ❙
Nat # ℤ ❙
zero # zero ❙
succ # S 1 prec 31 ❙
pred # Pre 1 prec 31 ❙
plus # 1 + 2 prec 40 ❙
times # 1 * 2 prec 45 ❙
div# 1 / 2 prec 50 ❙
rule rules?Realize rat/Nat uom?StandardRat❙
rule rules?Realize zero uom?Arithmetic/Zero❙
\ No newline at end of file
namespace latin:/❚
fixmeta ?TypedEquality❚
import rules scala://lf.mmt.kwarc.info❚
import uom scala://uom.api.mmt.kwarc.info❚
theory String =
char: tp ❘# %n ❙
string: tp ❘# %n ❙
Char = tm char ❘# %n ❙
String = tm string ❘# %n❙
rule rules?Realize String uom?StandardString❙
theory String_operators =
include ?String ❙
include ?List_operators❙
string_to_char : tm string ⟶ tm List char ❘# %n 1 ❙
char_to_string : tm List char ⟶ tm string ❘# %n 1 ❙
empty: tm string ❙
String_concat: tm string ⟶ tm string ⟶ tm string ❘# %n 1 2 prec 30 ❘
= [x,y] char_to_string((string_to_char x) concat (string_to_char y)) ❙
rule rules?Realize empty uom?StringOperations/Empty❙
size: tm string ⟶ tm naturalnumber ❘# %n 1 prec 30 ❘
= [s] list/length (string_to_char s)❙
charAt: tm string ⟶ tm naturalnumber ⟶ tm char❘# %n 1 2 prec 30 ❘
= [s,n] hd drop(string_to_char s) n ❙
substring : tm string ⟶ tm naturalnumber ⟶ tm naturalnumber ⟶ tm string ❘# %n 1 2 3 prec 30 ❙
less : tm string ⟶ tm string ⟶ prop❘# %n 1 2 prec 30 ❙
greater : tm string ⟶ tm string ⟶ prop❘# %n 1 2 prec 30 ❘
= [l,m] ¬ (l =ͭ m) ∧ ¬ less l m ❙
less_equal : tm string ⟶ tm string ⟶ prop❘# %n 1 2 prec 30 ❘
= [l,m] less l m ∨ (l =ͭ m)❙
file ../../build_config.msl
// proggraming types
//depends on collection types and natural numbers
//build MMT/LATIN2 mmt-omdoc ./Strings.mmt
//depends on first order logic and Boolean
//build MMT/LATIN2 mmt-omdoc ./logicaloperations.mmt
//String and logicaloperations are build in endofunctors
\ No newline at end of file
namespace latin:/❚
fixmeta ?TypedEquality❚
theory If_then_else =
include ?TypedTerms❙
include ?Negation❙
include ?IPL ❙
if: {a} prop ⟶ tm a ⟶ tm a ⟶ tm a ❘ # if 2 then 3 else 4 prec 30❙
if_true : {a, b: prop, f1, f2: tm a} ⊦ if ⊤ then f1 else f2 =ͭ f1❘role Simplify❙
if_false : {a, b: prop ,f1 ,f2: tm a} ⊦ if ⊥ then f1 else f2 =ͭ f2❘role Simplify❙
theory Booleanooperations =
include ?Booleans ❙
include ?If_then_else ❙
prop_to_bolean: prop ⟶ tm bool ❘# %n 1 ❘
= [x] if x then tt else ff❙
bolean_to_prop: tm bool ⟶ prop ❘# %n 1 ❘
= [x] x =ͭ tt ❙
theory lazy_prop =
include ?PLND ❙
include ?If_then_else ❙
include ?Booleanooperations❙
lazy_and : prop⟶ prop⟶prop ❘# 1 AND 2 ❘
= [x,y] bolean_to_prop if x then (prop_to_bolean y) else ff❙
lazy_or : prop⟶ prop⟶prop ❘# 1 OR 2 ❘
= [x,y] bolean_to_prop if x then tt else prop_to_bolean y ❙
......@@ -9,9 +9,13 @@ build MMT/LATIN2 mmt-omdoc type_theory/endofunctors/endofunctors.mmt
// dependent on endofunctors
build MMT/LATIN2 mmt-omdoc type_theory/endofunctors/endomagmas.mmt
// collection_types depends on programming/logicaloperations.mmt
build MMT/LATIN2 mmt-omdoc programming/logicaloperations.mmt
// dependent on endomagmas
build MMT/LATIN2 mmt-omdoc type_theory/endofunctors/collection_types.mmt
//monads depends on programming/Strings
build MMT/LATIN2 mmt-omdoc programming/Strings.mmt
// dependent on endofunctors and hol
build MMT/LATIN2 mmt-omdoc type_theory/endofunctors/monads.mmt
namespace latin:/❚
fixmeta ?TypedEquality❚
theory Collection =
include ?EndoMagma❙
include ?EndoNeutral❙
singleton : {a} tm a ⟶ tm &a❘# S 2 prec 60❙
cons : {a} tm a ⟶ tm &a ⟶ tm &a❘= [a,x,xs] S x ∘ xs❙
theory ListSpec =
include ?Collection❙
include ?EndoMonoid❙
theory MultisetSpec =
include ?ListSpec❙
include ?EndoCommutative❙
theory FiniteSetSpec =
include ?MultisetSpec❙
include ?EndoIdempotent❙
theory OptionSpec =
include ?ListSpec❙
include ?EndoFirstNonNeutral❙
theory Lists =
structure list : ?ListSpec =
applyType # List 1❙
op # 2 concat 3❙
e # nil %I1❙
singleton # list 2❙
theory Multisets =
structure multiset : ?MultisetSpec =
applyType # Multiset 1❙
op # 2 munion 3❙
e # mempty %I1❙
singleton # multiset 2❙
theory FiniteSets =
structure finset : ?FiniteSetSpec =
applyType # FinSet 1❙
op # 2 union 3❙
e # empty %I1❙
singleton # finset 2❙
theory Options =
structure option : ?OptionSpec =
applyType # Option 1❙
op # 2 orelse 3❙
e # none %I1❙
singleton # option 2❙
\ No newline at end of file
namespace latin:/❚
fixmeta ?TypedEquality❚
theory Collection =
include ?EndoMagma❙
include ?EndoNeutral❙
include ?Booleanooperations❙
include ?Nat_realization❙
include ?SFOL❙
null_collection : {a} tm &a❘ # %n 1❘= [a] neutral❙
singleton : {a} tm a ⟶ tm &a❘# %n 2 prec 60❙
cons : {a} tm a ⟶ tm &a ⟶ tm &a❘# %n 2 3 prec 60❘= [a,x,xs] singleton x ∘ xs❙
inductive_proof: {a,P: tm & a ⟶ prop} ⊦ P neutral ⟶ ({x,xs} ⊦ P xs ⟶ ⊦ P (cons x xs)) ⟶ {xs} ⊦ P xs ❙
is_empty : {a} tm &a ⟶ prop❘# %n 2 prec 30❙
is_empty_neutral: {a} ⊦ is_empty (null_collection a)❙
is_empty_cons : {a,x,xs: tm & a} ⊦ ¬(is_empty (cons x xs))❙
is_empty_singelton : {a,x: tm a} ⊦ ¬(is_empty (singleton x))❙
is_empty_op : {a,l, m: tm &a} ⊦ is_empty l ⟶ ⊦ is_empty m ⟶ ⊦ is_empty l∘m❙
is_nonempty : {a} tm &a ⟶ prop❘# %n 2 prec 30❘
= [a,xs] ¬(is_empty xs)❙
length: {a} tm &a ⟶ tm naturalnumber❘# %n 2 prec 30❙
length_neutral : {a} ⊦ length (null_collection a) =ͭ zero ❙
length_cons : {a,x,xs: tm &a} ⊦(length (cons x xs)) =ͭ (S (length xs))❙
length_singelton : {a,x: tm a} ⊦ length (singleton x) =ͭ (S zero)❙
length_op : {a,l, m: tm &a} ⊦ length l∘m =ͭ (length l) + (length m)❙
contain : {a} tm & a ⟶ tm a ⟶ prop❘# %n 2 3 prec 30❙
contain_neutral: {a,x: tm a} ⊦ ¬ contain (null_collection a) x❙
contain_cons : {a,x:tm a,xs} ⊦ contain (cons x xs) x ❙
contain_cons2 : {a,x,y,ys: tm & a} ⊦ contain (cons y ys) x ⇔ contain ys x❙
map2 : {a,b} (tm a ⟶ tm & b) ⟶ tm & a ⟶ tm & b❘# %n 3 4 prec 30❙
map2_neutral : {a,b,f: tm a ⟶ tm & b} ⊦ (map2 f neutral) =ͭ neutral ❙
map2_cons : {a,b, f: tm a ⟶ tm & b,x,xs} ⊦ map2 f (cons x xs) =ͭ ((f x) ∘ (map2 f xs))❙
map2_singleton1 : {a,b,f: tm a ⟶ tm & b,x} ⊦ map2 f (singleton x) =ͭ f x❙
map2_op: {a,b,f: tm a ⟶ tm & b,l, m} ⊦ map2 f (l ∘ m) =ͭ ((map2 f l)∘ (map2 f m))❙
theory ListSpec =
include ?Collection❙
include ?EndoMonoid❙
theory MultisetSpec =
include ?ListSpec❙
include ?EndoCommutative❙
theory FiniteSetSpec =
include ?MultisetSpec❙
include ?EndoIdempotent❙
theory BinaryTreeSpec =
include ?Collection ❙
theory OptionSpec =
include ?ListSpec❙
include ?EndoFirstNonNeutral❙
theory ResultSpec =
include ?Collection❙
include ?EndoMonoid❙
theory Lists =
include ?Nat_realization ❙
structure list : ?ListSpec =
include ?Nat_realization❙
applyType # List 1❙
op # 2 concat 3❙
neutral # nil %I1❙
theory Multisets =
include ?Nat_realization ❙
structure multiset : ?MultisetSpec =
include ?Nat_realization ❙
applyType # Multiset 1❙
op # 2 munion 3❙
neutral # mempty %I1❙
singleton # multiset 2❙
theory FiniteSets =
include ?Nat_realization ❙
structure finset : ?FiniteSetSpec =
include ?Nat_realization ❙
applyType # FinSet 1❙
op # 2 union 3❙
neutral # empty %I1❙
singleton # finset 2❙
theory BinaryTree =
structure binarytree : ?BinaryTreeSpec =
applyType # BinaryTree 1❙
op # 2 union 3❙
neutral # none %I1❙
singleton # leaf 2❙
cons # node 2 3 ❙
theory Options =
structure option : ?OptionSpec =
applyType # Option 1❙
op # 2 orelse 3❙
neutral # none %I1❙
singleton # option 2❙
theory List_operators =
include ?Lists❙
hd : {a} tm List a ⟶ tm a❘# %n 2 prec 30❙
hd_cons : {a,x: tm a,xs: tm List a} ⊦ hd (list/cons x xs) =ͭ x❙
hd_singleton : {a,x: tm a} ⊦ hd list/singleton x =ͭ x❙
hd_op1: {a,l, m: tm List a}⊦ list/is_empty l ⟶ ⊦ hd (l concat m) =ͭ hd m❙
hd_op2: {a,l, m: tm List a}⊦ list/is_nonempty l ⟶ ⊦ hd (l concat m) =ͭ hd l❙
tl: {a} tm List a ⟶ tm List a❘# %n 2 prec 30❙
tl_nil : {a} ⊦ tl (list/null_collection a) =ͭ nil ❙
tl_cons : {a,x,xs: tm List a} ⊦ tl (list/cons x xs) =ͭ xs❙
tl_singleton : {a,x: tm a} ⊦ tl list/singleton x =ͭ nil❙
tl_op1: {a,l, m: tm List a}⊦ tl (l concat m) =ͭ ((tl l) concat m)❙
drop: {a} tm List a ⟶ tm naturalnumber ⟶ tm List a❘# %n 2 3 prec 30❙
drop_nil : {a,n} ⊦ drop (list/null_collection a) n =ͭ nil ❙
drop_cons1 : {a, n,x,xs: tm List a} ⊦ n =ͭ zero ⟶ ⊦ drop (list/cons x xs) n =ͭ (list/cons x xs) ❙
drop_cons2 : {a, n,x,xs: tm List a} ⊦ ¬ (S n) =ͭ (zero) ⟶ ⊦ drop (list/cons x xs) (S n) =ͭ drop xs n❙
drop_singleton1 : {a,n,x: tm a} ⊦ n =ͭ zero ⟶ ⊦ drop (list/singleton x) n =ͭ list/singleton x❙
drop_singleton2 : {a,n,x: tm a} ⊦ ¬ n =ͭ zero ⟶ ⊦ drop (list/singleton x) n =ͭ nil❙
drop_op1: {a,n,l, m: tm List a} ⊦ n =ͭ zero ⟶ ⊦ (drop (l concat m) (S n)) =ͭ (l concat m)❙
drop_op2: {a,n,l, m: tm List a} ⊦ ¬ (S n) =ͭ (zero) ⟶ ⊦ list/is_empty l ⟶ ⊦ drop (l concat m) (S n) =ͭ drop l n❙
drop_op3: {a,n,l, m: tm List a} ⊦ ¬ (S n) =ͭ (zero) ⟶ ⊦ list/is_nonempty l ⟶ ⊦ drop (l concat m) (S n) =ͭ drop ((drop l (S n)) concat m) (S n)❙
add_last: {a} tm a ⟶ tm List a ⟶ tm List a❘# %n 2 3 prec 30❙
add_last_nil : {a,x: tm a} ⊦ add_last x nil =ͭ list/cons x nil ❙
add_last_cons : {a, y,x,xs: tm List a} ⊦ add_last y (list/cons x xs) =ͭ list/cons x add_last y xs❙
add_last_singleton : {a,y,x: tm a} ⊦ add_last y (list/singleton x) =ͭ list/cons x (list/singleton y)❙
add_last_op : {a,y,l, m: tm List a} ⊦ add_last y (l concat m) =ͭ (l concat add_last y m)❙
rev: {a} tm List a ⟶ tm List a❘# %n 2 prec 30❙
rev_nil: {a} ⊦ rev (list/null_collection a) =ͭ nil❙
rev_cons: {a,x,xs: tm List a} ⊦ rev (list/cons x xs) =ͭ add_last x (rev xs)❙
rev_singleton : {a,x: tm a} ⊦ rev (list/singleton x) =ͭ list/singleton x❙
rev_op: {a,l, m: tm List a} ⊦ rev (l concat m) =ͭ ((rev m) concat (rev l))❙
list_match : {a,b} tm List a ⟶ tm b ⟶ ( tm a ⟶ tm List a ⟶ tm b) ⟶ tm b❘# 3 match_list case_nil 4 case_cons 5 prec 50❙
list_match_nil: {a,b,nilcase,conscase:tm a ⟶ tm List a ⟶ tm b}
⊦ (nil match_list case_nil nilcase case_cons conscase)
=ͭ nilcase❙
list_match_cons: {a,b,nilcase: tm b,conscase,x,xs:tm List a}