103 val concl = |
103 val concl = |
104 HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj}) |
104 HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj}) |
105 (map (fn ((((i, _), T), U), tname) => |
105 (map (fn ((((i, _), T), U), tname) => |
106 make_pred i U T (mk_proj i is r) (Free (tname, T))) |
106 make_pred i U T (mk_proj i is r) (Free (tname, T))) |
107 (descr ~~ recTs ~~ rec_result_Ts ~~ tnames))); |
107 (descr ~~ recTs ~~ rec_result_Ts ~~ tnames))); |
108 val inst = map (apply2 (Thm.global_cterm_of thy)) (map head_of (HOLogic.dest_conj |
108 val inst = map (apply2 (Thm.cterm_of ctxt)) (map head_of (HOLogic.dest_conj |
109 (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps); |
109 (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps); |
110 |
110 |
111 val thm = |
111 val thm = |
112 Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems) (Thm.global_cterm_of thy concl) |
112 Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl) |
113 (fn prems => |
113 (fn prems => |
114 EVERY [ |
114 EVERY [ |
115 rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]), |
115 rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]), |
116 rtac (cterm_instantiate inst induct) 1, |
116 rtac (cterm_instantiate inst induct) 1, |
117 ALLGOALS (Object_Logic.atomize_prems_tac ctxt), |
117 ALLGOALS (Object_Logic.atomize_prems_tac ctxt), |
183 |
183 |
184 val y = Var (("y", 0), Logic.varifyT_global T); |
184 val y = Var (("y", 0), Logic.varifyT_global T); |
185 val y' = Free ("y", T); |
185 val y' = Free ("y", T); |
186 |
186 |
187 val thm = |
187 val thm = |
188 Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems) |
188 Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) |
189 (Thm.global_cterm_of thy |
189 (Thm.cterm_of ctxt |
190 (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y'])))) |
190 (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y'])))) |
191 (fn prems => |
191 (fn prems => |
192 EVERY [ |
192 EVERY [ |
193 rtac (cterm_instantiate [apply2 (Thm.global_cterm_of thy) (y, y')] exhaust) 1, |
193 rtac (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust) 1, |
194 ALLGOALS (EVERY' |
194 ALLGOALS (EVERY' |
195 [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites), |
195 [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites), |
196 resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])]) |
196 resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])]) |
197 |> Drule.export_without_context; |
197 |> Drule.export_without_context; |
198 |
198 |