equal
deleted
inserted
replaced
79 |
79 |
80 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)" |
80 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)" |
81 by (auto simp add: prefix_def) |
81 by (auto simp add: prefix_def) |
82 |
82 |
83 lemma less_eq_list_code [code]: |
83 lemma less_eq_list_code [code]: |
84 "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True" |
84 "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True" |
85 "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False" |
85 "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False" |
86 "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys" |
86 "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys" |
87 by simp_all |
87 by simp_all |
88 |
88 |
89 lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)" |
89 lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)" |
90 by (induct xs) simp_all |
90 by (induct xs) simp_all |
91 |
91 |