src/HOL/List.thy
changeset 14538 1d9d75a8efae
parent 14495 e2a1c31cf6d3
child 14565 c6dc17aab88a
     1.1 --- a/src/HOL/List.thy	Mon Apr 12 19:54:09 2004 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Apr 12 19:54:32 2004 +0200
     1.3 @@ -18,13 +18,11 @@
     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 @@ -42,10 +40,6 @@
    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 @@ -114,9 +108,6 @@
    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 @@ -183,8 +174,6 @@
    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 @@ -1241,21 +1230,6 @@
    1.48  by (induct ns) auto
    1.49  
    1.50  
    1.51 -subsection {* folding a relation over a list *}
    1.52 -
    1.53 -(*"fold_rel R cs \<equiv> foldl (%r c. r O {(x,y). (c,x,y):R}) Id cs"*)
    1.54 -inductive "fold_rel R" intros
    1.55 -  Nil:  "(a, [],a) : fold_rel R"
    1.56 -  Cons: "[|(a,x,b) : R; (b,xs,c) : fold_rel R|] ==> (a,x#xs,c) : fold_rel R"
    1.57 -inductive_cases fold_rel_elim_case [elim!]:
    1.58 -   "(a, [] , b) : fold_rel R"
    1.59 -   "(a, x#xs, b) : fold_rel R"
    1.60 -
    1.61 -lemma fold_rel_Nil [intro!]: "a = b ==> (a, [], b) : fold_rel R" 
    1.62 -by (simp add: fold_rel.Nil)
    1.63 -declare fold_rel.Cons [intro!]
    1.64 -
    1.65 -
    1.66  subsection {* @{text upto} *}
    1.67  
    1.68  lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])"
    1.69 @@ -1444,31 +1418,6 @@
    1.70  by (simp add: set_replicate_conv_if split: split_if_asm)
    1.71  
    1.72  
    1.73 -subsection {* @{text postfix} *}
    1.74 -
    1.75 -lemma postfix_refl [simp, intro!]: "xs \<sqsupseteq> xs" by (auto simp add: postfix_def)
    1.76 -lemma postfix_trans: "\<lbrakk>xs \<sqsupseteq> ys; ys \<sqsupseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsupseteq> zs" 
    1.77 -         by (auto simp add: postfix_def)
    1.78 -lemma postfix_antisym: "\<lbrakk>xs \<sqsupseteq> ys; ys \<sqsupseteq> xs\<rbrakk> \<Longrightarrow> xs = ys" 
    1.79 -         by (auto simp add: postfix_def)
    1.80 -
    1.81 -lemma postfix_emptyI [simp, intro!]: "xs \<sqsupseteq> []" by (auto simp add: postfix_def)
    1.82 -lemma postfix_emptyD [dest!]: "[] \<sqsupseteq> xs \<Longrightarrow> xs = []"by(auto simp add:postfix_def)
    1.83 -lemma postfix_ConsI: "xs \<sqsupseteq> ys \<Longrightarrow> x#xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
    1.84 -lemma postfix_ConsD: "xs \<sqsupseteq> y#ys \<Longrightarrow> xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
    1.85 -lemma postfix_appendI: "xs \<sqsupseteq> ys \<Longrightarrow> zs@xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
    1.86 -lemma postfix_appendD: "xs \<sqsupseteq> zs@ys \<Longrightarrow> xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
    1.87 -
    1.88 -lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
    1.89 -by (induct zs, auto)
    1.90 -lemma postfix_is_subset: "xs \<sqsupseteq> ys \<Longrightarrow> set ys \<subseteq> set xs"
    1.91 -by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
    1.92 -
    1.93 -lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs \<sqsupseteq> ys"
    1.94 -by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
    1.95 -lemma postfix_ConsD2: "x#xs \<sqsupseteq> y#ys \<Longrightarrow> xs \<sqsupseteq> ys"
    1.96 -by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
    1.97 -
    1.98  subsection {* Lexicographic orderings on lists *}
    1.99  
   1.100  lemma wf_lexn: "wf r ==> wf (lexn r n)"