155 lthy') |
155 lthy') |
156 end |
156 end |
157 |
157 |
158 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = |
158 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = |
159 let |
159 let |
160 val thy = ProofContext.theory_of ctxt |
160 val thy = Proof_Context.theory_of ctxt |
161 |
161 |
162 val oqnames = map fst pre_qs |
162 val oqnames = map fst pre_qs |
163 val (qs, _) = Variable.variant_fixes oqnames ctxt |
163 val (qs, _) = Variable.variant_fixes oqnames ctxt |
164 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
164 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
165 |
165 |
227 val goal_rhs = list_comb (f, map (mk_perm p) args) |
227 val goal_rhs = list_comb (f, map (mk_perm p) args) |
228 in |
228 in |
229 Goal.prove ctxt' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs)) |
229 Goal.prove ctxt' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs)) |
230 (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) |
230 (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) |
231 THEN (asm_full_simp_tac ss 1)) |
231 THEN (asm_full_simp_tac ss 1)) |
232 |> singleton (ProofContext.export ctxt' ctxt) |
232 |> singleton (Proof_Context.export ctxt' ctxt) |
233 |> restore_cond |
233 |> restore_cond |
234 |> export |
234 |> export |
235 end |
235 end |
236 |
236 |
237 fun mk_applied_form ctxt caTs thm = |
237 fun mk_applied_form ctxt caTs thm = |
238 let |
238 let |
239 val thy = ProofContext.theory_of ctxt |
239 val thy = Proof_Context.theory_of ctxt |
240 val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) |
240 val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) |
241 in |
241 in |
242 fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm |
242 fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm |
243 |> Conv.fconv_rule (Thm.beta_conversion true) |
243 |> Conv.fconv_rule (Thm.beta_conversion true) |
244 |> fold_rev Thm.forall_intr xs |
244 |> fold_rev Thm.forall_intr xs |
245 |> Thm.forall_elim_vars 0 |
245 |> Thm.forall_elim_vars 0 |
246 end |
246 end |
247 |
247 |
248 fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) = |
248 fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) = |
249 let |
249 let |
250 val cert = cterm_of (ProofContext.theory_of lthy) |
250 val cert = cterm_of (Proof_Context.theory_of lthy) |
251 val newPs = |
251 val newPs = |
252 map2 (fn Pname => fn MutualPart {cargTs, ...} => |
252 map2 (fn Pname => fn MutualPart {cargTs, ...} => |
253 Free (Pname, cargTs ---> HOLogic.boolT)) |
253 Free (Pname, cargTs ---> HOLogic.boolT)) |
254 (mutual_induct_Pnames (length parts)) parts |
254 (mutual_induct_Pnames (length parts)) parts |
255 |
255 |
338 |
338 |
339 fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac |
339 fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac |
340 in |
340 in |
341 Goal.prove ctxt' (flat arg_namess) [] goal |
341 Goal.prove ctxt' (flat arg_namess) [] goal |
342 (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms))) |
342 (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms))) |
343 |> singleton (ProofContext.export ctxt' ctxt) |
343 |> singleton (Proof_Context.export ctxt' ctxt) |
344 |> split_conj_thm |
344 |> split_conj_thm |
345 |> map (fn th => th RS mp) |
345 |> map (fn th => th RS mp) |
346 end |
346 end |
347 |
347 |
348 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
348 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |