366 val _ = Output.debug (fn () => " index_th2: " ^ Int.toString index_th2) |
366 val _ = Output.debug (fn () => " index_th2: " ^ Int.toString index_th2) |
367 in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end |
367 in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end |
368 end; |
368 end; |
369 |
369 |
370 (* INFERENCE RULE: REFL *) |
370 (* INFERENCE RULE: REFL *) |
371 val refl_x = cterm_of @{theory} (hd (term_vars (prop_of REFL_THM))); |
371 val refl_x = cterm_of (the_context ()) (hd (term_vars (prop_of REFL_THM))); |
372 val refl_idx = 1 + Thm.maxidx_of REFL_THM; |
372 val refl_idx = 1 + Thm.maxidx_of REFL_THM; |
373 |
373 |
374 fun refl_inf ctxt t = |
374 fun refl_inf ctxt t = |
375 let val thy = ProofContext.theory_of ctxt |
375 let val thy = ProofContext.theory_of ctxt |
376 val i_t = singleton (fol_terms_to_hol ctxt) t |
376 val i_t = singleton (fol_terms_to_hol ctxt) t |
470 (* Translation of HO Clauses *) |
470 (* Translation of HO Clauses *) |
471 (* ------------------------------------------------------------------------- *) |
471 (* ------------------------------------------------------------------------- *) |
472 |
472 |
473 fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th); |
473 fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th); |
474 |
474 |
475 val equal_imp_fequal' = cnf_th @{theory} (thm"equal_imp_fequal"); |
475 val equal_imp_fequal' = cnf_th (the_context ()) (thm"equal_imp_fequal"); |
476 val fequal_imp_equal' = cnf_th @{theory} (thm"fequal_imp_equal"); |
476 val fequal_imp_equal' = cnf_th (the_context ()) (thm"fequal_imp_equal"); |
477 |
477 |
478 val comb_I = cnf_th @{theory} ResHolClause.comb_I; |
478 val comb_I = cnf_th (the_context ()) ResHolClause.comb_I; |
479 val comb_K = cnf_th @{theory} ResHolClause.comb_K; |
479 val comb_K = cnf_th (the_context ()) ResHolClause.comb_K; |
480 val comb_B = cnf_th @{theory} ResHolClause.comb_B; |
480 val comb_B = cnf_th (the_context ()) ResHolClause.comb_B; |
481 val comb_C = cnf_th @{theory} ResHolClause.comb_C; |
481 val comb_C = cnf_th (the_context ()) ResHolClause.comb_C; |
482 val comb_S = cnf_th @{theory} ResHolClause.comb_S; |
482 val comb_S = cnf_th (the_context ()) ResHolClause.comb_S; |
483 |
483 |
484 fun type_ext thy tms = |
484 fun type_ext thy tms = |
485 let val subs = ResAtp.tfree_classes_of_terms tms |
485 let val subs = ResAtp.tfree_classes_of_terms tms |
486 val supers = ResAtp.tvar_classes_of_terms tms |
486 val supers = ResAtp.tvar_classes_of_terms tms |
487 and tycons = ResAtp.type_consts_of_terms thy tms |
487 and tycons = ResAtp.type_consts_of_terms thy tms |