18153
|
1 |
|
|
2 |
(* $Id$ *)
|
8676
|
3 |
|
10007
|
4 |
header {* Nested datatypes *}
|
8676
|
5 |
|
16417
|
6 |
theory NestedDatatype imports Main begin
|
8676
|
7 |
|
10007
|
8 |
subsection {* Terms and substitution *}
|
8676
|
9 |
|
|
10 |
datatype ('a, 'b) "term" =
|
|
11 |
Var 'a
|
10007
|
12 |
| App 'b "('a, 'b) term list"
|
8676
|
13 |
|
|
14 |
consts
|
8717
|
15 |
subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
|
8676
|
16 |
subst_term_list ::
|
10007
|
17 |
"('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
|
8676
|
18 |
|
|
19 |
primrec (subst)
|
|
20 |
"subst_term f (Var a) = f a"
|
|
21 |
"subst_term f (App b ts) = App b (subst_term_list f ts)"
|
|
22 |
"subst_term_list f [] = []"
|
10007
|
23 |
"subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
|
8676
|
24 |
|
|
25 |
|
|
26 |
text {*
|
|
27 |
\medskip A simple lemma about composition of substitutions.
|
10007
|
28 |
*}
|
8676
|
29 |
|
|
30 |
lemma
|
|
31 |
"subst_term (subst_term f1 o f2) t =
|
8717
|
32 |
subst_term f1 (subst_term f2 t) &
|
8676
|
33 |
subst_term_list (subst_term f1 o f2) ts =
|
10007
|
34 |
subst_term_list f1 (subst_term_list f2 ts)"
|
11809
|
35 |
by (induct t and ts) simp_all
|
8676
|
36 |
|
9659
|
37 |
lemma "subst_term (subst_term f1 o f2) t =
|
10007
|
38 |
subst_term f1 (subst_term f2 t)"
|
|
39 |
proof -
|
|
40 |
let "?P t" = ?thesis
|
|
41 |
let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
|
|
42 |
subst_term_list f1 (subst_term_list f2 ts)"
|
|
43 |
show ?thesis
|
|
44 |
proof (induct t)
|
|
45 |
fix a show "?P (Var a)" by simp
|
|
46 |
next
|
|
47 |
fix b ts assume "?Q ts"
|
|
48 |
thus "?P (App b ts)" by (simp add: o_def)
|
|
49 |
next
|
|
50 |
show "?Q []" by simp
|
|
51 |
next
|
|
52 |
fix t ts
|
|
53 |
assume "?P t" "?Q ts" thus "?Q (t # ts)" by simp
|
|
54 |
qed
|
|
55 |
qed
|
8676
|
56 |
|
|
57 |
|
10007
|
58 |
subsection {* Alternative induction *}
|
8676
|
59 |
|
|
60 |
theorem term_induct' [case_names Var App]:
|
18153
|
61 |
assumes var: "!!a. P (Var a)"
|
|
62 |
and app: "!!b ts. list_all P ts ==> P (App b ts)"
|
|
63 |
shows "P t"
|
|
64 |
proof (induct t)
|
|
65 |
fix a show "P (Var a)" by (rule var)
|
|
66 |
next
|
|
67 |
fix b t ts assume "list_all P ts"
|
|
68 |
thus "P (App b ts)" by (rule app)
|
|
69 |
next
|
|
70 |
show "list_all P []" by simp
|
|
71 |
next
|
|
72 |
fix t ts assume "P t" "list_all P ts"
|
|
73 |
thus "list_all P (t # ts)" by simp
|
10007
|
74 |
qed
|
8676
|
75 |
|
8717
|
76 |
lemma
|
|
77 |
"subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
|
11809
|
78 |
proof (induct t rule: term_induct')
|
|
79 |
case (Var a)
|
18153
|
80 |
show ?case by (simp add: o_def)
|
10007
|
81 |
next
|
11809
|
82 |
case (App b ts)
|
18153
|
83 |
thus ?case by (induct ts) simp_all
|
10007
|
84 |
qed
|
8676
|
85 |
|
10007
|
86 |
end
|