src/HOL/List.thy
 changeset 46176 1898e61e89c4 parent 46156 f58b7f9d3920 child 46313 0c4f18fe8218
equal inserted replaced
46175:48c534b22040 46176:1898e61e89c4
`  4557 inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"`
`  4557 inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"`
`  4558 `
`  4558 `
`  4559 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"`
`  4559 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"`
`  4560 by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)`
`  4560 by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)`
`  4561 `
`  4561 `
`  4562 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]`
`  4562 lemmas lists_mono = listsp_mono [to_set]`
`  4563 `
`  4563 `
`  4564 lemma listsp_infI:`
`  4564 lemma listsp_infI:`
`  4565   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l`
`  4565   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l`
`  4566 by induct blast+`
`  4566 by induct blast+`
`  4567 `
`  4567 `
`  4573   show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)`
`  4573   show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)`
`  4574 qed`
`  4574 qed`
`  4575 `
`  4575 `
`  4576 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def]`
`  4576 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def]`
`  4577 `
`  4577 `
`  4578 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]`
`  4578 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set]`
`  4579 `
`  4579 `
`  4580 lemma Cons_in_lists_iff[simp]: "x#xs : lists A \<longleftrightarrow> x:A \<and> xs : lists A"`
`  4580 lemma Cons_in_lists_iff[simp]: "x#xs : lists A \<longleftrightarrow> x:A \<and> xs : lists A"`
`  4581 by auto`
`  4581 by auto`
`  4582 `
`  4582 `
`  4583 lemma append_in_listsp_conv [iff]:`
`  4583 lemma append_in_listsp_conv [iff]:`