85 by (asm_simp_tac HOL_ss 1); |
85 by (asm_simp_tac HOL_ss 1); |
86 qed "is_recfun_undef"; |
86 qed "is_recfun_undef"; |
87 |
87 |
88 (*** NOTE! some simplifications need a different finish_tac!! ***) |
88 (*** NOTE! some simplifications need a different finish_tac!! ***) |
89 fun indhyp_tac hyps = |
89 fun indhyp_tac hyps = |
90 resolve_tac (TrueI::refl::hyps) ORELSE' |
|
91 (cut_facts_tac hyps THEN' |
90 (cut_facts_tac hyps THEN' |
92 DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
91 DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
93 eresolve_tac [transD, mp, allE])); |
92 eresolve_tac [transD, mp, allE])); |
94 val wf_super_ss = HOL_ss setsolver indhyp_tac; |
93 val wf_super_ss = HOL_ss addsolver indhyp_tac; |
95 |
94 |
96 val prems = goalw WF.thy [is_recfun_def,cut_def] |
95 val prems = goalw WF.thy [is_recfun_def,cut_def] |
97 "[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \ |
96 "[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \ |
98 \ (x,a):r --> (x,b):r --> f(x)=g(x)"; |
97 \ (x,a):r --> (x,b):r --> f(x)=g(x)"; |
99 by (cut_facts_tac prems 1); |
98 by (cut_facts_tac prems 1); |