136 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
136 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
137 let |
137 let |
138 val ((f, (_, f_defthm)), lthy') = |
138 val ((f, (_, f_defthm)), lthy') = |
139 Local_Theory.define |
139 Local_Theory.define |
140 ((Binding.name fname, mixfix), |
140 ((Binding.name fname, mixfix), |
141 ((Binding.conceal (Binding.name (fname ^ "_def")), []), |
141 ((Binding.concealed (Binding.name (fname ^ "_def")), []), |
142 Term.subst_bound (fsum, f_def))) lthy |
142 Term.subst_bound (fsum, f_def))) lthy |
143 in |
143 in |
144 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
144 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
145 f=SOME f, f_defthm=SOME f_defthm }, |
145 f=SOME f, f_defthm=SOME f_defthm }, |
146 lthy') |
146 lthy') |
154 lthy') |
154 lthy') |
155 end |
155 end |
156 |
156 |
157 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = |
157 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = |
158 let |
158 let |
159 val thy = Proof_Context.theory_of ctxt |
|
160 |
|
161 val oqnames = map fst pre_qs |
159 val oqnames = map fst pre_qs |
162 val (qs, _) = Variable.variant_fixes oqnames ctxt |
160 val (qs, _) = Variable.variant_fixes oqnames ctxt |
163 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
161 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
164 |
162 |
165 fun inst t = subst_bounds (rev qs, t) |
163 fun inst t = subst_bounds (rev qs, t) |
166 val gs = map inst pre_gs |
164 val gs = map inst pre_gs |
167 val args = map inst pre_args |
165 val args = map inst pre_args |
168 val rhs = inst pre_rhs |
166 val rhs = inst pre_rhs |
169 |
167 |
170 val cqs = map (cterm_of thy) qs |
168 val cqs = map (Thm.cterm_of ctxt) qs |
171 val (ags, ctxt') = fold_map Thm.assume_hyps (map (cterm_of thy) gs) ctxt |
169 val (ags, ctxt') = fold_map Thm.assume_hyps (map (Thm.cterm_of ctxt) gs) ctxt |
172 |
170 |
173 val import = fold Thm.forall_elim cqs |
171 val import = fold Thm.forall_elim cqs |
174 #> fold Thm.elim_implies ags |
172 #> fold Thm.elim_implies ags |
175 |
173 |
176 val export = fold_rev (Thm.implies_intr o cprop_of) ags |
174 val export = fold_rev (Thm.implies_intr o Thm.cprop_of) ags |
177 #> fold_rev forall_intr_rename (oqnames ~~ cqs) |
175 #> fold_rev forall_intr_rename (oqnames ~~ cqs) |
178 in |
176 in |
179 F ctxt' (f, qs, gs, args, rhs) import export |
177 F ctxt' (f, qs, gs, args, rhs) import export |
180 end |
178 end |
181 |
179 |
240 |> export |
238 |> export |
241 end |
239 end |
242 |
240 |
243 fun mk_applied_form ctxt caTs thm = |
241 fun mk_applied_form ctxt caTs thm = |
244 let |
242 let |
245 val thy = Proof_Context.theory_of ctxt |
243 val xs = map_index (fn (i,T) => Thm.cterm_of ctxt (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) |
246 val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) |
|
247 in |
244 in |
248 fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm |
245 fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm |
249 |> Conv.fconv_rule (Thm.beta_conversion true) |
246 |> Conv.fconv_rule (Thm.beta_conversion true) |
250 |> fold_rev Thm.forall_intr xs |
247 |> fold_rev Thm.forall_intr xs |
251 |> Thm.forall_elim_vars 0 |
248 |> Thm.forall_elim_vars 0 |
252 end |
249 end |
253 |
250 |
254 fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) = |
251 fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) = |
255 let |
252 let |
256 val cert = cterm_of (Proof_Context.theory_of ctxt) |
253 val cert = Thm.cterm_of ctxt |
257 val newPs = |
254 val newPs = |
258 map2 (fn Pname => fn MutualPart {cargTs, ...} => |
255 map2 (fn Pname => fn MutualPart {cargTs, ...} => |
259 Free (Pname, cargTs ---> HOLogic.boolT)) |
256 Free (Pname, cargTs ---> HOLogic.boolT)) |
260 (mutual_induct_Pnames (length parts)) parts |
257 (mutual_induct_Pnames (length parts)) parts |
261 |
258 |
312 val ([p_name], ctxt') = Variable.variant_fixes ["p"] ctxt |
309 val ([p_name], ctxt') = Variable.variant_fixes ["p"] ctxt |
313 val p = Free (p_name, @{typ perm}) |
310 val p = Free (p_name, @{typ perm}) |
314 |
311 |
315 (* extracting the acc-premises from the induction theorems *) |
312 (* extracting the acc-premises from the induction theorems *) |
316 val acc_prems = |
313 val acc_prems = |
317 map prop_of induct_thms |
314 map Thm.prop_of induct_thms |
318 |> map2 forall_elim_list argss |
315 |> map2 forall_elim_list argss |
319 |> map (strip_qnt_body @{const_name Pure.all}) |
316 |> map (strip_qnt_body @{const_name Pure.all}) |
320 |> map (curry Logic.nth_prem 1) |
317 |> map (curry Logic.nth_prem 1) |
321 |> map HOLogic.dest_Trueprop |
318 |> map HOLogic.dest_Trueprop |
322 |
319 |
331 val goal = fold_conj_balanced (map2 mk_goal acc_prems (fs ~~ argss)) |
328 val goal = fold_conj_balanced (map2 mk_goal acc_prems (fs ~~ argss)) |
332 |> HOLogic.mk_Trueprop |
329 |> HOLogic.mk_Trueprop |
333 |
330 |
334 val induct_thm = case induct_thms of |
331 val induct_thm = case induct_thms of |
335 [thm] => thm |
332 [thm] => thm |
336 |> Drule.gen_all |
333 |> Drule.gen_all (Variable.maxidx_of ctxt') |
337 |> Thm.permute_prems 0 1 |
334 |> Thm.permute_prems 0 1 |
338 |> (fn thm => atomize_rule ctxt' (length (prems_of thm) - 1) thm) |
335 |> (fn thm => atomize_rule ctxt' (length (Thm.prems_of thm) - 1) thm) |
339 | thms => thms |
336 | thms => thms |
340 |> map Drule.gen_all |
337 |> map (Drule.gen_all (Variable.maxidx_of ctxt')) |
341 |> map (Rule_Cases.add_consumes 1) |
338 |> map (Rule_Cases.add_consumes 1) |
342 |> snd o Rule_Cases.strict_mutual_rule ctxt' |
339 |> snd o Rule_Cases.strict_mutual_rule ctxt' |
343 |> atomize_concl ctxt' |
340 |> atomize_concl ctxt' |
344 |
341 |
345 fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac |
342 fun tac ctxt thm = |
|
343 rtac (Drule.gen_all (Variable.maxidx_of ctxt) thm) THEN_ALL_NEW assume_tac ctxt |
346 in |
344 in |
347 Goal.prove ctxt' (flat arg_namess) [] goal |
345 Goal.prove ctxt' (flat arg_namess) [] goal |
348 (fn {context, ...} => HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map tac eqvts_thms))) |
346 (fn {context = ctxt'', ...} => |
|
347 HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map (tac ctxt'') eqvts_thms))) |
349 |> singleton (Proof_Context.export ctxt' ctxt) |
348 |> singleton (Proof_Context.export ctxt' ctxt) |
350 |> split_conj_thm |
349 |> split_conj_thm |
351 |> map (fn th => th RS mp) |
350 |> map (fn th => th RS mp) |
352 end |
351 end |
353 |
352 |
433 |
432 |
434 val (G_name, G_type) = dest_Free G |
433 val (G_name, G_type) = dest_Free G |
435 val G_name_aux = G_name ^ "_aux" |
434 val G_name_aux = G_name ^ "_aux" |
436 val subst = [(G, Free (G_name_aux, G_type))] |
435 val subst = [(G, Free (G_name_aux, G_type))] |
437 val GIntros_aux = GIntro_thms |
436 val GIntros_aux = GIntro_thms |
438 |> map prop_of |
437 |> map Thm.prop_of |
439 |> map (Term.subst_free subst) |
438 |> map (Term.subst_free subst) |
440 |> map (subst_all case_sum_exp) |
439 |> map (subst_all case_sum_exp) |
441 |
440 |
442 val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = |
441 val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = |
443 Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy'' |
442 Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy'' |
476 |
475 |
477 val inj_thm = Goal.prove lthy''' [] [] goal_inj |
476 val inj_thm = Goal.prove lthy''' [] [] goal_inj |
478 (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac simpset1))) |
477 (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac simpset1))) |
479 |
478 |
480 fun aux_tac thm = |
479 fun aux_tac thm = |
481 rtac (Drule.gen_all thm) THEN_ALL_NEW (asm_full_simp_tac (simpset1 addsimps [inj_thm])) |
480 rtac (Drule.gen_all (Variable.maxidx_of lthy''') thm) THEN_ALL_NEW |
|
481 asm_full_simp_tac (simpset1 addsimps [inj_thm]) |
482 |
482 |
483 val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 |
483 val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 |
484 (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms)))) |
484 (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms)))) |
485 |> Drule.gen_all |
485 |> Drule.gen_all (Variable.maxidx_of lthy''') |
486 val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 |
486 val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 |
487 (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE |
487 (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE |
488 (map (aux_tac o simplify simpset0) GIntro_aux_thms)))) |
488 (map (aux_tac o simplify simpset0) GIntro_aux_thms)))) |
489 |> Drule.gen_all |
489 |> Drule.gen_all (Variable.maxidx_of lthy''') |
490 |
490 |
491 val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux))) |
491 val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux))) |
492 (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm])))) |
492 (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm])))) |
493 |
493 |
494 val tac = HEADGOAL (simp_tac (put_simpset HOL_basic_ss lthy''' addsimps [iff_thm])) |
494 val tac = HEADGOAL (simp_tac (put_simpset HOL_basic_ss lthy''' addsimps [iff_thm])) |