equal
deleted
inserted
replaced
315 done |
315 done |
316 |
316 |
317 (** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **) |
317 (** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **) |
318 |
318 |
319 (* c : list(Collect(B,P)) ==> c : list(B) *) |
319 (* c : list(Collect(B,P)) ==> c : list(B) *) |
320 lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD, standard] |
320 lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD] |
321 |
321 |
322 lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)" |
322 lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)" |
323 apply (induct_tac "l") |
323 apply (induct_tac "l") |
324 apply (simp_all (no_asm_simp)) |
324 apply (simp_all (no_asm_simp)) |
325 done |
325 done |