src/HOL/List.thy
changeset 46176 1898e61e89c4
parent 46156 f58b7f9d3920
child 46313 0c4f18fe8218
equal deleted 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]: