src/HOL/List.thy
changeset 46313 0c4f18fe8218
parent 46176 1898e61e89c4
child 46317 80dccedd6c14
     1.1 --- a/src/HOL/List.thy	Mon Jan 23 14:06:19 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Jan 23 14:07:36 2012 +0100
     1.3 @@ -4556,6 +4556,10 @@
     1.4  inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
     1.5  inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
     1.6  
     1.7 +inductive_simps listsp_simps[code]:
     1.8 +  "listsp A []"
     1.9 +  "listsp A (x # xs)"
    1.10 +
    1.11  lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
    1.12  by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
    1.13  
    1.14 @@ -4590,7 +4594,7 @@
    1.15  -- {* eliminate @{text listsp} in favour of @{text set} *}
    1.16  by (induct xs) auto
    1.17  
    1.18 -lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
    1.19 +lemmas in_lists_conv_set [code_unfold] = in_listsp_conv_set [to_set]
    1.20  
    1.21  lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
    1.22  by (rule in_listsp_conv_set [THEN iffD1])
    1.23 @@ -5021,7 +5025,7 @@
    1.24  lemma listrel_eq_len:  "(xs, ys) \<in> listrel r \<Longrightarrow> length xs = length ys"
    1.25  by(induct rule: listrel.induct) auto
    1.26  
    1.27 -lemma listrel_iff_zip: "(xs,ys) : listrel r \<longleftrightarrow>
    1.28 +lemma listrel_iff_zip [code_unfold]: "(xs,ys) : listrel r \<longleftrightarrow>
    1.29    length xs = length ys & (\<forall>(x,y) \<in> set(zip xs ys). (x,y) \<in> r)" (is "?L \<longleftrightarrow> ?R")
    1.30  proof
    1.31    assume ?L thus ?R by induct (auto intro: listrel_eq_len)
    1.32 @@ -5327,6 +5331,36 @@
    1.33    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
    1.34    by (simp add: list_ex_iff)
    1.35  
    1.36 +text {* Executable checks for relations on sets *}
    1.37 +
    1.38 +definition listrel1p :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.39 +"listrel1p r xs ys = ((xs, ys) \<in> listrel1 {(x, y). r x y})"
    1.40 +
    1.41 +lemma [code_unfold]:
    1.42 +  "(xs, ys) \<in> listrel1 r = listrel1p (\<lambda>x y. (x, y) \<in> r) xs ys"
    1.43 +unfolding listrel1p_def by auto
    1.44 +
    1.45 +lemma [code]:
    1.46 +  "listrel1p r [] xs = False"
    1.47 +  "listrel1p r xs [] =  False"
    1.48 +  "listrel1p r (x # xs) (y # ys) \<longleftrightarrow>
    1.49 +     r x y \<and> xs = ys \<or> x = y \<and> listrel1p r xs ys"
    1.50 +by (simp add: listrel1p_def)+
    1.51 +
    1.52 +definition
    1.53 +  lexordp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.54 +  "lexordp r xs ys = ((xs, ys) \<in> lexord {(x, y). r x y})"
    1.55 +
    1.56 +lemma [code_unfold]:
    1.57 +  "(xs, ys) \<in> lexord r = lexordp (\<lambda>x y. (x, y) \<in> r) xs ys"
    1.58 +unfolding lexordp_def by auto
    1.59 +
    1.60 +lemma [code]:
    1.61 +  "lexordp r xs [] = False"
    1.62 +  "lexordp r [] (y#ys) = True"
    1.63 +  "lexordp r (x # xs) (y # ys) = (r x y | (x = y & lexordp r xs ys))"
    1.64 +unfolding lexordp_def by auto
    1.65 +
    1.66  text {* Bounded quantification and summation over nats. *}
    1.67  
    1.68  lemma atMost_upto [code_unfold]: