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