156 val ((ps, t'), _) = focus_ex t nctxt |
156 val ((ps, t'), _) = focus_ex t nctxt |
157 val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t') |
157 val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t') |
158 in |
158 in |
159 (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs)) |
159 (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs)) |
160 end |
160 end |
161 val x = (Thm.cterm_of thy o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o |
161 val x = (Thm.global_cterm_of thy o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o |
162 Logic.dest_implies o Thm.prop_of) @{thm exI} |
162 Logic.dest_implies o Thm.prop_of) @{thm exI} |
163 fun prove_introrule (index, (ps, introrule)) = |
163 fun prove_introrule (index, (ps, introrule)) = |
164 let |
164 let |
165 val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1 |
165 val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1 |
166 THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1 |
166 THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1 |
167 THEN (EVERY (map (fn y => |
167 THEN (EVERY (map (fn y => |
168 rtac (Drule.cterm_instantiate [(x, Thm.cterm_of thy (Free y))] @{thm exI}) 1) ps)) |
168 rtac (Drule.cterm_instantiate [(x, Thm.global_cterm_of thy (Free y))] @{thm exI}) 1) ps)) |
169 THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1) |
169 THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1) |
170 THEN TRY (assume_tac ctxt' 1) |
170 THEN TRY (assume_tac ctxt' 1) |
171 in |
171 in |
172 Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac) |
172 Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac) |
173 end |
173 end |