1 theory Prefix_subtract

     2   imports Main "~~/src/HOL/Library/List_Prefix"

     3 begin

     4 

     5 

     6 section {* A small theory of prefix subtraction *}

     7 

     8 text {*

     9   The notion of @{text "prefix_subtract"} makes 

    10   the second direction of the Myhill-Nerode theorem 

    11   more readable.

    12 *}

    13 

    14 instantiation list :: (type) minus

    15 begin

    16 

    17 fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 

    18 where

    19   "minus_list []     xs     = []" 

    20 | "minus_list (x#xs) []     = x#xs" 

    21 | "minus_list (x#xs) (y#ys) = (if x = y then minus_list xs ys else (x#xs))"

    22 

    23 instance by default

    24 

    25 end

    26 

    27 lemma [simp]: "x - [] = x"

    28 by (induct x) (auto)

    29 

    30 lemma [simp]: "(x @ y) - x = y"

    31 by (induct x) (auto)

    32 

    33 lemma [simp]: "x - x = []"

    34 by (induct x) (auto)

    35 

    36 lemma [simp]: "x = z @ y \<Longrightarrow> x - z = y "

    37 by (induct x) (auto)

    38 

    39 lemma diff_prefix:

    40   "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"

    41 by (auto elim: prefixE)

    42 

    43 lemma diff_diff_append: 

    44   "\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)"

    45 apply (clarsimp simp:strict_prefix_def)

    46 by (drule diff_prefix, auto elim:prefixE)

    47 

    48 lemma append_eq_cases:

    49   assumes a: "x @ y = m @ n"

    50   shows "x \<le> m \<or> m \<le> x"

    51 unfolding prefix_def using a

    52 by (auto simp add: append_eq_append_conv2)

    53 

    54 lemma append_eq_dest:

    55   assumes a: "x @ y = m @ n" 

    56   shows "(x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"

    57 using append_eq_cases[OF a] a

    58 by (auto elim: prefixE)

    59 

    60 end