1 theory Prefix_subtract |
1 theory Prefix_subtract |
2 imports Main |
2 imports Main "~~/src/HOL/Library/List_Prefix" |
3 "~~/src/HOL/Library/List_Prefix" |
|
4 begin |
3 begin |
|
4 |
5 |
5 |
6 section {* A small theory of prefix subtraction *} |
6 section {* A small theory of prefix subtraction *} |
7 |
7 |
8 text {* |
8 text {* |
9 The notion of @{text "prefix_subtract"} is need to make proofs more readable. |
9 The notion of @{text "prefix_subtract"} makes |
10 *} |
10 the second direction of the Myhill-Nerode theorem |
|
11 more readable. |
|
12 *} |
11 |
13 |
12 fun prefix_subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51) |
14 instantiation list :: (type) minus |
|
15 begin |
|
16 |
|
17 fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
13 where |
18 where |
14 "prefix_subtract [] xs = []" |
19 "minus_list [] xs = []" |
15 | "prefix_subtract (x#xs) [] = x#xs" |
20 | "minus_list (x#xs) [] = x#xs" |
16 | "prefix_subtract (x#xs) (y#ys) = (if x = y then prefix_subtract xs ys else (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) |
17 |
29 |
18 lemma [simp]: "(x @ y) - x = y" |
30 lemma [simp]: "(x @ y) - x = y" |
19 apply (induct x) |
31 by (induct x) (auto) |
20 by (case_tac y, simp+) |
|
21 |
32 |
22 lemma [simp]: "x - x = []" |
33 lemma [simp]: "x - x = []" |
23 by (induct x, auto) |
34 by (induct x) (auto) |
24 |
35 |
25 lemma [simp]: "x = xa @ y \<Longrightarrow> x - xa = y " |
36 lemma [simp]: "x = z @ y \<Longrightarrow> x - z = y " |
26 by (induct x, auto) |
37 by (induct x) (auto) |
27 |
|
28 lemma [simp]: "x - [] = x" |
|
29 by (induct x, auto) |
|
30 |
|
31 lemma [simp]: "(x - y = []) \<Longrightarrow> (x \<le> y)" |
|
32 proof- |
|
33 have "\<exists>xa. x = xa @ (x - y) \<and> xa \<le> y" |
|
34 apply (rule prefix_subtract.induct[of _ x y], simp+) |
|
35 by (clarsimp, rule_tac x = "y # xa" in exI, simp+) |
|
36 thus "(x - y = []) \<Longrightarrow> (x \<le> y)" by simp |
|
37 qed |
|
38 |
38 |
39 lemma diff_prefix: |
39 lemma diff_prefix: |
40 "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a" |
40 "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a" |
41 by (auto elim:prefixE) |
41 by (auto elim: prefixE) |
42 |
42 |
43 lemma diff_diff_appd: |
43 lemma diff_diff_append: |
44 "\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)" |
44 "\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)" |
45 apply (clarsimp simp:strict_prefix_def) |
45 apply (clarsimp simp:strict_prefix_def) |
46 by (drule diff_prefix, auto elim:prefixE) |
46 by (drule diff_prefix, auto elim:prefixE) |
47 |
47 |
48 lemma app_eq_cases[rule_format]: |
48 lemma append_eq_cases: |
49 "\<forall> x . x @ y = m @ n \<longrightarrow> (x \<le> m \<or> m \<le> x)" |
49 assumes a: "x @ y = m @ n" |
50 apply (induct y, simp) |
50 shows "x \<le> m \<or> m \<le> x" |
51 apply (clarify, drule_tac x = "x @ [a]" in spec) |
51 unfolding prefix_def using a |
52 by (clarsimp, auto simp:prefix_def) |
52 by (auto simp add: append_eq_append_conv2) |
53 |
53 |
54 lemma app_eq_dest: |
54 lemma append_eq_dest: |
55 "x @ y = m @ n \<Longrightarrow> |
55 assumes a: "x @ y = m @ n" |
56 (x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)" |
56 shows "(x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)" |
57 by (frule_tac app_eq_cases, auto elim:prefixE) |
57 using append_eq_cases[OF a] a |
|
58 by (auto elim: prefixE) |
58 |
59 |
59 end |
60 end |