51 | transp xs = map hd xs :: transp (map tl xs); |
51 | transp xs = map hd xs :: transp (map tl xs); |
52 |
52 |
53 fun add_binders thy i (t as (_ $ _)) bs = (case strip_comb t of |
53 fun add_binders thy i (t as (_ $ _)) bs = (case strip_comb t of |
54 (Const (s, T), ts) => (case strip_type T of |
54 (Const (s, T), ts) => (case strip_type T of |
55 (Ts, Type (tname, _)) => |
55 (Ts, Type (tname, _)) => |
56 (case NominalPackage.get_nominal_datatype thy tname of |
56 (case Nominal.get_nominal_datatype thy tname of |
57 NONE => fold (add_binders thy i) ts bs |
57 NONE => fold (add_binders thy i) ts bs |
58 | SOME {descr, index, ...} => (case AList.lookup op = |
58 | SOME {descr, index, ...} => (case AList.lookup op = |
59 (#3 (the (AList.lookup op = descr index))) s of |
59 (#3 (the (AList.lookup op = descr index))) s of |
60 NONE => fold (add_binders thy i) ts bs |
60 NONE => fold (add_binders thy i) ts bs |
61 | SOME cargs => fst (fold (fn (xs, x) => fn (bs', cargs') => |
61 | SOME cargs => fst (fold (fn (xs, x) => fn (bs', cargs') => |
146 |
146 |
147 fun prove_strong_ind s avoids ctxt = |
147 fun prove_strong_ind s avoids ctxt = |
148 let |
148 let |
149 val thy = ProofContext.theory_of ctxt; |
149 val thy = ProofContext.theory_of ctxt; |
150 val ({names, ...}, {raw_induct, intrs, elims, ...}) = |
150 val ({names, ...}, {raw_induct, intrs, elims, ...}) = |
151 InductivePackage.the_inductive ctxt (Sign.intern_const thy s); |
151 Inductive.the_inductive ctxt (Sign.intern_const thy s); |
152 val ind_params = InductivePackage.params_of raw_induct; |
152 val ind_params = Inductive.params_of raw_induct; |
153 val raw_induct = atomize_induct ctxt raw_induct; |
153 val raw_induct = atomize_induct ctxt raw_induct; |
154 val elims = map (atomize_induct ctxt) elims; |
154 val elims = map (atomize_induct ctxt) elims; |
155 val monos = InductivePackage.get_monos ctxt; |
155 val monos = Inductive.get_monos ctxt; |
156 val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt; |
156 val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt; |
157 val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of |
157 val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of |
158 [] => () |
158 [] => () |
159 | xs => error ("Missing equivariance theorem for predicate(s): " ^ |
159 | xs => error ("Missing equivariance theorem for predicate(s): " ^ |
160 commas_quote xs)); |
160 commas_quote xs)); |
228 if T = U then SOME (HOLogic.mk_Trueprop |
228 if T = U then SOME (HOLogic.mk_Trueprop |
229 (HOLogic.mk_not (HOLogic.eq_const T $ x $ y))) |
229 (HOLogic.mk_not (HOLogic.eq_const T $ x $ y))) |
230 else NONE) xs @ mk_distinct xs; |
230 else NONE) xs @ mk_distinct xs; |
231 |
231 |
232 fun mk_fresh (x, T) = HOLogic.mk_Trueprop |
232 fun mk_fresh (x, T) = HOLogic.mk_Trueprop |
233 (NominalPackage.fresh_const T fsT $ x $ Bound 0); |
233 (Nominal.fresh_const T fsT $ x $ Bound 0); |
234 |
234 |
235 val (prems', prems'') = split_list (map (fn (params, bvars, prems, (p, ts)) => |
235 val (prems', prems'') = split_list (map (fn (params, bvars, prems, (p, ts)) => |
236 let |
236 let |
237 val params' = params @ [("y", fsT)]; |
237 val params' = params @ [("y", fsT)]; |
238 val prem = Logic.list_implies |
238 val prem = Logic.list_implies |
252 val ind_Ts = rev (map snd ind_vars); |
252 val ind_Ts = rev (map snd ind_vars); |
253 |
253 |
254 val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
254 val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
255 (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem, |
255 (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem, |
256 HOLogic.list_all (ind_vars, lift_pred p |
256 HOLogic.list_all (ind_vars, lift_pred p |
257 (map (fold_rev (NominalPackage.mk_perm ind_Ts) |
257 (map (fold_rev (Nominal.mk_perm ind_Ts) |
258 (map Bound (length atomTs downto 1))) ts)))) concls)); |
258 (map Bound (length atomTs downto 1))) ts)))) concls)); |
259 |
259 |
260 val concl' = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
260 val concl' = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
261 (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem, |
261 (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem, |
262 lift_pred' (Free (fs_ctxt_name, fsT)) p ts)) concls)); |
262 lift_pred' (Free (fs_ctxt_name, fsT)) p ts)) concls)); |
266 (List.mapPartial (fn prem => |
266 (List.mapPartial (fn prem => |
267 if null (preds_of ps prem) then SOME prem |
267 if null (preds_of ps prem) then SOME prem |
268 else map_term (split_conj (K o I) names) prem prem) prems, q)))) |
268 else map_term (split_conj (K o I) names) prem prem) prems, q)))) |
269 (mk_distinct bvars @ |
269 (mk_distinct bvars @ |
270 maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop |
270 maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop |
271 (NominalPackage.fresh_const U T $ u $ t)) bvars) |
271 (Nominal.fresh_const U T $ u $ t)) bvars) |
272 (ts ~~ binder_types (fastype_of p)))) prems; |
272 (ts ~~ binder_types (fastype_of p)))) prems; |
273 |
273 |
274 val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; |
274 val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; |
275 val pt2_atoms = map (fn aT => PureThy.get_thm thy |
275 val pt2_atoms = map (fn aT => PureThy.get_thm thy |
276 ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs; |
276 ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs; |
294 fun protect t = |
294 fun protect t = |
295 let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end; |
295 let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end; |
296 val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1); |
296 val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1); |
297 val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop |
297 val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop |
298 (HOLogic.exists_const T $ Abs ("x", T, |
298 (HOLogic.exists_const T $ Abs ("x", T, |
299 NominalPackage.fresh_const T (fastype_of p) $ |
299 Nominal.fresh_const T (fastype_of p) $ |
300 Bound 0 $ p))) |
300 Bound 0 $ p))) |
301 (fn _ => EVERY |
301 (fn _ => EVERY |
302 [resolve_tac exists_fresh' 1, |
302 [resolve_tac exists_fresh' 1, |
303 resolve_tac fs_atoms 1]); |
303 resolve_tac fs_atoms 1]); |
304 val (([cx], ths), ctxt') = Obtain.result |
304 val (([cx], ths), ctxt') = Obtain.result |
323 split_last; |
323 split_last; |
324 val bvars' = map |
324 val bvars' = map |
325 (fn (Bound i, T) => (nth params' (length params' - i), T) |
325 (fn (Bound i, T) => (nth params' (length params' - i), T) |
326 | (t, T) => (t, T)) bvars; |
326 | (t, T) => (t, T)) bvars; |
327 val pi_bvars = map (fn (t, _) => |
327 val pi_bvars = map (fn (t, _) => |
328 fold_rev (NominalPackage.mk_perm []) pis t) bvars'; |
328 fold_rev (Nominal.mk_perm []) pis t) bvars'; |
329 val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl)); |
329 val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl)); |
330 val (freshs1, freshs2, ctxt'') = fold |
330 val (freshs1, freshs2, ctxt'') = fold |
331 (obtain_fresh_name (ts @ pi_bvars)) |
331 (obtain_fresh_name (ts @ pi_bvars)) |
332 (map snd bvars') ([], [], ctxt'); |
332 (map snd bvars') ([], [], ctxt'); |
333 val freshs2' = NominalPackage.mk_not_sym freshs2; |
333 val freshs2' = Nominal.mk_not_sym freshs2; |
334 val pis' = map NominalPackage.perm_of_pair (pi_bvars ~~ freshs1); |
334 val pis' = map Nominal.perm_of_pair (pi_bvars ~~ freshs1); |
335 fun concat_perm pi1 pi2 = |
335 fun concat_perm pi1 pi2 = |
336 let val T = fastype_of pi1 |
336 let val T = fastype_of pi1 |
337 in if T = fastype_of pi2 then |
337 in if T = fastype_of pi2 then |
338 Const ("List.append", T --> T --> T) $ pi1 $ pi2 |
338 Const ("List.append", T --> T --> T) $ pi1 $ pi2 |
339 else pi2 |
339 else pi2 |
341 val pis'' = fold (concat_perm #> map) pis' pis; |
341 val pis'' = fold (concat_perm #> map) pis' pis; |
342 val env = Pattern.first_order_match thy (ihypt, prop_of ihyp) |
342 val env = Pattern.first_order_match thy (ihypt, prop_of ihyp) |
343 (Vartab.empty, Vartab.empty); |
343 (Vartab.empty, Vartab.empty); |
344 val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy)) |
344 val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy)) |
345 (map (Envir.subst_vars env) vs ~~ |
345 (map (Envir.subst_vars env) vs ~~ |
346 map (fold_rev (NominalPackage.mk_perm []) |
346 map (fold_rev (Nominal.mk_perm []) |
347 (rev pis' @ pis)) params' @ [z])) ihyp; |
347 (rev pis' @ pis)) params' @ [z])) ihyp; |
348 fun mk_pi th = |
348 fun mk_pi th = |
349 Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}] |
349 Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}] |
350 addsimprocs [NominalPackage.perm_simproc]) |
350 addsimprocs [Nominal.perm_simproc]) |
351 (Simplifier.simplify eqvt_ss |
351 (Simplifier.simplify eqvt_ss |
352 (fold_rev (mk_perm_bool o cterm_of thy) |
352 (fold_rev (mk_perm_bool o cterm_of thy) |
353 (rev pis' @ pis) th)); |
353 (rev pis' @ pis) th)); |
354 val (gprems1, gprems2) = split_list |
354 val (gprems1, gprems2) = split_list |
355 (map (fn (th, t) => |
355 (map (fn (th, t) => |
367 _ $ (fresh $ lhs $ rhs) => |
367 _ $ (fresh $ lhs $ rhs) => |
368 (fn t => fn u => fresh $ t $ u, lhs, rhs) |
368 (fn t => fn u => fresh $ t $ u, lhs, rhs) |
369 | _ $ (_ $ (_ $ lhs $ rhs)) => |
369 | _ $ (_ $ (_ $ lhs $ rhs)) => |
370 (curry (HOLogic.mk_not o HOLogic.mk_eq), lhs, rhs)); |
370 (curry (HOLogic.mk_not o HOLogic.mk_eq), lhs, rhs)); |
371 val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop |
371 val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop |
372 (bop (fold_rev (NominalPackage.mk_perm []) pis lhs) |
372 (bop (fold_rev (Nominal.mk_perm []) pis lhs) |
373 (fold_rev (NominalPackage.mk_perm []) pis rhs))) |
373 (fold_rev (Nominal.mk_perm []) pis rhs))) |
374 (fn _ => simp_tac (HOL_basic_ss addsimps |
374 (fn _ => simp_tac (HOL_basic_ss addsimps |
375 (fresh_bij @ perm_bij)) 1 THEN rtac th' 1) |
375 (fresh_bij @ perm_bij)) 1 THEN rtac th' 1) |
376 in Simplifier.simplify (eqvt_ss addsimps fresh_atm) th'' end) |
376 in Simplifier.simplify (eqvt_ss addsimps fresh_atm) th'' end) |
377 vc_compat_ths; |
377 vc_compat_ths; |
378 val vc_compat_ths'' = NominalPackage.mk_not_sym vc_compat_ths'; |
378 val vc_compat_ths'' = Nominal.mk_not_sym vc_compat_ths'; |
379 (** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **) |
379 (** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **) |
380 (** we have to pre-simplify the rewrite rules **) |
380 (** we have to pre-simplify the rewrite rules **) |
381 val swap_simps_ss = HOL_ss addsimps swap_simps @ |
381 val swap_simps_ss = HOL_ss addsimps swap_simps @ |
382 map (Simplifier.simplify (HOL_ss addsimps swap_simps)) |
382 map (Simplifier.simplify (HOL_ss addsimps swap_simps)) |
383 (vc_compat_ths'' @ freshs2'); |
383 (vc_compat_ths'' @ freshs2'); |
384 val th = Goal.prove ctxt'' [] [] |
384 val th = Goal.prove ctxt'' [] [] |
385 (HOLogic.mk_Trueprop (list_comb (P $ hd ts, |
385 (HOLogic.mk_Trueprop (list_comb (P $ hd ts, |
386 map (fold (NominalPackage.mk_perm []) pis') (tl ts)))) |
386 map (fold (Nominal.mk_perm []) pis') (tl ts)))) |
387 (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1, |
387 (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1, |
388 REPEAT_DETERM_N (nprems_of ihyp - length gprems) |
388 REPEAT_DETERM_N (nprems_of ihyp - length gprems) |
389 (simp_tac swap_simps_ss 1), |
389 (simp_tac swap_simps_ss 1), |
390 REPEAT_DETERM_N (length gprems) |
390 REPEAT_DETERM_N (length gprems) |
391 (simp_tac (HOL_basic_ss |
391 (simp_tac (HOL_basic_ss |
392 addsimps [inductive_forall_def'] |
392 addsimps [inductive_forall_def'] |
393 addsimprocs [NominalPackage.perm_simproc]) 1 THEN |
393 addsimprocs [Nominal.perm_simproc]) 1 THEN |
394 resolve_tac gprems2 1)])); |
394 resolve_tac gprems2 1)])); |
395 val final = Goal.prove ctxt'' [] [] (term_of concl) |
395 val final = Goal.prove ctxt'' [] [] (term_of concl) |
396 (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss |
396 (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss |
397 addsimps vc_compat_ths'' @ freshs2' @ |
397 addsimps vc_compat_ths'' @ freshs2' @ |
398 perm_fresh_fresh @ fresh_atm) 1); |
398 perm_fresh_fresh @ fresh_atm) 1); |
433 (0, 0, ctxt, [], [], [], []) |
433 (0, 0, ctxt, [], [], [], []) |
434 in |
434 in |
435 ((ps, qs, is, map (curry subst_bounds (rev ts)) prems), ctxt') |
435 ((ps, qs, is, map (curry subst_bounds (rev ts)) prems), ctxt') |
436 end) (prems ~~ avoids) ctxt') |
436 end) (prems ~~ avoids) ctxt') |
437 end) |
437 end) |
438 (InductivePackage.partition_rules' raw_induct (intrs ~~ avoids') ~~ |
438 (Inductive.partition_rules' raw_induct (intrs ~~ avoids') ~~ |
439 elims); |
439 elims); |
440 |
440 |
441 val cases_prems' = |
441 val cases_prems' = |
442 map (fn (prem, args, concl, (prems, _)) => |
442 map (fn (prem, args, concl, (prems, _)) => |
443 let |
443 let |
446 | mk_prem (ps, qs, _, prems) = |
446 | mk_prem (ps, qs, _, prems) = |
447 list_all (ps, Logic.mk_implies |
447 list_all (ps, Logic.mk_implies |
448 (Logic.list_implies |
448 (Logic.list_implies |
449 (mk_distinct qs @ |
449 (mk_distinct qs @ |
450 maps (fn (t, T) => map (fn u => HOLogic.mk_Trueprop |
450 maps (fn (t, T) => map (fn u => HOLogic.mk_Trueprop |
451 (NominalPackage.fresh_const T (fastype_of u) $ t $ u)) |
451 (Nominal.fresh_const T (fastype_of u) $ t $ u)) |
452 args) qs, |
452 args) qs, |
453 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
453 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
454 (map HOLogic.dest_Trueprop prems))), |
454 (map HOLogic.dest_Trueprop prems))), |
455 concl)) |
455 concl)) |
456 in map mk_prem prems end) cases_prems; |
456 in map mk_prem prems end) cases_prems; |
497 end; |
497 end; |
498 val (vc_compat_ths1, vc_compat_ths2) = |
498 val (vc_compat_ths1, vc_compat_ths2) = |
499 chop (length vc_compat_ths - length args * length qs) |
499 chop (length vc_compat_ths - length args * length qs) |
500 (map (first_order_mrs hyps2) vc_compat_ths); |
500 (map (first_order_mrs hyps2) vc_compat_ths); |
501 val vc_compat_ths' = |
501 val vc_compat_ths' = |
502 NominalPackage.mk_not_sym vc_compat_ths1 @ |
502 Nominal.mk_not_sym vc_compat_ths1 @ |
503 flat (fst (fold_map inst_fresh hyps1 vc_compat_ths2)); |
503 flat (fst (fold_map inst_fresh hyps1 vc_compat_ths2)); |
504 val (freshs1, freshs2, ctxt3) = fold |
504 val (freshs1, freshs2, ctxt3) = fold |
505 (obtain_fresh_name (args @ map fst qs @ params')) |
505 (obtain_fresh_name (args @ map fst qs @ params')) |
506 (map snd qs) ([], [], ctxt2); |
506 (map snd qs) ([], [], ctxt2); |
507 val freshs2' = NominalPackage.mk_not_sym freshs2; |
507 val freshs2' = Nominal.mk_not_sym freshs2; |
508 val pis = map (NominalPackage.perm_of_pair) |
508 val pis = map (Nominal.perm_of_pair) |
509 ((freshs1 ~~ map fst qs) @ (params' ~~ freshs1)); |
509 ((freshs1 ~~ map fst qs) @ (params' ~~ freshs1)); |
510 val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis); |
510 val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis); |
511 val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms |
511 val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms |
512 (fn x as Free _ => |
512 (fn x as Free _ => |
513 if x mem args then x |
513 if x mem args then x |
514 else (case AList.lookup op = tab x of |
514 else (case AList.lookup op = tab x of |
515 SOME y => y |
515 SOME y => y |
516 | NONE => fold_rev (NominalPackage.mk_perm []) pis x) |
516 | NONE => fold_rev (Nominal.mk_perm []) pis x) |
517 | x => x) o HOLogic.dest_Trueprop o prop_of) case_hyps)); |
517 | x => x) o HOLogic.dest_Trueprop o prop_of) case_hyps)); |
518 val inst = Thm.first_order_match (Thm.dest_arg |
518 val inst = Thm.first_order_match (Thm.dest_arg |
519 (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj); |
519 (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj); |
520 val th = Goal.prove ctxt3 [] [] (term_of concl) |
520 val th = Goal.prove ctxt3 [] [] (term_of concl) |
521 (fn {context = ctxt4, ...} => |
521 (fn {context = ctxt4, ...} => |
522 rtac (Thm.instantiate inst case_hyp) 1 THEN |
522 rtac (Thm.instantiate inst case_hyp) 1 THEN |
523 SUBPROOF (fn {prems = fresh_hyps, ...} => |
523 SUBPROOF (fn {prems = fresh_hyps, ...} => |
524 let |
524 let |
525 val fresh_hyps' = NominalPackage.mk_not_sym fresh_hyps; |
525 val fresh_hyps' = Nominal.mk_not_sym fresh_hyps; |
526 val case_ss = cases_eqvt_ss addsimps freshs2' @ |
526 val case_ss = cases_eqvt_ss addsimps freshs2' @ |
527 simp_fresh_atm (vc_compat_ths' @ fresh_hyps'); |
527 simp_fresh_atm (vc_compat_ths' @ fresh_hyps'); |
528 val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh; |
528 val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh; |
529 val hyps1' = map |
529 val hyps1' = map |
530 (mk_pis #> Simplifier.simplify fresh_fresh_ss) hyps1; |
530 (mk_pis #> Simplifier.simplify fresh_fresh_ss) hyps1; |
546 Proof.theorem_i NONE (fn thss => fn ctxt => |
546 Proof.theorem_i NONE (fn thss => fn ctxt => |
547 let |
547 let |
548 val rec_name = space_implode "_" (map Long_Name.base_name names); |
548 val rec_name = space_implode "_" (map Long_Name.base_name names); |
549 val rec_qualified = Binding.qualify false rec_name; |
549 val rec_qualified = Binding.qualify false rec_name; |
550 val ind_case_names = RuleCases.case_names induct_cases; |
550 val ind_case_names = RuleCases.case_names induct_cases; |
551 val induct_cases' = InductivePackage.partition_rules' raw_induct |
551 val induct_cases' = Inductive.partition_rules' raw_induct |
552 (intrs ~~ induct_cases); |
552 (intrs ~~ induct_cases); |
553 val thss' = map (map atomize_intr) thss; |
553 val thss' = map (map atomize_intr) thss; |
554 val thsss = InductivePackage.partition_rules' raw_induct (intrs ~~ thss'); |
554 val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss'); |
555 val strong_raw_induct = |
555 val strong_raw_induct = |
556 mk_ind_proof ctxt thss' |> InductivePackage.rulify; |
556 mk_ind_proof ctxt thss' |> Inductive.rulify; |
557 val strong_cases = map (mk_cases_proof ##> InductivePackage.rulify) |
557 val strong_cases = map (mk_cases_proof ##> Inductive.rulify) |
558 (thsss ~~ elims ~~ cases_prems ~~ cases_prems'); |
558 (thsss ~~ elims ~~ cases_prems ~~ cases_prems'); |
559 val strong_induct = |
559 val strong_induct = |
560 if length names > 1 then |
560 if length names > 1 then |
561 (strong_raw_induct, [ind_case_names, RuleCases.consumes 0]) |
561 (strong_raw_induct, [ind_case_names, RuleCases.consumes 0]) |
562 else (strong_raw_induct RSN (2, rev_mp), |
562 else (strong_raw_induct RSN (2, rev_mp), |
585 |
585 |
586 fun prove_eqvt s xatoms ctxt = |
586 fun prove_eqvt s xatoms ctxt = |
587 let |
587 let |
588 val thy = ProofContext.theory_of ctxt; |
588 val thy = ProofContext.theory_of ctxt; |
589 val ({names, ...}, {raw_induct, intrs, elims, ...}) = |
589 val ({names, ...}, {raw_induct, intrs, elims, ...}) = |
590 InductivePackage.the_inductive ctxt (Sign.intern_const thy s); |
590 Inductive.the_inductive ctxt (Sign.intern_const thy s); |
591 val raw_induct = atomize_induct ctxt raw_induct; |
591 val raw_induct = atomize_induct ctxt raw_induct; |
592 val elims = map (atomize_induct ctxt) elims; |
592 val elims = map (atomize_induct ctxt) elims; |
593 val intrs = map atomize_intr intrs; |
593 val intrs = map atomize_intr intrs; |
594 val monos = InductivePackage.get_monos ctxt; |
594 val monos = Inductive.get_monos ctxt; |
595 val intrs' = InductivePackage.unpartition_rules intrs |
595 val intrs' = Inductive.unpartition_rules intrs |
596 (map (fn (((s, ths), (_, k)), th) => |
596 (map (fn (((s, ths), (_, k)), th) => |
597 (s, ths ~~ InductivePackage.infer_intro_vars th k ths)) |
597 (s, ths ~~ Inductive.infer_intro_vars th k ths)) |
598 (InductivePackage.partition_rules raw_induct intrs ~~ |
598 (Inductive.partition_rules raw_induct intrs ~~ |
599 InductivePackage.arities_of raw_induct ~~ elims)); |
599 Inductive.arities_of raw_induct ~~ elims)); |
600 val k = length (InductivePackage.params_of raw_induct); |
600 val k = length (Inductive.params_of raw_induct); |
601 val atoms' = NominalAtoms.atoms_of thy; |
601 val atoms' = NominalAtoms.atoms_of thy; |
602 val atoms = |
602 val atoms = |
603 if null xatoms then atoms' else |
603 if null xatoms then atoms' else |
604 let val atoms = map (Sign.intern_type thy) xatoms |
604 let val atoms = map (Sign.intern_type thy) xatoms |
605 in |
605 in |
633 val prems' = map (fn th => the_default th (map_thm ctxt' |
633 val prems' = map (fn th => the_default th (map_thm ctxt' |
634 (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems; |
634 (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems; |
635 val prems'' = map (fn th => Simplifier.simplify eqvt_ss |
635 val prems'' = map (fn th => Simplifier.simplify eqvt_ss |
636 (mk_perm_bool (cterm_of thy pi) th)) prems'; |
636 (mk_perm_bool (cterm_of thy pi) th)) prems'; |
637 val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~ |
637 val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~ |
638 map (cterm_of thy o NominalPackage.mk_perm [] pi o term_of) params) |
638 map (cterm_of thy o Nominal.mk_perm [] pi o term_of) params) |
639 intr |
639 intr |
640 in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1 |
640 in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1 |
641 end) ctxt' 1 st |
641 end) ctxt' 1 st |
642 in |
642 in |
643 case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of |
643 case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of |
653 let |
653 let |
654 val (h, ts) = strip_comb p; |
654 val (h, ts) = strip_comb p; |
655 val (ts1, ts2) = chop k ts |
655 val (ts1, ts2) = chop k ts |
656 in |
656 in |
657 HOLogic.mk_imp (p, list_comb (h, ts1 @ |
657 HOLogic.mk_imp (p, list_comb (h, ts1 @ |
658 map (NominalPackage.mk_perm [] pi') ts2)) |
658 map (Nominal.mk_perm [] pi') ts2)) |
659 end) ps))) |
659 end) ps))) |
660 (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs => |
660 (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs => |
661 full_simp_tac eqvt_ss 1 THEN |
661 full_simp_tac eqvt_ss 1 THEN |
662 eqvt_tac context pi' intr_vs) intrs')) |> |
662 eqvt_tac context pi' intr_vs) intrs')) |> |
663 singleton (ProofContext.export ctxt' ctxt))) |
663 singleton (ProofContext.export ctxt' ctxt))) |