equal
deleted
inserted
replaced
158 val ind_params = Inductive.params_of raw_induct; |
158 val ind_params = Inductive.params_of raw_induct; |
159 val raw_induct = atomize_induct ctxt raw_induct; |
159 val raw_induct = atomize_induct ctxt raw_induct; |
160 val elims = map (atomize_induct ctxt) elims; |
160 val elims = map (atomize_induct ctxt) elims; |
161 val monos = Inductive.get_monos ctxt; |
161 val monos = Inductive.get_monos ctxt; |
162 val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt; |
162 val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt; |
163 val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of |
163 val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of |
164 [] => () |
164 [] => () |
165 | xs => error ("Missing equivariance theorem for predicate(s): " ^ |
165 | xs => error ("Missing equivariance theorem for predicate(s): " ^ |
166 commas_quote xs)); |
166 commas_quote xs)); |
167 val induct_cases = map fst (fst (RuleCases.get (the |
167 val induct_cases = map fst (fst (RuleCases.get (the |
168 (Induct.lookup_inductP ctxt (hd names))))); |
168 (Induct.lookup_inductP ctxt (hd names))))); |
174 val ps = map (fst o snd) concls; |
174 val ps = map (fst o snd) concls; |
175 |
175 |
176 val _ = (case duplicates (op = o pairself fst) avoids of |
176 val _ = (case duplicates (op = o pairself fst) avoids of |
177 [] => () |
177 [] => () |
178 | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs))); |
178 | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs))); |
179 val _ = (case map fst avoids \\ induct_cases of |
179 val _ = (case subtract (op =) induct_cases (map fst avoids) of |
180 [] => () |
180 [] => () |
181 | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs)); |
181 | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs)); |
182 fun mk_avoids params name sets = |
182 fun mk_avoids params name sets = |
183 let |
183 let |
184 val (_, ctxt') = ProofContext.add_fixes |
184 val (_, ctxt') = ProofContext.add_fixes |
298 NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; |
298 NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; |
299 val fresh_star_bij = PureThy.get_thms thy "fresh_star_bij"; |
299 val fresh_star_bij = PureThy.get_thms thy "fresh_star_bij"; |
300 val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms; |
300 val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms; |
301 val at_insts = map (NominalAtoms.at_inst_of thy) atoms; |
301 val at_insts = map (NominalAtoms.at_inst_of thy) atoms; |
302 val dj_thms = maps (fn a => |
302 val dj_thms = maps (fn a => |
303 map (NominalAtoms.dj_thm_of thy a) (atoms \ a)) atoms; |
303 map (NominalAtoms.dj_thm_of thy a) (remove (op =) a atoms)) atoms; |
304 val finite_ineq = map2 (fn th => fn th' => th' RS (th RS |
304 val finite_ineq = map2 (fn th => fn th' => th' RS (th RS |
305 @{thm pt_set_finite_ineq})) pt_insts at_insts; |
305 @{thm pt_set_finite_ineq})) pt_insts at_insts; |
306 val perm_set_forget = |
306 val perm_set_forget = |
307 map (fn th => th RS @{thm dj_perm_set_forget}) dj_thms; |
307 map (fn th => th RS @{thm dj_perm_set_forget}) dj_thms; |
308 val perm_freshs_freshs = atomTs ~~ map2 (fn th => fn th' => th' RS (th RS |
308 val perm_freshs_freshs = atomTs ~~ map2 (fn th => fn th' => th' RS (th RS |