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