theory Prefix_subtract+ −
imports Main "~~/src/HOL/Library/List_Prefix"+ −
begin+ −
+ −
+ −
section {* A small theory of prefix subtraction *}+ −
+ −
text {*+ −
The notion of @{text "prefix_subtract"} makes + −
the second direction of the Myhill-Nerode theorem + −
more readable.+ −
*}+ −
+ −
instantiation list :: (type) minus+ −
begin+ −
+ −
fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" + −
where+ −
"minus_list [] xs = []" + −
| "minus_list (x#xs) [] = x#xs" + −
| "minus_list (x#xs) (y#ys) = (if x = y then minus_list xs ys else (x#xs))"+ −
+ −
instance by default+ −
+ −
end+ −
+ −
lemma [simp]: "x - [] = x"+ −
by (induct x) (auto)+ −
+ −
lemma [simp]: "(x @ y) - x = y"+ −
by (induct x) (auto)+ −
+ −
lemma [simp]: "x - x = []"+ −
by (induct x) (auto)+ −
+ −
lemma [simp]: "x = z @ y \<Longrightarrow> x - z = y "+ −
by (induct x) (auto)+ −
+ −
lemma diff_prefix:+ −
"\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"+ −
by (auto elim: prefixE)+ −
+ −
lemma diff_diff_append: + −
"\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)"+ −
apply (clarsimp simp:strict_prefix_def)+ −
by (drule diff_prefix, auto elim:prefixE)+ −
+ −
lemma append_eq_cases:+ −
assumes a: "x @ y = m @ n"+ −
shows "x \<le> m \<or> m \<le> x"+ −
unfolding prefix_def using a+ −
by (auto simp add: append_eq_append_conv2)+ −
+ −
lemma append_eq_dest:+ −
assumes a: "x @ y = m @ n" + −
shows "(x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"+ −
using append_eq_cases[OF a] a+ −
by (auto elim: prefixE)+ −
+ −
end+ −