removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
authoroheimb
Mon Apr 12 19:54:32 2004 +0200 (2004-04-12)
changeset 145381d9d75a8efae
parent 14537 e95ba267e3d5
child 14539 90c625edaee1
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
src/HOL/Library/List_Prefix.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Apr 12 19:54:09 2004 +0200
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Apr 12 19:54:32 2004 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  *)
     1.5  
     1.6  header {*
     1.7 -  \title{List prefixes}
     1.8 +  \title{List prefixes and postfixes}
     1.9    \author{Tobias Nipkow and Markus Wenzel}
    1.10  *}
    1.11  
    1.12 @@ -215,4 +215,43 @@
    1.13    qed
    1.14  qed
    1.15  
    1.16 +
    1.17 +subsection {* Postfix order on lists *}
    1.18 +
    1.19 +constdefs
    1.20 +  postfix :: "'a list => 'a list => bool"  ("(_/ >= _)" [51, 50] 50)
    1.21 +  "xs >= ys == \<exists>zs. xs = zs @ ys"
    1.22 +
    1.23 +lemma postfix_refl [simp, intro!]: "xs >= xs" by (auto simp add: postfix_def)
    1.24 +lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs" 
    1.25 +         by (auto simp add: postfix_def)
    1.26 +lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys" 
    1.27 +         by (auto simp add: postfix_def)
    1.28 +
    1.29 +lemma Nil_postfix [iff]: "xs >= []" by (simp add: postfix_def)
    1.30 +lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])"by (auto simp add:postfix_def)
    1.31 +
    1.32 +lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys" by (auto simp add: postfix_def)
    1.33 +lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys" by (auto simp add: postfix_def)
    1.34 +
    1.35 +lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs@xs >= ys" by(auto simp add: postfix_def)
    1.36 +lemma postfix_appendD: "xs >= zs@ys \<Longrightarrow> xs >= ys" by(auto simp add: postfix_def)
    1.37 +
    1.38 +lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
    1.39 +by (induct zs, auto)
    1.40 +lemma postfix_is_subset: "xs >= ys \<Longrightarrow> set ys \<subseteq> set xs"
    1.41 +by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
    1.42 +
    1.43 +lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >= ys"
    1.44 +by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
    1.45 +lemma postfix_ConsD2: "x#xs >= y#ys \<Longrightarrow> xs >= ys"
    1.46 +by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
    1.47 +
    1.48 +lemma postfix2prefix: "(xs >= ys) = (rev ys <= rev xs)"
    1.49 +apply (unfold prefix_def postfix_def, safe)
    1.50 +apply (rule_tac x = "rev zs" in exI, simp)
    1.51 +apply (rule_tac x = "rev zs" in exI)
    1.52 +apply (rule rev_is_rev_conv [THEN iffD1], simp)
    1.53 +done
    1.54 +
    1.55  end
     2.1 --- a/src/HOL/List.thy	Mon Apr 12 19:54:09 2004 +0200
     2.2 +++ b/src/HOL/List.thy	Mon Apr 12 19:54:32 2004 +0200
     2.3 @@ -18,13 +18,11 @@
     2.4    concat:: "'a list list => 'a list"
     2.5    foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
     2.6    foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
     2.7 -  fold_rel :: "('a * 'c * 'a) set => ('a * 'c list * 'a) set"
     2.8    hd:: "'a list => 'a"
     2.9    tl:: "'a list => 'a list"
    2.10    last:: "'a list => 'a"
    2.11    butlast :: "'a list => 'a list"
    2.12    set :: "'a list => 'a set"
    2.13 -  o2l :: "'a option => 'a list"
    2.14    list_all:: "('a => bool) => ('a list => bool)"
    2.15    list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool"
    2.16    map :: "('a=>'b) => ('a list => 'b list)"
    2.17 @@ -42,10 +40,6 @@
    2.18    null:: "'a list => bool"
    2.19    "distinct":: "'a list => bool"
    2.20    replicate :: "nat => 'a => 'a list"
    2.21 -  postfix :: "'a list => 'a list => bool"
    2.22 -
    2.23 -syntax (xsymbols)
    2.24 -  postfix :: "'a list => 'a list => bool"             ("(_/ \<sqsupseteq> _)" [51, 51] 50)
    2.25  
    2.26  nonterminals lupdbinds lupdbind
    2.27  
    2.28 @@ -114,9 +108,6 @@
    2.29  "set [] = {}"
    2.30  "set (x#xs) = insert x (set xs)"
    2.31  primrec
    2.32 - "o2l  None    = []"
    2.33 - "o2l (Some x) = [x]"
    2.34 -primrec
    2.35  list_all_Nil:"list_all P [] = True"
    2.36  list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)"
    2.37  primrec
    2.38 @@ -183,8 +174,6 @@
    2.39  replicate_0: "replicate 0 x = []"
    2.40  replicate_Suc: "replicate (Suc n) x = x # replicate n x"
    2.41  defs
    2.42 - postfix_def: "postfix xs ys == \<exists>zs. xs = zs @ ys"
    2.43 -defs
    2.44   list_all2_def:
    2.45   "list_all2 P xs ys == length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)"
    2.46  
    2.47 @@ -1241,21 +1230,6 @@
    2.48  by (induct ns) auto
    2.49  
    2.50  
    2.51 -subsection {* folding a relation over a list *}
    2.52 -
    2.53 -(*"fold_rel R cs \<equiv> foldl (%r c. r O {(x,y). (c,x,y):R}) Id cs"*)
    2.54 -inductive "fold_rel R" intros
    2.55 -  Nil:  "(a, [],a) : fold_rel R"
    2.56 -  Cons: "[|(a,x,b) : R; (b,xs,c) : fold_rel R|] ==> (a,x#xs,c) : fold_rel R"
    2.57 -inductive_cases fold_rel_elim_case [elim!]:
    2.58 -   "(a, [] , b) : fold_rel R"
    2.59 -   "(a, x#xs, b) : fold_rel R"
    2.60 -
    2.61 -lemma fold_rel_Nil [intro!]: "a = b ==> (a, [], b) : fold_rel R" 
    2.62 -by (simp add: fold_rel.Nil)
    2.63 -declare fold_rel.Cons [intro!]
    2.64 -
    2.65 -
    2.66  subsection {* @{text upto} *}
    2.67  
    2.68  lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])"
    2.69 @@ -1444,31 +1418,6 @@
    2.70  by (simp add: set_replicate_conv_if split: split_if_asm)
    2.71  
    2.72  
    2.73 -subsection {* @{text postfix} *}
    2.74 -
    2.75 -lemma postfix_refl [simp, intro!]: "xs \<sqsupseteq> xs" by (auto simp add: postfix_def)
    2.76 -lemma postfix_trans: "\<lbrakk>xs \<sqsupseteq> ys; ys \<sqsupseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsupseteq> zs" 
    2.77 -         by (auto simp add: postfix_def)
    2.78 -lemma postfix_antisym: "\<lbrakk>xs \<sqsupseteq> ys; ys \<sqsupseteq> xs\<rbrakk> \<Longrightarrow> xs = ys" 
    2.79 -         by (auto simp add: postfix_def)
    2.80 -
    2.81 -lemma postfix_emptyI [simp, intro!]: "xs \<sqsupseteq> []" by (auto simp add: postfix_def)
    2.82 -lemma postfix_emptyD [dest!]: "[] \<sqsupseteq> xs \<Longrightarrow> xs = []"by(auto simp add:postfix_def)
    2.83 -lemma postfix_ConsI: "xs \<sqsupseteq> ys \<Longrightarrow> x#xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
    2.84 -lemma postfix_ConsD: "xs \<sqsupseteq> y#ys \<Longrightarrow> xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
    2.85 -lemma postfix_appendI: "xs \<sqsupseteq> ys \<Longrightarrow> zs@xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
    2.86 -lemma postfix_appendD: "xs \<sqsupseteq> zs@ys \<Longrightarrow> xs \<sqsupseteq> ys" by (auto simp add: postfix_def)
    2.87 -
    2.88 -lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
    2.89 -by (induct zs, auto)
    2.90 -lemma postfix_is_subset: "xs \<sqsupseteq> ys \<Longrightarrow> set ys \<subseteq> set xs"
    2.91 -by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
    2.92 -
    2.93 -lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs \<sqsupseteq> ys"
    2.94 -by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
    2.95 -lemma postfix_ConsD2: "x#xs \<sqsupseteq> y#ys \<Longrightarrow> xs \<sqsupseteq> ys"
    2.96 -by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
    2.97 -
    2.98  subsection {* Lexicographic orderings on lists *}
    2.99  
   2.100  lemma wf_lexn: "wf r ==> wf (lexn r n)"