Nuprl Definition : fun-do-Intro
fun-do-Intro(exname;H;G;numhyps;val;fullevd) ==
  let F,M = fullevd 
  in mFOL_ind(G;
              mFOatomic(P,vars)
⇒ "should not happen??";
              mFOconnect(knd,A,B)
⇒ _,__.if knd =a "imp"
                                           then let M' ⟵ update-fun(M;A;numhyps)
                                                in <impI, [<λM.(F M (M numhyps)), M'>]>
              if knd =a "and" then <andI, [<λM.(fst((F M))), M> <λM.(snd((F M))), M>]>
              if knd =a "or"
                then case val of inl(_) => <orI left, [<λM.outl(F M), M>]> | inr(_) => <orI right, [<λM.outr(F M), M>]>
              else "funny connective??"
              fi
              mFOquant(isall,v,body)
⇒ _.if isall
              then eval m = new-mFO-var(H) in
                   <allI with m, [<λM.(F M m), M>]>
              else eval j = fst(val) in
                   <existsI with j, [<λM.(snd((F M))), M>]>
              fi ) 
Definitions occuring in Statement : 
update-fun: update-fun(M;A;hnum)
, 
new-mFO-var: new-mFO-var(H)
, 
fRuleorI: fRuleorI(left)
, 
fRuleexistsI: existsI with var
, 
fRuleallI: allI with var
, 
fRuleimpI: impI
, 
fRuleandI: andI
, 
mFOL_ind: mFOL_ind, 
cons: [a / b]
, 
nil: []
, 
callbyvalueall: callbyvalueall, 
callbyvalue: callbyvalue, 
outr: outr(x)
, 
outl: outl(x)
, 
ifthenelse: if b then t else f fi 
, 
eq_atom: x =a y
, 
bfalse: ff
, 
btrue: tt
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
apply: f a
, 
lambda: λx.A[x]
, 
spread: spread def, 
pair: <a, b>
, 
decide: case b of inl(x) => s[x] | inr(y) => t[y]
, 
token: "$token"
Definitions occuring in definition : 
nil: []
, 
apply: f a
, 
pi2: snd(t)
, 
lambda: λx.A[x]
, 
pair: <a, b>
, 
cons: [a / b]
, 
fRuleexistsI: existsI with var
, 
pi1: fst(t)
, 
callbyvalue: callbyvalue, 
fRuleallI: allI with var
, 
new-mFO-var: new-mFO-var(H)
, 
ifthenelse: if b then t else f fi 
, 
token: "$token"
, 
outr: outr(x)
, 
bfalse: ff
, 
fRuleorI: fRuleorI(left)
, 
outl: outl(x)
, 
btrue: tt
, 
decide: case b of inl(x) => s[x] | inr(y) => t[y]
, 
eq_atom: x =a y
, 
fRuleandI: andI
, 
fRuleimpI: impI
, 
update-fun: update-fun(M;A;hnum)
, 
callbyvalueall: callbyvalueall, 
mFOL_ind: mFOL_ind, 
spread: spread def
FDL editor aliases : 
fun-do-Intro
Latex:
fun-do-Intro(exname;H;G;numhyps;val;fullevd)  ==
    let  F,M  =  fullevd 
    in  mFOL\_ind(G;
                            mFOatomic(P,vars){}\mRightarrow{}  "should  not  happen??";
                            mFOconnect(knd,A,B){}\mRightarrow{}  $_{}$,\_$_{}$.if  knd  =a  "\000Cimp"
                                                                                  then  let  M'  \mleftarrow{}{}  update-fun(M;A;numhyps)
                                                                                            in  <impI,  [<\mlambda{}M.(F  M  (M  numhyps)),  M'>]>
                            if  knd  =a  "and"  then  <andI,  [<\mlambda{}M.(fst((F  M))),  M>  <\mlambda{}M.(snd((F  M))),  M>]>
                            if  knd  =a  "or"
                                then  case  val
                                            of  inl($_{}$)  =>
                                            <orI  left,  [<\mlambda{}M.outl(F  M),  M>]>
                                            |  inr($_{}$)  =>
                                            <orI  right,  [<\mlambda{}M.outr(F  M),  M>]>
                            else  "funny  connective??"
                            fi  ;
                            mFOquant(isall,v,body){}\mRightarrow{}  $_{}$.if  isall
                            then  eval  m  =  new-mFO-var(H)  in
                                      <allI  with  m,  [<\mlambda{}M.(F  M  m),  M>]>
                            else  eval  j  =  fst(val)  in
                                      <existsI  with  j,  [<\mlambda{}M.(snd((F  M))),  M>]>
                            fi  ) 
Date html generated:
2017_01_19-PM-02_32_11
Last ObjectModification:
2017_01_18-PM-06_23_29
Theory : minimal-first-order-logic
Home
Index