1 theory Prefix_subtract

     2   imports Main List_Prefix

     3 begin

     4 

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

     6 

     7 text {*

     8   The notion of @{text "prefix_subtract"} is need to make proofs more readable.

     9   *}

    10 

    11 fun prefix_subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51)

    12 where

    13   "prefix_subtract []     xs     = []" 

    14 | "prefix_subtract (x#xs) []     = x#xs" 

    15 | "prefix_subtract (x#xs) (y#ys) = (if x = y then prefix_subtract xs ys else (x#xs))"

    16 

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

    18 apply (induct x)

    19 by (case_tac y, simp+)

    20 

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

    22 by (induct x, auto)

    23 

    24 lemma [simp]: "x = xa @ y \<Longrightarrow> x - xa = y "

    25 by (induct x, auto)

    26 

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

    28 by (induct x, auto)

    29 

    30 lemma [simp]: "(x - y = []) \<Longrightarrow> (x \<le> y)"

    31 proof-   

    32   have "\<exists>xa. x = xa @ (x - y) \<and> xa \<le> y"

    33     apply (rule prefix_subtract.induct[of _ x y], simp+)

    34     by (clarsimp, rule_tac x = "y # xa" in exI, simp+)

    35   thus "(x - y = []) \<Longrightarrow> (x \<le> y)" by simp

    36 qed

    37 

    38 lemma diff_prefix:

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

    40 by (auto elim:prefixE)

    41 

    42 lemma diff_diff_appd: 

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

    44 apply (clarsimp simp:strict_prefix_def)

    45 by (drule diff_prefix, auto elim:prefixE)

    46 

    47 lemma app_eq_cases[rule_format]:

    48   "\<forall> x . x @ y = m @ n \<longrightarrow> (x \<le> m \<or> m \<le> x)"

    49 apply (induct y, simp)

    50 apply (clarify, drule_tac x = "x @ [a]" in spec)

    51 by (clarsimp, auto simp:prefix_def)

    52 

    53 lemma app_eq_dest:

    54   "x @ y = m @ n \<Longrightarrow> 

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

    56 by (frule_tac app_eq_cases, auto elim:prefixE)

    57 

    58 end