src/HOL/List.thy
changeset 14099 55d244f3c86d
parent 14050 826037db30cd
child 14111 993471c762b8
     1.1 --- a/src/HOL/List.thy	Fri Jul 11 14:11:56 2003 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Jul 11 14:12:02 2003 +0200
     1.3 @@ -18,11 +18,13 @@
     1.4    concat:: "'a list list => 'a list"
     1.5    foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
     1.6    foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
     1.7 +  fold_rel :: "('a * 'c * 'a) set => ('a * 'c list * 'a) set"
     1.8    hd:: "'a list => 'a"
     1.9    tl:: "'a list => 'a list"
    1.10    last:: "'a list => 'a"
    1.11    butlast :: "'a list => 'a list"
    1.12    set :: "'a list => 'a set"
    1.13 +  o2l :: "'a option => 'a list"
    1.14    list_all:: "('a => bool) => ('a list => bool)"
    1.15    list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool"
    1.16    map :: "('a=>'b) => ('a list => 'b list)"
    1.17 @@ -40,6 +42,10 @@
    1.18    null:: "'a list => bool"
    1.19    "distinct":: "'a list => bool"
    1.20    replicate :: "nat => 'a => 'a list"
    1.21 +  postfix :: "'a list => 'a list => bool"
    1.22 +
    1.23 +syntax (xsymbols)
    1.24 +  postfix :: "'a list => 'a list => bool"             ("(_/ \<sqsupseteq> _)" [51, 51] 50)
    1.25  
    1.26  nonterminals lupdbinds lupdbind
    1.27  
    1.28 @@ -108,6 +114,9 @@
    1.29  "set [] = {}"
    1.30  "set (x#xs) = insert x (set xs)"
    1.31  primrec
    1.32 + "o2l  None    = []"
    1.33 + "o2l (Some x) = [x]"
    1.34 +primrec
    1.35  list_all_Nil:"list_all P [] = True"
    1.36  list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)"
    1.37  primrec
    1.38 @@ -174,6 +183,8 @@
    1.39  replicate_0: "replicate 0 x = []"
    1.40  replicate_Suc: "replicate (Suc n) x = x # replicate n x"
    1.41  defs
    1.42 + postfix_def: "postfix xs ys == \<exists>zs. xs = zs @ ys"
    1.43 +defs
    1.44   list_all2_def:
    1.45   "list_all2 P xs ys == length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)"
    1.46  
    1.47 @@ -277,6 +288,12 @@
    1.48  apply blast
    1.49  done
    1.50  
    1.51 +lemma impossible_Cons [rule_format]: 
    1.52 +  "length xs <= length ys --> xs = x # ys = False"
    1.53 +apply (induct xs)
    1.54 +apply auto
    1.55 +done
    1.56 +
    1.57  
    1.58  subsection {* @{text "@"} -- append *}
    1.59  
    1.60 @@ -523,9 +540,17 @@
    1.61  lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)"
    1.62  by (induct xs) auto
    1.63  
    1.64 +lemma hd_in_set: "l = x#xs \<Longrightarrow> x\<in>set l"
    1.65 +apply (case_tac l)
    1.66 +apply auto
    1.67 +done
    1.68 +
    1.69  lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
    1.70  by auto
    1.71  
    1.72 +lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs" 
    1.73 +by auto
    1.74 +
    1.75  lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
    1.76  by (induct xs) auto
    1.77  
    1.78 @@ -1164,6 +1189,21 @@
    1.79  by (induct ns) auto
    1.80  
    1.81  
    1.82 +subsection {* folding a relation over a list *}
    1.83 +
    1.84 +(*"fold_rel R cs \<equiv> foldl (%r c. r O {(x,y). (c,x,y):R}) Id cs"*)
    1.85 +inductive "fold_rel R" intros
    1.86 +  Nil:  "(a, [],a) : fold_rel R"
    1.87 +  Cons: "[|(a,x,b) : R; (b,xs,c) : fold_rel R|] ==> (a,x#xs,c) : fold_rel R"
    1.88 +inductive_cases fold_rel_elim_case [elim!]:
    1.89 +   "(a, []  , b) : fold_rel R"
    1.90 +   "(a, x#xs, b) : fold_rel R"
    1.91 +
    1.92 +lemma fold_rel_Nil [intro!]: "a = b ==> (a, [], b) : fold_rel R" 
    1.93 +by (simp add: fold_rel.Nil)
    1.94 +declare fold_rel.Cons [intro!]
    1.95 +
    1.96 +
    1.97  subsection {* @{text upto} *}
    1.98  
    1.99  lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])"
   1.100 @@ -1348,7 +1388,32 @@
   1.101  by (simp add: set_replicate_conv_if split: split_if_asm)
   1.102  
   1.103  
   1.104 -subsection {* Lexcicographic orderings on lists *}
   1.105 +subsection {* @{text postfix} *}
   1.106 +
   1.107 +lemma postfix_refl [simp, intro!]: "xs \<sqsupseteq> xs" by (auto simp add: postfix_def)
   1.108 +lemma postfix_trans: "\<lbrakk>xs \<sqsupseteq> ys; ys \<sqsupseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsupseteq> zs" 
   1.109 +         by (auto simp add: postfix_def)
   1.110 +lemma postfix_antisym: "\<lbrakk>xs \<sqsupseteq> ys; ys \<sqsupseteq> xs\<rbrakk> \<Longrightarrow> xs = ys" 
   1.111 +         by (auto simp add: postfix_def)
   1.112 +
   1.113 +lemma postfix_emptyI [simp, intro!]: "xs \<sqsupseteq> []" by (auto simp add: postfix_def)
   1.114 +lemma postfix_emptyD [dest!]: "[] \<sqsupseteq> xs \<Longrightarrow> xs = []"by(auto simp add:postfix_def)
   1.115 +lemma postfix_ConsI: "xs \<sqsupseteq> ys \<Longrightarrow> x#xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
   1.116 +lemma postfix_ConsD: "xs \<sqsupseteq> y#ys \<Longrightarrow> xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
   1.117 +lemma postfix_appendI: "xs \<sqsupseteq> ys \<Longrightarrow> zs@xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
   1.118 +lemma postfix_appendD: "xs \<sqsupseteq> zs@ys \<Longrightarrow> xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
   1.119 +
   1.120 +lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
   1.121 +by (induct zs, auto)
   1.122 +lemma postfix_is_subset: "xs \<sqsupseteq> ys \<Longrightarrow> set ys \<subseteq> set xs"
   1.123 +by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
   1.124 +
   1.125 +lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs \<sqsupseteq> ys"
   1.126 +by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
   1.127 +lemma postfix_ConsD2: "x#xs \<sqsupseteq> y#ys \<Longrightarrow> xs \<sqsupseteq> ys"
   1.128 +by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
   1.129 +
   1.130 +subsection {* Lexicographic orderings on lists *}
   1.131  
   1.132  lemma wf_lexn: "wf r ==> wf (lexn r n)"
   1.133  apply (induct_tac n)