equal
deleted
inserted
replaced
245 in |
245 in |
246 (list_all (params', prem), (rev vs, subst_bounds (vs, prem))) |
246 (list_all (params', prem), (rev vs, subst_bounds (vs, prem))) |
247 end) prems); |
247 end) prems); |
248 |
248 |
249 val ind_vars = |
249 val ind_vars = |
250 (DatatypeProp.indexify_names (replicate (length atomTs) "pi") ~~ |
250 (Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~ |
251 map NominalAtoms.mk_permT atomTs) @ [("z", fsT)]; |
251 map NominalAtoms.mk_permT atomTs) @ [("z", fsT)]; |
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, |
645 | SOME (th, _) => Seq.single th |
645 | SOME (th, _) => Seq.single th |
646 end; |
646 end; |
647 val thss = map (fn atom => |
647 val thss = map (fn atom => |
648 let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, []))) |
648 let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, []))) |
649 in map (fn th => zero_var_indexes (th RS mp)) |
649 in map (fn th => zero_var_indexes (th RS mp)) |
650 (DatatypeAux.split_conj_thm (Goal.prove ctxt' [] [] |
650 (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] |
651 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p => |
651 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p => |
652 let |
652 let |
653 val (h, ts) = strip_comb p; |
653 val (h, ts) = strip_comb p; |
654 val (ts1, ts2) = chop k ts |
654 val (ts1, ts2) = chop k ts |
655 in |
655 in |