Nuprl Definition : ex-do-Intro

ex-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' ←─ note-is-function(A;numhyps;M)
                                                in <impI, [<λM.(F M modelEval(exname;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 :  note-is-function: note-is-function(A;hnum;M),  modelEval: modelEval(exname;M;n),  new-mFO-var: new-mFO-var(H),  mRuleorI: mRuleorI(left),  mRuleexistsI: existsI with var,  mRuleallI: allI with var,  mRuleimpI: impI,  mRuleandI: 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"
ex-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{}{}  note-is-function(A;numhyps;M)
                                                                                            in  <impI,  [<\mlambda{}M.(F  M  modelEval(exname;M;numhyps)),  M'>]\000C>
                            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: 2015_07_17-AM-07_57_42
Last ObjectModification: 2014_06_12-PM-05_50_35

Home Index