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