opentheory/postbool/Opentheory.sml

158   fun f "absTerm"(st as {stack=OTerm b::OVar v::os,...}) = st_(OTerm(mk_abs(v,b))::os,st)
159     | f "absThm" (st as {stack=OThm th::OVar v::os,...}) = (st_(OThm(ABS v th)::os,st)
161     | f "appTerm"(st as {stack=OTerm x::OTerm f::os,...})= st_(OTerm(mk_comb(f,x))::os,st)
162     | f "appThm" (st as {stack=OThm xy::OThm fg::os,...})= let
167       in st_(OThm(TRANS fxgx gxgy)::os,st) end
168     | f "assume"       (st as {stack=OTerm t::os,...})          = st_(OThm(ASSUME t)::os,st)
169     | f "axiom"        (st as {stack=OTerm t::OList ts::os,thms,...}) = st_(OThm(axiom thms (unOTermls "axiom" ts,t))::os,st)
170     | f "betaConv"     (st as {stack=OTerm t::os,...})          = st_(OThm(BETA_CONV t)::os,st)
171     | f "cons"         (st as {stack=OList t::h::os,...})       = st_(OList(h::t)::os,st)
172     | f "const"        (st as {stack=OName n::os,...})          = st_(OConst (ot_to_const "const" n)::os,st)
173     | f "constTerm"    (st as {stack=OType Ty::OConst {Thy,Name}::os,...})
174                      = st_(OTerm(mk_thy_const {Ty=Ty,Thy=Thy,Name=Name})::os,st)
175     | f "deductAntisym"(st as {stack=OThm t1::OThm t2::os,...}) = st_(OThm(DEDUCT_ANTISYM t1 t2)::os,st)
176     | f "def"         {stack=ONum k::x::os,dict,thms,...}       = {stack=x::os,dict=Map.insert(dict,k,x),thms=thms}
177     | f "defineConst" (st as {stack=OTerm t::OName n::os,...})  = let
181       in st_(OThm def::OConst c::os,st) end
182     | f "defineTypeOp"  (st as {stack=OThm ax::OList ls::OName rep::OName abs::OName n::os,...}) = let
191       in st_(OThm rep_abs::OThm abs_rep::OConst rep::OConst abs::OTypeOp tyop::os,st) end
192     | f "eqMp"   (st as {stack=OThm f::OThm fg::os,...})     = (st_(OThm(EQ_MP fg f)::os,st)
195     | f "opType" (st as {stack=OList ls::OTypeOp {Thy,Tyop}::os,...})
196                = st_(OType(mk_thy_type{Thy=Thy,Tyop=Tyop,Args=unOTypels "opType" ls})::os,st)
198     | f "pop"    (st as {stack=OList[OList hl,OTerm c]::OThm th::os,line_num,...}) = let
213      in st_(OThm th::os,st) end
215     | f "pop"    (st as {stack=x::os,...})                   = st_(os,st)
216     | f "ref"    (st as {stack=ONum k::os,dict,...})         = st_(Map.find(dict,k)::os,st)
217     | f "refl"   (st as {stack=OTerm t::os,...})             = st_(OThm(REFL t)::os,st)
218     | f "remove" {stack=ONum k::os,dict,thms,...}            = let
220       in {stack=x::os,dict=dict,thms=thms} end
221     | f "subst"  (st as {stack=OThm th::OList[OList tys,OList tms]::os,...}) = let
228       in st_(OThm th::os,st) end
229     | f "thm"    {stack=OTerm c::OList ls::OThm th::os,dict,thms,...} = let
246       in {stack=os,dict=dict,thms=Net.insert(concl th,th)thms} end
247     | f "typeOp"  (st as {stack=OName n::os,...})          = st_(OTypeOp (ot_to_tyop "typeOp" n)::os,st)
248     | f "version" (st as {stack=ONum n::os,...})           = if n = 6 then st_(os,st) else raise ERR "unsupported article version"
249     | f "var"     (st as {stack=OType t::OName n::os,...}) = st_(OVar(mk_var(n,t))::os,st)
250     | f "varTerm" (st as {stack=OVar t::os,...})           = st_(OTerm t::os,st)
251     | f "varType" (st as {stack=OName n::os,...})          = st_(OType(mk_vartype n)::os,st)