examples/HolCheck/cearTools.sml

465 (* note enveq thm requires that both env and aenv be empty: this is true for instance if mf was originally in CTL*/LTL/CTL etc. *)
468 fun mk_abs_cons_thm mf (apl,ks_def,wfKS_ks) env aenv hd_def iaf_ vm =
481                                                    list_mk_comb(inst [alpha|->s_ty] pred_setSyntax.in_tm,[svar,mk_comb(env,Qvar)]))))
483         (*``(!Q s sh. (^hnc) (s,sh) ==> sh IN (^aenv) Q ==> s IN (^env) Q)``*)
487         val _ = dbgTools.DTM (dpfx^"mact_ env") env (*DBG*)
488         val _ = dbgTools.DTY (dpfx^"mact_ env") (type_of env) (*DBG*)
490         val iaf = ISPEC env iaf_
493                                          (ISPECL [mf,hnc,lhs(concl(ks_def)),env,aenv] ABS_CONS_MODEL)
500                                         [mf,hnc,lhs(concl(ks_def)),env,aenv]) (instf conc) end
678                  env aenv Ree k (nf,mf) (aksinfo,abs_aks) mu_ic_snd vm (aapl,apsubs) =
713                       then let val acm = mk_abs_cons_thm mf (apl,ks_def,wfKS_ks) env aenv hd_def iaf vm
742                    hd_def af aksname ath_lem1 ath_lem2 iaf env aenv Ree (k+1) (nf,mf) (NONE,NONE) (#th(mu_ic)) vm
757         val ((astate,af),state,env,aenv,Ree,k,unwind_thm,hR_defs_,hd_def) =
760                      val env = inst [alpha |-> type_of state] envTools.empty_env_tm
764                  in ((astate,af),state,env,aenv,Ree,k,unwind_thm,hR_defs_,hd_def) end
784                      ((astate,af),state,env,aenv,Ree,k,unwind_thm,hR_defs_,hd_def),
813              val env = el 3 (snd(strip_comb(snd(strip_forall(concl th)))))
814              val _ = dbgTools.DTM (dpfx^"fin_env") env(*DBG*)
832                                           val _ = dbgTools.DTM (dpfx^"fin_env") env(*DBG*)
833                                           val _ = dbgTools.CBTM (dpfx^"fin_env") env (*DBG*)
834                                           val sapth = ISPECL [mf,g,rand ap,env] apth
874                                 ((astate,af),state,env,aenv,Ree,k,abst_def,hR_defs_,hd_def),
882                                                               env aenv Ree k (nf,mf2)
893                             {abs_df=SOME((astate,af),state,env,aenv,Ree,k,abst_def,hR_defs_,hd_def)}))