(* Title: HOL/Eisbach/eisbach_rule_insts.ML
Author: Daniel Matichuk, NICTA/UNSW
Eisbach-aware variants of the "where" and "of" attributes.
Alternate syntax for rule_insts.ML participates in token closures by
examining the behaviour of Rule_Insts.where_rule and instantiating token
values accordingly. Instantiations in re-interpretation are done with
infer_instantiate.
*)structureEisbach_Rule_Insts:sigend=structfunrestore_tagsthm=Thm.map_tags(K(Thm.get_tagsthm));valmk_term_type_internal=Logic.protectoLogic.mk_termoLogic.mk_type;funterm_type_casesfgt=(case\<^try>‹Logic.dest_type(Logic.dest_term(Logic.unprotectt))›ofSOMET=>fT|NONE=>(case\<^try>‹Logic.dest_termt›ofSOMEt=>gt|NONE=>raiseFail"Lost encoded instantiation"))funadd_thm_instsctxtthm=letvaltyvars=Thm.fold_terms{hyps=false}Term.add_tvarsthm[];valtyvars'=tyvars|>map(mk_term_type_internaloTVar);valtvars=Thm.fold_terms{hyps=false}Term.add_varsthm[];valtvars'=tvars|>map(Logic.mk_termoVar);valconj=Logic.mk_conjunction_list(tyvars'@tvars')|>Thm.cterm_ofctxt|>Drule.mk_term;in((tyvars,tvars),Conjunction.intrthmconj)end;funget_thm_inststhm=letval(thm',insts)=Conjunction.elimthm;valinsts'=insts|>Drule.dest_term|>Thm.term_of|>Logic.dest_conjunction_list|>(fnf=>fold(fnt=>fn(tys,ts)=>term_type_cases(fnT=>(T::tys,ts))(fnt=>(tys,t::ts))t)f([],[]))||>rev|>>rev;in(thm',insts')end;funinstantiate_xisctxtinststhm=letvaltyvars=Thm.fold_terms{hyps=false}Term.add_tvarsthm[];valtvars=Thm.fold_terms{hyps=false}Term.add_varsthm[];funadd_inst(xi,t)(Ts,ts)=(caseAList.lookup(op=)tyvarsxiofSOMES=>(((xi,S),Thm.ctyp_ofctxt(Logic.dest_typet))::Ts,ts)|NONE=>(caseAList.lookup(op=)tvarsxiofSOME_=>(Ts,(xi,Thm.cterm_ofctxtt)::ts)|NONE=>error"indexname not found in thm"));val(instT,inst)=foldadd_instinsts([],[]);in(Thm.instantiate(TVars.makeinstT,Vars.empty)thm|>infer_instantiatectxtinstCOMP_INCRasm_rl)|>Thm.adjust_maxidx_thm~1|>restore_tagsthmend;datatyperule_inst=Named_Instsof((indexname * string) * (term -> unit)) list * (binding * string option * mixfix) list
|Term_Instsof(indexname * term) list
|Unchecked_Term_Instsof term option list * term option list;funmk_pair(t,t')=Logic.mk_conjunction(Logic.mk_termt,Logic.mk_termt');fundest_pairt=apply2Logic.dest_term(Logic.dest_conjunctiont);funembed_indexname((xi,s),f)=letfunwrap_xixit=mk_pair(Var(xi,fastype_oft),t);in((xi,s),fowrap_xixi)end;fununembed_indexnamet=dest_pairt|>apfst(Term.dest_Var#>fst);funread_where_insts(insts,fixes)=letvalinsts'=ifforall(fn(_,v)=>Parse_Tools.is_real_valv)inststhenTerm_Insts(map(unembed_indexnameoParse_Tools.the_real_valosnd)insts)elseNamed_Insts(map(fn(xi,p)=>embed_indexname((xi,Parse_Tools.the_parse_valp),Parse_Tools.the_parse_funp))insts,fixes);ininsts'end;funof_rulethm(args,concl_args)=letfunzip_vars_[]=[]|zip_vars(_::xs)(NONE::rest)=zip_varsxsrest|zip_vars((x,_)::xs)(SOMEt::rest)=(x,t)::zip_varsxsrest|zip_vars[]_=error"More instantiations than variables in theorem";valinsts=zip_vars(rev(Term.add_vars(Thm.full_prop_ofthm)[]))args@zip_vars(rev(Term.add_vars(Thm.concl_ofthm)[]))concl_args;ininstsend;valinst=Args.maybeParse_Tools.name_term;valconcl=Args.$$$"concl"--Args.colon;funclose_unchecked_instscontext((insts,concl_inst),fixes)=letvalctxt=Context.proof_ofcontext;valctxt1=ctxt|>Proof_Context.add_fixes_cmdfixes|>#2;valinsts'=insts@concl_inst;valterm_insts=map(the_listo(Option.mapParse_Tools.the_parse_val))insts'|>burrow(Syntax.read_termsctxt1#>Variable.export_termsctxt1ctxt)|>map(trythe_single);val_=(insts',term_insts)|>ListPair.app(fn(SOMEp,SOMEt)=>Parse_Tools.the_parse_funpt|_=>());val(insts'',concl_insts'')=chop(lengthinsts)term_insts;inUnchecked_Term_Insts(insts'',concl_insts'')end;funread_of_instscheckedcontext((insts,concl_insts),fixes)=ifforall(fnSOMEt=>Parse_Tools.is_real_valt|NONE=>true)(insts@concl_insts)thenifcheckedthen(fn_=>Term_Insts(map(unembed_indexnameoParse_Tools.the_real_val)(map_filterI(insts@concl_insts))))else(fn_=>Unchecked_Term_Insts(map(Option.mapParse_Tools.the_real_val)insts,map(Option.mapParse_Tools.the_real_val)concl_insts))elseifcheckedthen(fnthm=>Named_Insts(apply2(map(Option.map(fnp=>(Parse_Tools.the_parse_valp,Parse_Tools.the_parse_funp))))(insts,concl_insts)|>of_rulethm|>map((fn(xi,(nm,f))=>embed_indexname((xi,nm),f))),fixes))elseletvalresult=close_unchecked_instscontext((insts,concl_insts),fixes);infn_=>resultend;funread_instantiate_closedctxt(Named_Insts(insts,fixes))thm=letvalinsts'=map(fn((v,t),_)=>((v,Position.none),t))insts;val(thm_insts,thm')=add_thm_instsctxtthm;val(thm'',thm_insts')=Rule_Insts.where_rulectxtinsts'fixesthm'|>get_thm_insts;valtyinst=ListPair.zip(fstthm_insts,fstthm_insts')|>map(fn((xi,_),typ)=>(xi,typ));valtinst=ListPair.zip(sndthm_insts,sndthm_insts')|>map(fn((xi,_),t)=>(xi,t));val_=map(fn((xi,_),f)=>(caseAList.lookup(op=)tyinstxiofSOMEtyp=>f(Logic.mk_typetyp)|NONE=>(caseAList.lookup(op=)tinstxiofSOMEt=>ft|NONE=>error"Lost indexname in instantiated theorem")))insts;in(thm''|>restore_tagsthm)end|read_instantiate_closedctxt(Unchecked_Term_Instsinsts)thm=letval(xis,ts)=ListPair.unzip(of_rulethminsts);valctxt'=Variable.declare_maxidx(Thm.maxidx_ofthm)ctxt;val(ts',ctxt'')=Variable.import_termsfalsetsctxt';valts''=Variable.export_termsctxt''ctxtts';valinsts'=ListPair.zip(xis,ts'');ininstantiate_xisctxtinsts'thmend|read_instantiate_closedctxt(Term_Instsinsts)thm=instantiate_xisctxtinststhm;val_=Theory.setup(Attrib.setup\<^binding>‹where›(Scan.lift(Parse.and_list1(Args.var--(Args.$$$"="|--Parse_Tools.name_term))--Parse.for_fixes)>>(fnargs=>letvalargs'=read_where_instsargsinfn(context,thm)=>(NONE,SOME(read_instantiate_closed(Context.proof_ofcontext)args'thm))end))"named instantiation of theorem");val_=Theory.setup(Attrib.setup\<^binding>‹of›(Scan.lift(Args.mode"unchecked"--(Scan.repeat(Scan.unlessconclinst)--Scan.optional(concl|--Scan.repeatinst)[]--Parse.for_fixes))--Scan.state>>(fn((unchecked,args),context)=>letvalread_insts=read_of_insts(notunchecked)contextargs;infn(context,thm)=>letvalthm'=ifThm.is_free_dummythmandalsouncheckedthenDrule.free_dummy_thmelseread_instantiate_closed(Context.proof_ofcontext)(read_inststhm)thmin(NONE,SOMEthm')endend))"positional instantiation of theorem");end;