1 (* Title: HOL/Nominal/nominal_inductive.ML
2 Author: Stefan Berghofer, TU Muenchen
4 Infrastructure for proving equivariance and strong induction theorems
5 for inductive predicates involving nominal datatypes.
8 signature NOMINAL_INDUCTIVE =
10 val prove_strong_ind: string -> (string * string list) list -> local_theory -> Proof.state
11 val prove_eqvt: string -> string list -> local_theory -> local_theory
14 structure NominalInductive : NOMINAL_INDUCTIVE =
17 val inductive_forall_def = @{thm induct_forall_def};
18 val inductive_atomize = @{thms induct_atomize};
19 val inductive_rulify = @{thms induct_rulify};
21 fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
24 Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
25 (HOL_basic_ss addsimps inductive_atomize);
26 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
27 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
28 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
30 fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []);
32 val fresh_prod = @{thm fresh_prod};
34 val perm_bool = mk_meta_eq @{thm perm_bool_def};
35 val perm_boolI = @{thm perm_boolI};
36 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
37 (Drule.strip_imp_concl (cprop_of perm_boolI))));
39 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
40 [(perm_boolI_pi, pi)] perm_boolI;
42 fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
43 (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
44 fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
45 if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
46 then SOME perm_bool else NONE
49 fun transp ([] :: _) = []
50 | transp xs = map hd xs :: transp (map tl xs);
52 fun add_binders thy i (t as (_ $ _)) bs = (case strip_comb t of
53 (Const (s, T), ts) => (case strip_type T of
54 (Ts, Type (tname, _)) =>
55 (case NominalDatatype.get_nominal_datatype thy tname of
56 NONE => fold (add_binders thy i) ts bs
57 | SOME {descr, index, ...} => (case AList.lookup op =
58 (#3 (the (AList.lookup op = descr index))) s of
59 NONE => fold (add_binders thy i) ts bs
60 | SOME cargs => fst (fold (fn (xs, x) => fn (bs', cargs') =>
61 let val (cargs1, (u, _) :: cargs2) = chop (length xs) cargs'
62 in (add_binders thy i u
64 if exists (fn j => j < i) (loose_bnos u) then I
65 else insert (op aconv o pairself fst)
66 (incr_boundvars (~i) u, T)) cargs1 bs'), cargs2)
67 end) cargs (bs, ts ~~ Ts))))
68 | _ => fold (add_binders thy i) ts bs)
69 | (u, ts) => add_binders thy i u (fold (add_binders thy i) ts bs))
70 | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
71 | add_binders thy i _ bs = bs;
73 fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
75 if member (op =) names name then SOME (f p q) else NONE
77 | split_conj _ _ _ _ = NONE;
79 fun strip_all [] t = t
80 | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
82 (*********************************************************************)
83 (* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *)
84 (* or ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t) *)
85 (* to R ... & id (ALL z. P z (pi_1 o ... o pi_n o t)) *)
86 (* or id (ALL z. P z (pi_1 o ... o pi_n o t)) *)
88 (* where "id" protects the subformula from simplification *)
89 (*********************************************************************)
91 fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
94 if member (op =) names name then SOME (HOLogic.mk_conj (p,
95 Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
96 (subst_bounds (pis, strip_all pis q))))
99 | inst_conj_all names ps pis t u =
100 if member (op aconv) ps (head_of u) then
101 SOME (Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
102 (subst_bounds (pis, strip_all pis t)))
104 | inst_conj_all _ _ _ _ _ = NONE;
106 fun inst_conj_all_tac k = EVERY
107 [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]),
108 REPEAT_DETERM_N k (etac allE 1),
109 simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1];
111 fun map_term f t u = (case f t u of
112 NONE => map_term' f t u | x => x)
113 and map_term' f (t $ u) (t' $ u') = (case (map_term f t t', map_term f u u') of
115 | (SOME t'', NONE) => SOME (t'' $ u)
116 | (NONE, SOME u'') => SOME (t $ u'')
117 | (SOME t'', SOME u'') => SOME (t'' $ u''))
118 | map_term' f (Abs (s, T, t)) (Abs (s', T', t')) = (case map_term f t t' of
120 | SOME t'' => SOME (Abs (s, T, t'')))
121 | map_term' _ _ _ = NONE;
123 (*********************************************************************)
124 (* Prove F[f t] from F[t], where F is monotone *)
125 (*********************************************************************)
127 fun map_thm ctxt f tac monos opt th =
129 val prop = prop_of th;
131 Goal.prove ctxt [] [] t (fn _ =>
132 EVERY [cut_facts_tac [th] 1, etac rev_mp 1,
133 REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
134 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
135 in Option.map prove (map_term f prop (the_default prop opt)) end;
137 val eta_contract_cterm = Thm.dest_arg o Thm.cprop_of o Thm.eta_conversion;
139 fun first_order_matchs pats objs = Thm.first_order_match
140 (eta_contract_cterm (Conjunction.mk_conjunction_balanced pats),
141 eta_contract_cterm (Conjunction.mk_conjunction_balanced objs));
143 fun first_order_mrs ths th = ths MRS
144 Thm.instantiate (first_order_matchs (cprems_of th) (map cprop_of ths)) th;
146 fun prove_strong_ind s avoids ctxt =
148 val thy = Proof_Context.theory_of ctxt;
149 val ({names, ...}, {raw_induct, intrs, elims, ...}) =
150 Inductive.the_inductive ctxt (Sign.intern_const thy s);
151 val ind_params = Inductive.params_of raw_induct;
152 val raw_induct = atomize_induct ctxt raw_induct;
153 val elims = map (atomize_induct ctxt) elims;
154 val monos = Inductive.get_monos ctxt;
155 val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
156 val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
158 | xs => error ("Missing equivariance theorem for predicate(s): " ^
160 val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
161 (Induct.lookup_inductP ctxt (hd names)))));
162 val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
163 val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
164 HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
165 val ps = map (fst o snd) concls;
167 val _ = (case duplicates (op = o pairself fst) avoids of
169 | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
170 val _ = assert_all (null o duplicates op = o snd) avoids
171 (fn (a, _) => error ("Duplicate variable names for case " ^ quote a));
172 val _ = (case subtract (op =) induct_cases (map fst avoids) of
174 | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
175 val avoids' = if null induct_cases then replicate (length intrs) ("", [])
177 (name, the_default [] (AList.lookup op = avoids name))) induct_cases;
178 fun mk_avoids params (name, ps) =
179 let val k = length params - 1
180 in map (fn x => case find_index (equal x o fst) params of
181 ~1 => error ("No such variable in case " ^ quote name ^
182 " of inductive definition: " ^ quote x)
183 | i => (Bound (k - i), snd (nth params i))) ps
186 val prems = map (fn (prem, avoid) =>
188 val prems = map (incr_boundvars 1) (Logic.strip_assums_hyp prem);
189 val concl = incr_boundvars 1 (Logic.strip_assums_concl prem);
190 val params = Logic.strip_params prem
193 fold (add_binders thy 0) (prems @ [concl]) [] @
194 map (apfst (incr_boundvars 1)) (mk_avoids params avoid),
195 prems, strip_comb (HOLogic.dest_Trueprop concl))
196 end) (Logic.strip_imp_prems raw_induct' ~~ avoids');
198 val atomTs = distinct op = (maps (map snd o #2) prems);
199 val ind_sort = if null atomTs then HOLogic.typeS
200 else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
201 ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
202 val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
203 val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
204 val fsT = TFree (fs_ctxt_tyname, ind_sort);
206 val inductive_forall_def' = Drule.instantiate'
207 [SOME (ctyp_of thy fsT)] [] inductive_forall_def;
209 fun lift_pred' t (Free (s, T)) ts =
210 list_comb (Free (s, fsT --> T), t :: ts);
211 val lift_pred = lift_pred' (Bound 0);
213 fun lift_prem (t as (f $ u)) =
214 let val (p, ts) = strip_comb t
216 if member (op =) ps p then HOLogic.mk_induct_forall fsT $
217 Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts))
218 else lift_prem f $ lift_prem u
220 | lift_prem (Abs (s, T, t)) = Abs (s, T, lift_prem t)
223 fun mk_distinct [] = []
224 | mk_distinct ((x, T) :: xs) = map_filter (fn (y, U) =>
225 if T = U then SOME (HOLogic.mk_Trueprop
226 (HOLogic.mk_not (HOLogic.eq_const T $ x $ y)))
227 else NONE) xs @ mk_distinct xs;
229 fun mk_fresh (x, T) = HOLogic.mk_Trueprop
230 (NominalDatatype.fresh_const T fsT $ x $ Bound 0);
232 val (prems', prems'') = split_list (map (fn (params, bvars, prems, (p, ts)) =>
234 val params' = params @ [("y", fsT)];
235 val prem = Logic.list_implies
236 (map mk_fresh bvars @ mk_distinct bvars @
238 if null (preds_of ps prem) then prem
239 else lift_prem prem) prems,
240 HOLogic.mk_Trueprop (lift_pred p ts));
241 val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params')
243 (Logic.list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
247 (Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
248 map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
249 val ind_Ts = rev (map snd ind_vars);
251 val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
252 (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem,
253 HOLogic.list_all (ind_vars, lift_pred p
254 (map (fold_rev (NominalDatatype.mk_perm ind_Ts)
255 (map Bound (length atomTs downto 1))) ts)))) concls));
257 val concl' = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
258 (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem,
259 lift_pred' (Free (fs_ctxt_name, fsT)) p ts)) concls));
261 val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
262 map (fn q => Logic.list_all (params, incr_boundvars ~1 (Logic.list_implies
263 (map_filter (fn prem =>
264 if null (preds_of ps prem) then SOME prem
265 else map_term (split_conj (K o I) names) prem prem) prems, q))))
267 maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
268 (NominalDatatype.fresh_const U T $ u $ t)) bvars)
269 (ts ~~ binder_types (fastype_of p)))) prems;
271 val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
272 val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
273 ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
274 val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
275 addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
276 addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}],
277 NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
278 val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
279 val perm_bij = Global_Theory.get_thms thy "perm_bij";
280 val fs_atoms = map (fn aT => Global_Theory.get_thm thy
281 ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
282 val exists_fresh' = Global_Theory.get_thms thy "exists_fresh'";
283 val fresh_atm = Global_Theory.get_thms thy "fresh_atm";
284 val swap_simps = Global_Theory.get_thms thy "swap_simps";
285 val perm_fresh_fresh = Global_Theory.get_thms thy "perm_fresh_fresh";
287 fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) =
289 (** protect terms to avoid that fresh_prod interferes with **)
290 (** pairs used in introduction rules of inductive predicate **)
292 let val T = fastype_of t in Const (@{const_name Fun.id}, T --> T) $ t end;
293 val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1);
294 val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
295 (HOLogic.exists_const T $ Abs ("x", T,
296 NominalDatatype.fresh_const T (fastype_of p) $
299 [resolve_tac exists_fresh' 1,
300 resolve_tac fs_atoms 1]);
301 val (([(_, cx)], ths), ctxt') = Obtain.result
304 full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
305 full_simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1,
306 REPEAT (etac conjE 1)])
308 in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
310 fun mk_ind_proof ctxt' thss =
311 Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
312 let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
313 rtac raw_induct 1 THEN
314 EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) =>
315 [REPEAT (rtac allI 1), simp_tac eqvt_ss 1,
316 SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
318 val (params', (pis, z)) =
319 chop (length params - length atomTs - 1) (map (term_of o #2) params) ||>
322 (fn (Bound i, T) => (nth params' (length params' - i), T)
323 | (t, T) => (t, T)) bvars;
324 val pi_bvars = map (fn (t, _) =>
325 fold_rev (NominalDatatype.mk_perm []) pis t) bvars';
326 val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl));
327 val (freshs1, freshs2, ctxt'') = fold
328 (obtain_fresh_name (ts @ pi_bvars))
329 (map snd bvars') ([], [], ctxt');
330 val freshs2' = NominalDatatype.mk_not_sym freshs2;
331 val pis' = map NominalDatatype.perm_of_pair (pi_bvars ~~ freshs1);
332 fun concat_perm pi1 pi2 =
333 let val T = fastype_of pi1
334 in if T = fastype_of pi2 then
335 Const (@{const_name List.append}, T --> T --> T) $ pi1 $ pi2
338 val pis'' = fold (concat_perm #> map) pis' pis;
339 val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
340 (Vartab.empty, Vartab.empty);
341 val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
342 (map (Envir.subst_term env) vs ~~
343 map (fold_rev (NominalDatatype.mk_perm [])
344 (rev pis' @ pis)) params' @ [z])) ihyp;
346 Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
347 addsimprocs [NominalDatatype.perm_simproc])
348 (Simplifier.simplify eqvt_ss
349 (fold_rev (mk_perm_bool o cterm_of thy)
350 (rev pis' @ pis) th));
351 val (gprems1, gprems2) = split_list
353 if null (preds_of ps t) then (SOME th, mk_pi th)
355 (map_thm ctxt (split_conj (K o I) names)
356 (etac conjunct1 1) monos NONE th,
357 mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
358 (inst_conj_all_tac (length pis'')) monos (SOME t) th))))
359 (gprems ~~ oprems)) |>> map_filter I;
360 val vc_compat_ths' = map (fn th =>
362 val th' = first_order_mrs gprems1 th;
363 val (bop, lhs, rhs) = (case concl_of th' of
364 _ $ (fresh $ lhs $ rhs) =>
365 (fn t => fn u => fresh $ t $ u, lhs, rhs)
366 | _ $ (_ $ (_ $ lhs $ rhs)) =>
367 (curry (HOLogic.mk_not o HOLogic.mk_eq), lhs, rhs));
368 val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop
369 (bop (fold_rev (NominalDatatype.mk_perm []) pis lhs)
370 (fold_rev (NominalDatatype.mk_perm []) pis rhs)))
371 (fn _ => simp_tac (HOL_basic_ss addsimps
372 (fresh_bij @ perm_bij)) 1 THEN rtac th' 1)
373 in Simplifier.simplify (eqvt_ss addsimps fresh_atm) th'' end)
375 val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths';
376 (** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **)
377 (** we have to pre-simplify the rewrite rules **)
378 val swap_simps_ss = HOL_ss addsimps swap_simps @
379 map (Simplifier.simplify (HOL_ss addsimps swap_simps))
380 (vc_compat_ths'' @ freshs2');
381 val th = Goal.prove ctxt'' [] []
382 (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
383 map (fold (NominalDatatype.mk_perm []) pis') (tl ts))))
384 (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1,
385 REPEAT_DETERM_N (nprems_of ihyp - length gprems)
386 (simp_tac swap_simps_ss 1),
387 REPEAT_DETERM_N (length gprems)
388 (simp_tac (HOL_basic_ss
389 addsimps [inductive_forall_def']
390 addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
391 resolve_tac gprems2 1)]));
392 val final = Goal.prove ctxt'' [] [] (term_of concl)
393 (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss
394 addsimps vc_compat_ths'' @ freshs2' @
395 perm_fresh_fresh @ fresh_atm) 1);
396 val final' = Proof_Context.export ctxt'' ctxt' [final];
397 in resolve_tac final' 1 end) context 1])
398 (prems ~~ thss ~~ ihyps ~~ prems'')))
400 cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
401 REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
402 etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
403 asm_full_simp_tac (simpset_of ctxt) 1)
404 end) |> singleton (Proof_Context.export ctxt' ctxt);
406 (** strong case analysis rule **)
408 val cases_prems = map (fn ((name, avoids), rule) =>
410 val ([rule'], ctxt') = Variable.import_terms false [prop_of rule] ctxt;
411 val prem :: prems = Logic.strip_imp_prems rule';
412 val concl = Logic.strip_imp_concl rule'
415 List.drop (snd (strip_comb (HOLogic.dest_Trueprop prem)), length ind_params),
417 fold_map (fn (prem, (_, avoid)) => fn ctxt =>
419 val prems = Logic.strip_assums_hyp prem;
420 val params = Logic.strip_params prem;
421 val bnds = fold (add_binders thy 0) prems [] @ mk_avoids params avoid;
422 fun mk_subst (p as (s, T)) (i, j, ctxt, ps, qs, is, ts) =
423 if member (op = o apsnd fst) bnds (Bound i) then
425 val ([s'], ctxt') = Variable.variant_fixes [s] ctxt;
427 in (i + 1, j, ctxt', ps, (t, T) :: qs, i :: is, t :: ts) end
428 else (i + 1, j + 1, ctxt, p :: ps, qs, is, Bound j :: ts);
429 val (_, _, ctxt', ps, qs, is, ts) = fold_rev mk_subst params
430 (0, 0, ctxt, [], [], [], [])
432 ((ps, qs, is, map (curry subst_bounds (rev ts)) prems), ctxt')
433 end) (prems ~~ avoids) ctxt')
435 (Inductive.partition_rules' raw_induct (intrs ~~ avoids') ~~
439 map (fn (prem, args, concl, (prems, _)) =>
441 fun mk_prem (ps, [], _, prems) =
442 Logic.list_all (ps, Logic.list_implies (prems, concl))
443 | mk_prem (ps, qs, _, prems) =
444 Logic.list_all (ps, Logic.mk_implies
447 maps (fn (t, T) => map (fn u => HOLogic.mk_Trueprop
448 (NominalDatatype.fresh_const T (fastype_of u) $ t $ u))
450 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
451 (map HOLogic.dest_Trueprop prems))),
453 in map mk_prem prems end) cases_prems;
455 val cases_eqvt_ss = Simplifier.global_context thy HOL_ss
456 addsimps eqvt_thms @ swap_simps @ perm_pi_simp
457 addsimprocs [NominalPermeq.perm_simproc_app,
458 NominalPermeq.perm_simproc_fun];
460 val simp_fresh_atm = map
461 (Simplifier.simplify (HOL_basic_ss addsimps fresh_atm));
463 fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))),
465 (name, Goal.prove ctxt' [] (prem :: prems') concl
466 (fn {prems = hyp :: hyps, context = ctxt1} =>
467 EVERY (rtac (hyp RS elim) 1 ::
468 map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) =>
469 SUBPROOF (fn {prems = case_hyps, params, context = ctxt2, concl, ...} =>
471 rtac (first_order_mrs case_hyps case_hyp) 1
474 val params' = map (term_of o #2 o nth (rev params)) is;
475 val tab = params' ~~ map fst qs;
476 val (hyps1, hyps2) = chop (length args) case_hyps;
477 (* turns a = t and [x1 # t, ..., xn # t] *)
478 (* into [x1 # a, ..., xn # a] *)
479 fun inst_fresh th' ths =
480 let val (ths1, ths2) = chop (length qs) ths
485 Thm.dest_comb (Thm.dest_arg (cprop_of th));
486 val arg_cong' = Drule.instantiate'
487 [SOME (ctyp_of_term ct)]
488 [NONE, SOME ct, SOME cf] (arg_cong RS iffD2);
489 val inst = Thm.first_order_match (ct,
490 Thm.dest_arg (Thm.dest_arg (cprop_of th')))
491 in [th', th] MRS Thm.instantiate inst arg_cong'
495 val (vc_compat_ths1, vc_compat_ths2) =
496 chop (length vc_compat_ths - length args * length qs)
497 (map (first_order_mrs hyps2) vc_compat_ths);
499 NominalDatatype.mk_not_sym vc_compat_ths1 @
500 flat (fst (fold_map inst_fresh hyps1 vc_compat_ths2));
501 val (freshs1, freshs2, ctxt3) = fold
502 (obtain_fresh_name (args @ map fst qs @ params'))
503 (map snd qs) ([], [], ctxt2);
504 val freshs2' = NominalDatatype.mk_not_sym freshs2;
505 val pis = map (NominalDatatype.perm_of_pair)
506 ((freshs1 ~~ map fst qs) @ (params' ~~ freshs1));
507 val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis);
508 val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
510 if member (op =) args x then x
511 else (case AList.lookup op = tab x of
513 | NONE => fold_rev (NominalDatatype.mk_perm []) pis x)
514 | x => x) o HOLogic.dest_Trueprop o prop_of) case_hyps));
515 val inst = Thm.first_order_match (Thm.dest_arg
516 (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj);
517 val th = Goal.prove ctxt3 [] [] (term_of concl)
518 (fn {context = ctxt4, ...} =>
519 rtac (Thm.instantiate inst case_hyp) 1 THEN
520 SUBPROOF (fn {prems = fresh_hyps, ...} =>
522 val fresh_hyps' = NominalDatatype.mk_not_sym fresh_hyps;
523 val case_ss = cases_eqvt_ss addsimps freshs2' @
524 simp_fresh_atm (vc_compat_ths' @ fresh_hyps');
525 val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh;
527 (mk_pis #> Simplifier.simplify fresh_fresh_ss) hyps1;
529 (mk_pis #> Simplifier.simplify case_ss) hyps2;
530 val case_hyps' = hyps1' @ hyps2'
532 simp_tac case_ss 1 THEN
533 REPEAT_DETERM (TRY (rtac conjI 1) THEN
534 resolve_tac case_hyps' 1)
536 val final = Proof_Context.export ctxt3 ctxt2 [th]
537 in resolve_tac final 1 end) ctxt1 1)
538 (thss ~~ hyps ~~ prems))) |>
539 singleton (Proof_Context.export ctxt' ctxt))
543 Proof.theorem NONE (fn thss => fn ctxt =>
545 val rec_name = space_implode "_" (map Long_Name.base_name names);
546 val rec_qualified = Binding.qualify false rec_name;
547 val ind_case_names = Rule_Cases.case_names induct_cases;
548 val induct_cases' = Inductive.partition_rules' raw_induct
549 (intrs ~~ induct_cases);
550 val thss' = map (map atomize_intr) thss;
551 val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
552 val strong_raw_induct =
553 mk_ind_proof ctxt thss' |> Inductive.rulify;
554 val strong_cases = map (mk_cases_proof ##> Inductive.rulify)
555 (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
557 if length names > 1 then
558 (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
559 else (strong_raw_induct RSN (2, rev_mp),
560 [ind_case_names, Rule_Cases.consumes 1]);
561 val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
562 ((rec_qualified (Binding.name "strong_induct"),
563 map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
565 Project_Rule.projects ctxt (1 upto length names) strong_induct';
569 ((rec_qualified (Binding.name "strong_inducts"),
570 [Attrib.internal (K ind_case_names),
571 Attrib.internal (K (Rule_Cases.consumes 1))]),
572 strong_inducts) |> snd |>
573 Local_Theory.notes (map (fn ((name, elim), (_, cases)) =>
574 ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
575 [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
576 Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
577 (strong_cases ~~ induct_cases')) |> snd
579 (map (map (rulify_term thy #> rpair [])) vc_compat)
582 fun prove_eqvt s xatoms ctxt =
584 val thy = Proof_Context.theory_of ctxt;
585 val ({names, ...}, {raw_induct, intrs, elims, ...}) =
586 Inductive.the_inductive ctxt (Sign.intern_const thy s);
587 val raw_induct = atomize_induct ctxt raw_induct;
588 val elims = map (atomize_induct ctxt) elims;
589 val intrs = map atomize_intr intrs;
590 val monos = Inductive.get_monos ctxt;
591 val intrs' = Inductive.unpartition_rules intrs
592 (map (fn (((s, ths), (_, k)), th) =>
593 (s, ths ~~ Inductive.infer_intro_vars th k ths))
594 (Inductive.partition_rules raw_induct intrs ~~
595 Inductive.arities_of raw_induct ~~ elims));
596 val k = length (Inductive.params_of raw_induct);
597 val atoms' = NominalAtoms.atoms_of thy;
599 if null xatoms then atoms' else
600 let val atoms = map (Sign.intern_type thy) xatoms
602 (case duplicates op = atoms of
604 | xs => error ("Duplicate atoms: " ^ commas xs);
605 case subtract (op =) atoms' atoms of
607 | xs => error ("No such atoms: " ^ commas xs);
610 val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
611 val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
612 (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
613 [mk_perm_bool_simproc names,
614 NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
615 val (([t], [pi]), ctxt') = ctxt |>
616 Variable.import_terms false [concl_of raw_induct] ||>>
617 Variable.variant_fixes ["pi"];
618 val ps = map (fst o HOLogic.dest_imp)
619 (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
620 fun eqvt_tac ctxt'' pi (intr, vs) st =
623 let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt
624 in error ("Could not prove equivariance for introduction rule\n" ^
625 Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
627 val res = SUBPROOF (fn {prems, params, ...} =>
629 val prems' = map (fn th => the_default th (map_thm ctxt'
630 (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
631 val prems'' = map (fn th => Simplifier.simplify eqvt_ss
632 (mk_perm_bool (cterm_of thy pi) th)) prems';
633 val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
634 map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of o #2) params)
636 in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
639 case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
640 NONE => eqvt_err ("Rule does not match goal\n" ^
641 Syntax.string_of_term ctxt'' (hd (prems_of st)))
642 | SOME (th, _) => Seq.single th
644 val thss = map (fn atom =>
645 let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, [])))
646 in map (fn th => zero_var_indexes (th RS mp))
647 (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
648 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
650 val (h, ts) = strip_comb p;
651 val (ts1, ts2) = chop k ts
653 HOLogic.mk_imp (p, list_comb (h, ts1 @
654 map (NominalDatatype.mk_perm [] pi') ts2))
656 (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
657 full_simp_tac eqvt_ss 1 THEN
658 eqvt_tac context pi' intr_vs) intrs')) |>
659 singleton (Proof_Context.export ctxt' ctxt)))
663 Local_Theory.notes (map (fn (name, ths) =>
664 ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
665 [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
666 (names ~~ transp thss)) |> snd
673 Outer_Syntax.local_theory_to_proof "nominal_inductive"
674 "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
676 (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name --
677 (Parse.$$$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
678 prove_strong_ind name avoids));
681 Outer_Syntax.local_theory "equivariance"
682 "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
683 (Parse.xname -- Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [] >>
684 (fn (name, atoms) => prove_eqvt name atoms));