#!/usr/local/bin/aut { ----------------------------- type.ml ----------------------------------3-- } * type : TYPE := PRIM * bool : type := PRIM * [A:type][B:type] fun : type := PRIM { ----------------------------- term.ml ----------------------------------4-- } A * term : TYPE := PRIM B * [t:term(fun(A,B))][u:term(A)] comb : term(B) := PRIM B * [t:[x,term(A)]term(B)] lambda : term(fun(A,B)) := PRIM # "abs" is used in the type definitions A * eq : term(fun(A,fun(A,bool))) := PRIM A * [t:term(A)][u:term(A)] eq' : term(bool) := comb(A,bool,comb(A,fun(A,bool),eq(A),t),u) { ----------------------------- thm.ml ----------------------------------13-- } * [t:term(bool)] thm : TYPE := PRIM A * [t:term(A)] REFL : thm(eq'(A,t,t)) := PRIM B * [s:term(fun(A,B))][t:term(fun(A,B))][u:term(A)][v:term(A)] [_st:thm(eq'(fun(A,B),s,t))][_uv:thm(eq'(A,u,v))] MK_COMB : thm(eq'(B,comb(s,u),comb(t,v))) := PRIM B * [s:[x,term(A)]term(B)][t:[x,term(A)]term(B)] [_st:[x,term(A)]thm(eq'(B,s,t))] ABS : thm(eq'(fun(A,B),lambda(s),lambda(t))) := PRIM B * [t:[x,term(A)]term(B)][x:term(A)] BETA : thm(eq'(B,comb(A,B,lambda(t),x),t)) := PRIM # ASSUME * [p:term(bool)][q:term(bool)][_pq:thm(eq'(bool,p,q))][_p:thm(p)] EQ_MP : thm(q) := PRIM q * [_p:[_q,thm(q)]thm(p)][_q:[_p,thm(p)]thm(q)] DEDUCT_ANTISYM_RULE : thm(eq'(bool,p,q)) := PRIM # INST # INST_TYPE { A * [s:term(A)][t:term(A)][u:term(A)][_st:thm(eq'(A,s,t))][_tu:thm(eq'(A,t,u))] TRANS : thm(eq'(A,s,u)) := EQ_MP(eq'(A,s,t),eq'(A,s,u), MK_COMB(A,bool,comb(A,fun(A,bool),eq(A),s),comb(A,fun(A,bool),eq(A),s), t,u,REFL(fun(A,bool),comb(A,fun(A,bool),eq(A),s)),_tu),_st) } # new_definition A * [P:term(fun(A,bool))][t:term(A)][_Pt:thm(comb(A,bool,P,t))] new_type : type := PRIM _Pt * abs : term(fun(A,new_type)) := PRIM _Pt * rep : term(fun(new_type,A)) := PRIM _Pt * [a:term(new_type)] _absrep : thm(eq'(new_type,comb(A,new_type,abs,comb(new_type,A,rep,a)),a)) := PRIM _Pt * [r:term(A)] _repabs : thm(eq'(bool,comb(A,bool,P,r), eq'(A,comb(new_type,A,rep,comb(A,new_type,abs,r)),r))) := PRIM { ----------------------------- bool.ml ----------------------------------0-- } * T : term(bool) := eq'(fun(bool,bool),lambda(bool,bool,[x,term(bool)]x), lambda(bool,bool,[x,term(bool)]x)) * and : term(fun(bool,fun(bool,bool))) := lambda(bool,fun(bool,bool),[t1,term(bool)]lambda(bool,bool,[t2,term(bool)] eq'(fun(fun(bool,fun(bool,bool)),bool), lambda(fun(bool,fun(bool,bool)),bool,[f,term(fun(bool,fun(bool,bool)))] comb(bool,bool,comb(bool,fun(bool,bool),f,t1),t2)), lambda(fun(bool,fun(bool,bool)),bool,[f,term(fun(bool,fun(bool,bool)))] comb(bool,bool,comb(bool,fun(bool,bool),f,T),T))))) * [p:term(bool)][q:term(bool)] and' : term(bool) := comb(bool,bool,comb(bool,fun(bool,bool),and,p),q) * imp : term(fun(bool,fun(bool,bool))) := lambda(bool,fun(bool,bool),[t1,term(bool)]lambda(bool,bool,[t2,term(bool)] eq'(bool,and'(t1,t2),t1))) q * imp' : term(bool) := comb(bool,bool,comb(bool,fun(bool,bool),imp,p),q) A * forall : term(fun(fun(A,bool),bool)) := lambda(fun(A,bool),bool,[P,term(fun(A,bool))] eq'(fun(A,bool),P,lambda(A,bool,[x,term(A)]T))) A * [P:[x,term(A)]term(bool)] forall' : term(bool) := comb(fun(A,bool),bool,forall,lambda(A,bool,P)) A * exists : term(fun(fun(A,bool),bool)) := lambda(fun(A,bool),bool,[P,term(fun(A,bool))] forall'(bool,[Q,term(bool)] imp'(forall'(A,[x,term(A)]imp'(comb(A,bool,P,x),Q)),Q))) P * exists' : term(bool) := comb(fun(A,bool),bool,exists,lambda(A,bool,P)) * F : term(bool) := forall'(bool,[t,term(bool)]t) * not : term(fun(bool,bool)) := lambda(bool,bool,[t,term(bool)]imp'(t,F)) p * not' : term(bool) := comb(bool,bool,not,p) { ----------------------------- num.ml -----------------------------------2-- } * ind : type := PRIM B * ONE_ONE : term(fun(fun(A,B),bool)) := lambda(fun(A,B),bool,[f,term(fun(A,B))] forall'(A,[x1,term(A)]forall'(A,[x2,term(A)] imp'(eq'(B,comb(A,B,f,x1),comb(A,B,f,x2)),eq'(A,x1,x2))))) B * ONTO : term(fun(fun(A,B),bool)) := lambda(fun(A,B),bool,[f,term(fun(A,B))] forall'(B,[y,term(B)]exists'(A,[x,term(A)]eq'(B,y,comb(A,B,f,x))))) * INFINITY_AX : thm(exists'(fun(ind,ind),[f,term(fun(ind,ind))] and'(comb(fun(ind,ind),bool,ONE_ONE(ind,ind),f), not'(comb(fun(ind,ind),bool,ONTO(ind,ind),f))))) := PRIM { ----------------------------- class.ml ---------------------------------3-- } B * ETA_AX : thm(forall'(fun(A,B),[t,term(fun(A,B))] eq'(fun(A,B),lambda(A,B,[x,term(A)]comb(A,B,t,x)),t))) := PRIM A * select : term(fun(fun(A,bool),A)) := PRIM A * SELECT_AX : thm(forall'(fun(A,bool),[P,term(fun(A,bool))]forall'(A,[x,term(A)] imp'(comb(A,bool,P,x),comb(A,bool,P,comb(fun(A,bool),A,select,P)))))) := PRIM