src/HOL/Library/List_Prefix.thy
changeset 37474 ce943f9edf5e
parent 30663 0b6aff7451b2
child 38857 97775f3e8722
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Jun 21 09:06:14 2010 +0200
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Jun 21 09:38:20 2010 +0200
     1.3 @@ -10,17 +10,20 @@
     1.4  
     1.5  subsection {* Prefix order on lists *}
     1.6  
     1.7 -instantiation list :: (type) order
     1.8 +instantiation list :: (type) "{order, bot}"
     1.9  begin
    1.10  
    1.11  definition
    1.12 -  prefix_def [code del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
    1.13 +  prefix_def: "xs \<le> ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    1.14  
    1.15  definition
    1.16 -  strict_prefix_def [code del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
    1.17 +  strict_prefix_def: "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
    1.18  
    1.19 -instance
    1.20 -  by intro_classes (auto simp add: prefix_def strict_prefix_def)
    1.21 +definition
    1.22 +  "bot = []"
    1.23 +
    1.24 +instance proof
    1.25 +qed (auto simp add: prefix_def strict_prefix_def bot_list_def)
    1.26  
    1.27  end
    1.28  
    1.29 @@ -77,6 +80,12 @@
    1.30  lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
    1.31    by (auto simp add: prefix_def)
    1.32  
    1.33 +lemma less_eq_list_code [code]:
    1.34 +  "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
    1.35 +  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
    1.36 +  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
    1.37 +  by simp_all
    1.38 +
    1.39  lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
    1.40    by (induct xs) simp_all
    1.41  
    1.42 @@ -125,10 +134,10 @@
    1.43  lemma prefix_length_less: "xs < ys \<Longrightarrow> length xs < length ys"
    1.44    by (auto simp: strict_prefix_def prefix_def)
    1.45  
    1.46 -lemma strict_prefix_simps [simp]:
    1.47 -    "xs < [] = False"
    1.48 -    "[] < (x # xs) = True"
    1.49 -    "(x # xs) < (y # ys) = (x = y \<and> xs < ys)"
    1.50 +lemma strict_prefix_simps [simp, code]:
    1.51 +  "xs < [] \<longleftrightarrow> False"
    1.52 +  "[] < x # xs \<longleftrightarrow> True"
    1.53 +  "x # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
    1.54    by (simp_all add: strict_prefix_def cong: conj_cong)
    1.55  
    1.56  lemma take_strict_prefix: "xs < ys \<Longrightarrow> take n xs < ys"
    1.57 @@ -301,7 +310,7 @@
    1.58      by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)
    1.59  qed
    1.60  
    1.61 -lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"
    1.62 +lemma postfix_to_prefix [code]: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"
    1.63  proof
    1.64    assume "xs >>= ys"
    1.65    then obtain zs where "xs = zs @ ys" ..
    1.66 @@ -370,21 +379,4 @@
    1.67    qed
    1.68  qed
    1.69  
    1.70 -
    1.71 -subsection {* Executable code *}
    1.72 -
    1.73 -lemma less_eq_code [code]:
    1.74 -    "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
    1.75 -    "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
    1.76 -    "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
    1.77 -  by simp_all
    1.78 -
    1.79 -lemma less_code [code]:
    1.80 -    "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
    1.81 -    "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
    1.82 -    "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
    1.83 -  unfolding strict_prefix_def by auto
    1.84 -
    1.85 -lemmas [code] = postfix_to_prefix
    1.86 -
    1.87  end