"List prefixes" library theory (replaces old Lex/Prefix);
authorwenzelm
Wed Oct 25 18:31:21 2000 +0200 (2000-10-25)
changeset 103304362e906b745
parent 10329 a9898d89a634
child 10331 7411e4659d4a
"List prefixes" library theory (replaces old Lex/Prefix);
src/HOL/IsaMakefile
src/HOL/Lex/Prefix.ML
src/HOL/Lex/Prefix.thy
src/HOL/Library/List_Prefix.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Oct 25 18:25:41 2000 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Oct 25 18:31:21 2000 +0200
     1.3 @@ -162,9 +162,9 @@
     1.4  HOL-Library: HOL $(LOG)/HOL-Library.gz
     1.5  
     1.6  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
     1.7 -  Library/Library.thy Library/Multiset.thy Library/Quotient.thy \
     1.8 -  Library/README.html Library/ROOT.ML Library/While_Combinator.thy \
     1.9 -  Library/While_Combinator_Example.thy
    1.10 +  Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
    1.11 +  Library/Quotient.thy Library/README.html Library/ROOT.ML \
    1.12 +  Library/While_Combinator.thy Library/While_Combinator_Example.thy
    1.13  	@$(ISATOOL) usedir $(OUT)/HOL Library
    1.14  
    1.15  
    1.16 @@ -254,9 +254,8 @@
    1.17    Lex/MaxChop.thy Lex/MaxChop.ML Lex/MaxPrefix.thy Lex/MaxPrefix.ML \
    1.18    Lex/NA.thy Lex/NA.ML Lex/NAe.thy Lex/NAe.ML Lex/RegExp2NAe.thy \
    1.19    Lex/RegExp2NAe.ML Lex/RegExp2NA.thy Lex/RegExp2NA.ML \
    1.20 -  Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \
    1.21 -  Lex/RegExp.thy Lex/RegSet.thy Lex/RegSet.ML \
    1.22 -  Lex/RegSet_of_nat_DA.thy Lex/RegSet_of_nat_DA.ML
    1.23 +  Lex/ROOT.ML Lex/RegExp.thy Lex/RegSet.thy Lex/RegSet.ML \
    1.24 +  Lex/RegSet_of_nat_DA.thy Lex/RegSet_of_nat_DA.ML Library/List_Prefix.thy
    1.25  	@$(ISATOOL) usedir $(OUT)/HOL Lex
    1.26  
    1.27  
     2.1 --- a/src/HOL/Lex/Prefix.ML	Wed Oct 25 18:25:41 2000 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,105 +0,0 @@
     2.4 -(*  Title:      HOL/Lex/Prefix.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Richard Mayr & Tobias Nipkow
     2.7 -    Copyright   1995 TUM
     2.8 -*)
     2.9 -
    2.10 -(** <= is a partial order: **)
    2.11 -
    2.12 -Goalw [prefix_def] "xs <= (xs::'a list)";
    2.13 -by (Simp_tac 1);
    2.14 -qed "prefix_refl";
    2.15 -AddIffs[prefix_refl];
    2.16 -
    2.17 -Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
    2.18 -by (Clarify_tac 1);
    2.19 -by (Simp_tac 1);
    2.20 -qed "prefix_trans";
    2.21 -
    2.22 -Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
    2.23 -by (Clarify_tac 1);
    2.24 -by (Asm_full_simp_tac 1);
    2.25 -qed "prefix_antisym";
    2.26 -
    2.27 -Goalw [strict_prefix_def] "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)";
    2.28 -by Auto_tac;
    2.29 -qed "prefix_less_le";
    2.30 -
    2.31 -
    2.32 -(** recursion equations **)
    2.33 -
    2.34 -Goalw [prefix_def] "[] <= xs";
    2.35 -by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    2.36 -qed "Nil_prefix";
    2.37 -AddIffs[Nil_prefix];
    2.38 -
    2.39 -Goalw [prefix_def] "(xs <= []) = (xs = [])";
    2.40 -by (induct_tac "xs" 1);
    2.41 -by (Simp_tac 1);
    2.42 -by (Simp_tac 1);
    2.43 -qed "prefix_Nil";
    2.44 -Addsimps [prefix_Nil];
    2.45 -
    2.46 -Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
    2.47 -by (rtac iffI 1);
    2.48 - by (etac exE 1);
    2.49 - by (rename_tac "zs" 1);
    2.50 - by (res_inst_tac [("xs","zs")] rev_exhaust 1);
    2.51 -  by (Asm_full_simp_tac 1);
    2.52 - by (hyp_subst_tac 1);
    2.53 - by (asm_full_simp_tac (simpset() delsimps [append_assoc]
    2.54 -                                 addsimps [append_assoc RS sym])1);
    2.55 -by (Force_tac 1);
    2.56 -qed "prefix_snoc";
    2.57 -Addsimps [prefix_snoc];
    2.58 -
    2.59 -Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
    2.60 -by (Simp_tac 1);
    2.61 -by (Fast_tac 1);
    2.62 -qed"Cons_prefix_Cons";
    2.63 -Addsimps [Cons_prefix_Cons];
    2.64 -
    2.65 -Goal "(xs@ys <= xs@zs) = (ys <= zs)";
    2.66 -by (induct_tac "xs" 1);
    2.67 -by (ALLGOALS Asm_simp_tac);
    2.68 -qed "same_prefix_prefix";
    2.69 -Addsimps [same_prefix_prefix];
    2.70 -
    2.71 -AddIffs   (* (xs@ys <= xs) = (ys <= []) *)
    2.72 - [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
    2.73 -
    2.74 -Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
    2.75 -by (Clarify_tac 1);
    2.76 -by (Simp_tac 1);
    2.77 -qed "prefix_prefix";
    2.78 -Addsimps [prefix_prefix];
    2.79 -
    2.80 -Goalw [prefix_def]
    2.81 -   "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
    2.82 -by (case_tac "xs" 1);
    2.83 -by Auto_tac;
    2.84 -qed "prefix_Cons";
    2.85 -
    2.86 -Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
    2.87 -by (rev_induct_tac "zs" 1);
    2.88 - by (Force_tac 1);
    2.89 -by (asm_full_simp_tac (simpset() delsimps [append_assoc]
    2.90 -                                 addsimps [append_assoc RS sym])1);
    2.91 -by (Simp_tac 1);
    2.92 -by (Blast_tac 1);
    2.93 -qed "prefix_append";
    2.94 -
    2.95 -Goalw [prefix_def]
    2.96 -  "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys";
    2.97 -by (auto_tac(claset(), simpset() addsimps [nth_append]));
    2.98 -by (case_tac "ys" 1);
    2.99 -by Auto_tac;
   2.100 -qed "append_one_prefix";
   2.101 -
   2.102 -Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";
   2.103 -by Auto_tac;
   2.104 -qed "prefix_length_le";
   2.105 -
   2.106 -Goal "mono length";
   2.107 -by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1);
   2.108 -qed "mono_length";
     3.1 --- a/src/HOL/Lex/Prefix.thy	Wed Oct 25 18:25:41 2000 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,16 +0,0 @@
     3.4 -(*  Title:      HOL/Lex/Prefix.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Tobias Nipkow
     3.7 -    Copyright   1995 TUM
     3.8 -*)
     3.9 -
    3.10 -Prefix = Main +
    3.11 -
    3.12 -instance list :: (term)ord
    3.13 -
    3.14 -defs
    3.15 -        prefix_def        "xs <= zs  ==  ? ys. zs = xs@ys"
    3.16 -
    3.17 -        strict_prefix_def "xs < zs  ==  xs <= zs & xs ~= (zs::'a list)"
    3.18 -  
    3.19 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/List_Prefix.thy	Wed Oct 25 18:31:21 2000 +0200
     4.3 @@ -0,0 +1,150 @@
     4.4 +(*  Title:      HOL/Library/List_Prefix.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4.7 +*)
     4.8 +
     4.9 +header {*
    4.10 +  \title{List prefixes}
    4.11 +  \author{Tobias Nipkow and Markus Wenzel}
    4.12 +*}
    4.13 +
    4.14 +theory List_Prefix = Main:
    4.15 +
    4.16 +subsection {* Prefix order on lists *}
    4.17 +
    4.18 +instance list :: ("term") ord ..
    4.19 +
    4.20 +defs (overloaded)
    4.21 +  prefix_def: "xs \<le> zs == \<exists>ys. zs = xs @ ys"
    4.22 +  strict_prefix_def: "xs < zs == xs \<le> zs \<and> xs \<noteq> (zs::'a list)"
    4.23 +
    4.24 +instance list :: ("term") order
    4.25 +proof
    4.26 +  fix xs ys zs :: "'a list"
    4.27 +  show "xs \<le> xs" by (simp add: prefix_def)
    4.28 +  { assume "xs \<le> ys" and "ys \<le> zs" thus "xs \<le> zs" by (auto simp add: prefix_def) }
    4.29 +  { assume "xs \<le> ys" and "ys \<le> xs" thus "xs = ys" by (auto simp add: prefix_def) }
    4.30 +  show "(xs < zs) = (xs \<le> zs \<and> xs \<noteq> zs)" by (simp only: strict_prefix_def)
    4.31 +qed
    4.32 +
    4.33 +constdefs
    4.34 +  parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
    4.35 +  "xs \<parallel> ys == \<not> (xs \<le> ys) \<and> \<not> (ys \<le> xs)"
    4.36 +
    4.37 +lemma parallelI [intro]: "\<not> (xs \<le> ys) ==> \<not> (ys \<le> xs) ==> xs \<parallel> ys"
    4.38 +  by (unfold parallel_def) blast
    4.39 +
    4.40 +lemma parellelE [elim]:
    4.41 +    "xs \<parallel> ys ==> (\<not> (xs \<le> ys) ==> \<not> (ys \<le> xs) ==> C) ==> C"
    4.42 +  by (unfold parallel_def) blast
    4.43 +
    4.44 +theorem prefix_cases:
    4.45 +  "(xs \<le> ys ==> C) ==>
    4.46 +    (ys \<le> xs ==> C) ==>
    4.47 +    (xs \<parallel> ys ==> C) ==> C"
    4.48 +  by (unfold parallel_def) blast
    4.49 +
    4.50 +
    4.51 +subsection {* Recursion equations *}
    4.52 +
    4.53 +theorem Nil_prefix [iff]: "[] \<le> xs"
    4.54 +  apply (simp add: prefix_def)
    4.55 +  done
    4.56 +
    4.57 +theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"
    4.58 +  apply (induct_tac xs)
    4.59 +   apply simp
    4.60 +  apply (simp add: prefix_def)
    4.61 +  done
    4.62 +
    4.63 +lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
    4.64 +  apply (unfold prefix_def)
    4.65 +  apply (rule iffI)
    4.66 +   apply (erule exE)
    4.67 +   apply (rename_tac zs)
    4.68 +   apply (rule_tac xs = zs in rev_exhaust)
    4.69 +    apply simp
    4.70 +   apply hypsubst
    4.71 +   apply (simp del: append_assoc add: append_assoc [symmetric])
    4.72 +  apply force
    4.73 +  done
    4.74 +
    4.75 +lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
    4.76 +  apply (auto simp add: prefix_def)
    4.77 +  done
    4.78 +
    4.79 +lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
    4.80 +  apply (induct_tac xs)
    4.81 +   apply simp_all
    4.82 +  done
    4.83 +
    4.84 +lemma [iff]: "(xs @ ys \<le> xs) = (ys = [])"
    4.85 +  apply (insert same_prefix_prefix [where ?zs = "[]"])
    4.86 +  apply simp
    4.87 +  apply blast
    4.88 +  done
    4.89 +
    4.90 +lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
    4.91 +  apply (unfold prefix_def)
    4.92 +  apply clarify
    4.93 +  apply simp
    4.94 +  done
    4.95 +
    4.96 +theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
    4.97 +  apply (unfold prefix_def)
    4.98 +  apply (case_tac xs)
    4.99 +   apply auto
   4.100 +  done
   4.101 +
   4.102 +theorem prefix_append:
   4.103 +    "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"
   4.104 +  apply (induct zs rule: rev_induct)
   4.105 +   apply force
   4.106 +  apply (simp del: append_assoc add: append_assoc [symmetric])
   4.107 +  apply simp
   4.108 +  apply blast
   4.109 +  done
   4.110 +
   4.111 +lemma append_one_prefix:
   4.112 +    "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
   4.113 +  apply (unfold prefix_def)
   4.114 +  apply (auto simp add: nth_append)
   4.115 +  apply (case_tac ys)
   4.116 +   apply auto
   4.117 +  done
   4.118 +
   4.119 +theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
   4.120 +  apply (auto simp add: prefix_def)
   4.121 +  done
   4.122 +
   4.123 +
   4.124 +subsection {* Prefix cases *}
   4.125 +
   4.126 +lemma prefix_Nil_cases [case_names Nil]:
   4.127 +  "xs \<le> [] ==>
   4.128 +    (xs = [] ==> C) ==> C"
   4.129 +  by simp
   4.130 +
   4.131 +lemma prefix_Cons_cases [case_names Nil Cons]:
   4.132 +  "xs \<le> y # ys ==>
   4.133 +    (xs = [] ==> C) ==>
   4.134 +    (!!zs. xs = y # zs ==> zs \<le> ys ==> C) ==> C"
   4.135 +  by (simp only: prefix_Cons) blast
   4.136 +
   4.137 +lemma prefix_snoc_cases [case_names prefix snoc]:
   4.138 +  "xs \<le> ys @ [y] ==>
   4.139 +    (xs \<le> ys ==> C) ==>
   4.140 +    (xs = ys @ [y] ==> C) ==> C"
   4.141 +  by (simp only: prefix_snoc) blast
   4.142 +
   4.143 +lemma prefix_append_cases [case_names prefix append]:
   4.144 +  "xs \<le> ys @ zs ==>
   4.145 +    (xs \<le> ys ==> C) ==>
   4.146 +    (!!us. xs = ys @ us ==> us \<le> zs ==> C) ==> C"
   4.147 +  by (simp only: prefix_append) blast
   4.148 +
   4.149 +lemmas prefix_any_cases [cases set: prefix] =    (*dummy set name*)
   4.150 +  prefix_Nil_cases prefix_Cons_cases
   4.151 +  prefix_snoc_cases prefix_append_cases
   4.152 +
   4.153 +end