| author | urbanc |
| Tue, 14 Feb 2012 04:14:18 +0000 | |
| changeset 330 | f86e099ac688 |
| parent 193 | 2a5ac68db24b |
| permissions | -rw-r--r-- |
|
193
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
1 |
theory Mirkin |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
2 |
imports Derivatives |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
3 |
begin |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
4 |
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
5 |
fun |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
6 |
pbase :: "'a rexp \<Rightarrow> 'a rexp set" |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
7 |
where |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
8 |
"pbase (Zero) = {}"
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
9 |
| "pbase (One) = {}"
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
10 |
| "pbase (Atom a) = {One}"
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
11 |
| "pbase (Plus r1 r2) = pbase r1 \<union> pbase r2" |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
12 |
| "pbase (Times r1 r2) = Timess (pbase r1) r2 \<union> pbase r2" |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
13 |
| "pbase (Star r) = Timess (pbase r) (Star r)" |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
14 |
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
15 |
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
16 |
lemma a: "A \<subseteq> B \<Longrightarrow> Timess A r \<subseteq> Timess B r" |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
17 |
apply(auto) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
18 |
done |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
19 |
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
20 |
lemma b: "pders_lang UNIV1 r \<subseteq> pbase r" |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
21 |
apply(induct r) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
22 |
apply(simp) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
23 |
apply(simp) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
24 |
apply(simp) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
25 |
apply(simp) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
26 |
apply(auto)[1] |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
27 |
apply(simp) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
28 |
apply(rule subset_trans) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
29 |
apply(rule pders_lang_Times) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
30 |
apply(simp) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
31 |
apply(rule conjI) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
32 |
apply(drule_tac r="r2" in a) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
33 |
apply(auto)[1] |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
34 |
apply(auto)[1] |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
35 |
apply(rule subset_trans) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
36 |
apply(rule pders_lang_Star) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
37 |
apply(simp) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
38 |
apply(rule a) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
39 |
apply(simp) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
40 |
done |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
41 |
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
42 |
lemma c: "pders_lang UNIV r \<subseteq> pbase r \<union> {r}"
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
43 |
using b |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
44 |
apply(auto simp add: pders_lang_UNIV) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
45 |
done |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
46 |
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
47 |
lemma d: "finite (pbase r)" |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
48 |
apply(induct r) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
49 |
apply(auto) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
50 |
done |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
51 |
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
52 |
lemma e: "pder c r \<subseteq> pbase r" |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
53 |
by (induct r) (auto) |
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
54 |
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
55 |
|
|
2a5ac68db24b
finished section about derivatives and closure properties
urbanc
parents:
diff
changeset
|
56 |
end |