paper about formalising parsing; seems to have done what we would like to do....probably also appears at ITP'11
theory Prefix_subtract imports Main "~~/src/HOL/Library/List_Prefix"beginsection {* A small theory of prefix subtraction *}text {* The notion of @{text "prefix_subtract"} is need to make proofs more readable. *}fun prefix_subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51)where "prefix_subtract [] xs = []" | "prefix_subtract (x#xs) [] = x#xs" | "prefix_subtract (x#xs) (y#ys) = (if x = y then prefix_subtract xs ys else (x#xs))"lemma [simp]: "(x @ y) - x = y"apply (induct x)by (case_tac y, simp+)lemma [simp]: "x - x = []"by (induct x, auto)lemma [simp]: "x = xa @ y \<Longrightarrow> x - xa = y "by (induct x, auto)lemma [simp]: "x - [] = x"by (induct x, auto)lemma [simp]: "(x - y = []) \<Longrightarrow> (x \<le> y)"proof- have "\<exists>xa. x = xa @ (x - y) \<and> xa \<le> y" apply (rule prefix_subtract.induct[of _ x y], simp+) by (clarsimp, rule_tac x = "y # xa" in exI, simp+) thus "(x - y = []) \<Longrightarrow> (x \<le> y)" by simpqedlemma diff_prefix: "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"by (auto elim:prefixE)lemma diff_diff_appd: "\<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 app_eq_cases[rule_format]: "\<forall> x . x @ y = m @ n \<longrightarrow> (x \<le> m \<or> m \<le> x)"apply (induct y, simp)apply (clarify, drule_tac x = "x @ [a]" in spec)by (clarsimp, auto simp:prefix_def)lemma app_eq_dest: "x @ y = m @ n \<Longrightarrow> (x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"by (frule_tac app_eq_cases, auto elim:prefixE)end