author | berghofe |
Fri, 01 Jul 2005 13:54:12 +0200 | |
changeset 16633 | 208ebc9311f2 |
parent 16417 | 9bc16273c2d4 |
child 19736 | d8d0f8f51d69 |
permissions | -rw-r--r-- |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/LList.thy |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
4 |
Copyright 1997 University of Cambridge |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
5 |
*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
6 |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
7 |
header {*The "filter" functional for coinductive lists |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
8 |
--defined by a combination of induction and coinduction*} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
9 |
|
16417 | 10 |
theory LFilter imports LList begin |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
11 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
12 |
consts |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
13 |
findRel :: "('a => bool) => ('a llist * 'a llist)set" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
14 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
15 |
inductive "findRel p" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
16 |
intros |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
17 |
found: "p x ==> (LCons x l, LCons x l) \<in> findRel p" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
18 |
seek: "[| ~p x; (l,l') \<in> findRel p |] ==> (LCons x l, l') \<in> findRel p" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
19 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
20 |
declare findRel.intros [intro] |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
21 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
22 |
constdefs |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
23 |
find :: "['a => bool, 'a llist] => 'a llist" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
24 |
"find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
25 |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
26 |
lfilter :: "['a => bool, 'a llist] => 'a llist" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
27 |
"lfilter p l == llist_corec l (%l. case find p l of |
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
3120
diff
changeset
|
28 |
LNil => None |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
3120
diff
changeset
|
29 |
| LCons y z => Some(y,z))" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
30 |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
31 |
|
13107 | 32 |
subsection {* @{text findRel}: basic laws *} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
33 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
34 |
inductive_cases |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
35 |
findRel_LConsE [elim!]: "(LCons x l, l'') \<in> findRel p" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
36 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
37 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
38 |
lemma findRel_functional [rule_format]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
39 |
"(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
40 |
by (erule findRel.induct, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
41 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
42 |
lemma findRel_imp_LCons [rule_format]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
43 |
"(l,l'): findRel p ==> \<exists>x l''. l' = LCons x l'' & p x" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
44 |
by (erule findRel.induct, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
45 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
46 |
lemma findRel_LNil [elim!]: "(LNil,l): findRel p ==> R" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
47 |
by (blast elim: findRel.cases) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
48 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
49 |
|
13107 | 50 |
subsection {* Properties of @{text "Domain (findRel p)"} *} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
51 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
52 |
lemma LCons_Domain_findRel [simp]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
53 |
"LCons x l \<in> Domain(findRel p) = (p x | l \<in> Domain(findRel p))" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
54 |
by auto |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
55 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
56 |
lemma Domain_findRel_iff: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
57 |
"(l \<in> Domain (findRel p)) = (\<exists>x l'. (l, LCons x l') \<in> findRel p & p x)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
58 |
by (blast dest: findRel_imp_LCons) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
59 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
60 |
lemma Domain_findRel_mono: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
61 |
"[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
62 |
apply clarify |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
63 |
apply (erule findRel.induct, blast+) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
64 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
65 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
66 |
|
13107 | 67 |
subsection {* @{text find}: basic equations *} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
68 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
69 |
lemma find_LNil [simp]: "find p LNil = LNil" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
70 |
by (unfold find_def, blast) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
71 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
72 |
lemma findRel_imp_find [simp]: "(l,l') \<in> findRel p ==> find p l = l'" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
73 |
apply (unfold find_def) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
74 |
apply (blast dest: findRel_functional) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
75 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
76 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
77 |
lemma find_LCons_found: "p x ==> find p (LCons x l) = LCons x l" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
78 |
by (blast intro: findRel_imp_find) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
79 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
80 |
lemma diverge_find_LNil [simp]: "l ~: Domain(findRel p) ==> find p l = LNil" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
81 |
by (unfold find_def, blast) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
82 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
83 |
lemma find_LCons_seek: "~ (p x) ==> find p (LCons x l) = find p l" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
84 |
apply (case_tac "LCons x l \<in> Domain (findRel p) ") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
85 |
apply auto |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
86 |
apply (blast intro: findRel_imp_find) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
87 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
88 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
89 |
lemma find_LCons [simp]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
90 |
"find p (LCons x l) = (if p x then LCons x l else find p l)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
91 |
by (simp add: find_LCons_seek find_LCons_found) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
92 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
93 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
94 |
|
13107 | 95 |
subsection {* @{text lfilter}: basic equations *} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
96 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
97 |
lemma lfilter_LNil [simp]: "lfilter p LNil = LNil" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
98 |
by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
99 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
100 |
lemma diverge_lfilter_LNil [simp]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
101 |
"l ~: Domain(findRel p) ==> lfilter p l = LNil" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
102 |
by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
103 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
104 |
lemma lfilter_LCons_found: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
105 |
"p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
106 |
by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
107 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
108 |
lemma findRel_imp_lfilter [simp]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
109 |
"(l, LCons x l') \<in> findRel p ==> lfilter p l = LCons x (lfilter p l')" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
110 |
by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
111 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
112 |
lemma lfilter_LCons_seek: "~ (p x) ==> lfilter p (LCons x l) = lfilter p l" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
113 |
apply (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
114 |
apply (case_tac "LCons x l \<in> Domain (findRel p) ") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
115 |
apply (simp add: Domain_findRel_iff, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
116 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
117 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
118 |
lemma lfilter_LCons [simp]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
119 |
"lfilter p (LCons x l) = |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
120 |
(if p x then LCons x (lfilter p l) else lfilter p l)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
121 |
by (simp add: lfilter_LCons_found lfilter_LCons_seek) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
122 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
123 |
declare llistD_Fun_LNil_I [intro!] llistD_Fun_LCons_I [intro!] |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
124 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
125 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
126 |
lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
127 |
apply (auto iff: Domain_findRel_iff) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
128 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
129 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
130 |
lemma lfilter_eq_LCons [rule_format]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
131 |
"lfilter p l = LCons x l' --> |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
132 |
(\<exists>l''. l' = lfilter p l'' & (l, LCons x l'') \<in> findRel p)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
133 |
apply (subst lfilter_def [THEN def_llist_corec]) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
134 |
apply (case_tac "l \<in> Domain (findRel p) ") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
135 |
apply (auto iff: Domain_findRel_iff) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
136 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
137 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
138 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
139 |
lemma lfilter_cases: "lfilter p l = LNil | |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
140 |
(\<exists>y l'. lfilter p l = LCons y (lfilter p l') & p y)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
141 |
apply (case_tac "l \<in> Domain (findRel p) ") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
142 |
apply (auto iff: Domain_findRel_iff) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
143 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
144 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
145 |
|
13107 | 146 |
subsection {* @{text lfilter}: simple facts by coinduction *} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
147 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
148 |
lemma lfilter_K_True: "lfilter (%x. True) l = l" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
149 |
by (rule_tac l = "l" in llist_fun_equalityI, simp_all) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
150 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
151 |
lemma lfilter_idem: "lfilter p (lfilter p l) = lfilter p l" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
152 |
apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
153 |
apply safe |
13107 | 154 |
txt{*Cases: @{text "p x"} is true or false*} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
155 |
apply (rule lfilter_cases [THEN disjE]) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
156 |
apply (erule ssubst, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
157 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
158 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
159 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
160 |
subsection {* Numerous lemmas required to prove @{text lfilter_conj} *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
161 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
162 |
lemma findRel_conj_lemma [rule_format]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
163 |
"(l,l') \<in> findRel q |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
164 |
==> l' = LCons x l'' --> p x --> (l,l') \<in> findRel (%x. p x & q x)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
165 |
by (erule findRel.induct, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
166 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
167 |
lemmas findRel_conj = findRel_conj_lemma [OF _ refl] |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
168 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
169 |
lemma findRel_not_conj_Domain [rule_format]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
170 |
"(l,l'') \<in> findRel (%x. p x & q x) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
171 |
==> (l, LCons x l') \<in> findRel q --> ~ p x --> |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
172 |
l' \<in> Domain (findRel (%x. p x & q x))" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
173 |
by (erule findRel.induct, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
174 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
175 |
lemma findRel_conj2 [rule_format]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
176 |
"(l,lxx) \<in> findRel q |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
177 |
==> lxx = LCons x lx --> (lx,lz) \<in> findRel(%x. p x & q x) --> ~ p x |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
178 |
--> (l,lz) \<in> findRel (%x. p x & q x)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
179 |
by (erule findRel.induct, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
180 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
181 |
lemma findRel_lfilter_Domain_conj [rule_format]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
182 |
"(lx,ly) \<in> findRel p |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
183 |
==> \<forall>l. lx = lfilter q l --> l \<in> Domain (findRel(%x. p x & q x))" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
184 |
apply (erule findRel.induct) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
185 |
apply (blast dest!: sym [THEN lfilter_eq_LCons] intro: findRel_conj, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
186 |
apply (drule sym [THEN lfilter_eq_LCons], auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
187 |
apply (drule spec) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
188 |
apply (drule refl [THEN rev_mp]) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
189 |
apply (blast intro: findRel_conj2) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
190 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
191 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
192 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
193 |
lemma findRel_conj_lfilter [rule_format]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
194 |
"(l,l'') \<in> findRel(%x. p x & q x) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
195 |
==> l'' = LCons y l' --> |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
196 |
(lfilter q l, LCons y (lfilter q l')) \<in> findRel p" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
197 |
by (erule findRel.induct, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
198 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
199 |
lemma lfilter_conj_lemma: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
200 |
"(lfilter p (lfilter q l), lfilter (%x. p x & q x) l) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
201 |
\<in> llistD_Fun (range (%u. (lfilter p (lfilter q u), |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
202 |
lfilter (%x. p x & q x) u)))" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
203 |
apply (case_tac "l \<in> Domain (findRel q)") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
204 |
apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
205 |
prefer 3 apply (blast intro: rev_subsetD [OF _ Domain_findRel_mono]) |
13107 | 206 |
txt{*There are no @{text qs} in @{text l}: both lists are @{text LNil}*} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
207 |
apply (simp_all add: Domain_findRel_iff, clarify) |
13107 | 208 |
txt{*case @{text "q x"}*} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
209 |
apply (case_tac "p x") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
210 |
apply (simp_all add: findRel_conj [THEN findRel_imp_lfilter]) |
13107 | 211 |
txt{*case @{text "q x"} and @{text "~(p x)"} *} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
212 |
apply (case_tac "l' \<in> Domain (findRel (%x. p x & q x))") |
13107 | 213 |
txt{*subcase: there is no @{text "p & q"} in @{text l'} and therefore none in @{text l}*} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
214 |
apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
215 |
prefer 3 apply (blast intro: findRel_not_conj_Domain) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
216 |
apply (subgoal_tac [2] "lfilter q l' ~: Domain (findRel p) ") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
217 |
prefer 3 apply (blast intro: findRel_lfilter_Domain_conj) |
13107 | 218 |
txt{* {\dots} and therefore too, no @{text p} in @{text "lfilter q l'"}. |
219 |
Both results are @{text LNil}*} |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
220 |
apply (simp_all add: Domain_findRel_iff, clarify) |
13107 | 221 |
txt{*subcase: there is a @{text "p & q"} in @{text l'} and therefore also one in @{text l} *} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
222 |
apply (subgoal_tac " (l, LCons xa l'a) \<in> findRel (%x. p x & q x) ") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
223 |
prefer 2 apply (blast intro: findRel_conj2) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
224 |
apply (subgoal_tac " (lfilter q l', LCons xa (lfilter q l'a)) \<in> findRel p") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
225 |
apply simp |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
226 |
apply (blast intro: findRel_conj_lfilter) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
227 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
228 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
229 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
230 |
lemma lfilter_conj: "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
231 |
apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
232 |
apply (blast intro: lfilter_conj_lemma rev_subsetD [OF _ llistD_Fun_mono]) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
233 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
234 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
235 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
236 |
subsection {* Numerous lemmas required to prove ??: |
13107 | 237 |
@{text "lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)"} |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
238 |
*} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
239 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
240 |
lemma findRel_lmap_Domain: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
241 |
"(l,l') \<in> findRel(%x. p (f x)) ==> lmap f l \<in> Domain(findRel p)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
242 |
by (erule findRel.induct, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
243 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
244 |
lemma lmap_eq_LCons [rule_format]: "lmap f l = LCons x l' --> |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
245 |
(\<exists>y l''. x = f y & l' = lmap f l'' & l = LCons y l'')" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
246 |
apply (subst lmap_def [THEN def_llist_corec]) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
247 |
apply (rule_tac l = "l" in llistE, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
248 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
249 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
250 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
251 |
lemma lmap_LCons_findRel_lemma [rule_format]: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
252 |
"(lx,ly) \<in> findRel p |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
253 |
==> \<forall>l. lmap f l = lx --> ly = LCons x l' --> |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
254 |
(\<exists>y l''. x = f y & l' = lmap f l'' & |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
255 |
(l, LCons y l'') \<in> findRel(%x. p(f x)))" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
256 |
apply (erule findRel.induct, simp_all) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
257 |
apply (blast dest!: lmap_eq_LCons)+ |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
258 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
259 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
260 |
lemmas lmap_LCons_findRel = lmap_LCons_findRel_lemma [OF _ refl refl] |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
261 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
262 |
lemma lfilter_lmap: "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
263 |
apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
264 |
apply safe |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
265 |
apply (case_tac "lmap f l \<in> Domain (findRel p)") |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
266 |
apply (simp add: Domain_findRel_iff, clarify) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
267 |
apply (frule lmap_LCons_findRel, force) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
268 |
apply (subgoal_tac "l ~: Domain (findRel (%x. p (f x)))", simp) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
269 |
apply (blast intro: findRel_lmap_Domain) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
270 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset
|
271 |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
272 |
end |