theory Pi_Gen imports HOL_Gen dtree begin consts apsnd :: "('a => 'b) => 'c * 'a => 'c * 'b" primrec "apsnd f (c, a) = (c, f a)" types 'a srseq = "'a set * 'a" consts pair :: "'a => 'a * 'a" rev_pair :: "'b * 'a => 'a * 'b" seqmap :: "('a => 'b) => 'a srseq => 'b srseq" primrec "seqmap f (oth, MN) = (f ` oth, f MN)" primrec "rev_pair (b, a) = (a, b)" defs pair_def : "pair == %x. (x, x)" consts slice_unif :: "('a * 'a) relation => 'a relation" pair_unif :: "'a * 'b => ('a * 'a) * ('b * 'b)" inductive "slice_unif r" intros I : "((a,a), (b,b)) : r ==> (a, b) : slice_unif r" primrec "pair_unif (a, b) = ((a,a), (b,b))" end